Re: Realizability and Partial Combinatory Algebras

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

Quoting Peter Lietz <lietz@mathematik.tu-darmstadt.de>:

> 1.) Let A be a c-pca. If I understand correctly, you say that the
> indexed poset that maps a set I to the set of maps from I to P(A),
> endowed with the usual entailment relation

Not quite - you have to define the entailment relation to match the
definition of implication (put a k in there!). The cheating way to
see that all this must work out is of course via the equivalence to a
PCA for which the standard construction works!

> 2.) Given a c-pca A, you say that A equipped with the application
> function a.b := akb is a (proper) pca. What exactly would be a
> good S combinator for the new algebra ?

Note that we can find elements if,true,false \in A satisfying
	if true x y = x, 	if false x y = y,
and furthermore we can arrange that true = k.
(I'll use "if then else" syntax below).
We want to construct S such that (in A),
     Skxkykz ~ (xkz)k(ykz), and Skxky is always defined.
Take S to be
	\lambda txuyvz. if v then (xkz)k(ykz) else false
using the usual Curry translation of lambda terms. To see that
Skxky is always defined, note that, provably, Skxky(false)z = false.

Clearly there are two versions of this result, one with the axiom
sxyz ~ (xz)(yz) and one with sxyz >~ (xz)(yz). Thomas asks whether every
PCA with >~ is equivalent to one with ~ (Gordon Plotkin has also asked me
this natural question). At the moment, the best I can do is: for any
PCA A with >~, there's a PCA B with ~ and an applicative inclusion A -> B
(giving rise to a geometric inclusion of toposes).

Cheers, John