Can LCF Be Topped? Flat Lattice Models of Typed $\lambda$-Calculus

Bloom, Bard

Can LCF Be Topped? Flat Lattice Models of Typed $\lambda$-Calculus

Abstract

Plotkin, [Plo77], examines the denotational semantics of PCF (essentially typed $\lambda$-calculus with arithmetic and looping). The standard Scott semantics $\bigvee$ 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 $\diamondsuit$, 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 $\pounds_{A}$(approx), based on Godel 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, operation extensionality, which prevents full abstraction with respect to $\diamondsuit$.) However, we show that Plotkin's program can be carried out for a non-confluent evaluator.

Date Issued

1989-12

Publisher

Cornell University

Keywords

computer science; technical report

Previously Published As

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR89-1073

Types

technical report