Full Abstraction and Semantic Equivalence

CMU-CS-85-148

Ketan Mulmuley

July 1985 - Thesis

This thesis proposes to throw light on the important problems of full abstraction and semantic equivalence. Both of these problems arise in connection with the Scott-Strachey approach to programming language semantics. In this approach, a language is given semantics by mapping each language construct to its meaning in an appropriately constructed mathematical domain - this map is called a denotational semantics of the language. The map is denotational in the sense that the denotation of a complex term depends only on the denotations of its constituents and not on their structure. Of course, if the language is to be of any use at all, it must also have an operational semantics. Generally this operational semantics is specified in terms of a compiler or an interpreter.

The first question which arises is: are the denotational and operational semantics equivalent? This is the problem of semantic equivalence. Milne and Reynolds gave a general technique for proving such semantic equivalences. Their technique involves constructing certain predicates, called inclusive predicates, which connect the demains used for denotational and operational semantics. The most difficult part of their technique is showing the existence of such inclusive predicates. Unfortunately these existence proofs are known to be quire complicated, hence one is reluctant to carry out these proofs. Moreover, so far one did not know any nontrivial example of a system of equations over inclusive predicates which does not have a solution. In the absence of such a counterexample it does not seem justified to carry out the complicated existence proofs with all their details. In this thesis we shall construct such a counterexample through diagonalization. This means one must carry out the existence proofs with care. It has been suspected for some time that much simpler methods for proving these existences will be discovered. For example, several people suggested that there might be a language which can define most of the frequently arising predicates. Unfortunately the above mentioned counterexample shows that there are some fundamental difficulties in doing this. However, in this thesis we shall give a theory to prove such semantic equivalences which has the distinct advantage of being mechanizable. In fact, a system which we shall call IPL Inclusive Predicate Logic , was implemented on top of LCF which can almost automatically prove the existence of most of the inclusive predicates which arise in practice.

Another issue this thesis deals with is the one of full abstraction. A model of a programming language is said to be fully abstract if denotations of two languages constructs are equal whenever those constructs behave the same in all programming contexts and vice versa. For a special case of typed lambda calculus, PCF, it was shown by Plotkin that the classical model consisting of all continuous functions is not fully abstract. G. Plotkins, "LCF Considered as a Programming Language", Theoretical Computer Science 13 1 , December 1977. However, he was able to make the model fully abstract by adding to the language a new programming construct which provided a parallel or facility. Milner showed that, under reasonable assumptions, typed lambda calculus has a unique fully abstract, extensional model, and he constructed the model syntactically R. Milner, "Fully Abstract Models of Typed Lambda-Calculi", Theoretical Computer Science 4 1 , 1977. . A model is said to be extensional if any object of a higher type is uniquely determined by its action on the objects of an appropriate lower type. In this thesis we shall connect Milner's model to the classical model. We shall show that one can construct an extensional, fully abstract and algebraic model of typed lambda calculus which is a homomorphic retraction or a submodel of the classical model, if the classical model is based on complete lattices. Milner's unique fully abstract model, which is based on consistently complete cpos instead of complete lattices, can be recovered from our fully abstract submodel in a very simple way. As a fully abstract model reflects the operational behaviour of the language precisely, our result says that the lattice theoretic model of a typed lambda calculus already contains within itself a submodel which precisely reflects the operational behaviour. This is particularly surprising as the lattice-theoretic models are generally constructed without giving much attention to the operational semantics of a language. Moreover, we shall show that the theory can extend to the case when a language has reflexive i.e. recursively defined types. This is important as most of the 'real' programming languages have recursively defined types. One distinguishing feature of this theory is that it uses the same inclusive predicates, which can be used to show the semantic equivalence between denotational and operational semantics, to construct fully abstract, extensional submodels. This strengthens our belief that the proofs of semantic equivalence and full abstraction go hand in hand.

133 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu