On abstraction and the expressive power of programming languages

John C. Mitchell^{∗} Department of Computer Science Stanford University Stanford, CA 94305

                          jcm@cs.stanford.edu

October 22, 1992

Abstract

This paper presents a tentative theory of programming language expressiveness based on reductions (language translations) that preserve observational equivalence. These are called “abstraction-preserving” reductions because of a connection with a definition of “abstraction” or “information-hiding” mechanism. If there is an abstractionpreserving reduction from one language to another, then (essentially) every function on natural numbers that is definable in the first is also definable in the second. Moreover, an abstraction-preserving reduction must map every abstraction construct in the source language to a construct that hides analogous distinctions in the target language. Several examples and counter-examples to abstraction-preserving reductions are given. It is not known whether any language is universal with respect to abstraction-preserving reduction.

1 Introduction

This paper presents a tentative theory of programming language expressiveness, originally described in unpublished notes that were circulated in 1986. The original motivation was to compare languages according to the ability to make sections of a program “abstract” by hiding some details of the internal workings of the code. This led to the definition of abstraction-preserving reductions, which are syntax-directed (homomorphic) language translations that preserve observational equivalence. Common translations such as replacing a block by a function declaration and call are abstractionpreserving, as is the addition of recursive types to a functional language that already allows recursive definition of functions. A motivating example was the comparison of weak sums (existential types) with strong sums, which were debated as the basis for data abstraction and module facilities in programming languages. In addition to showing that the replacement of weak sums by strong sums is not abstraction-preserving, we point out that many languages are not reducible to Lisp (with fexpr), in spite of the fact that any partial recursive function on the natural numbers may be written in Lisp. While the Lisp example is contrived, it does illustrate the kind of language feature that can rule out abstraction-preserving reductions.

∗Supported in part by an NSF PYI Award, matching funds from Digital Equipment Corporation, the Powell Foundation, and Xerox Corporation; a gift from Mitsubishi Corporation and the Wallace F. and Lucille M. Davis Faculty Scholarship.

Since the first version of this paper was circulated, abstraction-preserving reductions have been used by Riecke, with some insightful refinements, to compare call-by-name, call-by-value and lazy lambda calculus [Rie91]. In independent work, Shapiro has proposed a general framework for comparing languages that includes the theory here as a special case [Sha91]. Also independently, Felleisen has proposed an alternative theory of expressiveness that has different motivations and consequences [Fel90]. All of these papers are discussed in Section 8.

We will give some motivation for abstraction-preserving reductions in the next section, and give precise definitions in Section 3. Some examples of reductions and non-reductions appear in Sections 4 through 6. In Section 7, we observe that since no language with an abstraction mechanism can be reduced to a language without, languages like Lisp (with fexpr) that can distinguish program phrases by their syntactic form are not universal with respect to our reductions. We do not know whether there is a reasonable language that is capable of simulating every other programming languages in an abstraction-preserving way. Some concluding remarks appear in Section 9.

The original title of this paper was “Lisp is not universal.” This seemed catchy, but gave the mistaken implication that the main topic was Lisp. The discussion of Lisp in this paper is not intended to be a criticism of the language as a whole. In particular, it is recognized that most Lisp programmers use fexpr’s sparingly. The main point of the Lisp example is to demonstrate the kind of programming construct that can prevent abstraction-preserving reduction. It is also arguable that the reason fexpr has been omitted from Common Lisp is because of the unusual characteristic that is highlighted by the theory proposed in this paper.

2 What properties should a “reduction” preserve?

Intuitively, a programming language L_{1} is no more expressive than a language L_{2} if there is a function θ “reducing” each construct of L_{1} to an essentially equivalent construct in L_{2} . The main difficulty in formalizing this intuition lies in formalizing the phrase “essentially equivalent.” To gain some perspective, we review some forms of reduction from the literature.

We may view recursion equations, Turing machine descriptions and untyped lambda terms as languages for programming functions on the integers. Each formalism has a way of representing integers and a way of coding functions between integers. We may compare the ability to express numeric functions using recursion-theoretic reductions: a language L_{1} is reducible to another language L_{2} if there is a mapping θ from L_{1} to L_{2} which sends every coding f of a numeric function in L_{1} to a coding θf of the same numeric function in L_{2} . Since all of the languages for partial recursive functions define the same class of numeric functions, each is reducible to any other. Therefore, this form of reduction does not make interesting or useful distinctions between practical programming languages.

A more useful definition of reduction is the one adopted in “program schematology” [Gre75, PH70]. In this theory, simple imperative programs are interpreted over arbitrary data types, or first-order structures. To simplify our discussion, let us consider deterministic programs only. A program S may mention some set x_{1} … x_{i} of variables, some set f_{1} … f_{j} of function symbols in its expressions and some set P_{1} … P_{k} of predicate symbols in its boolean tests. For any set A, functions f_{1}^{A} … f_{j}^{A} on A and predicates P_{1}^{A} … P_{k}^{A} on A, a deterministic imperative program computes a partial function from sequences of initial values for x_{1} … x_{i} from A to final values of x_{1} … x_{i}. Thus, for any first-order structure A = ⟨A, f_{1}^{A} … f_{j}^{A}, P_{1}^{A} … P_{k}^{A}⟩ interpreting the function and predicate symbols in P , a program P computes an input-output function on sequences of values from A. In program schematology, language L_{1} is reducible to L_{2} if, for every program P in L_{1} there is a program Q = θP in L_{2} computing the same input-output function for every A. (Often the simulating program is allowed to use extra “scratch” variables.) Using this definition of reduction, we can distinguish between recursion and iteration, for example [PH70]. Thus program schematology does a better job of explaining the intuitive “expressive power” of programming languages than recursion theory.

We can actually view program schematology as a theory of “higher-order expressiveness,” as follows. For most classes of imperative programs, we could fix the carrier A to be some suitably large set without loss of generality, and think of a program text S as defining the higher-order function

λf_{1}…. λf_{j}. λP_{1}…. λP_{k}. λx_{1}…. λx_{i}. ⟨S_{1}, …, S_{i}⟩

where S_{n} is the final value of x_{n} after running S on the indicated input. Then a reduction from L_{1} to L_{2} becomes a mapping which preserves the set of higher-order functions definable in the language.

A more general approach to higher-order expressiveness would be to use denotational semantics. We discuss this possibility as an intermediate step towards a definition that is essentially based on operational semantics, but has a close connection to a traditional topic in denotational semantics. If languages L_{1} and L_{2} come equipped with denotational semantics, then for every class of phrases in each language, the denotational semantics gives us some way of determining whether phrases of this class are equivalent. For example, the usual denotational semantics of languages with higherorder procedures determines an equivalence of higher-order procedures. A useful notation is to write P =^{den} Q if expressions P and Q of L_{1} have the same meaning according to the denotational semantics of L_{1} . A natural definition of reduction is a mapping θ from L_{1} to L_{2} with

