Re: Realizibility and Partial Combinatory Algebras

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

>  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