Full Abstraction and the Context Lemma
Abstract
It is impossible to add a combinator to PCF to achieve full abstraction for models such as Berry's stable domains in a way analogous to the addition of the parallel-or combinator that achieves full abstraction for the familiar cpo model. In particular, we define a general notion of rewriting system of the kind used for evaluating simply typed lambda-terms in Scott's PCF. Any simply typed lambda-calculus with such a PCF-like rewriting semantics is shown necessarily to satisfy Milner's Context Lemma. A simple argument demonstrates that any denotational semantics that is adequate for PCF, and in which certain simple Boolean functionals exist, cannot be fully abstract for any extension of PCF satisfying the Context Lemma. An immediate corollary is that stable domains cannot be fully abstract for any extension of PCF definable by PCF-like rules. Stable functions, full abstraction, context lemma, PCF, standardization.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1991
- Accession Number
- ADA247062
Entities
People
- Albert R. Meyer
- Trevor Jim
Organizations
- Massachusetts Institute of Technology