Re: Realizibility and Partial Combinatory Algebras

[Peter Lietz <lietz@mathematik.tu-darmstadt.de>]

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