Realizibility and Partial Combinatory Algebras

Realizibility and Partial Combinatory Algebras

[Galchin Vasili]

Hello,

     I understand (to some degree) full combinatory algebra, but I don't
understand the motivation behind the definition of a partial combinatory
algebra. E.g. why do we have Sxy converges/is defined? Or Kxy ~ x?

Regards, Bill Halchin

Re: Realizibility and Partial Combinatory Algebras

[John Longley]

Bill Halchin writes:

> I understand (to some degree) full combinatory algebra, but I
> don't
> understand the motivation behind the definition of a partial
> combinatory
> algebra. E.g. why do we have Sxy converges/is defined? Or Kxy ~ x?

The somewhat mysterious definition of (partial or full)
combinatory algebras is really motivated by the fact that it
is equivalent to a "combinatory completeness" property, which is
a bit less mysterious but more cumbersome to state. Informally,
combinatory completeness says that all functions definable in the
language of A are themselves representable by elements of A.
More precisely:

  A is a PCA iff for every formal expression e (built up from
  variables x,y_1,...,y_n and constants from A via juxtaposition),
  there is a formal expression called (\lambda x.e), whose variables
  are just y_1,...,y_n, such that
    (\lambda x.e)[b_1/y_1,...,b_n/y_n] is defined for all b_1,...,b_n \in A,
    (\lambda x.e) a [b_1/y_1,...,b_n/y_n] ~ e[a/x,b_1/y_1,...,b_n/y_n]

(This is easiest to understand in the case n=0.) A similar statement holds
for full combinatory algebras where everything is always defined.

The term (\lambda x.e) can be constructed via the Curry translation from
lambda calculus to combinatory logic. The condition "Sxy is defined" is
needed for this to work. Also, I should say the whole theory of realizability
models goes through much more smoothly with this condition, otherwise one
has to keep making tiresome exemptions for the case of the object 0. I imagine
the condition becomes strictly necessary at some point, e.g. in the proof that
PER is an internal category.

As for Kxy ~ x, that's the same as saying Kxy=x, because all elements x of A
are of course defined.

Cheers, John

Re: Realizibility and Partial Combinatory Algebras

[Prof. Peter Johnstone]

On Mon, 3 Feb 2003, Galchin Vasili wrote:

>
> Hello,
>
>      I understand (to some degree) full combinatory algebra, but I don't
> understand the motivation behind the definition of a partial combinatory
> algebra. E.g. why do we have Sxy converges/is defined?

I'd like to know the answer to this too. Why does *everyone*, in writing
down the definition of a PCA, include the assumption that Sxy is always
defined? As far as I can see, the only answer is "because everyone else
does so"; the condition is never used in the construction of
realizability toposes, or in establishing any of their properties.
In every case where you need to know that a particular term Sab is
defined, it's easy to find a particular c such that Sabc is provably
defined.

Peter Johnstone

Re: Realizibility and Partial Combinatory Algebras

[Peter Lietz]

Hello,

On Thu, 6 Feb 2003, Prof. Peter Johnstone wrote:

> I'd like to know the answer to this too. Why does *everyone*, in writing
> down the definition of a PCA, include the assumption that Sxy is always
> defined? As far as I can see, the only answer is "because everyone else
> does so"; the condition is never used in the construction of
> realizability toposes, or in establishing any of their properties.
> In every case where you need to know that a particular term Sab is
> defined, it's easy to find a particular c such that Sabc is provably
> defined.


I'd like to vehemently contradict the claim that the condition "sab is
always defined" is never used in the construction of realizability
toposes.

In the paper "Modified Realizability Toposes and Strong Normalization
Proofs (Extended Abstract)" by Martin Hyland and Luke Ong, a weaker notion
of combinatory algebra, called "conditionally partial combinatory algebra
c-pca)", in which the requirement in question is actually dropped, is
thoroughly examined. The axioms for a c-pca are that

	(K)	 kxy  = y
	(S)	sxyz ~= xz(yz)

where by "~=" I mean Kleene-equality (i.e. the r.h.s. is defined iff the
l.h.s. is defined in which case they are equal). It is not required for a
c-pca that "sxy" exists, but if z exists such that xz(yz) exists then sxyz
and hence sxy exists by the axiom (S).

The motivation for introducing the notion of a c-pca in the paper is that
there is a very relevant c-pca which is not a pca. It consists of strongly
normalizing lambda terms modulo closed beta equivalence and can be used
for providing a categorical point of view on the "candidates of
reducibility" method for strong normalization proof.

It is shown in the paper that the standard realizability tripos
construction will fail to actually deliver a tripos: The set of subsets of
the c-pca taken as the set of truth-values won't even model minimal logic,
which is why a "modified realizability topos" construction is used in the
paper. So there is a strong reason for stipulating the existence of sxy.