P =^{den} Q iff θP =^{den} θQ.

If we think of the denotation of a set of recursion equations as a numeric function, or the denotation of a program scheme as a mapping from predicate and function symbols in the first-order signature to functions, then the reductions we have discussed so far may be put in this form.

An important property of denotational semantics is substitutivity: if P =^{den} Q, then P may be substituted for Q in any program without changing the meaning of a program. As a consequence of substitutivity, whenever one language is reducible to another by a mapping that preserves denotational equivalence, we know that every expression in the first language may be translated to an expression in the second which serves the same purpose in every program context. This gives a good justification for using mappings that preserve denotational equivalence. The problem, however, is that many programming languages have many semantic interpretations, and it is not clear whether we want reductions to respect equivalence for all semantics, or for some “standard” one.

Instead of using denotational equivalence with respect to some model, we will use an equivalence relation based on operational semantics called observational equivalence. This relation coincides with denotational equivalence in the fully-abstract model of the language [Mil77, Plo77, Sto88], if it exists. We describe observational equivalence in this paragraph, and give the full, standard definition in the next section. Independent of any denotation semantics, observational equivalence is substitutive. We assume that full programs of a language L either run forever, or produce some kind of basic value as output. To simplify matters, we may assume that the inputs to a program are built into the program, and there is only one output. There is no harm in doing this because we will be able to compare programs with inputs and outputs by comparing their behaviors inside all possible “full programs” that supply inputs and select a single output. We say that two program phrases P and Q are observationally equivalent if, for any full program C[P] which produces a basic output value, the program C[Q] with Q replacing P produces the same value, and vice versa. Generally speaking, observational equivalence does not depend much on what we choose as the “basic values.” Observational equivalence is more robust than arbitrary denotational equivalence, and seems to lead to a plausible study of expressiveness and abstraction mechanisms. One technical difficulty, however, is that since fully abstract models are difficult to construct, there is a shortage of techniques for reasoning about observational equivalence.

3 Programming languages and abstraction-preserving reductions

Before defining reductions, we describe the assumptions we need to make about programming languages. In addition to a set of expressions, we need program contexts. Intuitively, a program context C[ ] is a program with a hole in it (represented by the empty brackets [ ] ). When a language is presented by, say, a BNF grammar, it is easy to see what the contexts are. However, we can develop at least part of the theory by taking the more abstract view that we are given some set of expressions and some set of contexts. We also need a set of observables, intuitively corresponding to the printable values of the language, and an operational semantics.

For the purposes of this paper, a programming language L = ⟨E, Ct, O, →^{eval}⟩ consists of a set E of expressions, a set Ct of contexts, a subset O ⊆ E of expressions which we will call the observables of the language, and an evaluation relation →^{eval}⊆ E × E .

We assume that every observable evaluates only to itself, i.e.,

If M ∈ O, then M →^{eval} N iff M ≡ N,

where ≡ is syntactic equivalence, and that every expression evaluates to at most one observable. (It is possible to extend the theory to nondeterministic programs, but for simplicity we will not do so.) A context C[ ] ∈ Ct may be any mapping from expressions to expressions. We will assume that every context is syntactically nontrivial in the sense that for any C[ ] , the expression M must occur as a subexpression of C[M] . This means that if C[M] ≡ C[N] then M ≡ N . We also assume, since we have not specified how contexts are derived from expressions, that the identity context C_{I}[ ] is included in Ct and the composition of any two contexts is a context. The identity context is the context mapping each expression of L to itself. For the purpose of defining observational equivalence, there is no loss of generality in assuming that the range of →^{eval} is O, i.e., if M →^{eval} N , then N ∈ O.

As the name suggests, two expressions M and N are observationally equivalent if we cannot observe any difference between them. Since the only way we can “observe” the behavior of an expression is by inserting it in a context which then yields an observable value, observational equivalence is defined as follows. Expressions M and N of a language L are observationally equivalent, written M =^{obs} N , if for every context C[ ] ,

For all P ∈ O, C[M] →^{eval} P iff C[N] →^{eval} P.

In other words, whenever C[M] or C[N] evaluates to an observable, both evaluate to the same observable.

A simple property of observational equivalence is that it is syntactic equality for observables.

Lemma 3.1 If M, N ∈ O are observables, then M =^{obs} N iff M ≡ N .

This follows from our assumption that there is an identity context C_{I}[ ] .

For most languages, observational equivalence does not depend heavily on the specific choice of observables (see [MC88] for some related discussion). For example, 3 and true may be distinguished in many ways. If both are considered observable, then the identity context C_{I}[ ] ≡ [ ] will distinguish them. If the integers are taken as observable but the booleans are not, then these expressions are still distinguishable by the identity context. If we take only the integer 0 as the single observable, then we can distinguish 3 from true using either context C[ ] ≡ [ ]−3 or C[ ] ≡ if [ ] then 0 else 1 fi . A more general statement about changes in observables is given in the following proposition.

Proposition 3.2 Let L = ⟨E, Ct, O_{1}, →^{eval}⟩ be any programming language and =^{obs}_{1} observational equivalence determined using observables O_{1} . Let O_{2} ⊆ E and let =^{obs}_{2} be observational equivalence on E determined using observables O_{2} . Suppose that for every P ∈ O_{1} there is some Q ∈ O_{2} and context C[ ] such that if M →^{eval} P then

C[M] →^{eval} Q and if M ↛^{eval} P then C[M] ↛^{eval} Q. Then =^{obs}_{2} ⊆ =^{obs}_{1} .

This gives a reasonable way of establishing that two sets of observables give the same observational equivalence.

It also seems appropriate to comment on the decision to treat contexts as total functions from expressions to expressions. An alternative and more detailed view is to treat contexts as partial function, since C[M] might not be well-formed. However, since evaluation is partial and we are only concerned with programs that evaluate to observables, we can account for the partiality of contexts by taking evaluation to be undefined on expressions that are not well-formed. More specifically, if a language is presented using a static semantics S: E → {OK , error} and a dynamic semantics Eval: E ⇀ E , then we can correctly model the language by defining

M →^{eval} N iff S(M) = OK and Eval(M) = N.

A similar approach may be used if evaluation is only defined on a subset P ⊆ E of expressions, such as the closed expressions that have certain types.

It is important to realize that the observational equivalence of two expressions M and N depends on the entire language, not just the way that M and N are evaluated. For example, if we could form pairs of basic values, but could not examine the components of a pair, then any two pairs might be observationally equivalent. However, if we add projection functions to the language, then pairs become observationally equivalent only if their components are equivalent. Thus adding new features to a language may make observationally equivalent expression inequivalent. For this reason, we must say which language we have in mind when we use the symbol =^{obs} .

