Re: Realizability and Partial Combinatory Algebras

Re: Realizability and Partial Combinatory Algebras

[jvoosten]

Dear John,

> Note that we can find elements if,true,false \in A satisfying
> 	if true x y = x, 	if false x y = y,
> and furthermore we can arrange that true = k.
> (I'll use "if then else" syntax below).
> We want to construct S such that (in A),
>      Skxkykz ~ (xkz)k(ykz), and Skxky is always defined.
> Take S to be
> 	\lambda txuyvz. if v then (xkz)k(ykz) else false
> using the usual Curry translation of lambda terms. To see that
> Skxky is always defined, note that, provably, Skxky(false)z = false.

There is a point I don't understand. If I work out Skxky, then I find
a term which contains subterms of the form xk, yk. So how can this be
defined if x or y represent nowhere defined functions?

It looks to me, that you are using a form of Combinatorial Completeness
that is not valid with the weaker S-axiom. If I am correct, one has
the following form of Combinatorial Completeness:

For every term t and variable z, there is a term \lambda z.t with the
property:

If \lambda z.t is defined, then for each a, (\lambda z.t)a ~ t[a/z]

(of course, a really correct version has more than one variable)

Best, Jaap

Re: Realizability and Partial Combinatory Algebras

[Peter Lietz]

Although in the meantime I was completely convinced by John's argument, I
now believe that Jaap has indeed raised a serious point.


However, I think that the flaw (if it indeed was) in John's argument is
not in the form of combinatory completeness that he applies, but it is an
illegal instance of substitution, which one has to be very careful with
within a logic of partial terms where variables range over existing
objects (as e.g. in E+ logic, presented in Troelstra & van Dalen, Vol. I).

From

	IF FALSE x y  >~  y

one cannot conclude

	IF FALSE q r  >~  r

for q and r arbitrary terms.



As to the definitive and correct form of combinatory completess in a c-pca
I make the following proposition (which I have checked):

  Let A be a c-pca and t be a term built up using application from
  A-constants and variables. Then there is a term (\lambda x. t) that has
  the same free variables as t save x such that for all a\in A and all
  valuations of free variables

	(\lambda x. t) a  >~  t[a/x]

That means, if w.r.t. some valuation the right hand side denotes a value
then the left hand side denotes the same value. In particular, if for some
valuation and some a in A the right hand side exists (denotes a value)
then so does the left hand side and hence (\lambda x. t) (for this
particular valuation), as application is a strict function.

The same is true for simultaneous abstraction (replace x and a by \vec{x}
and \vec{a} resp.). One only needs to prove a little substitution lemma.

This proposition is essentially in the Hyland-Ong paper (the small
difference is that, in the paper all variables get abstracted away,
but that is inessential).



Best,

Peter

Re: Realizability and Partial Combinatory Algebras

[jvoosten]

Dear Peter and John,

Peter correctly pointed out the error in my message:
the problem was in the use of the "if then .. else .." syntax,
not in any form of combinatorial completeness.

Answering John: I was using a construction of \lambda x.t where
\lambda x.M is KM whenever M is any term not containing x free
(this works just as well); so in my construction,
\lambda vz. if v then xkzk(ykz) else false
DOES contain subterms xk and yk.

Anyway, I do now believe that John's latest version is correct.
This is really very nice, and a surprise (for me, at least).
I stand corrected and must apologize for my first posting in this
discussion, casting doubt on PTJ's message.

One little point, regarding Combinatorial Completeness. I believe
the following form is valid (in the situation with the weak S-axiom):
suppose t is a term, x a variable. There is a term \lambda x.t such
that for all a,a_1,...,a_n in A:
((\lambda x.t)[a_1,...,a_n])a ~ t[a,a_1,...,a_n]
So this is just like the ordinary form, except for the assertion that
(\lambda x.t)[a_1,...,a_n] is always defined. We have that
(\lambda x.t)[a_1,...,a_n] is defined whenever for some a in A,
t[a,a_1,...,a_n] is defined.

Best, Jaap

Re: Realizability and Partial Combinatory Algebras

[Peter Lietz]

Dear Jaap, John and Thomas,

I am not yet convinced.

What I do more or less believe is that the operation of `thunking' works
for a c-pca.

But it does *not* seem to be the case that the combinator S that John
defined (using thunking) satisfies the equations

    Skxky(false)z = false   and   Skxkykz = (xkz)k(ykz) ,

even in a total combinatory algebra!

As I do not trust my term manipulation skills so much any more in this
context, I wrote a little Haskell Program to compute the normal forms.
The left hand side terms are indeed normalizing but their normal forms
are considerably longer than the respective right hand side terms. Oddly
enough, the normal form of the former term even contains variables.

Now it is very well possible that my program has a bug, programming is
hardly my main occupation. If you like to play with it you are invited to
access it via

	http://www.mathematik.tu-darmstadt.de/~lietz/cpca/cpca.hs

and if you find a bug please do let me know.

I cannot put my finger on exactly what is the gap in the proof. I think it
has to do with the fact that thunk(e,c) does not commute with substitution
in the way one might expect. Or put differently, the `thunk' algorithm and
the Curry algorithm don't play along very well. Something in that
direction.


Finally, I should apologize for taxing the categories mailing list
readers' patience with a subject that is likely only of marginal
interest to most.

have a nice weekend,

Peter

Re: Realizibility and Partial Combinatory Algebras

[Prof. Peter Johnstone]

On Fri, 7 Feb 2003 jvoosten@math.uu.nl wrote:
>
> I think the relevance of this condition (Sxy defined) is explained in the
> Hyland-Ong paper "Modified Realizability Toposes and Strong Normalization
> Proofs" (TLCA, LNCS 664, 1993; reference 466 in the Elephant) where they
> have a definition of "c-pca" which is just omitting this requirement.
> They show that the standard P(A)-indexed preordered set, for a c-pca A,
> can fail to be a tripos. So the condition IS used.
>
I hope Jaap and Peter will forgive me for saying that I think they
missed the point of my message. (Perhaps it's my fault -- with hindsight,
I wasn't as clear as I should have been. I really ought to stop trying
to reply to things like this late at night -- although, as you'll see
from the header of this message, I'm doing it again.)

Of course I know about the Hyland--Ong paper: indeed, I reviewed it for
Zentralblatt. However, the point I was trying to make was that the
construction of the quasitopos of A-valued assemblies, and the proof
that its effectivization is a topos, make no use whatever of the
condition that Sxy is always defined. The fact that the tautology
((p => (q => r)) => ((p => q) => (p => r))) fails (or may fail) to
be realized by S when p is empty has no effect on this construction,
because one never has to deal with "propositions" having an empty
set of realizers. So, whilst a tripos-theorist (if such a creature
exists) may indeed have cause to worry about whether Sxy might be
undefined, there seems to be no reason why a topos-theorist should do so.

[Yes, yes, I know that I was responsible for inventing the term
"tripos", and therefore that if anyone can legitimately be called a
tripos-theorist then I can. But I don't believe that I am a
tripos-theorist (which implies that no-one is).]

Peter Johnstone

Re: Realizability and Partial Combinatory Algebras

[John Longley]

Peter Johnstone wrote:

> However, the point I was trying to make was that the
> construction of the quasitopos of A-valued assemblies, and the proof
> that its effectivization is a topos, make no use whatever of the
> condition that Sxy is always defined.

As far as I can see, Peter Johnstone is essentially correct.
Even without the condition "sxy is defined", Asm(A) is locally cartesian
closed (though the correct construction of local exponentials is not quite
the "obvious" one), and its exact/regular completion is a topos. Peter
Lietz's argument (which is the one that occurred to me too) seems to fail
at his point 1: to get a realizer for the mediating morphism from the
true local exponential to the object he constructs, one actually needs
the condition "sxy is defined". For the record, in Peter L's example,
the true exponential m^m in the slice over Nabla(P(A)), for instance,
may be described as follows:
	   |T| = P(A)
   [|X \in T|] = {a | for all b \in X. akb \in X}
(where k plays the role of an arbitrary element which forces the "thunked"
operation X -> X to manifest itself.)

I think I can now appreciate Peter Johnstone's point of view, though it
seems to me that to follow it through consistently would require some
substantial changes to the way one develops the whole theory.
For instance, in defining the category Asm(A), one really ought to say
e.g. that an element r \in A *tracks* f : X -> Y iff

   for all x \in X, a \in A.  a \in [|x \in X|] => rka \in [|f(x) \in Y|]

so as not to get mired down in case splits on whether X is inhabited,
which (I humbly submit) are here an abomination and totally out of keeping
with the spirit of realizability and topos theory in general. [Classically,
of course, the above definition leads to exactly the same category as the
usual one.] One can then do everything else in the same way, and it all
works out - e.g. there is a perfectly respectable tripos over A (with Heyting
implication defined as in the object T above), and the theory of internal
categories such as PER also works fine.

I don't think one can really call this "standard realizability" any more,
in the sense of being derived from (a simple abstraction of) Kleene's
realizability interpretation. Of course, one might say that doesn't matter
much, but for my part, I feel one loses something of the directness of
standard realizability, where application in the PCA corresponds immediately
to function application in Asm(A) and also to Modus Ponens in the logic.
There is also of course the evident analogy with the Brouwer-Heyting-
Kolmogorov interpretation of intuitionistic logic. If one adopts the above
alternative, there is less of a clear intuition about what the significance
of application in the PCA is.

However, no sooner has one reached this point, than one notices that
doing realizability of the above kind over A is just tantamount to doing
standard realizability over the "derived PCA" a la Freyd [?], where
application is defined by a.b ~ akb. Indeed, one has the following easy
proposition:

   For any PCA A (where we don't assume "sxy defined"), there is an
   applicatively equivalent PCA B (in the sense of my thesis) in which
   sxy is always defined. In particular, the realizability topos on A
   (constructed as outlined above) is equivalent to the (usual) standard
   realizability topos on B.

   Proof: Let B have the same set as A, and define application in B by
   a.b ~ akb. It's easy to construct K,S \in B such that K.a.b = a,
   S.a.b.c ~ a.c.(b.c), and with a little additional care one can arrange
   that S.a.b is always defined. Now, application in B is realized in A
   by \lambda ab. akb (constructed as normal); and application in A is
   realized in B by i=skk, since i.a.b = ikakb = kakb = ab.
   The equivalence of toposes can now most easily be seen by noticing that
   the categories Asm(A), Asm(B) are equal on the nose.

So, it seems it's largely just a question of taste whether one adopts the
definedness condition. For my money, I would rather adopt this condition,
retain the directness of standard realizability and all the familiar
constructions, do all the proofs in an "effective" spirit, and know that
I'm not sacrificing any generality. Who could ask for anything more?

(Quite a lot of the above was new to me, and was all good fun!)

Finally, I'd like to remark briefly on the other issue in the definition
of PCA, which Jaap, Peter L and myself have now all mentioned: whether
one should require sxyz ~ xz(yz) or just sxyz >~ xz(yz). I know of no
reason not to adopt the latter, more general condition, and it seems
to me much more in the spirit of realizability: e.g. one never cares if
a realizer for a morphism assemblies is defined on more elements than
required. On the other hand, I do not have any particular use yet for
any of the extra examples admitted by this definition.

An interesting case in point is Kleene's second model, K_2. It is a PCA
in the sense of the axiom with ~, but the "natural" construction of an
element s gives one that only satisfies the axiom with >~. Some artificial
hackery is needed to produce an element s satisfying the stronger axiom -
and of course, my attitude would be: why bother?

Best wishes,
John

Re: Realizability and Partial Combinatory Algebras

[Peter Lietz]

Dear John,

would you please fill me in on either (or better yet, both) of the
following points, as I failed to figure them out by myself:

1.) Let A be a c-pca. If I understand correctly, you say that the indexed
    poset that maps a set I to the set of maps from I to P(A), endowed
    with the usual entailment relation [ for phi,psi: I -> P(A),
    phi |- psi iff there is an r in A such that for all i in I and
    for all a in phi(i), ra exists and ra is in psi(i) ]
    is indeed an indexed Heyting-Algebra and that the implication of
    phi,psi : I -> P(A) is given by

        (phi=>psi)(i) = {r in A | forall a in phi(i). rka in psi(i)}.

    My question is: given phi, psi and theta such that

        theta /\ phi |- psi over I

    via some realizer r, what would be a realizer witnessing

        theta |- phi => psi

    with => defined in the way you indicated?


2.) Given a c-pca A, you say that A equipped with the application
    function a.b := akb is a (proper) pca. What exactly would be a good
    S combinator for the new algebra ? (You wrote that some additional
    care is needed to construct S)


Many thanks in advance,

Peter



ps: in an attempt to give the shortest possible of the many reasons, why
    Heyting algebras do not form a CCC I suggest: The one-element poset
    is the terminal Heyting algebra. Therefore, every object has at most
    one global section. Hence, there can only be one morphism between each
    two Heyting algebras, as the global sections of the exponent correspond
    to the morphisms (which is absurd).

pps: The one-element poset *is* a Heyting-algebra, in fact all topologies
     are.




On Wed, 12 Feb 2003, John Longley wrote:

> As far as I can see, Peter Johnstone is essentially correct.
> Even without the condition "sxy is defined", Asm(A) is locally cartesian
> closed (though the correct construction of local exponentials is not quite
> the "obvious" one), and its exact/regular completion is a topos. Peter
> Lietz's argument (which is the one that occurred to me too) seems to fail
> at his point 1: to get a realizer for the mediating morphism from the
> true local exponential to the object he constructs, one actually needs
> the condition "sxy is defined". For the record, in Peter L's example,
> the true exponential m^m in the slice over Nabla(P(A)), for instance,

....

Re: Realizability and Partial Combinatory Algebras

[John Longley]

Quoting Peter Lietz <lietz@mathematik.tu-darmstadt.de>:

> 1.) Let A be a c-pca. If I understand correctly, you say that the
> indexed poset that maps a set I to the set of maps from I to P(A),
> endowed with the usual entailment relation

Not quite - you have to define the entailment relation to match the
definition of implication (put a k in there!). The cheating way to
see that all this must work out is of course via the equivalence to a
PCA for which the standard construction works!

> 2.) Given a c-pca A, you say that A equipped with the application
> function a.b := akb is a (proper) pca. What exactly would be a
> good S combinator for the new algebra ?

Note that we can find elements if,true,false \in A satisfying
	if true x y = x, 	if false x y = y,
and furthermore we can arrange that true = k.
(I'll use "if then else" syntax below).
We want to construct S such that (in A),
     Skxkykz ~ (xkz)k(ykz), and Skxky is always defined.
Take S to be
	\lambda txuyvz. if v then (xkz)k(ykz) else false
using the usual Curry translation of lambda terms. To see that
Skxky is always defined, note that, provably, Skxky(false)z = false.

Clearly there are two versions of this result, one with the axiom
sxyz ~ (xz)(yz) and one with sxyz >~ (xz)(yz). Thomas asks whether every
PCA with >~ is equivalent to one with ~ (Gordon Plotkin has also asked me
this natural question). At the moment, the best I can do is: for any
PCA A with >~, there's a PCA B with ~ and an applicative inclusion A -> B
(giving rise to a geometric inclusion of toposes).

Cheers, John