Re: Realizability and Partial Combinatory Algebras

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

Although in the meantime I was completely convinced by John's argument, I
now believe that Jaap has indeed raised a serious point.


However, I think that the flaw (if it indeed was) in John's argument is
not in the form of combinatory completeness that he applies, but it is an
illegal instance of substitution, which one has to be very careful with
within a logic of partial terms where variables range over existing
objects (as e.g. in E+ logic, presented in Troelstra & van Dalen, Vol. I).

From

	IF FALSE x y  >~  y

one cannot conclude

	IF FALSE q r  >~  r

for q and r arbitrary terms.



As to the definitive and correct form of combinatory completess in a c-pca
I make the following proposition (which I have checked):

  Let A be a c-pca and t be a term built up using application from
  A-constants and variables. Then there is a term (\lambda x. t) that has
  the same free variables as t save x such that for all a\in A and all
  valuations of free variables

	(\lambda x. t) a  >~  t[a/x]

That means, if w.r.t. some valuation the right hand side denotes a value
then the left hand side denotes the same value. In particular, if for some
valuation and some a in A the right hand side exists (denotes a value)
then so does the left hand side and hence (\lambda x. t) (for this
particular valuation), as application is a strict function.

The same is true for simultaneous abstraction (replace x and a by \vec{x}
and \vec{a} resp.). One only needs to prove a little substitution lemma.

This proposition is essentially in the Hyland-Ong paper (the small
difference is that, in the paper all variables get abstracted away,
but that is inessential).



Best,

Peter