Intuitively, an abstraction mechanism is a way of hiding some of the differences between program phrases. For example, in Algol-like languages, procedures with local variable declarations provide abstraction because we can take algorithms that work in different ways and hide their differences by placing them inside procedure declarations. To be more concrete, we may take two sorting algorithms that have different effects on temporary variables and enclose the two algorithms inside procedure bodies with local declarations of temporaries. If the two algorithms have the same effect on arrays, the two procedures will be equivalent. Thus, we can explain how procedures provide abstraction by observing that the context

procedure sort (a: int array)

begin temp: int ; [ ] end

allows us to transform inequivalent expressions (sorting algorithms with different side effects on temporary variables) into equivalent ones. For the purpose of this paper, it seems reasonable to define abstraction by this property.

A context C[ ] is an abstraction context for L if C[M] =^{obs} C[N] for some expressions

M ≠^{obs} N which are not observationally equivalent. The reason why such a context is called an “abstraction context” is that it obscures the difference between two otherwise distinguishable phrases. If we allowed syntactically trivial contexts C[ ] with M not occurring in C[M] , then every language would have an abstraction context. However, we do not consider syntactically trivial contexts. Even among the syntactically nontrivial contexts, there may be contexts C[ ] with C[M] =^{obs} C[N] for all M, N . Any of these semantically trivial contexts fits our definition since it maps inequivalent arguments to equivalent results. This is not completely satisfactory, but it is not clear how far to go in patching the definition to avoid this.

An abstraction-preserving reduction from L_{1} to L_{2} is a mapping θ of expressions to expressions and contexts to contexts satisfying the following two conditions.

(R1)  θ(C[M]) =^{obs} (θC)[θM],
(R2)  M =^{obs} N iff θM =^{obs} θN.

Intuitively, the first condition says that θ respects the compositional meaning of programs, while the second condition is that θ must preserve observational equivalence (and inequivalence).

The name “abstraction-preserving reduction” is now explained by the following lemma.

Lemma 3.3 Suppose language L_{1} has an abstraction context C and θ is an abstractionpreserving reduction from L_{1} to L_{2} . Then θC is an abstraction context for L_{2} . More-

over, if C hides the difference between inequivalent M ≠^{obs} N in L_{1} , by C[M] =^{obs} C[N] ,

then θC similarly hides the difference between inequivalent θM ≠^{obs} θN in L_{2} .

An immediate consequence of the lemma is that if L_{1} has an abstraction context and L_{2} does not, then there is no abstraction-preserving reduction from L_{1} to L_{2} . This will lead us to conclude, in Section 7, that no language with an abstraction context is reducible to Lisp with fexpr.

Proof of Lemma 3.3: We assume that C[ ] is an abstraction context for L_{1} and θ is an abstraction-preserving reduction from L_{1} to L_{2} . Since C[ ] is an abstraction

context, C[M] =^{obs} C[N] for some M ≠^{obs} N in L_{1} .

From the definition of abstraction-preserving reduction, we know that

θ(C[M]) = (θC)[θM]

and similarly for N . Since C[M] =^{obs} C[N] , it follows that

(θC)[θM] =^{obs} (θC)[θN].

If we can show that θM ≠^{obs} θN , then it will follow that θC is an abstraction context

for L_{2} . But θM ≠^{obs} θN follows directly from the assumption that M ≠^{obs} N and the fact that θ preserves observational equivalence (and inequivalence).

Before considering the implications for parts of programs, we show that given a correspondence between observables, the existence of an abstraction-preserving reduction from L_{1} to L_{2} implies that every function on observables definable in L_{1} is also definable in L_{2} . To explain this concretely, let us assume that the observables for each language are the natural numbers, and that we have an abstraction-preserving reduction θ: L_{1} → L_{2} that maps each natural number n ∈ N to itself. A partial function f on natural numbers is definable in L_{i} if there is a context C_{f}[ ] with the

property that for all n, m ∈ N , C_{f}[n] →^{eval} m iff f(n) is defined and equal to m. It is easy to see that if f is definable in L_{1} , and θ: L_{1} → L_{2} preserves natural numbers, then f is definable in L_{2} , as follows. If f is defined by by C_{f}[ ] , then since θ maps contexts to contexts, there is a context θC_{f}[ ] in L_{2} with the property

θC_{f}[n] →^{eval} m iff θC_{f}[θn] →^{eval} θm iff C_{f}[n] →^{eval} m iff f(n) is defined and equal to m.

Therefore, θC_{f}[ ] defines f in L_{2} . A more general statement, with essentially the same proof, follows.

Proposition 3.4 Suppose θ: L_{1} → L_{2} is an abstraction-preserving reduction giving a bijective correspondence between some subset N_{1} ⊆ O_{1} of the L_{1} observables and some subset N_{2} ⊆ O_{2} of the L_{2} observables. If partial function f: N_{1} → N_{1} is definable in L_{1} by context C_{f}[ ] , then θC_{f}[ ] defines the partial function θ ∘ f ∘ θ^{−1}: N_{2} → N_{2} in L_{2} .

Therefore, an abstraction-preserving reduction not only preserves abstraction contexts, but also the set of definable functions on observable values. It is easy to show that the composition of two abstraction-preserving reductions is abstraction preserving.

Proposition 3.5 The composition of two abstraction-preserving reductions is an abstractionpreserving reduction.

4 A Simple Abstraction-Preserving Reduction

Many commonly-used equivalences between program constructs, such as the equivalence between a block with an initialized local variable, and a procedure declaration followed by a call may be described as abstraction-preserving reductions. Instead of proving this for a language with assignment, we will consider a similar translation in a functional setting. Specifically, we can reduce lambda calculus with let declarations

                             let x = M in N

to pure lambda calculus by mapping a let declaration (as above) the lambda term

(λx.N)M.

To demonstrate what is involved in proving that a very simple translation is abstractionpreserving, we will go through this in some detail.

Let L_{1} be the ordinary untyped lambda calculus, with expressions defined by

M: : = x | M_{1}M_{2} | λx.M

and evaluation the least congruence relation containing α -conversion (renaming of bound variables) and β -reduction

(λx.M)N →^{β} [N/x]M,

where [N/x]M is the result of substituting N for free occurrences of x in M . (We assume bound variables are renamed during substitution to avoid capture, as usual). Let L_{2} be the lambda calculus extended with the additional construct

                             let x = M in N

and associated evaluation rule

let x = M in N → [M/x]N.

The contexts of each language are obtained by deleting one subexpression from any expression of the language, as usual. We take the normal forms, expressions which cannot be reduced, as the observables of both languages.

We will give an abstraction-preserving reduction of L_{2} to L_{1} . The reduction θ is defined inductively as follows.