One relaxation of the notion of pca which won't break the usual
constructions but is nevertheless rarely employed (exception is e.g.
Longley's work) is the following: instead of sxyx ~= xz(yz) one might
merely require sxyz ~> xz(yz), i.e., sxyz is allowed to be more defined
than xz(yz). However, I don't know of any interesting models which do not
satisfy (S) with Kleene equality anyway.


Respectfully yours,

Peter Lietz

Re: Realizibility and Partial Combinatory Algebras

[John Longley]

>  I understand (to some degree) full combinatory algebra, but I don't
>  understand the motivation behind the definition of a partial combinatory
>  algebra. E.g. why do we have Sxy converges/is defined? Or Kxy ~ x?

Here's another way to motivate the definition of PCAs, which
I believe also shows (in response to Peter Johnstone's message)
where the definedness condition is used in the standard
realizability construction.

Let A be any set with a partial binary operation (thought of
as "application"). Let PA be the powerset of A. The idea is that
we want to use PA as a little model for minimal implicational logic.
We think of sets X \in PA as "propositions", and elements
a \in X as "proofs" or "witnesses" for X. We think of the
empty set as "false" since it has no witnesses. We next
define an operation => on PA, corresponding to "implication",
as follows:
   X => Y  =  { a \in A | for all b \in X. ab defined and ab \in Y }
[Idea: a proof of X=>Y should map any proof of X to a proof of Y.]
The basic idea here is often attributed to Dana Scott.

Now, given any formula \phi built up from propositional variables
p_1,...,p_n using implication, and any valuation v assigning
elements of PA to these variables, we can interpret \phi in PA
to get an element [[\phi]]_v \in PA. Let us say \phi holds
in our model ( A |= \phi ) if there's some a \in A such that
for all valuations v we have a \in [[\phi]]_v. [In other words,
there's a uniform proof that all instances of \phi are true.]

We'd like this model to be sound for the (intuitionistic) logic
of pure implication. As is well known, the two axioms
	p -> q -> p
	(p -> q -> r) -> (p -> q) -> (p -> r)
and the modus ponens rule suffice for deriving all theorems of
this logic. Since modus ponens is clearly sound for the above
interpretation, we just need to assume we have "uniform proofs"
in A of the above two formulae.

Now suppose A contains elements k,s satisfying the axioms of a PCA.
Then it is simple to show that k,s respectively provide realizers
for the above two formulae, and hence A soundly models minimal
implicational logic. The condition "sxy defined" is important here,
as can be seen by interpreting p as \emptyset, and q and r as A.

The question of the converse is quite interesting. I have occasionally
suggested that the definition of PCA should be weakened to allow
sxyz >~ (xz)(yz), where >~ means "if the RHS is defined then so is
the LHS and they are equal". Some support for this proposal could perhaps
be drawn from the following result, which I had not noticed before:

  Let A be any partial applicative structure.
  Then (PA,=>) as above soundly models minimal implicational logic
   iff there exist k,s \in A satisfying
       kxy = x,  sxy defined,  sxyz >~ (xz)(yz)

(I do have examples of structures that are PCAs in this weaker sense
but not in the standard sense, but they are a little obscure.)

Anyhow, the "PA construction" above is an important part of the
tripos-theoretic construction of realizability models, so I think this
shows that "sxy defined" is needed even to ensure the realizability model
is a model for implicational logic. (My suggestion regarding internal
categories in my previous message was overkill!)

Incidentally, a few years ago, Hyland and Ong considered structures
called "conditionally partial combinatory algebras", where one assumes
sx defined but not sxy defined. They observed that the standard
realizability construction does not in general work for CPCAs, but
(in certain interesting cases) a modified realizability construction does.

Cheers, John

Re: Realizibility and Partial Combinatory Algebras

[Thomas Streicher]

John L. has recalled that the traditional definition of pca is motivated
by functional completeness.

> The somewhat mysterious definition of (partial or full)
> combinatory algebras is really motivated by the fact that it
> is equivalent to a "combinatory completeness" property, which is
> a bit less mysterious but more cumbersome to state. Informally,
> combinatory completeness says that all functions definable in the
> language of A are themselves representable by elements of A.
> More precisely:
>
>   A is a PCA iff for every formal expression e (built up from
>   variables x,y_1,...,y_n and constants from A via juxtaposition),
>   there is a formal expression called (\lambda x.e), whose variables
>   are just y_1,...,y_n, such that
>     (\lambda x.e)[b_1/y_1,...,b_n/y_n] is defined for all b_1,...,b_n \in A,
>     (\lambda x.e) a [b_1/y_1,...,b_n/y_n] ~ e[a/x,b_1/y_1,...,b_n/y_n]

He also has pointed out that in realizability one always may replace a realizer
by one which is defined for more arguments. Thus, it appears as natural to
weaken the notion of functional completeness to the following "asymmetric"
variant:

    for every formal expression e (built up from variables x,y_1,...,y_n and
    constants from A via juxtaposition),
    there is a formal expression called (\lambda x.e), whose variables
    are just y_1,...,y_n, such that for all  a, b_1,...,b_n in A

       (\lambda x.e) a [b_1/y_1,...,b_n/y_n] = e[a/x,b_1/y_1,...,b_n/y_n]

    whenever the right hand side is defined

Certainly, this assymmetric version of functional completeness ensures the
existence of a  k  (with the usual properties) and an  s  in A with the
property that

    (*)  sabc = ac(bc)  whenever ac(bc) is defined

Obviously, from a  k  and an  s  satisfying (*) one can prove the assymmetric
version of functional completeness. Axiom (*) doesn't even exclude
undefinedness of  sa  (if  a.x  undefined for all x in A).

Probably, such very weak pca's are also equivalent to an ordinary one?

In any case the notion of pca is somewhat intensional in character. As we
know Asm(A) and Asm(A') are equivalent iff their categories of modest
projectives are equivalent. Concretely, for a pca A the category MP(A) of
modest projectives is nothing but the category of subsets of A and maps
f : P -> Q such that for some r in A we have ra = f(a)  for all  a in P.
Of course, we know from John L.'s work that MP(A) and MP(A') are equivalent
iff A and A' are applicatively equivalent.

What, alas, is not known is an intrinsic categorical characterisation of those
categories equivalent to MP(A) for some pca A. If we had such a
characterisation we would have arrived at a categorical characterisation of
categories of assemblies and, this, also of realizability toposes.

Thomas

Re: Realizibility and Partial Combinatory Algebras

[Peter Lietz]

On Fri, 7 Feb 2003, Prof. Peter Johnstone wrote:

> 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.

Dear Professor Johnstone,

I obviously assumed strongly that you know the Hyland-Ong paper and was
hence rather puzzled by what I mistakenly took for your question.

As to the question regarding A-valued assemblies when A is a c-pca, I
think I can give a justification for the axiom "Sab exists" as well.
I claim that if the axiom "Sab exists" is absent, then the resulting
category of A-valued assemblies is not a quasi-topos.

One can form the category of A-valued assemblies and it is regular and
cartesian closed.  However, the realizers for the evaluation maps and also
the construction of a realizer for the transpose of a map may exist, but
one has to make a case analysis as to whether the source object is
inhabited or not. Therefore it seems unlikely that the category is locally
cartesian closed, as these operations cannot be carried out in a uniform
manner. If this is the case then the category's exact completion is not a
topos. I am aware that this argument is pretty vague.

For a rigorous proof I would try to show that IF the subobjects of the
threefold product of Nabla(P(A)) do form a Heyting-algebra, which if I am
right is one of the requirements for a quasi-topos, THEN "Sab always
exists". I would go about it as follows.

1. Show that the exponent subobject of two subobjects of an object is - if
   it exists -  constructed as in the "unconditional" pca case.

2. Define the subobject m:S->Nabla(P(A)) with S = {M\subseteq A | M
   inhabited} and the set of realizers of M w.r.t. S being M (and m
   being the obvious map).

3. Interpret the S-tautology of intuitionistic propositional logic
   taking u,v and w as the pullbacks of m along the 1st, 2nd and 3rd
   projection of Nabla(P(A)) x Nabla(P(A)) x Nabla(P(A)),
   respectively.

4. Observe that it is the full subobject and use the reasoning of the
   Hyland-Ong paper to show that "Sab always exists".

Should I be wrong, this would also be good news in a way, because it would
imply that the standard construction of A-valued assemblies could be used
for semantic strong normalization proofs instead of the more complicated
construction of modified assemblies.

Best regards,

Peter Lietz

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: Realizibility and Partial Combinatory Algebras

[jvoosten]

> Date: Thu, 6 Feb 2003 10:44:33 +0000 (GMT)
> From: "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>
> Subject: categories: Re: Realizibility and Partial Combinatory Algebras
>
> On Mon, 3 Feb 2003, Galchin Vasili wrote:
>
> >
> > Hello,
> >
> >      I understand (to some degree) full combinatory algebra, but I don't
> > understand the motivation behind the definition of a partial combinatory
> > algebra. E.g. why do we have Sxy converges/is defined?
>
> I'd like to know the answer to this too. Why does *everyone*, in writing
> down the definition of a PCA, include the assumption that Sxy is always
> defined? As far as I can see, the only answer is "because everyone else
> does so"; the condition is never used in the construction of
> realizability toposes, or in establishing any of their properties.
> In every case where you need to know that a particular term Sab is
> defined, it's easy to find a particular c such that Sabc is provably
> defined.
>
> Peter Johnstone

Dear Peter,

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.

Another condition which is often imposed is really redundant: it is the
requirement that, if sxyz defined, then xz(yz) defined and equal to sxyz.
There are important constructions of realizability toposes where this
fails to hold.

Jaap van Oosten