Can LCF be topped? Flat lattice models of typed lambda calculus

G. Plotkin (1977) examined the denotational semantics of LCF (essentially typed lambda calculus with arithmetic and looping). He showed that the standard Scott semantics is computationally adequate but not fully abstract; with the addition of some parallel facilities, it becomes fully abstract, and with the addition of an extential operator, denotationally universal. This treatment is extended to Scott models built from flat lattices rather than flat cpo´s. It is found that no extension of LCF can be denotationally universal. A fully abstract extension based on Godel numbering and synthetic analysis is the best that can be achieved. Operators defined by LCF-style rules cannot give fully abstract language. It is shown that Plotkin´s program can be carried out for a nonconfluent evaluator.<>