\begin{matrix}θx = & x \\ θ(M_{1}M_{2}) = & (θM_{1}) (θM_{2}) \\ θ(λx.M) = & λx.θM \\ θ(let x = M in N) = & (λx.θN)(θM) \end{matrix}

Since contexts are derived from expressions, this is also a translation of L_{2} contexts to L_{1} contexts. Furthermore, since θ is defined by induction on the structure of expressions, it is easy to verify (R1) . It remains to verify condition (R2) of the definition of abstraction-preserving reduction.

We will show that M =^{obs} N iff θM =^{obs} θN using properties of lambda calculus reduction. It is helpful to first realize that for any M in L_{2} , the terms M and θM have a common reduct P . We reduce M to P by reducing all the let redexes (from the bottom of the parse tree of the term up, so as to eliminate all let’s from M ), and reduce θM to P by “mimicking” this reduction in θM . Another helpful observation is that every L_{1} context is an L_{2} context and, similarly, every L_{2} context may be converted to an equivalent L_{1} context.

Suppose that M =^{obs} N . Let C[ ] be any L_{1} context with C[θM] reducing to a normal form P . Let Q be any common reduct of M and θM . Then C[M] reduces to C[Q] and so C[M] reduces to P . Since M =^{obs} N , we know that C[N] also reduces to P . By similar reasoning we can show that C[θN] reduces to P . This demonstrates that θM =^{obs} θN . The converse implication is proved using the same ideas.

5 Abstraction-Preserving Extensions

If the expressions and contexts of one language are subsets of the expressions and contexts of another (respectively), we might ask whether the identity map on expressions and contexts is abstraction-preserving. In general, if we have two languages,

L_{1} = ⟨E_{1}, Ct_{1}, O_{1}, →^{eval}_{1}⟩ and L_{2} = ⟨E_{2}, Ct_{2}, O_{2}, →^{eval}_{2}⟩ with E_{1} ⊆ E_{2} and Ct_{1} ⊆ Ct_{2} ,

then the identity map from L_{1} expressions and contexts to L_{2} expressions and contexts is abstraction-preserving iff we have

M =^{obs}_{1} N iff M =^{obs}_{2} N

for all expressions M and N of L_{1} , where =^{obs}_{i} is observational equivalence in language L_{i}. This amounts to saying that the observational equivalence theory of L_{2} is a conservative extension of the observational equivalence theory of L_{1} . It does not follow that the observables of L_{1} are a subset of those of L_{2} , or that →^{eval}_{2} restricted to E_{1} coincides with →^{eval}_{1} . Since all of the examples we wish to consider have these additional properties, we will incorporate them into the definition of “abstractionpreserving extension” below.

We say language L_{1} is a sublanguage of L_{2} , written L_{1} ⊆ L_{2} or L_{2} ⊇ L_{1} , if the E_{1} ⊆ E_{2} , Ct_{1} ⊆ Ct_{2} , O_{1} ⊆ O_{2} , and the restriction of →^{eval}_{2} to E_{1} expressions is →^{eval}_{1} . It is easy to show that if L_{1} is a sublanguage of L_{2} , then whenever M, N ∈ L_{1} are distinguishable in L_{1} , they are also distinguishable in L_{2} . (This would not follow from only E_{1} ⊆ E_{2} and Ct_{1} ⊆ Ct_{2} .) However, two expressions M, N ∈ L_{1} may be observationally equivalent in L_{1} and observationally distinct in L_{2} . This is because the richer language L_{2} may provide more contexts for observing M and N . We will say that L_{2} ⊇ L_{1} is an abstraction-preserving extension of L_{1} if M =^{obs} N ∈ L_{1} iff

M =^{obs} N ∈ L_{2} for all M, N ∈ L_{1} .

There are many trivial examples of abstraction-preserving extensions, and some nontrivial ones. A relatively trivial example is the extension of untyped lambda calculus (language L_{1} of the last section) to lambda calculus with let (language L_{2} of the last section). In general, an abstraction-preserving extension L_{2} ⊇ L_{1} may contain many more constructs than L_{1} , or only a few. The definition does not require any particular relationship between L_{1} and L_{2} other than when we compare L_{1} expressions using L_{2} contexts, we make precisely the same distinctions as if we only consider L_{1} contexts.

A non-example that may be intuitively familiar is the relationship between a simple concurrent extension of an Algol-like language and its sequential sublanguage. We explain this using the construct

                          cobegin S_{1} and S_{2} end

which executes statements S_{1} and S_{2} concurrently. The same phenomenon occurs in a variety of concurrent programming languages. The single assignment x: = 2 is observationally equivalent to the sequence of assignments x: = 1; x: = x + 1 in many common sequential languages. However, assuming we compare programs by printed output, these may be distinguished by the concurrent context

                 C[ ] : : = cobegin [ ] and x: = 2 end; print x

which executes the inserted statement in parallel with another assignment to the variable x. If we assume that assignments to x are atomic, but sequences of assignments are not, then C[x: = 1; x: = x + 1] may produce more possible final values of x than C[x: = 2] . An interesting variation on this example is that if we have an atomicity primitive in our concurrent language, then we could embed the sequential sublanguage into the full language in an abstraction-preserving way. The main idea is to reduce a sequential statement S to the statement atomic(S) which would be guaranteed atomic. We conjecture that with suitable treatment of procedure declarations and other constructs, a language embedding along these lines could be proved abstraction-preserving.

An interesting abstraction-preserving language extension involves the addition of recursive types to typed functional languages. Let L_{1} be a typed lambda calculus with an arbitrary selection of base types like the integers and booleans, and function types like int → int , int → bool , (int → int) →(int → int) , and so on. We assume that L_{1} allows recursive function declarations, and may add sum or product types if we wish. Let L_{2} be obtained from L_{1} by adding recursively-defined types. The richer language L_{2} lets us write type declarations like

tree = atom + tree × tree which we could not write in L_{1} . It follows immediately from the construction in [Mul87, Chapter 4] that L_{2} is an abstraction-preserving extension of L_{1} . This follows from the fact, summarized in [Mul87, Section 4.6], that the fully-abstract (sub)model for typed lambda calculus with recursive types is an extension of the fully-abstract (sub)model for typed lambda calculus without recursive types.

6 A Translation That is Not Abstraction Preserving

At the time the first version of this paper was written, there was some debate about the application of so-called strong and weak sums from type theory to programming languages. In particular, MacQueen argued against existential types, or weak sums, as a basis for the ML module facility [Mac86]. Instead, he used strong sums. In retrospect, the argument seems to be one of apples vs. oranges: weaks sums provide data abstraction, while strong sums allow programs to be modularized with minimum restriction. Clarifying the difference between strong and weak sums and, in particular, showing that weak sums have an advantage for providing abstraction, was one of the original motivations for formulating the theory presented here. In this section, we show that any map taking a weak sum expression to the corresponding strong sum expression is not abstraction-preserving. The proof is essentially straightforward, drawing on [Rey83, Mit86, Mit91], but requires some definitions.

