Accession Number:

ADA247062

Title:

Full Abstraction and the Context Lemma

Descriptive Note:

Corporate Author:

MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE

Personal Author(s):

• Jim, Trevor
• Meyer, Albert R.

Report Date:

1991-12-01

Pagination or Media Count:

49.0

Abstract:

It is impossible to add a combinator to PCF to achieve full abstraction for models such as Berrys 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 Scotts PCF. Any simply typed lambda-calculus with such a PCF-like rewriting semantics is shown necessarily to satisfy Milners 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.

Descriptors:

• *FUNCTIONS
• *SEMANTICS
• MODELS
• ABSTRACTS
• STANDARDIZATION
• CALCULUS
• ADDITION

Subject Categories:

• Operations Research

Distribution Statement:

APPROVED FOR PUBLIC RELEASE