A Universal Realizability Model for Sequential Functional Computation

We construct a universal and even logically fully abstract realizability model for the sequential functional programming language of call-by-name FPC. This model is defined within the category of modest sets over the total combinatory algebra L of observational equivalence classes of closed terms of the untyped programming language lambda+Error. This language is untyped lazy call-by-name lambda-calculus extended by a single constant ERR and a conditional construct which distinguishes this constant from any other syntactic value. Universality and (constructive) logical full abstraction of the model are proved in three steps. Firstly, a canonical universal and logically fully abstract realizability model for FPC over the typed combinatory algebra T of observational equivalence classes of closed FPC-terms is constructed. Then the recursive type U := mu alpha. void + [ alpha --> alpha ] is shown to be universal, i.e. any other type is a definable retract of U. Hence this type gives rise to an untyped combinatory algebra U which is applicatively equivalent to the typed combinatory algebra T. As a consequence, the realizability toposes over T and U are equivalent and hence the realizability model for FPC over U also universal and logically fully abstract. Finally it is shown that every closed FPC-term of type U can be defined in the untyped language lambda+Error. Hence the combinatory algebras l U and L are applicatively equivalent. It follows that the realizability model over L is universal and logically fully abstract. As a consequence we prove a variant of the Longley-Phoa Conjecture