Can LCF be topped? Flat lattice models of typed λ-calculus

AbstractPlotkin ((1977) Theoret. Comput. Sci. 5: 223–256) examines the denotational semantics of PCF (essentially typed λ-calculus with arithmetic and looping). The standard Scott semantics V is computationally adequate but not fully abstract; with the addition of some parallel facilities, it becomes fully abstract, and with the addition of an existential operator, denotationally universal. We consider carrying out the same program for ⊙, the Scott models built from flat lattices rather than flat cpo's. Surprisingly, no computable extension of PCF can be denotationally universal; perfectly reasonable semantic values such as supremum and Plotkin's “parallel or” cannot be definable. There is an unenlightening fully abstract extension LA (approx), based on Gödel numbering and syntactic analysis. Unfortunately, this is the best we can do; operators defined by PCF-style rules cannot give a fully abstract language. (There is a natural and desirable property, operational extensionality, which prevents full abstraction with respect to ⊙.) However, we show that Plotkin's program can be carried out for a nonconfluent evaluator