We extend the typed lambda calculus with two forms of sums. To keep the notation as simple as possible, the syntax of the two extensions will overlap. We will refer to the language with weak sums as λ^{→, weak Σ} and the language with strong sums as λ^{→, strong Σ} . In both languages, there are two universes of type expressions (see [Mar84, MH88]). The types of the first universe, U_{1} , have the form

τ : : = t | b | τ_{1} → τ_{2}

where t is any type variable, b a type constant, τ_{1} → τ_{2} the type of functions from τ_{1} to τ_{2} . The additional types of the second universe are sums

σ : : = τ | Σt.σ,

where Σt.σ is the sum type whose elements are a form of pair consisting of a type and an element of a type, and first projections applied to strong sums (described below). The terms common to both languages have the form

M : : = x | c | λx: τ.M | M_{1}M_{2} | ⟨t = τ, M: σ⟩

where c is any constant symbol of the language, ⟨t = τ, M: σ⟩ has type Σt.σ if M has type [τ/t]σ. Precise typing rules are given in the Appendix. For weak sums, we add the form

                     abstype t with x: σ is M in N

which binds type variable t and term variable x to the first and second components of M: Σt.σ with scope N . The additional typing constraints associated with abstype are that t cannot be free in the type of any free variable of N other than x, and t cannot occur free in the type of N . The evaluation rule for abstype is

abstype t with x: σ is ⟨t = τ, M: σ⟩ in N → [M/x][τ/t]N.

Further description of the correspondence between this construct and abstract types in programming languages may be found in [MP88], and also [CW85].

Strong sums are similar to weak sums, but with fewer typing restrictions. Instead of abstype, we add projection functions Fst and Snd . If M has type Σt.σ, then

Fst M is a type expression, and

Snd M is a term with type [Fst M/t]σ.

The evaluation rules for Fst and Snd are

\begin{aligned}Fst ⟨t = τ, M: σ⟩ & → & τ \\ Snd ⟨t = τ, M: σ⟩ & → & M \end{aligned}

There are several translations from weak to strong sums which leave all the common type and term expressions fixed. For example, we may map abstype expressions to a combination of Fst and Snd according to the scheme

             abstype t with x: σ is ⟨t = τ, M: σ⟩ in N

↦ (λy: (Σt.σ).[Snd y/x][Fst y/t]N)⟨t = τ, M: σ⟩.

We show that no translation that leaves expressions of sum type fixed is abstractionpreserving.

Proposition 6.1 No translation from λ^{→, weak Σ} to λ^{→, strong Σ} that maps each expression M: Σt.σ not containing Fst or Snd to itself is abstraction preserving.

Proof We will give two expressions, ⟨t = τ, M_{1}: σ⟩ and ⟨t = τ, M_{2}: σ⟩ of type Σt.σ, not containing Fst or Snd , which are observationally equivalent in λ^{→, weak Σ} , but distinguishable using strong sums. From the results of [Rey83, Mit86, Mit91], in particular Corollary 1 of [Mit91], it follows that if there is a binary relation on the set of elements of type τ such that M_{1} and M_{2} map related arguments to related results, then if we take elements of some basic type (named by a type constant) as observables, ⟨t = τ, M_{1}: σ⟩ and ⟨t = τ, M_{2}: σ⟩ will be indistinguishable. In particular, if M_{1} and M_{2} both define elements of τ or first-order functions from τ to τ , and the pairs ⟨t = τ, M_{1}: σ⟩ and ⟨t = τ, M_{2}: σ⟩ define isomorphic algebras (with carriers given by τ and operations given by M_{1} or M_{2} ), then they will be indistinguishable. A simple example, therefore, is just to let

\begin{aligned}τ & : : = & b → b → b \\ M_{1} & : : = & λx: b.λy: b. x \\ M_{2} & : : = & λx: b.λy: b. y \\ σ & : : = & t \end{aligned}

so that ⟨t = τ, M_{1}: σ⟩, ⟨t = τ, M_{2}: σ⟩: Σt.t are trivially indistinguishable using only weak sums, but easily distinguished using Snd and application to a pair of distinguishable elements of type b.

We may explain this proposition using the terminology of the programming language Ada. Ada packages may have public types, corresponding to strong sums, and private types, corresponding to weak sums. It may seem that we can eliminate private types, since any program with private types may be written using public types without changing the output of the program. However, merely changing private types to public types does not preserve abstraction. One way to understand this distinction is to consider the problem of writing and maintaining a stack package in a program library. If a private type is used, and several programs are written using the package, then we are free to change the implementation of stacks. The abstraction provided by private types guarantees that changes in the type will not be observable by client programs, as long as the stack operations are implemented correctly. In contrast, if the stack package is written using public types, some client programs may depend on the actual type used to represent stacks. This makes it impossible for the author of the stack package, who cannot see all the client programs, to safely change the implementation. Since the form of abstraction provided by private types is useful in practice, it seems worthwhile to have a theory of expressiveness that distinguishes public from private types.

7 Lisp is Not Universal

Recall that an abstraction context is a context C[ ] with C[M] =^{obs} C[N] for some

expressions M ≠^{obs} N which are not observationally equivalent. In languages where expressions can examine the text of their subexpressions, there are no abstraction contexts. An example is Lisp, when we have the ability to define special forms that do not evaluate their arguments.

Claim 7.1 Lisp with fexpr has no abstraction contexts.

The justification of this claim rests on the fact that if two Lisp expressions M and N are syntactically different, then there is some context C[ ] using fexpr which distinguishes M from N . Recall that a fexpr is a function which does not evaluate its arguments [WH81]. Instead, the unevaluated arguments are put together in a list and passed to the fexpr. For example, if we apply the function f defined by

(defun f fexpr ( x) (car x)).

to the arguments A, B, C , as in

( f A B C ),

the result is the unevaluated first argument A. Thus, given any syntactically distinct M and N , a context C[ ] which applies a fexpr to its argument may distinguish between M and N . The context may return an observable value like 0 or 1 depending on what the n -th character is. For n chosen properly, we will have C[M] →^{eval} 0

and C[N] →^{eval} 1 , so M ≠^{obs} N . Thus syntactically different Lisp expressions are not observationally equivalent.

Now suppose C[ ] is an abstraction context for Lisp. We will see that this leads

to a contradiction. We have C[M] =^{obs} C[N] for some M ≠^{obs} N . But C[M] =^{obs} C[N] implies that C[M] and C[N] are syntactically identical. Therefore, since M and N appear in C[M] and C[N] (respectively), it follows that M and N are syntactically identical. This contradicts the assumption that C[ ] is an abstraction context and justifies the claim.

We have the following consequence of Lemma 3.3 and Claim 7.1.

