Re: Realizibility and Partial Combinatory Algebras

[<jvoosten@math.uu.nl>]

> 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