Re: Realizibility and Partial Combinatory Algebras

[John Longley <jrl@inf.ed.ac.uk>]

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