Proposition 7.2 If L is a language with an abstraction context, then there is no abstraction-preserving reduction from L to Lisp with fexpr.

It is worth recalling from Lemma 3.3 that if C[ ] is an abstraction context and θ an abstraction-preserving reduction, then the behavior of C[ ] on equivalence classes of expressions determines the behavior of θC[ ] on equivalence classes in the range of θ. Consequently, if C[ ] is semantically nontrivial, θC[ ] must be as well. Thus no language with a semantically nontrivial abstraction context can be reduced to a language with only semantically trivial abstraction contexts. In future research, it would be worthwhile to explore this form of argument more carefully. In particular, it seems possible to use the way that the translation θC of an abstraction context C must hide differences between translations of inequivalent expressions to derive more significant negative results.

8 Comparison with related work

Three related papers are Riecke’s comparative study of three standard evaluation strategies [Rie91], Shapiro’s general framework [Sha91] and Felleisen’s general theory of programming language expressiveness [Fel90]. Since Riecke’s paper uses abstractionpreserving reductions, we discuss this first.

Riecke compares call-by-value, call-by-name and lazy versions of the language PCF, which is a typed lambda calculus with natural numbers, parallel and sequential conditional and recursion operators. In rough terms, the main results are that call-by-value and lazy PCF are equally expressive, and both are more expressive than call-by-name PCF. In symbols,

call-by-name ≁^{<} call-by-value ≅ lazy PCF

The three reductions, from call-by-name to call-by-value, and between call-by-value and lazy PCF are first given as abstraction preserving reductions, as defined in this paper. However, to show that neither call-by-value nor lazy PCF may be reduced to call-by-name PCF, Riecke requires additional assumptions in the form of a stronger notion of reduction. The stronger definition, called functional translation, is roughly similar to an abstraction-preserving reduction induced by a logical relation between the two languages [Sta85, Mit90]. This relies on the type structures of the two languages, which apparently must be identical. Along with the negative results based on functional translations, Riecke observes that his reductions from call-by-name to call-by-value, and between call-by-value and lazy PCF are all functional translations. An apparently minor point is that the paper leaves open whether the composition of two functional translations is a functional translation.

The difference between the three versions of PCF is essentially evaluation order, except for an additional construct in lazy PCF. For all of the languages, the observables are the numerals. Call-by-value evaluation of an application MN first evaluates the function and argument to “values,” which are either lambda abstractions or atomic symbols, and then evaluates the function application. In call-by-name evaluation of MN , only M must be evaluated. If M ignores its argument, and the evaluation of N does not terminate, the application MN will terminate in call-by-name but not in call-by-value. In lazy PCF we use call-by-name evaluation order, but also observe termination of function expressions. Termination in lazy PCF is observed using convergence testing primitive conv^{σ,τ}: σ → τ → τ . We may observe convergence at type σ using the context C_{σ}[ ] ≡ conv^{σ,nat} [ ] 0 which has the property that if M has type σ, then C_{σ}[M] either diverges or evaluates to the numeral 0 .

A technically important construct of all three language is parallel conditional. With this operator, we have standard domain-theoretic constructions of fully abstract models [Plo77, Sto88]. These are used in an essential way to prove that the reductions from call-by-name to call-by-value, and between call-by-value and lazy PCF preserve observational equivalence. Without fully-abstract models, it seems difficult to show that such reductions are abstraction-preserving.

In motivating functional translations, Riecke makes some important observations about the weaker possibility of effective (computable) translations that preserve observational equivalence. By a simple Gödel-numbering trick, we may construct a reduction satisfying (R2) from any language, L_{1} , to any other, L_{2} , provided only that we are able to write an interpreter interp_{1,2} for L_{1} in L_{2} . Given such an interpreter, we reduce L_{1} to L_{2} by mapping a term M to the application interp_{1,2}⌈M⌉, where ⌈M⌉ is the Gödel number of M . Analyzing this suggestion using the definitions of the present paper, we can see that in order to satisfy (R2), the interpreter interp_{1,2} must “execute” the code, or text, ⌈M⌉, for a full program M , producing the correct observable if M halts with an observable value, and diverging otherwise. In the case that M is, for example, an expression defining a function on the natural numbers, then interp_{1,2}⌈M⌉ cannot produce a string, natural number, or an element of any other set whose equality function is definable by computing observables. The reason is that otherwise we would be able to decide equality of numeric functions, which is impossible if all partial recursive functions are definable in L_{1} . This observation is important, since it suggests that it is difficult to satisfy condition (R1). The Gödel-numbering translation is “almost” compositional since ⌈M⌉ may be defined compositionally from M . However, the way interp_{1,2} is used keeps this translation from being obviously compositional. More specifically, for condition (R1) to hold, we would need

Θ(C[M]) ≡ interp_{1,2}⌈C[M]⌉ =^{obs} (ΘC)[ΘM] ≡ (ΘC)[interp_{1,2}⌈M⌉]

Regardless of how we might define ΘC[ ] , if M is the definition of a numeric function, then we need interp_{1,2}⌈M⌉ to produce some kind of L_{2} expression that is not an observable or Gödel number of some kind. This apparently requires expressiveness of L_{2} beyond the ability to define all partial recursive functions on natural numbers.

An interesting open problem is whether there is an abstraction-preserving reduction from either call-by-value or lazy PCF to call-by-name PCF. To show that no abstraction-preserving reductions exist would strengthen Riecke’s negative results. Another interesting direction would be to develop the theory of functional translations in greater depth, including the generalization to languages with other type structures.

Felleisen proposes a general theory for determining whether a set of constructs within a language are “eliminable,” or expressible by the remaining constructs [Fel90]. The apparent connection with language reductions is that when L_{1} ⊆ L_{2} , we might expect there to be a reduction from L_{2} to L_{1} exactly if the additional constructs of L_{2} are eliminable, relative to L_{1} . Felleisen’s theory is described as an adaptation of Kleene’s notion of definitional extension from logic [Kle52] to programming languages. The paper discusses two forms of expressiveness, called eliminability and macro-eliminability. Since the first is much closer to the concepts discussed here, we will not consider the more restrictive notion of macro-eliminability. (In fairness, we should point out that macro-eliminability is a major focus of [Fel90].) If the constructs of L_{2} ⊇ L_{1} are eliminable, we say L_{2} is a definitional extension of L_{1} .

In Felleisen’s theory, a programming language is modeled as a set of phrases, freely generated by a set of constructors F_{1}, F_{2}, …, each with a specificed arity. The set of well-formed programs must be some recursive subset of the phrases. Programs are compared using a predicate halts? which is true if the program halts under the implicit operational semantics. (Felleisen calls this predicate eval, but we will write halts? to avoid confusion with the notation of the present paper.) A significant difference between Felleisen’s theory and the one suggested here is the difference between the termination theory of a language and the observational equivalence theory. Termination is determined directly by evaluation, while observational equivalence involves consideration of all program contexts, and therefore depends on the surrounding language. A recursion-theoretic distinction is that the termination theory of a language is typically re-complete, while the observational equivalence theory is typically Π_{2} -complete. This makes Felleisen’s definitional extensions easier to reason about; definitional extensions provide different information from abstraction-preserving reductions.

