Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Can LCF Be Topped? Flat Lattice Models of Typed $\lambda$-Calculus

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

File(s)
89-1073.pdf (3.24 MB)
89-1073.ps (827.92 KB)
Permanent Link(s)
https://hdl.handle.net/1813/6872
Collections
Computer Science Technical Reports
Author
Bloom, Bard
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
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance