Re: Realizability and Partial Combinatory Algebras

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

Dear Jaap, John and Thomas,

I am not yet convinced.

What I do more or less believe is that the operation of `thunking' works
for a c-pca.

But it does *not* seem to be the case that the combinator S that John
defined (using thunking) satisfies the equations

    Skxky(false)z = false   and   Skxkykz = (xkz)k(ykz) ,

even in a total combinatory algebra!

As I do not trust my term manipulation skills so much any more in this
context, I wrote a little Haskell Program to compute the normal forms.
The left hand side terms are indeed normalizing but their normal forms
are considerably longer than the respective right hand side terms. Oddly
enough, the normal form of the former term even contains variables.

Now it is very well possible that my program has a bug, programming is
hardly my main occupation. If you like to play with it you are invited to
access it via

	http://www.mathematik.tu-darmstadt.de/~lietz/cpca/cpca.hs

and if you find a bug please do let me know.

I cannot put my finger on exactly what is the gap in the proof. I think it
has to do with the fact that thunk(e,c) does not commute with substitution
in the way one might expect. Or put differently, the `thunk' algorithm and
the Curry algorithm don't play along very well. Something in that
direction.


Finally, I should apologize for taxing the categories mailing list
readers' patience with a subject that is likely only of marginal
interest to most.

have a nice weekend,

Peter