An important subsidiary definition in Felleisen’s theory is that L_{2} is a conservative extension of L_{1} if the phrases of L_{2} contain those of L_{1} , program-hood is conservative, and the termination theory of L_{2} is conservative over the termination theory of L_{1} . This is very similar to our definition of language extension, given in Section 5, except for the difference between the two models of programming languages. The main definition is that when L_{2} is a conservative extension of L_{1} , the additional constructs of L_{2} are eliminable if there is a recursive mapping Φ of L_{2} phrases to L_{1} phrases which is compositional with respect to L_{1} constructors only, maps programs to programs, and which preserves the termination theory. The main positive example is that let is eliminable from a λ -calculus extended with let, which is analogous to the abstraction-preserving reduction given in Section 4 of this paper. The only negative example claimed in [Fel90] is that call-by-name lambda abstraction is not eliminable from a lambda calculus containing both call-by-value and call-by-name lambda abstraction. This is similar to Riecke’s theorem showing that there is no functional translation from call-by-name to call-by-value.

As mentioned above, we might compare Felleisen’s theory of eliminability with our definition of reduction by seeing whether, given L_{2} conservative over L_{1} , there is an abstraction-preserving reduction from L_{2} to L_{1} iff L_{2} is a definitional extension of L_{1} . A special case of conservative extension makes it easy to see that these two conditions are not equivalent, on very general grounds. Given any two languages, L_{1} and L_{2} , modeled either as in Felleisen’s paper or this one, there is an obvious definition of their disjoint union, which we will write symbolically as L_{1} ⊎ L_{2} . By Felleisen’s definition of conservative extension, L_{2} ⊎ L_{1} is always a conservative extension of L_{1} . Thus, we might conjecture, a priori, that there is an abstraction-preserving reductions from L_{2} to L_{1} iff L_{2} ⊎ L_{1} is a definitional extension of L_{1} . However, in this special case, definitional extension is a largely degenerate concept. All that is required for L_{2} ⊎ L_{1} to be a definitional extension of L_{1} is a recursive map Φ from L_{2} phrases to L_{1} phrases such that for every L_{2} program e, we have halts?_{L2}(e) iff halts?_{L1}(Φe) . Riecke’s Gödel numbering argument, summarized above, shows that there exists such a recursive map from L_{2} to L_{1} whenever an L_{2} interpreter is definable in L_{1} . More specifically, we can see that L_{2} ⊎ L_{1} is a definitional extension of L_{1} whenever the halting predicate for L_{2} is derived from an effective (computable) operational semantics, there is a Gödel numbering of L_{2} phrases as L_{1} expressions, and all partial recursive functions are definable in L_{1} .

For the reader familiar with [Fel90], we give a few additional comparisons. Theorems 3.6 and 3.8 of [Fel90] relate definitional extension to the existence of compositional (homomorphic) mappings that send each L_{2} expression to an L_{2} -observationally equivalent L_{1} expression. Theorem 3.6 gives a sufficient condition, in these terms, for L_{2} being a definitional extension of L_{1} , and Theorem 3.8 relates non-existence of homomorphic mappings to L_{2} not being a definitional extension of L_{1} . Together, these two theorems provide an intuitive point of comparison between Felleisen’s theory of expressiveness and the existence of abstraction-preserving reductions. However, both of these theorems are uninformative if we wish to compare L_{2} ⊎L_{1} with L_{1} . This problematic special case makes it difficult to prove any precise connections between the theories. In more detail, Theorem 3.6 does not apply to L_{2} ⊎ L_{1} and L_{1} , due to a detail in Felleisen’s definition of observational equivalence that allows e and e′ to be equivalent only if there is a context C[ ] such that both C[e] and C[e′] are programs. This makes e from L_{2} and e′ from L_{1} observationally inequivalent in the disjoint union L_{2} ⊎L_{1} , and therefore no translation Φ satisfying the hypotheses of the theorem could possibly exist. For similar reasons, Theorem 3.8 does not give any sufficient condition implying that L_{2} ⊎ L_{1} is not a definitional extension of L_{1} . In addition, these theorems only require the maps from L_{2} to L_{1} to be compositional on L_{1} only, not on all of L_{2} . Therefore, by Riecke’s argument, these allow Gödel numbering translations. However, with some modification to eliminate Gödel numbering translations, the criteria given in Theorems 3.6 and 3.8 of [Fel90] might provide a basis for a general theory closer to the one given here.

Motivated by the need to compare parallel languages, Shapiro discusses the general issues involved in using language translations to make language comparisons. The first few sections of [Sha91] contain useful general discussion that puts the theory suggested here in perspective, suggesting and evaluating a number of alternatives. The main theories discussed in the paper use translations that respect observational equivalence in some way. However, instead of choosing one specific class of language translations, Shapiro analyzes several variants that respect observational equivalences to differing degrees. The strongest conditions correspond closely to the theory given in the present paper. All of the translations in [Sha91] are required to satisfy a homomorphism condition similar to (R1). However, the paper raises the interesting possibility of selecting certain favored operations. In the terminology of the present paper, one may choose to require (R1) only with respect to certain contexts. All of the results in [Sha91] use language translations that are only homomorphic with respect to parallel composition.

9 Conclusions and Directions for Further Investigation

This paper defines abstraction-preserving reductions, which are syntax-directed (homomorphic) reductions that preserve observational equivalence. Some simple translations and language embeddings are easily seen to be abstraction preserving. One example is the translation of blocks to function declarations and calls. A nontrivial example is the extension of a functional language with finite types to a language with recursivelydefined types. The proof that this extension is abstraction-preserving involves detailed reasoning about the inclusive predicates which link the operational and denotational semantics of each language (developed in [Mul87], not here). One kind of reduction that is not abstraction preserving is the kind of reduction that replaces abstract “private” types with concrete “public” types (in Ada terminology). In addition, we show that many languages are not reducible to Lisp with user-defined special forms.

