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