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