The general theory sketched here is tentative, and it would be interesting to extend the preliminary definitions in several ways. One refinement would be to adopt a more specific language model, in which a context-free or context-sensitive grammar determines both the expressions and the contexts. Some related comments and suggestions may be found in [Rie91]. Another direction is to examine the two clauses of our definition more closely. The constraint (R2) that a reduction must preserve observational equivalence seems quite natural, although we could consider weakening the “iff” to an implication or reverse implication. (These variations are discussed in [Sha91].) The intent of clause (R1), which forces reductions to preserve contexts, or be “homomorphic,” is intended to rule out language reductions such as Gödel numberings. An open question is whether (R1) actually eliminates all reductions that we would intuitively recognize as Gödel-numberings. Therefore, it may be desirable to strengthen or alter this condition on the basis of further investigation, as discussed in [Rie91]. An open question is whether abstract data type declarations can be reduced to polymorphic function declarations and calls. Two translations have been proposed [Rey83, MP88], and one is easily shown not to preserve abstraction. It would be interesting to show that the other one is abstraction preserving.

It is easy to argue that Lisp with fexpr is not a “universal” language, since no language with an abstraction mechanism can be reduced to Lisp in an abstractionpreserving manner. This points out an unusual aspect of fexpr that is intuitively recognized by many Lisp programmers. It also shows that the existence of abstractionpreserving reductions depends on more than the set of definable functions. This is important since the set of definable first-order functions is the same for all practical programming languages. We do not know whether there is a natural universal language for the theory outlined here, restricting our attention to languages with a finite presentation and computable evaluation relation. An additional condition that might impose some useful structure on the problem of finding a universal language is to require that if M →^{eval} N , then M =^{obs} N . This is relevant to Lisp with user-defined special forms since our proof that Lisp has no abstraction contexts involves showing that this general principle is violated.

Acknowledgements: Thanks to Jon Riecke, Kim Bruce and the anonymous referees for helpful suggestions.

References

[CW85] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471–522, 1985.

[Fel90] M. Felleisen. On the expressive power of programming languages. In Proc. European Symp. on Programming, pages 134–151, Berlin, 1990. Springer LNCS 432.

[Gre75] S.A. Greibach. Theory of Program Structures: Schemes, Semantics, Verification. Springer LNCS 36, Berlin, 1975.

[Kle52] S.C. Kleene. Introduction to Metamathematics. Van Nostrand, New York, 1952.

[Mac86] D.B. MacQueen. Using dependent types to express modular structure. In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 277– 286, 1986.

[Mar84] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.

[MC88] A.R. Meyer and S.S. Cosmadakis. Semantical paradigms: Notes for an invited lecture. In Proc. IEEE Symp. Logic in Computer Science, pages 236–263, 1988.

[MH88] J.C. Mitchell and R. Harper. The essence of ML. In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 28–46, January 1988.

[Mil77] R. Milner. Fully abstract models of typed lambda calculi. Theoretical Computer Science, 4(1), 1977.

[Mit86] J.C. Mitchell. Representation independence and data abstraction. In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 263–276, January 1986.

[Mit90] J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, pages 365–458. North-Holland, Amsterdam, 1990.

[Mit91] J.C. Mitchell. On the equivalence of data representations. In V. Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 305–330. Academic Press, 1991.

[MP88] J.C. Mitchell and G.D. Plotkin. Abstract types have existential types. ACM Trans. on Programming Languages and Systems, 10(3):470–502, 1988. Preliminary version appeared in Proc. 12th ACM Symp. on Principles of Programming Languages, 1985.

[Mul87] K. Mulmuley. Full abstraction and semantic equivalence. The MIT Press, 1987.

[PH70] M. Paterson and C. Hewitt. Comparative schematology. In Proj. MAC Conf. on Concurrent Systems and Parallel Computation. MIT, 1970.

[Plo77] G.D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[Rey83] J.C. Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing ’83, pages 513–523. North-Holland, Amsterdam, 1983.

[Rie91] J.G. Riecke. Fully abstract translations between functional languages. In Proc. 18th ACM Symp. on Principles of Programming Languages, pages 245–254, January 1991.

[Sha91] E. Shapiro. Separating concurrent languages with categories of embeddings. In Proc. ACM Symp. Theory of Computing, pages 198–208, 1991.

[Sta85] R. Statman. Logical relations and the typed lambda calculus. Information and Control, 65:85–97, 1985.

[Sto88] A. Stoughton. Fully Abstract Models of Programming Languages. Pitman, London, and John Wiley and Sons, New York, 1988.

[WH81] P.H. Winston and B.K.P. Horn. Lisp. Addison-Wesley, 1981.

Appendix. Typing rules for weak and strong sums

⟨⟩ environment

\frac{Γ ▷ τ : U_{1}}{Γ, x: τ environment}

\frac{Γ ▷ σ : U_{2}}{Γ, x: σ environment}
(x ∉ Dom(Γ))
\frac{Γ environment c: σ given}{Γ ▷ c : σ}  \frac{Γ environment Γ(x) = σ}{Γ ▷ x : σ}
\frac{Γ ▷ α Γ ▷ τ : U_{1}}{Γ, x: τ ▷ α}  \frac{Γ ▷ α Γ ▷ σ : U_{2}}{Γ, x: σ ▷ α}
(x ∉ Dom(Γ), α is M: τ or M: σ)
\frac{Γ ▷ M : τ Γ ▷ τ = τ′ : U_{1}}{Γ ▷ M : τ′}  \frac{Γ ▷ M : σ Γ ▷ σ = σ′ : U_{2}}{Γ ▷ M : σ′}

Table 1: Environment and structural rules

\frac{Γ environment}{Γ ▷ U_{1} : U_{2}}  \frac{Γ ▷ τ : U_{1}}{Γ ▷ τ : U_{2}}

Table 2: Universes

\frac{Γ ▷ τ : U_{1} Γ ▷ τ′ : U_{1}}{Γ ▷ τ → τ′ : U_{1}}

\frac{Γ ▷ τ : U_{1} Γ ▷ τ′ : U_{1} Γ, x: τ ▷ M : τ′}{Γ ▷ λx: τ.M : τ → τ′}  (x ∉ Dom(Γ))

\frac{Γ ▷ M : τ → τ′ Γ ▷ N : τ}{Γ ▷ MN : τ′}

Table 3: Types and terms in U_{1}

\frac{Γ, t: U_{1} ▷ σ : U_{2}}{Γ ▷ Σt.σ : U_{2}}  (t ∉ Dom(Γ))
\frac{Γ ▷ τ : U_{1} Γ ▷ [τ/t]M : [τ/t]σ Γ, t: U_{1} ▷ σ : U_{2}}{Γ ▷ ⟨t=τ, M: σ⟩ : Σt.σ}  (x ∉ Dom(Γ))
\frac{Γ ▷ M : Σt.σ}{Γ ▷ Fst(M) : U_{1}}  \frac{Γ ▷ M : Σt.σ}{Γ ▷ Snd(M) : [Fst(M)/t]σ}
\frac{Γ ▷ M : Σt.σ Γ, t: U_{1}, x: σ ▷ N : τ}{Γ ▷ abstype t with x: σ is M in N : τ}  t not free in Γ or τ

Table 4: Types and terms in U_{2}