On the Expressive Power of Programming Languages

Matthias Felleisen^{∗} Department of Computer Science Rice University Houston, TX 77251-1892

Abstract

The literature on programming languages contains an abundance of informal claims on the relative expressive power of programming languages, but there is no framework for formalizing such statements nor for deriving interesting consequences. As a first step in this direction, we develop a formal notion of expressiveness and investigate its properties. To validate the theory, we analyze some widely held beliefs about the expressive power of several extensions of functional languages. Based on these results, we believe that our system correctly captures many of the informal ideas on expressiveness, and that it constitutes a foundation for further research in this direction.

1 Comparing Programming Languages

The literature on programming languages contains an abundance of informal claims on the expressive power of programming languages. Arguments in these contexts typically assert the expressibility or non-expressibility of programming constructs relative to a language. Unfortunately, programming language theory does not provide a formal framework for specifying and verifying such statements. Comparing the set of computable functions that a language can represent is useless because the languages in question are usually universal; other measures do not exist. The lack of a comparison relation makes it impossible to draw any firm conclusions from expressiveness claims or to use them for an objective decision about the use of a programming language.

∗Supported in part by NSF grant CCR 89-17022 and Darpa/NSF grant CCR 87-20277.

Landin [24] was the first to propose the development of a formal framework for comparing programming languages. He studied the relationship between programming languages and constructs, and began to classify some as “essential” and some as “syntactic sugar.” A typical example of an inessential construct in Landin’s sense is the let-expression in a functional language with first-class procedures. It declares and initializes a new, lexically-scoped variable before evaluating an expression. Whether it is present or absent is inconsequential for a programmer since

let x be v in e is expressible as apply (procedure (x) e) v.

Similarly, few programmers would consider it a loss if a goto-free, Algol-like language had a while but not a repeat construct. After all,

repeat s until e is expressible as s; while ¬e do s.

Others, most notably Reynolds [36, 37] and Steele and Sussman [40], followed Landin’s example. They introduced the informal notion of the core of a language and studied the expressiveness of imperative extensions of higher-order functional languages. Steele and Sussman [40:29] summarized the crucial idea behind this kind of classification of language features with the remark that a number of programming constructs are expressible in an applicative notation based on syntactically local, structure- and behavior-preserving translations, but that some, notably control statements and assignments, involve complex reformulations of large fractions of programs.

In the realm of logic, Kleene anticipated the idea of expressible or eliminable syntactic symbols in his study of formal systems [21:§74]. Troelstra [42:I.2] resumed this work and introduced further refinements and extensions. Roughly, the additional symbols of a conservative extension of a core logic are eliminable if there is a translation from the extended logic to its core that satisfies a number of conditions. Two of these are important for our purposes. First, the mapping is the identity on the formulae of the core language and is homomorphic in the logical connectors. Second, if a formula is provable in the extension then so is its translation in the core. Clearly, these two conditions imply that this translation preserves the structure of formulae and removes symbols on a local basis.

By adapting the ideas about the relationship among formal systems to programming languages, we obtain a relation that determines whether a programming language can express a programming construct. More precisely, given two universal programming languages that only differ by a set of programming constructs, {c_{1},…, c_{n}}, the relation holds if the additional constructs make the larger language more expressive than the smaller one. Here “more expressive” means that the translation of a program with occurrences of one of the constructs c_{i} to the smaller language requires a global reorganization of the entire program. A first analysis shows that this measure of expressiveness supports many informal judgements in the literature. Moreover, we discover that an increase in expressive power comes at the expense of less “intuitive” semantic equivalence relations. We also discuss some attempts at generalizing the measure to a comparison relation for arbitrary programming languages.

The next section briefly reviews the logical notions of eliminable symbols and definitional extensions. In subsequent sections, we propose a formal model of expressibility and expressiveness along the lines of logical expressiveness, investigate some of its properties, and analyze the expressive powers of several extensions of functional languages. More specifically, we introduce our formal framework of expressiveness based on the notion of expressibility. We demonstrate the abstract concepts by proving some sample theorems about λ-calculus-based languages as well as a number of meta-theorems. Next, we study the expressiveness of an idealized version of Scheme and verify the informal expressiveness philosophy behind its design [41]. Following this analysis, we briefly speculate how the use of a more expressive language increases programming convenience. Finally, we compare our ideas to related work and address some open questions.

2 Eliminable Symbols and Definitional Extensions

The theory of comparing formal systems is a peripheral topic in logical studies and finds little or no space in most textbooks. The following short overview summarizes and adapts Troelstra’s [42:I.2] descriptions of Kleene’s work [21].

A formal system is a triple of sets: expressions, formulae, and theorems. The second is a subset of the first, the third a subset of the second. Expressions are freely generated (in the sense of a term algebra) from a number of non-logical and logical operators, e.g., ∧, →, ↔, etc. The set of formulae is a recursive subset of the set of expressions and satisfies certain well-formedness criteria. The set of theorems is the subset of the formulae that the formal system defines to be true. If L is a formal system, then Exp(L) is its set of expressions, Fm(L) the set of formulae, and Thm(L) the set of theorems; L ⊢ t also means t is a theorem of L.

A conservative extension L of a formal system L′ is a formal system whose expressions are a superset of the expressions over L′, generated from a richer set of operators, and whose formulae and theorems restricted to the expressions of L′ are the formulae and theorems of L′:

Fm(L) ∩ Exp(L′) = Fm(L′); Thm(L) ∩ Exp(L′) = Thm(L′).

A conservative extension L is a definitional extension of L′ if there is a mapping φ : Exp(L) → Exp(L′) that satisfies the following conditions:

F1 φ(f) ∈ Fm(L′) for each f ∈ Fm(L);

F2 φ(f) = f for all f ∈ Fm(L′);

F3 φ is homomorphic in all logical operators; F4 L ⊢ t if and only if L′ ⊢ φ(t); and

F5 L ⊢ t ↔ φ(t).

Kleene referred to those symbols that generate the additional expressions of the extended formal system as eliminable.

Remark 1 (Weak Expressibility). Kleene’s original definition contains a weaker version of Condition 3, namely,

F4′ if L ⊢ t then L′ ⊢ φ(t).

Based on condition F5, it is possible to show that the two definitions are equivalent, assuming the usual axioms for ↔ [21:§74]. As we shall discuss in several remarks below, this is not the case in the context of programming languages. Instead, condition F4′ leads to a different but related notion of language expressiveness.

3 A Formal Theory of Expressiveness

As a first step towards a formal theory of expressiveness for programming languages, we adapt the logical theory of eliminable symbols to the programming language context. We develop the idea of a programming language as a formal system and reinterpret the concepts of conservative extension and eliminability accordingly. Since many of the examples in the work of Landin, Reynolds, Steele, and Sussman preserve not only the global structure of the program but also the local structure of the transformed phrases, we consider a stricter notion of eliminability as a second step. We refer to this second notion as macro expressibility. It satisfies the additional constraint that the transformation of eliminated phrases is always compositional. In the two subsections on the respective topics, we prove theorems about the eliminability and non-eliminability of programming constructs and apply them to a simplistic prototype language based on the λ-calculus. Both notions of expressibility suggest natural comparative measures of the expressive power of programming languages, which we present in the third subsection.

3.1 Expressibility

Like a formal system, a programming language is a system of subsets of a general language. More precisely, a programming language is a set of phrases, a subset of programs, and a semantics that determines some aspects of the behavior of programs.

Definition 3.1. (Programming Language) A programming language L consists of • a set of L-phrases, which is a set of freely generated abstract syntax trees (or

terms), based on a possibly infinite^{1} number of function symbols , _{1},… with arities a, a_{1},…;

• a set of L-programs, which is a non-empty, recursive subset of the set of phrases; and

• a semantics, eval_{L}, which is a recursively enumerable predicate on the set of L-programs. If eval_{L} holds for a program P, the program terminates.

The function symbols are referred to as programming constructs or programming facilities.

Definition 3.1 is an abstraction of the typical specifications of many realistic programming languages. Most languages have a context-free syntax yet enforce additional context-sensitive constraints by recursive^{2} decision procedures. Examples of such constraints are scoping^{3} and typing rules, which ensure that names only occur in certain pieces of text and only range over a restricted set of values.

To avoid restrictive assumptions about the set of programming languages, the definition only requires that the semantics observe the termination behavior of programs. By omitting any references to the characteristics of results, it is possible to consider programming languages with and without observable data. For programming languages with simple output data, i.e., constants or opaque representations of procedures, the definition is in many cases equivalent to a definition that refers to the observable output of a program. For a consideration of languages with infinite output, e.g., through imperative output statements or through potentially infinite lists, the definition needs some adjustments.

Finally, the above definition of a programming language also shows that, in a certain sense, a programming language is a formal system. The set of phrases corresponds to the expressions of a formal system, the set of programs plays the role of the set of formulae, and the set of terminating programs is the analog of the set of theorems. In the terminology of universal algebra, the set of expressions is the universe of a free term algebra [5]; instead of relying on the more typical algebraic

1We assume that there is enough structure on an infinite set of constructors for specifying the decidability of predicates and the recursiveness of translations on the set of phrases. In the following examples, this is obviously the case.

2A notable exception is Scheme as defined in the standard report [35], which only has a recursively enumerable set of programs: An expression is a Scheme program if and only if it has the same result for all possible evaluation orders in its applications. We consider this an unfortunate aberration rather than an interesting extension of our definition.

3Although most languages impose lexical scoping, Definition 3.1 only accounts for this fact through the recursive selection of programs from the set of phrases. An explicit inclusion of the lexical scoping structure through a Church encoding [7] of the language in a typed lambda calculus is a feasible and interesting alternative but would probably lead to a slightly different definition of expressibility and expressiveness.

Phrases

e ::= x | v | (ee)  (expressions)
v ::= (λ_{v}x.e) | (λ_{n}x.e)  (values)

Programs e is a program if and only if fv(e) = ∅

where fv(e) is the set of free variables in e

Semantics eval_{Λ}(e) holds if and only if e ⟶^{∗} v for some v

Evaluation Contexts

E ::= α | ((λ_{v}x.e)E) | (Ee)

Reduction Steps

\begin{matrix}E((λ_{n}x.e)e′) & ⟶ & E(e[x/e′]) & (β) \\ E((λ_{v}x.e)v) & ⟶ & E(e[x/v]) & (β_{v}) \end{matrix}

where e[x/e′] is the capture-free substituion of e′ for all free x in e

Figure 1: The programming language Λ

approach of equational restrictions, the definition uses arbitrary recursive predicates for filtering out the interesting subset of programs. Unlike logic, the programming language world does not know such ubiquitous constructs as the logical connectors.

Our prototypical example of a programming language is a derivative of the language Λ of the pure λ-calculus [3]. Figure 1 summarizes its (concrete) syntax and semantics. In order to compare the expressiveness of call-by-value and call-by-name procedures later in this section, we extend Λ with a new constructor, λ_{v}, and rename λ to λ_{n}. More specifically, the Λ-phrases are generated from a set of variables (0ary constructors), {x, y, z,…}, and two families of unary constructors, one for each variable x: λ_{v}x : term ⟶ term (call-by-value abstraction), λ_{n}x : term ⟶ term (call-by-name abstraction), and one binary constructor: · : term × term ⟶ term (juxtaposition). Below, λ_{v} and λ_{n} denote the sets of all λ-constructors. For readability, we use concrete syntax for Λ-terms and adopt the traditional λ-calculus conventions about its use [3].

The constructors λ_{v}x and λ_{n}x bind the variable x in their term arguments. The set of free variables in an expression e, fv(e), is the set of variables that are in e and are not bound. If all variables in a Λ-term are bound, the term is closed. The set of Λ-programs is the set of closed phrases, i.e., there is only one recursive constraint that distinguishes programs from arbitrary phrases.

The operational semantics of Λ reflects the semantics of realistic programming languages like Iswim, ML, and Scheme [34].^{4} The specification of the semantics in Figure 1 follows the style of extensible operational semantics [8, 10], which is easily adaptable to the imperative extensions of Λ in the following section. An evaluation is a sequence of reduction steps on programs according to the normal-order strategy. If the program is a value (an abstraction), the evaluation stops. Otherwise, the reduction function (uniquely) decomposes the program into an evaluation context, a term with a hole (α), and a redex, the contents of the hole. A redex is either an application of a call-by-name abstraction to an arbitrary expression (β) or an application of a call-by-value abstraction to a value (β_{v}). In either case, the reduction function replaces the redex, ((λ_{x}.b)a), by a new version of the procedure body, b[x/a]. Then the evaluation process starts over again.

Summarizing the standard reduction process as a predicate on programs yields the operational semantics of Λ. Some useful examples of phrases are the call-by-name and call-by-value fixed point operators, which facilitate the recursive definition of functions:

Y_{n} = (λ_{n}f.(λ_{n}x.f(xx))(λ_{n}x.f(xx)))

and

Y_{v} = (λ_{v}fx.(λ_{v}g.gg)(λ_{v}x.f(λ_{v}x.(gg)x))x).

Two simple diverging programs are Ω_{n} = Y_{n}(λ_{n}x.x) and Ω_{v} = Y_{v}(λ_{v}xy.xy)(λ_{v}x.x).

To illustrate the impact of syntactic constraints on programs, we also define Λ^{t}, a typed variant of Λ. Λ^{t} has the same set of phrases as Λ but uses a type checking algorithm for filtering out valid programs. A Λ^{t} program is not only closed but is also typable as either an integer or a higher-order functional on integers according to the type inference system in Figure 2. It easily follows from Milner’s [27] initial work on polymorphism that typability is a recursive predicate for Λ^{t}. The semantics of Λ^{t}-programs is the same as that of their untyped counterparts.

Λ^{t} is a typical example of a monomorphic language: all occurrences of a λ-bound variable have the same type. As a consequnce, the typing constraints of Λ^{t} exclude typical Λ-programs like λx.(xx) or phrases like (xx) in programs. Indeed, the Y operator for defining recursive functions must be typed explicitly because it would not pass the other type rules.

Based on the interpretation of a programming language as a formal system, it is easy to define the notion of a conservative programming language extension.

Definition 3.2. (Conservative Extension & Restriction) A programming language L is a conservative extension of a language L′ if

• the constructors of L′ are a subset of the constructors of L with the difference being { _{1},…, _{n},…}, which are not constructors of L′;

4As usual, this operational semantics has only remote connections to the equational theory of the λ-calculus.

Programs e is a program if and only if it is closed and ∅ ⊢ e : τ

Types

τ ::= ι | τ ⟶ τ

Type Assertion A: Variables ⟶ ∘ Types (finite functions)

where A[x/τ](x) = τ  A[x/τ](y) = A(y)  (functional update)

Type Inference

A ⊢ x : τ if A(x) = τ  \frac{A[x/τ] ⊢ e : τ′}{A ⊢ λ_{v,n}x.e : τ ⟶ τ′}  \frac{A ⊢ e : τ′ ⟶ τ; A ⊢ e′ : τ′}{A ⊢ (ee′) : τ}

A ⊢ Y_{n} : (τ ⟶ τ) ⟶ τ A ⊢ Y_{v} : ((τ ⟶ τ′) ⟶ (τ ⟶ τ′)) ⟶ (τ ⟶ τ′)

Figure 2: Λ^{t}

• the set of L′-phrases is the full subset of L-phrases that do not contain any constructs in { _{1},…, _{n},…};

• the set of L′-programs is the full subset of L-programs that do not contain any constructs in { _{1},…, _{n},…}; and

• the semantics of L′, eval_{L}′, is a restriction of L’s semantics, i.e., for all L′- programs P, eval_{L}′(P) holds if and only if eval_{L}(P) holds.

Conversely, L′ is a conservative restriction of L.

To emphasize the constructors on which the restriction and extension differ, we write L′ = L \ { _{1},…, _{n},…} and L = L′ + { _{1},…, _{n},…}. We also use the notation to denote the natural restriction and extension that result from subtracting or adding facilities to the syntax (provided the respective languages and, in the latter case, a semantic specification exist).

In our running example, the restricted language Λ_{n} is Λ without λ_{v}-abstractions, Λ_{v} is Λ without call-by-name abstractions:

Λ_{n} = Λ \ λ_{v}; Λ_{v} = Λ \ λ_{n}.

A restriction of the above evaluation process to Λ_{v}- and Λ_{n}-phrases yields a call-by-value and a call-by-name semantics, respectively. The corresponding sublanguages of Λ^{t} are defined similarly.

To enrich the set of examples, we add a let construct to Λ. There is one binary let constructor for each variable x: let_{x} : term × term ⟶ term. Like λx, let_{x} binds its variable, namely in the second subexpression. The concrete syntax for let_{x}(e, e′) is

(let x be e in e′).

The semantics of Λ + {let_{x}}, or Λ + let for short, requires an additional clause in the specification of evaluation contexts

E ::= … | (let x be E in e)

and an additional clause for the reduction function:

E(let x be v in e) ⟶ E(e[x/v]).  (let_{v})

Otherwise the definition of the semantic predicate in Figure 1 stays the same. It is trivial to check that Λ + let is a conservative extension of Λ.

The extension of Λ^{t} with let additionally requires a type inference rule for the new construct. For greater flexibility, the new rule only requires that, at each occurrence of the abstracted variable, the named subexpression is typable with some type:

\frac{A ⊢ e : τ; A ⊢ e[x/e′] : τ′}{A ⊢ (let x be e in e′) : τ′}

Λ_{v}^{t} + let is polymorphic in the spirit of ML [27, 28, 43:43, 44]. Unlike λ-bound variables, let-bound variables can have several types. For example, x in (let x be (λy.y) in (xx)) conceptually assumes two different types: (ι ⟶ ι) ⟶ (ι ⟶ ι) and (ι ⟶ ι), which makes the expression a legal program despite the self-application of a variable. Again, it is easy to see that the extension is conservative with respect to Λ^{t}.

For the re-interpretation of the logical notion of eliminability, we need to be more flexible. The non-existence of ubiquitous programming language features in the sense of logical connectors raises the question whether the mapping from the extended language to the core should be homomorphic and, if so, on which set of features. At this point, we recall the above-mentioned desire that our translations be structurepreserving, and the idea that the homomorphic character of a translation naturally corresponds to this property. To preserve the structure of programs as much as possible, we require that the translations be homomorphic in all programming facilities of the core language.

Definition 3.3. (Eliminability; Expressible Programming Constructs) Let L be a programming language and let { _{1},…, _{n},…} be a subset of its constructors such that L′ = L\{ _{1},…, _{n},…} is a conservative restriction. The programming facilities 1,…, _{n},… are eliminable if there is a recursive mapping φ from L-phrases to L′- phrases that satisfies the following conditions:

E1 φ(e) is an L′-program for all L-programs e;

E2 φ( (e_{1},…, e_{a})) = (φ(e_{1}),…, φ(e_{a})) for all facilities of L′ , i.e., φ is homomorphic in all constructs of L′; and

E3 eval_{L}(e) holds if and only if eval_{L}′(φ(e)) holds for all L-programs e.

We also say that L′ can express the facilities _{1},…, _{n},… with respect to L. We omit the qualification if the language universe is clear from the context. By abuse of notation, we write φ : L ⟶ L′.

Condition E2 in this definition implies that the mapping φ is the identity on the language L′. It corresponds to conditions F2 and F3 of the logical notion of eliminability. According to the above interpretation of a programming language as a formal system, an interpretation of condition F4 in Section 2 requires that the translation of a terminating program in the extended language is a terminating program in the restricted language. This is precisely the contents of Condition E3. Finally, the last condition of the logical notion of eliminability, F5, has no counterpart in a programming language context because of the lack of a ubiquitous programming construct.

Remark 2 (Weak Expressibility). By using an adaptation of Kleene’s original Condition F4′ (see Remark 1 in the previous section) instead of the third condition in the preceding definition, we get a weak notion of expressibility. The revised condition takes on the following shape:

F3′. if eval_{L}(e) holds then eval_{L}′(φ(e)) holds,

The intuition behind this definition is that the translated phrase has at least as many capabilities as the original one. The terminology reflects our belief that any differences in behavior should be noted as a failure of complete expressibility. Moreover, the terminology is also consistent with the fact that expressibility implies weak expressibility.

An alternative understanding of the above definition is that the translation maps phrases constructed from eliminated symbols to observationally indistinguishable phrases in the smaller language. In other words, replacing the original phrase with its translation does not affect the termination behavior of the surrounding programs. This relation between two phrases of programming languages is widely studied in semantics and is known as operational (or observational) equivalence [25, 29, 33, 34]. After developing the formal definition of operational equivalence, we can characterize sufficient conditions for the eliminability of programming constructs.

A formal definition of the operational equivalence relation relies on the auxiliary notion of a program context.

Definition 3.4. (Contexts; Program Contexts) An n-ary context over L, C(α_{1},…, α_{n}), is a freely generated tree based on L’s constructors and the additional, 0-ary constructors α_{1},…, α_{n}, called meta-variables. All subtrees of C(α_{1},…, α_{n}) are also n-ary contexts. If C(α_{1},…, α_{n}) is a context and e_{1},…, e_{n} are phrases in L, then the instance C(e_{1},…, e_{n}) is a phrase in L that is like C(α_{1},…, α_{n}) except at occurrences of α_{i} where it contains the phrase e_{i}:

• if C(α_{1},…, α_{n}) = α_{i} then C(e_{1},…, e_{n}) = e_{i}, and

• if C(α_{1},…, α_{n}) = (C_{1}(α_{1},…, α_{n}),…, C_{a}(α_{1},…, α_{n})) for some with arity a then C(e_{1},…, e_{n}) = (C_{1}(e_{1},…, e_{n}),…, C_{a}(e_{1},…, e_{n})).

An L-program context for a phrase e is a unary context, C(α), such that C(e) is a program.

For Λ_{n}, the context C_{0}(α) = (λ_{n}xy.α)(λ_{n}x.x)Ω_{n} is a program context for all expressions whose free variables are among x and y.

Since the semantic predicate of a programming language only tests a program for its termination behavior, our definition of operational equivalence compares the termination behavior of programs.^{5}

Definition 3.5. (Operational Equivalence) Let L be a programming language and let eval_{L} be its operational semantics. The L-phrases e_{1} and e_{2} are operationally equivalent, e_{1} ≅_{L} e_{2}, if there are contexts that are program contexts for both e_{1} and e_{2}, and if for all such contexts, C(α), eval_{L}(C(e_{1})) holds if and only if eval_{L}(C(e_{2})) holds.

With the above program context C_{0}, it is possible, for example, to differentiate the phrases x and y. Since Ω_{n} diverges, C_{0}(x) = (λ_{n}xy.x)(λ_{n}x.x)Ω_{n} terminates whereas C_{0}(y) = (λ_{n}xy.y)(λ_{n}x.x)Ω_{n} diverges.

Figure 3 contains a sequent calculus of operational equivalence on Λ_{v} + let, which is used below in Proposition 3.7; the proof system is similar to Riecke’s for a typed version of Λ_{v} [38]. The calculus proves equations over the language from premisses (Γ) that are finite sets of equations. It is sound but incomplete, i.e., if ∅ ⊢ e = e′ then e ≅ e′ but not vice versa.

Remark 3 (Weak Expressibility). A replacement of the “if-and-only-if” condition with a simple “if” condition yields the notion of operational approximation, which plays the same role for weak expressibility as operational equivalence for expressibility. More specifically, the term e_{1} operationally approximates e_{2}, e_{1} ∼_{L} e_{2}, if for all program contexts, C(α), for e_{1} and e_{2}, eval_{L}(C(e_{2})) holds if eval_{L}(C(e_{1})) holds. — In conjunction with the above context C_{0}, the program context C_{1}(α) = (λ_{n}yx.α)(λ_{n}x.x)Ω_{n} shows that x and y do not approximate each other.

5In many cases, our definition is equivalent to the more traditional definition that compares the termination behavior of programs and the results, provided they are among a set of observable data.

Γ ⊢ (λ_{v}x.e)v = e[x/v]  Γ ⊢ Ωe = Ω  Γ ⊢ eΩ = Ω

\frac{Γ ⊢ e = e′}{Γ ⊢ λ_{v}x.e = λ_{v}x.e′} x ∉ fv(Γ)  \frac{Γ ⊢ e = e′}{Γ ⊢ ee′′ = e′e′′}  \frac{Γ ⊢ e = e′}{Γ ⊢ e′′e = e′′e′}

Γ ⊢ (let x be v in e) = e[x/v] Γ ⊢ (let x be Ω in e) = Ω

\frac{Γ ⊢ e = e′}{Γ ⊢ (let x be e in e′′) = (let x be e′ in e′′)} x ∉ fv(Γ)

Γ ∪ \{e = e′\} ⊢ e = e′ \frac{Γ ∪ \{e = Ω\} ⊢ e_{1} = e_{2}; Γ ∪ \{e = v\} ⊢ e_{1} = e_{2} for all v}{Γ ⊢ e_{1} = e_{2}}

Γ ⊢ e = e  \frac{Γ ⊢ e = e′}{Γ ⊢ e′ = e}  \frac{Γ ⊢ e = e′; Γ ⊢ e′ = e′′}{Γ ⊢ e = e′′}

Figure 3: A Calculus for Operational Equivalence on Λ_{v} + let

We now have everything in place to formalize our above idea about the connection between eliminable programming constructs and their translations. The following theorem shows that, at least to some extent, the elimination of expressible programming constructs from a program is a local process and keeps the program structure intact.

Theorem 3.6 Let L = L′ + { _{1},…, _{n},…} be a conservative extension of L′. If φ : L ⟶ L′ is homomorphic in all facilities of L′ and preserves program-ness, and if i(e_{1},…, e_{a_{i}}) ≅_{L} φ( _{i}(e_{1},…, e_{a_{i}})) for all _{i} and all L-expressions e_{1},…, e_{a_{i}}, then L′ can express the facilities _{1},…, _{n},….

Proof. It suffices to show that condition E3 of Definition 3.3 holds for φ. Assume that P is an L-program such that eval_{L}(P) holds. By the construction of P, there is a context C(α_{1},…, α_{n}) such that

P = C(p_{1},…, p_{n})

where p_{1}, …, p_{n} are the finite number of outermost occurrences of phrases constructed from some facilities in _{1},…, _{n},…. Thus, C(α_{1}, p_{2},…, p_{n}) is a program context for p_{1}. It follows from the theorem’s assumption that

eval_{L}(C(p_{1},…, p_{n})) holds if and only if eval_{L}(C(φ(p_{1}),…, p_{n})) holds.

Repeating this step n times proves that

eval_{L}(C(p_{1},…, p_{n})) holds if and only if eval_{L}(C(φ(p_{1}),…, φ(p_{n}))) holds.

But, since C does not contain any facilities in _{1},…, _{n},…,

C(φ(p_{1}),…, φ(p_{n})) = φ(C(p_{1},…, p_{n})) = φ(P).

Moreover, since L conservatively extends L′,

eval_{L}(P) holds if and only if eval_{L}′(φ(P)) holds.

This completes the proof.

Remark 4 (Weak Expressibility). The theorem holds for weak expressibility even if we replace operational equivalence by operational approximation: If _{i}(e_{1},…, e_{a_{i}}) ∼_{L} φ( _{i}(e_{1},…, e_{a_{i}})), then the _{1},…, _{n},… are weakly eliminable.

An application of this theorem shows that let is an example of an eliminable construct. For the typed setting, this provides a precise formalization of the folk theorem that ML-style polymorphism is expressible in a monomorphic language.^{6} The two examples also reveal a striking difference between the typed and the untyped language variant. Whereas the untyped let expression simply abbreviates an application as illustrated in the introduction, its typed counterpart maps to a version of the let body in which each occurrence of the abstracted variable is substituted with a copy of the named expression. The reason for this difference is that in the typed case the translation must not only preserve the semantics but also the typability in order to preserve program-ness.

Proposition 3.7 The constructor let is eliminable in call-by-value languages.

(i) Λ_{v} can express let with respect to Λ_{v} + let.

(ii) Λ_{v}^{t} can express let with respect to Λ_{v}^{t} + let.

Proof. (i) Set φ(let x be e in e′) = (λ_{v}x.φ(e′))φ(e). To show that the two phrases are operationally equivalent we proceed by induction on the number of let’s in the subexpression. The base case for e, e′ in Λ_{v} proceeds as follows. By the homomorphism constraint, φ(e) = e and φ(e′) = e′. By the laws in Figure 3,

e = Ω ⊢ (let x be e in e′) = Ω = (λx.e′)e

and, for all values v,

e = v ⊢ (let x be e in e′) = e′[x/v] = (λx.e′)e,

6An alternative approach to a formalization of this folk theorem is due to Wand [44].

and therefore,

(let x be e in e′) ≅_{Λ+let} (λx.e′)e.

The induction step proceeds along the same line.

(ii) Set φ(let x be e in e′) = ((λ_{v}d.φ(e′)[x/φ(e)])φ(e)) where d does not occur free in e or e′. To verify that this translation maps programs to programs, it suffices to prove that the translation preserves the implicit type assignment. We proceed by induction on the number of let-expressions in the program and show that, given a fixed set of type assumptions, φ(e) has the same type as e. Assume e and e′ are let-free, and consider the typing of an instance of let:

A ⊢ (let x be e in e′) : τ′

for some A and τ′. By the setup of the inference system, A ⊢ e : τ for some τ and A ⊢ e′[x/e] : τ′. Since, by assumption, φ(e) = e and φ(e′) = e′, A ⊢ φ(e) : τ and A ⊢ φ(e′)[x/φ(e)] : τ′. The rest follows easily: A ⊢ (λ_{v}d.φ(e)[x/φ(e′)]) : τ ⟶ τ′ and also

A ⊢ (λ_{v}d.φ(e)[x/φ(e′)])φ(e) : τ′.

The induction step requires a lemma that proves φ(e)[x/φ(e′)] has the same type as e[x/e′] if φ(e) and φ(e′) have the same type as e and e′.

The proof that φ preserves the semantics of typed let-programs follows the same pattern as part (i). Observe that

e = Ω ⊢ (let x be e in e′) = Ω = (λd.e′[x/e])Ω = (λd.e′[x/e])e

and also, for all v,

e = v ⊢ (let x be e in e′) = e′[x/v] = (λd.e′[x/v])v = (λd.e′[x/e])e.

The rest is obvious.

The converse of Theorem 3.6 does not hold. That is, the facilities _{1},…, _{n},… may still be expressible in L′ even though the translation from L to L′ maps an eliminable phrase to an observably distinct element. One reason for this is that the set of programs may not contain an element such that _{i}(e_{1},…, e_{a_{i}}) for some _{i} occurs in a context over the restricted language, in which case it is irrelevant how the mapping φ translates this phrase. Thus, by imposing an appropriate condition, we can get a theorem on the non-expressibility of programming constructs.

Theorem 3.8 Let L = L′ + { _{1},…, _{n},…} be a conservative extension of L′. If for all mappings φ : L ⟶ L′ that are homomorphic in all facilities of L′, i(e_{1},…, e_{a_{i}}) ≅_{L̸} φ( _{i}(e_{1},…, e_{a_{i}})) for some L-expressions e_{1},…, e_{a_{i}} and _{i} in _{1},…, _{n},…, and if there is a context C(α) over L′ that witnesses this inequality, then L′ cannot express the facilities _{1},…, _{n},….

Proof. Let φ : L ⟶ L′ be an arbitrary mapping that is homomorphic in all facilities of L′. Suppose φ( _{i}(e_{1},…, e_{a_{i}})) = e and let C(α) be the context over L′ that observes the operational difference between e and _{i}(e_{1},…, e_{a_{i}}). Since φ is homomorphic over L′,

φ(C( _{i}(e_{1},…, e_{a_{i}}))) = C(φ( _{i}(e_{1},…, e_{a_{i}}))) = C(e).

But, by assumption, eval_{L}(C( _{i}(e_{1},…, e_{a_{i}}))) holds while eval_{L}(C(e)) and eval_{L}′(C(e)) do not hold (or vice versa). This implies that no mapping that is homomorphic over L′ can possibly satisfy condition E3 of Definition 3.3 if the antecedent of the theorem holds, and that consequently the programming constructs _{1},…, _{n},… cannot be eliminable.

Based on this first non-expressibility theorem, we can now prove that call-by-name Λ cannot express call-by-value abstractions and vice versa.

Proposition 3.9 Λ extends both Λ_{v} and Λ_{n}.

(i) Λ_{n} cannot express λ_{v} with respect to Λ.

(ii) Λ_{v} cannot express λ_{n} with respect to Λ.

Proof. ^{7} (i) According to the semantics for Λ_{n}, the application of an abstraction (λ_{n}y.p) to an argument can only proceed in one of the following three manners:

1. it may uniformly diverge for all arguments: whenever (λ_{n}y.p)e ⟶^{∗} e′ there is always an e′′ such that e′ ⟶ e′′;

2. it may uniformly converge to a value for all arguments, including Ω_{n}: for all expressions e there is a value v_{e} such that (λ_{n}y.p)e ⟶^{∗} v_{e};

3. it may activate the argument for a first time: (λ_{n}y.p)e ⟶^{∗} ee_{1} … e_{k} for some e_{1},…, e_{k}.

The proof of this auxiliary claim is a simple induction on the length of the reduction sequence. Also, it is easy to check that whenever e ⟶^{∗} e′ then E(e) ⟶^{∗} E(e′).

Let (λ_{v}x.e) be an abstraction in Λ that converges upon application to some values. More specifically, let e and v be in Λ_{n} and assume that for some value u, (λ_{v}x.e)v(λ_{n}x.x) ⟶^{∗} u. Then we claim that C(α) = (α v)(λ_{n}x.x) is the context that we are looking for in order to apply Theorem 3.8.

Assume that φ : Λ ⟶ Λ_{n} is a structure-preserving translation. Then φ(λ_{x}v.e) is or reduces to a value in Λ_{n}. Let λ_{n}y.p be this value. Since the original abstraction terminates upon application to some value, the translation of this application must terminate as well. Therefore λ_{n}y.p cannot diverge uniformly. On the other hand, the pre-image, λ_{v}x.e, also diverges upon application to Ω_{n}, which implies that the translation cannot converge uniformly. Thus, let e_{1},…, e_{k} be the expressions such that

7Improved by Carolyn Talcott.

C(φ(λ_{v}x.e)) = φ(λ_{v}x.e)v(λ_{n}x.x) ⟶^{∗} (λ_{n}y.p)v(λ_{n}x.x) ⟶^{∗} ve_{1} … e_{k}(λ_{n}x.x).

Setting e = λ_{n}x.x and v = λ_{n}x.Ω_{n} (which satisfy the original asumptions), it is trivial to see that this program now diverges. If n = 0 the reduction continues with:

… ⟶ (λ_{n}x.Ω_{n})(λ_{n}x.x) ⟶ Ω_{n} ⟶ …;

otherwise, it is:

… ⟶ (λ_{n}x.Ω_{n})e_{1} … e_{k}(λ_{n}x.x) ⟶ Ω_{n}e_{2} … e_{k}(λ_{n}x.x) ⟶ …

That is, whereas C(λ_{v}x.e) converges to (λ_{n}x.x), C(φ(λ_{v}x.e)) diverges. By the preceding theorem, we have shown our claim.

(ii) This part is much simpler. Take C(α) = (αΩ_{v}), e = (λ_{n}x.(λ_{n}x.x)) and assume that φ is a structure-preserving translation. Clearly, eval(C(λ_{n}x.(λ_{n}x.x))) holds, but, C(φ((λ_{n}x.(λ_{n}x.x)))) diverges. Hence, a structure-preserving translation cannot preserve operational equivalence, which proves the claim.

Remark 5 (Weak Expressibility). By Remark 4, Λ_{n} can weakly express λ_{v} because λ_{v}x.e ∼_{Λ} λ_{n}x.e.

An immediate corollary of Theorem 3.8 is that if for some phrase with an eliminable symbol there is no operationally indistinguishable expression in the restricted language, then the restricted language is less expressive than the full language. We use this corollary instead of the full theorem in Section 4.2.

Corollary 3.10 Let L = L′ + { _{1},…, _{n},…} be a conservative extension of L′. If for some _{i}(e_{1},…, e_{a_{i}}) there is a program context C over L′ but there is no e in L′ such that _{i}(e_{1},…, e_{a_{i}}) ≅_{L} e, then L′ cannot express the facilities _{1},…, _{n},…

3.2 Macro Expressibility

Although the definition of eliminable programming construct is a satisfactory first step towards a better understanding of the formal structure of programming languages, it does not completely account for the idealized notion of “syntactic sugar” of Landin and others [24, 36, 37, 40] as discussed in the introduction. In many cases, the elimination of “syntactic sugar” constructs not only preserves the global program structure but also the structure of the subexpressions of phrases built from eliminable constructs.

Recall the two examples from the introduction:

1. In a functional language with first-class functions, a let expression is simply an abbreviation of the immediate application of an anonymous procedure to an argument:

let x be v in e is expressible as apply (procedure (x) e) v.

2. In a goto-free, Algol-like language,

repeat s until e is expressible as s; while ¬e do s.

In both examples, the translation of a composite phrase is the (fixed) composition of the translation of its subphrases. More technically, the translation of a phrase is the evaluation of a term (in the sense of universal algebra [5]) over the restricted language at the translations of the subphrases. As mentioned above, terms correspond to contexts in our framework; for clarity, we refer to contexts as syntactic abstractions^{8} in relation to the following definition and its uses.

Definition 3.11. (Macro Eliminability; Macro Expressibility) Let L be a programming language and let { _{1},…, _{n},…} be a subset of its constructors such that L′ = L \ { _{1},…, _{n},…} is a conservative restriction. The programming facilities 1,…, _{n},… are macro eliminable if they are eliminable and if the eliminating mapping φ from L to L′ satisfies the following, additional condition:

E4 For each a-ary construct ∈ { _{1},…, _{n},…} there exists an a-ary syntactic abstraction, A, over L′ such that

φ( (e_{1},…, e_{a})) = A(φ(e_{1}),…, φ(e_{a})).

We also say that L′ can macro-express the facilities _{1},…, _{n},… with respect to L.

Remark 6 (Weak Expressibility). If some facilities are weakly expressible and satisfy the additional condition, we call them weakly macro-expressible.

Since macro expressibility is a restriction of simple expressibility, Theorem 3.6 on the eliminability of constructs requires some adaptation.

Theorem 3.12 Let L = L′ + { _{1},…, _{n},…} be a conservative extension of L′. If φ : L ⟶ L′ is homomorphic in all facilities of L′ and preserves program-ness, and if there is a syntactic abstraction A_{i} for each _{i} in _{1},…, _{n},… such that i(e_{1},…, e_{a_{i}}) ≅_{L} A_{i}(φ(e_{1}),…, φ(e_{a_{i}})) for all L-expressions e_{1},…, e_{a_{i}}, then L′ can macro-express the facilities _{1},…, _{n},….

8In Lisp-like languages, syntactic abstractions are realized as macros [22]; logical frameworks know them as notational abbreviations [17]. The terminology of equational algebraic specifications [16] refers to syntactic abstractions as derived operators.

Proof. It is easy to see that the additional condition in the antecedent is precisely what is needed to adapt the proof of Theorem 3.6 to the stronger conclusion.

Moreover, the additional condition E4 permits a simplification of the theorem to a corollary that no longer makes any reference to the translating map. The corollary is used in Section 4.

Corollary 3.13 Let L = L′ + { _{1},…, _{n},…} be a conservative extension of L′. If there is a syntactic abstraction A_{i} for each _{i} in _{1},…, _{n},… so that _{i}(e_{1},…, e_{a_{i}}) ≅_{L} A_{i}(e_{1},…, e_{a_{i}}) for all L-expressions e_{1},…, e_{a_{i}}, then L′ can macro-express the facilities 1,…, _{n},….

By Proposition 3.7, Λ_{v} can express let. A simple check of the proof reveals that the translation between the two languages satisfies the antecedent of the corollary, and that therefore let is also macro-expressible. More importantly, however, the additional condition E4 in Definition 3.11 also leads to a stronger meta-theorem on the non-expressibility of facilities. The new theorem shows that new programming constructs add to the expressive power of a language if their addition affects existing operational equivalences.

Theorem 3.14 Let L_{1} = L_{0} + { _{1},…, _{n},…} be a conservative extension of L_{0}. Let ≅_{0} and ≅_{1} be the operational equivalence relations of L_{0} and L_{1}, respectively.

(i) If the operational equivalence relation of L_{1} restricted to L_{0} expressions is not equal to the operational equivalence relation of L_{0}, i.e., ≅_{0} ≠ (≅_{1} |L_{0}), then L_{0} cannot macro-express the facilities _{1},…, _{n},….^{9}

(ii) The converse of (i) does not hold. That is, there are cases where L_{0} cannot express some facilities _{1},…, _{n},…, even though the operational equivalence relation of L_{1} restricted to L_{0} is identical to the operational equivalence relation of L_{0}, i.e., ≅_{0}= (≅_{1} |L_{0}).

Proof. Let eval_{0} and eval_{1} be the respective evaluation predicates for L_{0} and L_{1}.

(i) A difference between the restricted operational equivalence relation of L_{1} and that of L_{0} implies that there are two phrases e and e′ in L_{0} and L_{1} such that either e ≅_{0} e′ and e ≅_{1̸} e′ or e ≅_{0̸} e′ and e ≅_{1} e′. For the first case, let C(α) be a context over L_{1} that can differentiate the two phrases e and e′. Let us say, without loss of generality, that

eval_{1} holds for C(e) but not for C(e′).

Now, assume contrary to the claim in the theorem that L_{0} can express the facilities 1,…, _{n},…. Then, there is a mapping φ : L_{1} ⟶ L_{0} that satisfies conditions E1 through E4 of Definitions 3.3 and 3.11. By conditions E1 and E3, the programs C(e) and C(e′) have counterparts in L_{0}, φ(C(e)) and φ(C(e′)), that have the same termination behavior:

9An extension of an equivalence relation to a larger language is also called conservative if the restriction to the old syntax yields the original equivalence relation. To avoid confusion, we will not use this terminology here.

eval_{0}(φ(C(e))) holds because eval_{1}(C(e)) holds

and

eval_{0}(φ(C(e′))) does not hold because eval_{1}(C(e′)) does not hold.  (†)

By conditions E2 and E4, the programs φ(C(e)) and φ(C(e′)) can only differ in a finite number of occurrences of e and e′. In other words, there is a program context D(α) over L_{0} such that φ(C(e)) = D(e) and φ(C(e′)) = D(e′): for the proof, see the Translation Lemma below. Next, from the assumption e ≅_{0} e′, it follows that φ(C(e)) = D(e) and φ(C(e′)) = D(e′) have the same termination behavior in L_{0}, i.e.,

eval_{0}(D(e)) holds if and only if eval_{0}(D(e′)) holds.

But this contradicts the above fact (†) that φ(C(e)) = D(e) converges and φ(C(e′)) = D(e′) diverges, which concludes the first case.

For the second case, assume e ≅_{0̸} e′ and e ≅_{1} e′. This assumption actually implies that

there are no contexts over L_{0} that complete both e and e′ to programs.  (∗)

For otherwise, there must be a context C(α) such that eval_{0}(C(e)) holds while eval_{0}(C(e′)) does not. Since L_{1} is a conservative extension of L_{0}, eval_{1}(C(e)) holds, eval_{1}(C(e′)) does not, and therefore contrary to the assumption, e ≅_{1̸} e′.

Now again, assume contrary to the claim of the theorem that L_{0} can express the additional facilities in L_{1} via an appropriate translation φ : L_{1} ⟶ L_{0}. Since e and e′ are operationally equivalent in L_{1}, there must be a context C(α) over L_{1} such that eval_{1}(C(e)) and eval_{1}(C(e′)). By assumption, eval_{0}(φ(C(e))) and eval_{0}(φ(C(e′))). Again by the Translation Lemma, the two translated programs are instances of the same program context D(α) such that φ(C(e)) = D(e) and φ(C(e′)) = D(e′). But by the above fact (*), such a context cannot exist, and we have thereby arrived at a contradiction. This concludes the second case of claim (i).

To finish the proof of claim (i), we must finally show that a homomorphic function preserves the structure of a program. Translation Lemma. Let φ : L_{1} ⟶ L_{0} be a translation that satisfies Conditions (0) through (3) in Definitions 3.3 and 3.11. Let C(α) be a context over L_{1}. Then, there is a context D(α) over L_{0} such that φ(C(e)) = D(e) and φ(C(e′)) = D(e′). Proof. The proof is an induction on the structure of C(α). The only interesting case is the following. Say, C(α) = (C_{1}(α),…, C_{a}(α)) for some in _{1},…, _{n},…. Then,

φ( (C_{1}(e),…, C_{a}(e)) = A(φ(C_{1}(e)),…, φ(C_{a}(e)))

and

φ( (C_{1}(e′),…, C_{a}(e′)) = A(φ(C_{1}(e′)),…, φ(C_{a}(e′)))

for some fixed syntactic abstraction A over L_{0} by condition E4. By inductive hypothesis, there are contexts D_{i}(α), for 1 ≤ i ≤ a, such that φ(C_{i}(e)) = D_{i}(e) and φ(C_{i}(e′)) = D_{i}(e′). But then D(α) = A(D_{1}(α),…, D_{a}(α)) is the context corresponding to C(α). The other cases are similar but easier. _{lemma}

The proof of the Translation Lemma finishes the proof of case (i).

(ii) We only sketch the construction of an example that proves claim (ii). For another example that is more interesting and fits more smoothly into this paper, see Subsection 4.2 on the control structure of Idealized Scheme.

For the base language, take the simply typed λ-calculus with a fixed point operator, whose types are either base types or arrow types. Because of the type system, it is impossible to define the typical cons, car, and cdr functions for pairs of values of arbitrary types. Hence this simply-typed language cannot express these functions. On the other hand, also due to the type system of the language, the new functions cannot be bound to free variables in phrases of the sublanguage, which implies that the additional functions on pairs (of distinctly typed components) cannot be used to distinguish phrases in the simply typed language. It follows that pairing functions and selectors increase the expressive power without destroying operational equivalences of the underlying language.

Based on Theorem 3.14, we can show that the sublanguage Λ_{v} is not strong enough to macro-express call-by-name abstraction, and that Λ_{n} is not strong enough to macro-express call-by-value abstraction. The proofs utilize the first half of the proof of claim (i).

Proposition 3.15 Λ extends both Λ_{v} and Λ_{n}.

(i) Λ_{n} cannot macro-express λ_{v} with respect to Λ.

(ii) Λ_{v} cannot macro-express λ_{n} with respect to Λ.

Proof. The claims are obviously consequences of Proposition 3.9.

(i) A direct proof for the first claim is derived from a theorem by Ong [31: Thm. 4.1.1],^{10} based on the preceding meta-theorem. Consider the phrases x(λ_{n}y.x(YK)Ωy)(YK) and x(x(YK)Ω)(YK). The two are equivalent in an adequate model of Λ_{n} [31] and are therefore operationally equivalent:

x(λ_{n}y.x(YK)Ωy)(YK) ≅_{Λ_{n}} x(x(YK)Ω)(YK).

The operational reasoning for a verification of this equivalence is as follows. No matter which argument the procedure x evaluates first, the expression (YK) eventually appears in the hole of the evaluation context, which leads to an immediate termination of the program evaluation.

10Gordon Plotkin pointed out Abramsky’s [1] and Ong’s [31] work on the lazy λ-calculus, which corrected a mistake in an early draft.

In the full language Λ, the above analysis no longer holds: Call-by-value procedures can evaluate and discard the expression (YK) in a way that does not affect the rest of the program. Thus, the context

C(α) = (λ_{n}x.α)(λ_{v}x.(λ_{n}y.y))

can distinguish between the two phrases: C(x(λ_{n}y.x(YK)Ωy)(YK)) terminates, but C(x(x(YK)Ω)(YK)) diverges. By Theorem 3.14, Λ_{n} cannot express λ_{v}.

(ii) Consider the expressions λ_{v}f.f(λ_{v}x.x)Ω and λ_{v}f.Ω. In the pure call-by-value setting, the two are operationally equivalent:

λ_{v}f.(f(λ_{v}x.x))Ω ≅_{Λ_{v}} λ_{v}f.Ω.

Both abstractions are values; upon application to an arbitrary value, both of them diverge. A formal proof is straightforward, based on the proof rules in Figure 3. In the extended language Λ, however, we can differentiate the two with the context

C(α) = α(λ_{v}x.(λ_{n}y.x)).

The context applies a phrase to a function that returns the value of the first argument after absorbing the second argument without evaluating it. Hence, C(λ_{v}f.f(λ_{v}x.x)Ω) terminates while C(λ_{v}f.Ω) diverges, which proves that the extension of Λ_{v} to Λ does not preserve the operational equivalence relation. Again by Theorem 3.14, λ_{n} is not expressible.

Remark 7 (Weak Expressibility). Remark 5 and the proof of Proposition 3.15 show that Theorem 3.14 does not carry over to weak expressibility because Λ_{n} can weakly macro-express λ_{v} and yet ≅_{Λ_{n}}⊈≅_{Λ} . That is, even in the case of a language extension that does not preserve the operational equivalence or approximation relation, the restricted language may already be able to express the new facilities in a weak sense.

For a second application of Theorem 3.14, we show that the polymorphic let construct of Λ_{v}^{t} is not macro-expressible in Λ^{t}. On one hand, this lemma confirms the folk knowledge that a polymorphic let adds expressive power to a monomorphically typed programming language. It does not contradict the above proposition, which only shows that a polymorphic let is expressible in a monomorphic language. On the other hand, this lemma provides an example of an interesting facility that is expressible but not macro-expressible relative to the same language. The proof relies on the second part of claim (i) in the meta-theorem.

Proposition 3.16 Λ_{v}^{t} cannot macro-express let with respect to Λ_{v}^{t} + let.

Proof. Consider the expressions ((gx)(ff))) and (λ_{v}d.((gx)(ff)))(gx). Since both contain a self-application of the variable f , there is no Λ_{v}^{t} program context for the two expressions, and the two programs cannot be operationally equivalent:

((gx)(ff))) ≅_{Λ̸^{t}} (λ_{v}d.((gx)(ff)))(gx)

Still their dynamic behavior is the same. The difference between the two programs is that the second computes the application of g to x twice, throwing away the first result via a vacuous abstraction:

gx = Ω ⊢ (gx)(ff) = Ω(ff) = Ω = (λ_{v}d.((gx)(ff)))Ω = (λ_{v}d.((gx)(ff)))(gx)

and, for all values v,

gx = v ⊢ (gx)(ff) = v(ff) = (λ_{v}d.((gx)(ff)))v = (λ_{v}d.((gx)(ff)))(gx).

Thus, in the extended language, where the variable f can be let-bound in an appropriate context, the two program fragments are equivalent:

((gx)(ff)) ≅_{Λ^{t}+let} (λ_{v}d.((gx)(ff)))(gx).

Together with the above inequality, this proves the proposition.

Propositions 3.15 and 3.16 provide several examples of pairs of universal programming languages that we can differentiate according to our expressiveness criterion. With the full language Λ, it also provides an example of a language that can express more than Λ_{v} and Λ_{n}. We have come to a point where we can formally distinguish the expressive power of programming languages.

3.3 Expressiveness

The two notions of expressibility are also simple comparison relations for languages and their conservative extensions. For a comparison of arbitrary programming languages, these relations are too weak. One solution is to conceive of our abstract programming languages as signatures (or types in the sense of universal algebra [5]) for classes of real programming languages. It is then possible to compare languages by comparing their signatures if one signature happens to be a conservative extension of the other. Though appealing at first glance, this idea only relaxes syntactic constraints such that the languages under comparion do not have to have the same syntax.

An alternative solution is to consider a common language universe that is a conservative extension of two or more programming languages. Given a common universe that fixes the meaning of a number of interesting programming constructs, there is a natural extension of the notion of expressibility to a notion of relative expressive power. Intuitively, a programming language is less expressive than another if the latter can express all the facilities the former can express in the language universe.

Definition 3.17. ((Macro) Expressiveness) Let L_{0} and L_{1} be conservative language restrictions of L. L_{1} is at least as (macro-) expressive as L_{0} with respect to L if L_{1} contains or can (macro-) express a set of L-constructs whenever L_{0} contains or can (macro-) express the additional facilities.

The expressiveness relation is obviously a pre-order on sublanguages in a given language framework; it is also monotonic in its third argument provided the extension to the universe is conservative.

Theorem 3.18 Let L_{0}, L_{1}, L_{2} be conservative restrictions of L, and let L be a conservative restriction of L′.

(i) L_{0} is less expressive than L_{0} with respect to to L.

(ii) If L_{0} is less expressive than L_{1} with respect to L and L_{1} is less expressive than L_{2} with respect to L, then L_{0} is less expressive than L_{2} with respect to L.

(iii) If L_{0} is less expressive than L_{1} with respect to L, then L_{0} is less expressive than L_{1} with respect to L′.

Proof. The proof is an easy calculation, verifying the conditions based on the above definitions.

However, a uniform change to all languages can change expressiveness relations.

Theorem 3.19 Expressiveness relationships are not invariant under uniform extensions of the languages.

Proof. For a simple example, consider Λ, Λ_{n}, and Λ_{v}, and recall that the two sublanguages are incomparable by Propositions 3.9 and 3.15. To prove the claim, we uniformly add a begin construct, (begin e e), that evaluates two expressions in sequence and then discards the first value. The formal specification requires an extension of the set of evaluation contexts to

E ::= … | (begin E e)

and an additional reduction clause:

E(begin v e) ⟶ E(e).

Now, Λ_{n}+{begin} can (macro-) express λ_{v}x.e as λ_{n}x.(begin x e), but begin does not add anything to the power of Λ_{v}: after all (begin e_{1} e_{2}) is (macro-) expressible as (λ_{v}xy.y)e_{1}e_{2} in Λ_{v}. Thus, in the extended setting Λ_{n} + {begin} is more expressive than Λ_{v} + {begin}.

The claim is still valid if the new facility is already in the language universe. Take the same example and add λ_{v}xy.y, i.e., Abramsky’s [1] convergence tester C for Λ_{n}, to both sub-languages, which is equivalent to adding begin.

The example in the preceding theorem formalizes Algol 60’s definition of call-by-value as an abbreviation of a call-by-name procedure preceded by an additional block or statement [30:12]; i.e., it is not the pure call-by-name subset of Algol that can define call-by-value but an extension thereof that includes a “strict” facility. The theorem thus shows how dangerous it is to use such informal claims as call-by-name can or cannot express call-by-value etc. These claims only tend to be true in specific language universes for specific conservative language restrictions: they often have no validity in other contexts!

Syntax

c ::= 0 | 1 | − 1 | 2 | − 2 | …  (numerals)
f ::= 0? | 1^{+} | 1^{−} | + | −  (numeric functions)
v ::= c | f  (constants)
| (lambda (x…) e)  (abstractions)
e ::= v  (values)
| x  (variables)
| (e e…)  (applications)

Semantics eval(e) holds iff e ⟶^{∗} v for some v

Evaluation Contexts

E ::= α | (v… E e…)

Reduction Steps

E((fv…)) ⟶ E(δ(f, v,…)) if δ(f, v,…) is defined
E(((lambda (x_{1} … x_{n}) e) v_{1} … v_{n})) ⟶ E(e[x_{1}/v_{1},…, x_{n}/v_{n}])

Constant Interpretation

δ(1^{+}, n) = n + 1_{δ(1^{−}, n) = n − 1} δ(+, n, m) = n + m_{δ(−, n, m) = n − m} δ(0?, 0) = (lambda (x y) x)

δ(0?, n) = (lambda (x y) y)
for n ≠ 0

Figure 4: Pure Scheme

4 The Structure of Idealized Scheme

Pure Scheme is a simple functional programming language. It has multi-ary, call-by-value procedures and algebraic constants. There are basic constants and functional constants. Following Plotkin, we assume the existence of a partial function (δ) from functional constants and closed values to closed values that specifies the behavior of constants in Pure Scheme and its extensions. Typically, the constants include integers, characters, booleans, and some appropriate functions; Figure 4 contains the appropriate definition of δ. In order to gain a complete understanding of Idealized Scheme, Pure Scheme only contains integers and a minimal set of functions on integers, elements that are expressible in a λ-calculus-based language like Λ_{v}.

Figure 4 contains the complete specification of Pure Scheme, based on a reduction semantics in the style of the previous section. Scheme programs satisfy two contextsensitive definitions: They are closed expressions, and they do not contain lambdaabstractions with repeated parameter names. The predicate eval holds for a program if the program reduces to an answer, that is, values in the case of Pure Scheme. If eval does not hold for a program, the program is either in an infinite loop or the reduction process is stuck.^{11} In Pure Scheme, an evaluation can become stuck because of the application of a constant symbol to a λ-expression, the application of a numeral to a value, the application of a constant function to a value for which δ is undefined, or the application of a lambda-abstraction to the wrong number of arguments. As before, the reduction rules for Pure Scheme constitute the basis for proof systems for the operational equivalence relation in the spirit of Figure 3. For brevity, however, we shall carry out most of the proofs in this section in an informal setting; it should be clear from the proofs, though, how to formalize the various steps. In the following subsections, ≅_{ps} denotes the operational equivalence relation on Pure Scheme; other indexes correspond to extensions of Pure Scheme and should be self-explanatory.

The main characteristic of Idealized Scheme [11, 12, 13] is the extension of the functional core language Pure Scheme with type predicates, local branching constructs, and imperative facilities:

• branching expressions for the local manipulation of control,

• predicate constants for determining the type of a value,

• control operators for the non-local manipulation of control, and

• assignment statements for the manipulation of state variables.

The extensions reflect the belief that these constructs increase the expressive power of the language [40, 41]. In this section, we demonstrate how to formulate these beliefs in our formal macro-expressiveness framework.

Subsection 1 simultaneously deals with local control and type predicates because the two sets of constructs are closely related. The second subsection is a study of two different control operators, one for stopping the execution of a program and another for handling the general flow of control. The third subsection shows how imperative assignments add expressive power to the core language. Finally, the last subsection addresses the unrelated issue of how Pure Scheme relates to so-called “lazy” functional languages, or more precisely, to call-by-value languages with callby-name data constructors. We thus hope to reconcile Proposition 3.15 on the nonexpressibility of call-by-name abstractions in Λ_{v} and Pure Scheme with the widespread belief that “lazy” data constructions are available in higher-order, by-value languages.

11Although this is common practice in semantic considerations, a more realistic specification would have to consider the introduction of an error mechanism. However, an error mechanism actually introduces additional expressive power, which is the reason why we consider it separately.

4.1 Local Control and Dynamic Types

The programming language world knows two types of local branching statements: the boolean-value based if-construct for distinguishing two values from each other, and the Lisp-style if-construct for distinguishing one special value from all others. The semantics of the former relies on the presence of two distinct values: false and true, or 0 and 1. Assuming an extension of the set of evaluation contexts to

E ::= … | (Bif E e e),

the following two additional reduction rules characterize the behavior of truth-value based Bif:

E(Bif 1 e_{t} e_{f}) ⟶ E(e_{t})  (Bif.true)
E(Bif 0 e_{t} e_{f}) ⟶ E(e_{f}).  (Bif.false)

If the test value in a Bif-expression is neither 0 nor 1, the evaluation of the program is undefined, or equivalently, such a Bif-expression is operationally indistinguishable from a diverging expression. The extension is obviously conservative; we refer to it as PS(Bif).

Clearly, Pure Scheme can express such a simple Bif.

Proposition 4.1 Pure Scheme can macro-express Bif.

Proof Sketch. The proposition follows from Corollary 3.13 and is basically due to Landin and Burge [23:115], who realized that vacuous lambda abstractions could be used to suspend computations. Consider the syntactic abstraction:

(Bif α α_{t} α_{f}) = ((lambda (t thn els)

(((0? (1^{−} t)) thn ((0? t) els (lambda () Ω))))) α (lambda () α_{t}) (lambda () α_{f}))

It is easy to show that this abstraction is operationally equivalent to Bif. If the replacement for α is neither 0 nor 1, then both expressions diverge. Otherwise, both expressions select one of the replacements for α_{t} or α_{f} and eliminates the other. The right-hand side accomplishes this by suspending the two expressions in 0-ary procedures and invoking one of them after the selection has been made.

Remark 8 (Weak Expressibility). An extension of Pure Scheme with Bif and two distinct new values, true and false, would not be macro-eliminable. Otherwise φ would have to map true to a term t in Pure Scheme, which implies that the programs

(Bif true 1 2),

and

(Bif t 1 2),

map to the same image, namely

A(t, φ(e_{1}), φ(e_{2}))

for some fixed syntactic abstraction A. But it is then impossible that the translation preserves program behavior because the first program terminates and the second one diverges.

Clearly, Bif is still weakly expressible since the translation will only force more programs to terminate. In a typed version of Pure Scheme, the problem would disappear. The type system would not admit a program with an ill-typed Bif-expression. Put differently, since a typed version of Pure Scheme admits fewer programs, expressiveness propositions are stronger.

The Lisp-style if assumes that there is one distinct value for false, in Lisp usually called nil, and all other values represent true. With 0 again serving as false, the reduction rules differ accordingly from (Bif.true) and (Bif.false):

(Lif v e_{t} e_{f}) ⟶ e_{t} for v ≠ 0  (Lif.v)
(Lif 0 e_{t} e_{f}) ⟶ e_{f}.  (Lif.nil)

Proposition 4.2 Pure Scheme cannot macro-express Lif.

Proof Sketch. For readability, we carry out the proof in PS(Bif). Since Bif is macro-expressible by Proposition 4.1, operational equivalences of terms hold in Pure Scheme after expanding the Bif-expressions.

The proposition is a consequence of Theorem 3.14. The interesting operational equivalence is based on the following context:

C(α) = (Bif (p (lambda () Ω)) (Bif (p 0) 1 α) Ω).

In Pure Scheme, the evaluation of (an instance of) this context cannot reach (the replacement of) α. First, if p is not bound to a procedure, the evaluation process diverges at the first invocation of p on (lambda () Ω). Thus assume p is replaced by a procedure. The rest of the proof proceeds by a case analysis on the following property of procedures: a procedure of one argument may (1) ignore its argument and return a constant result, or (2) apply a constant function symbol to its argument, or (3) use its argument in the procedure position of an application. For the evaluation of C(α) to reach α, the procedure must return two different results: 1 on (lambda () Ω), and 0 on 0. Let us then consider the other two alternatives. On one hand, if p applies a functional constant in Pure Scheme to its argument, then the application (p (lambda () Ω)) diverges. On the other, when p uses its argument as a procedure, the evaluation again diverges in the first test position. In short, either the evaluation of C diverges at the first test position, or the procedure p produces a result that is independent of its argument. Both cases imply that an evaluation cannot reduce a redex in the replacement of α.

It follows from the above that it is inconsequential what α represents. Therefore, C(1) ≅_{ps} C(Ω). In the larger setting of PS(Lif), however, the preceding analysis does not hold. A context over PS(Lif), could bind the variable p to the procedure

(lambda (x) (Lif x 0 1)),

which can distinguish the arguments 0 and (lambda () Ω) in the correct manner: C(1) ≅_{L̸if} C(Ω).

As an alternative to the addition of Lif, dynamically typed languages generally include type predicates. For extending Pure Scheme with a predicate symbol like int?, it suffices to extend the interpretation function δ with the clauses

δ(int?, c) = (lambda (x y) x)
δ(int?, (lambda (…) e)) = (lambda (x y) y)

Again, the extension, PS(int?), is clearly conservative.

With int?, programs in the extended language can now effectively test the type of a value, and indeed, int? can express Lif. It follows that int? is not expressible in Pure Scheme.

Proposition 4.3 (i) Pure Scheme cannot express int?. (ii) PS(int?) can express Lif.

Proof Sketch. This proof illustrates the use of reduction proofs in the framework of expressiveness. First, PS(int?) can macro-express Lif:

(Lif α α_{t} α_{f}) = (Bif (cand (int? α) (0? (1^{−} α))) α_{t} α_{f}),

where

(cand α_{1} α_{2}) = (Bif α_{1} α_{2} 0)

and Bif is expressed as in Proposition 4.1 above. Second, since PS(int?) can express Lif, it is stronger than Pure Scheme by the preceding proposition.

The converse does not hold: A Lisp-style Lif can distinguish between 0 and all other values but not an arbitrary integer from the class of procedures.

Proposition 4.4 PS(Lif) cannot macro-express int?.

Proof Sketch. The proof proceeds along the lines of the proof of Proposition 4.2. Instead of applying the procedure variable p to 0, the modified context invokes p on 1:

C′(α) = (Bif (p (lambda () Ω)) (Bif (p 1) 1 α) Ω).

The analysis uses the same reasoning as the above proposition with one exception: a procedure argument may now also appear in the test position of a Lif-expression. As above, for the evaluation of (an instance of) C′ to reach (the replacement of) α, the procedure may not invoke its argument, may not submit it to a constant function, but can test it with a Lif-expression. But this is irrelevant because both 1 and (lambda () Ω) cause a Lif-expression to take the same branch. Hence, C′(1) ≅_{Lif} C′(Ω), yet, with int? in the language, this is no longer the case: C′(1) ≅_{i̸nt?} C′(Ω).

Putting it all together, we see that Pure Scheme can handle some but not all types of local branching decisions. A simple, boolean-valued if construct is expressible. The more typical Lisp-style if adds the expressive power to distinguish one integer value from all other values, whereas the domain predicate int? permits a distinction between each integer value and the class of all other values.

Additional Syntax

e ::= … | (call/cc e)  (continuation captures)
| (abort e)  (program stops)

Additional Reduction Steps

E(call/cc e) ⟶ E(e (lambda (x) (abort E(x))))
E(abort e) ⟶ e

Figure 5: Pure Scheme with control

4.2 Non-Local Control

A more interesting expressiveness constellation arises in the context of non-local control abstractions. Idealized Scheme has the operations abort and call/cc. The former facility abandons the current evaluation context, realizing a simplistic form of error handling. The latter applies its subexpression to an abstraction of the current control state, permitting almost arbitrary manipulations of the flow of control. Its name stands for “call with current continuation” because the Scheme-terminology refers to an abstraction of the control state as a “continuation” in analogy to denotational semantics. Figure 5 specifies the syntax and a simple reduction semantics of Pure Scheme with both control operators. We refer to the entire extension as PS(control); ≅_{c+a} denotes its operational equivalence. Two interesting conservative restrictions of PS(control) are PS(abort) = Pure Scheme + abort and PS(call/cc) = Pure Scheme + call/cc with ≅_{a} and ≅_{c} as their respective operational equivalences.

With the semantics of Figure 5, it is trivial to verify that the extensions are conservative over Pure Scheme. The semantics forms the basis of a simple equational calculus for abort and call/cc, and permits simple, algebra-like reasoning about programs with control operations [12, 13]. All three languages are more expressive than Pure Scheme.

Proposition 4.5 Pure Scheme cannot macro-express non-local control constructs: Pure Scheme cannot macro-express abort or call/cc relative to PS(abort), PS(call/cc), and PS(control).

Proof Sketch. The proof relies on Theorem 3.14, i.e., the addition of abort and call/cc invalidate operational equivalences over Pure Scheme. A typical example^{12} is the operational equivalence

(lambda (f ) ((f 0) Ω)) ≅_{ps} (lambda (f ) Ω).

As argued in the proof of Proposition 3.15(i), these two procedures are equivalent in a functional setting: both diverge when applied to a value. It is easy to check that this argument still holds in Pure Scheme.

With abort and call/cc, however, there are contexts that invalidate this equivalence. Two examples are (α (lambda (x) (abort x))) and (call/cc α). Whereas the composition of the first expression with these contexts evaluates to 0, the second expression diverges in the same contexts:

(lambda (f ) ((f 0) Ω)) ≅_{x̸} (lambda (f ) Ω).

for x ranging over a, c, and c+a.

The next natural question is whether the two control operations are related or whether they provide distinct facilities. The following proposition shows that in Idealized Scheme, the two are actually independent enhancements of the expressive power of the core language.^{13} Proposition 4.6 The control constructs abort and call/cc cannot express each other:

12This example is a folk theorem example in the theoretical “continuation” community, but it was also used by Meyer and Riecke to argue the “unreasonableness” of continuations [26].

13The non-expressibility of abort appears to be an artifact of our modeling of Scheme. A more realistic model of Scheme systems (as opposed to the Scheme semantics [35]) would have to include the interactive loop, which provides a delimiter for control actions [9]. By including an appropriate version of this delimiter in PS(control), abort becomes macro-expressible as a combination of call/cc and the control delimiter [39]. Put differently, interactive programming systems actually add expressive power to the programming language. Peter Lee [personal communication] pointed out another example of this phenomenon: The addition of a read-eval-print loop also introduces true, non-eliminable polymorphism into a language like Λ^{t} + let by providing top-level let declarations with an open-ended body expression. The fact that such interactive programming environments add power to their underlying languages suggests that they should be specified as a part of the language standards!

(i) PS(abort) cannot macro-express call/cc with respect to PS(control) [39].

(ii) PS(call/cc) cannot (macro-) express abort with respect to PS(control).

Proof Sketch. (i) The proof of the first claim shows that call/cc destroys operational equivalences in PS(abort). A typical example is C(1) ≅_{a} C(Ω) where

C(α) = (Bif (f (lambda (k) ((k 1) Ω))) (Bif (f (lambda (k) ((k α) Ω))) 0 1) Ω)

These two terms could only differ if the procedure f invokes its argument, and if this invocation could return a result. In PS(abort), this is impossible because expressions can either produce a value, diverge, or abort. Therefore, the body of f ’s first argument, (lambda (k) ((k 1) Ω)), either aborts or diverges, but certainly cannot return a value. After adding call/cc, however, a context that binds f to

(lambda (x) (call/cc x))

can distinguish the term C(1) from C(Ω): C(1) ≅_{c̸+a} C(Ω).

(ii) The second claim is a consequence of Corollary 3.10, i.e., there is a program with an abort expression for which it is impossible to find an operationally equivalent call/cc expresion. The program is ((lambda (d) Ω) (abort 1)); it is the composition of the context ((lambda (d) Ω) α) over PS(call/cc)and an abort expression.

The absence of an operationally equivalent expression for (abort 1) from PS(call/cc) follows from the property that expressions in the restricted language cannot eliminate their evaluation context. More technically, if E(e) is a program over PS(control) such that all occurrences of abort expressions have the form (abort E(e′)) for some e′, then either E(e) ⟶^{∗} E(v) or e ≅_{c+a} Ω. The proof of this auxiliary claim is a routine induction on n in the following statement:

If E(e) ⟶^{n} E(e′) then either (1) e′ is a value, or (2) e′ contains a stuck redex, or (3) there is an e′′ such that E(e′) ⟶ E(e′′) and E(e′′) satisfies the above condition.

Since an expression over PS(call/cc) does not contain any abort expression, it vacuously satisfies the antecedent of the auxiliary claim. Hence, it either diverges or it returns a value and cannot be interchanged with an abort expression without effect on the behavior of a PS(control) program.

From the existence of a program that contains (abort 1) and the non-existence of an operationally equivalent expression, it follows that PS(call/cc) cannot express abort in PS(control).

The preceding proposition not only establishes the formal expressiveness relationship among the control operators of Idealized Scheme, but it also provides a concrete example for the second claim in Theorem 3.14.

Theorem 3.14 (restated) Let L_{1} = L_{0} + { _{1},…, _{n},…} be a conservative restriction of L_{0}. Let ≅_{0} and ≅_{1} be the operational equivalence relations of L_{0} and L_{1}, respectively.

(ii) The converse of (i) does not hold. That is, there are cases where L_{0} cannot express some facilities _{1},…, _{n},…, even though the operational equivalence relation of L_{1} restricted to L_{0} is identical to the operational equivalence relation of L_{0}, i.e., ≅_{0}= (≅_{1} |L_{0}).

Proof. By the preceding proposition we know that PS(call/cc) cannot express abort. To finish the proof, we only need to prove that the operational equivalence relation of PS(call/cc) is a subset of the operational equivalence relation of PS(control): ≅_{c} ⊆ (≅_{c+a} |PS(call/cc)); the other direction is obvious.

Assume that e ≅_{c̸+a} e′. We prove that e ≅_{c̸} e′. Suppose there is a context C that can distinguish e and e′ in PS(control). If the context is also a context over PS(call/cc), the result is immediate. Otherwise, C contains a number of abort expressions, and there exists a context D(α, α_{1},…, α_{n}) such that

C(α) = D(α, (abort e_{1}),…, (abort e_{n})).

Now let a be a variable that does not occur in C , and let the context C′(e) be defined as follows:

C′(α) = ((call/cc (lambda (a)

(lambda () D(α, (a (lambda () e_{1})), …, (a (lambda () e_{n})))))))

Next, we show that eval(C(e)) holds if and only if eval(C′(e)) holds. First, the program C′ evaluates to an intermediate program with a few administrative steps:

C′(e) ⟶^{+} D(e, ((lambda (x) (abort (x))) (lambda () e_{1})), …,

((lambda (x) (abort (x))) (lambda () e_{n})))

Second, by a generalized version of the call-by-value β axiom,

((lambda (x) (abort (x))) (lambda () e_{i})) ≅_{c+a} (abort e_{i}),

and therefore D(e, ((lambda (x) (abort (x))) (lambda () e_{1})), …, ((lambda (x) (abort (x))) (lambda () e_{n})))

terminates if and only if

D(e, (abort e_{1}), …, (abort e_{n})) = C (e)

terminates. The same analysis holds for the program C(e′), and we have thus shown that the context C′(α) distinguishes e and e′: e≅_{c̸}e′.^{14}

In summary, we have shown that PS(control) extends both PS(abort) and PS(call/cc) with respect to expressive power, and the latter two individually extend Pure Scheme itself. An interesting point is that the extension of PS(abort) to PS(control) is qualitatively different from the extension of PS(call/cc) to PS(control). We expect this point to be a topic of further investigations.

4.3 Assignments

The final addition to Pure Scheme is the set!-construct, Scheme’s form of assignment statement. Like in a traditional Algol-like programming language, the set!-expression destructively alters a binding of an identifier to a value. A simple reduction semantics for PS(state), Pure Scheme with set! and letrec (for recursive declarations of variables with initial values), is given in Figure 6. Clearly, PS(state) is a conservative extension of Pure Scheme; the new semantics is the basis for an equational calculus for reasoning about operational equivalences in PS(state) [11, 12].

Proposition 4.7 Pure Scheme cannot express set! and letrec.

Proof Sketch. Consider the expression ((lambda (d) (f 0)) (f 0)), which contains the same subexpression, (f 0), twice. In a functional language like Pure Scheme, the two subexpressions return the same value, if any, and, given that the value of the first subexpression is discarded, the expression is operationally equivalent to (f 0):

((lambda (d) (f 0)) (f 0)) ≅_{ps} (f 0).

The verification of this equivalence in the proof system of Figure 3 is straightforward. In the extended language, this is no longer true. Consider the context

C(α) = (letrec (f (lambda (x) (set! f (lambda (x) Ω)))) α),

14The transformation of C(e) into C(e′) is not a homomorphic translation because it changes the top-level structure of the program. Since such a translation could encode a program as an integer and an interpreter as a function on the integers, a restricted language with all computable functions could express any feature if we allowed such global changes to programs.

Additional Syntax

e ::= … | (set! x e)  (assignments)
| (letrec ([x v] …) e)  (recursive definitions)

Extended Semantics

eval(e) holds iff e ⟶^{∗} v or (letrec () e) ⟶^{∗} (letrec (…) v) for some v

Additional Evaluation Contexts

E ::= … | (set! x E)

Additional Reduction Steps

(letrec (…) E((fv…))) ⟶ (letrec (…) E(δ(f, v,…)))

provided δ(f, v,…) is defined

(letrec (…) E((lambda (x_{1} …) e) v_{1} …)) ⟶ (letrec (… [x_{i} v_{i}] …) E(e[x_{j}/v_{j},…]))

if the x_{i},… are assignable

and the x_{j},… are not assignable

(letrec (… [x v] …) E(x)) ⟶ (letrec (… [x v] …) E(v))
(letrec (… [x u] …) E((set! x v)) ⟶ (letrec (… [x v] …) E(v))
(letrec ([x v] …) E((letrec ([y u] …) e))) ⟶ (letrec ([x v] … [y u] …) E(e))

Figure 6: Pure Scheme with state

which declares a procedure f . Upon the first application, the procedure modifies its declaration so that a second invocation leads to divergence. Consequently, an expression with a single use of the function converges, but an expression with two uses diverges:

((lambda (d) (f 0)) (f 0)) ≅_{s̸et!} (f 0).

Not surprisingly, assignments increase the expressive power of Idealized Scheme. Without proof, we add that Scheme’s form of assignment is equivalent to cells with a destructive update operation but without domain predicate.

4.4 Non-evaluating Constructors

Functional languages often use the call-by-name parameter-passing protocol instead of Pure Scheme’s call-by-value technique. Alternatively, such languages offer data constructors, say cons, that do not evaluate their arguments [15]. It is a widely held belief that such provisions are superfluous in the presence of higher-order procedural abstractions.

Evaluation Contexts

E ::= α | (u… E e…) where u = v \ {cons$}

Additional Reduction Steps

E((cons$ e_{1} e_{2}) 1) ⟶ E(e_{1})
E((cons$ e_{1} e_{2}) 2) ⟶ E(e_{2})

Figure 7: Pure Scheme(cons$)

As shown in the previous section, call-by-value languages cannot express callby-name abstractions. This result also holds in the extended framework of Pure Scheme. However, the introduction of non-evaluating data constructors is a bit more subtle. To study this issue more thoroughly, we consider two different conservative extensions of Pure Scheme, each of which incorporates a different form of a callby-name constructor. The first extension, PS(lazy), provides the constructor as a first-class function:

v ::= … | cons$  (call-by-name cons)
| (cons$ e e)  (“lazy” values)

For simplicity, “lazy” values are functions, and 1 and 2 serve as selector arguments. Figure 7 contains the corresponding extension of the reduction relation. Though not equivalent to full call-by-name abstractions, this addition of a single call-by-name primitive still introduces new semantic capabilities. A proof of this statement is easily derivable from Proposition 3.15.

The second extension, PS(delayed), is a restriction of the first. The non-evaluating constructor is no longer a first-class function but is only available in first-order form:

v ::= … | (cons$ e e)  (“lazy” values)

The reduction relation remains the same (Figure 7). It is this restricted extension that is expressible in Pure Scheme.

Proposition 4.8 Pure Scheme can macro-express cons$ relative to PS(delayed).

Proof. The desired syntactic abstraction is

(cons$ α_{1} α_{2}) = (lambda (s)
(Bif (0? (1^{−} s)) α_{1} (Bif (0? (1^{−} (1^{−} s))) α_{2} Ω)))

It is easy to check that the corresponding translation satisfies the reduction clauses of the original functions. The result follows from Corollary 3.13.

Remark 9 (Weak Expressibility). If the extended language contained selector functions for lazy values, the new values would only be weakly expressible for the same reason as Bif, true, and false are only weakly expressible (see Remark 8).

5 The Conciseness Conjecture

If a programming language can represent all computable functions (on the integers), it contains a functionally equivalent counterpart to each program in a more expressive language. This raises the question as to what advantages there are to programming in the more expressive language when equivalent programs in the simpler language already exist. By the definition of an expressible construct, programs in a less expressive language generally have a globally different structure from functionally equivalent programs in a more expressive language. But, is this really all we can say about programming in more expressive languages?

By studying a number of examples, we have come to the conclusion that programs in less expressive languages exhibit repeated occurrences of programming patterns, and that this pattern-oriented style is detrimental to the programming process. To illustrate our point, we begin by presenting two examples. The first example compares two equivalent programs in variants of full Scheme and Scheme without assignment.^{15} Consider the following program fragment:

(let (…

[TransManager (let (TransCounter 0)

(lambda (TransType)

(if (counter? TransType) TransCounter (begin

(set! TransCounter (add1 TransCounter)) BODY ))))]

…) … (TransManager t1 ) …)

The program first binds the variable TransManager to a procedure that handles transactions and simultaneously counts how many transactions it performs. The procedure accomplishes the counting by allocating a local variable, TransCounter, in its private scope with initial value 0. For every subsequent proper transaction, the procedure then uses an assignment to increase TransCounter by 1. There is a special transaction of appropriate type that can check the number of past transactions.

15This comparison is part of the folklore of the expressiveness discussion [24:165]; the particular example is adapted from our previous paper on the equational semantics of assignments [11].

A program in Pure Scheme—or any other functional language without assignments— must realize the counting of transactions in a different way. For example, the above program fragment would have to be rewritten into something like the following code:

(let (…

[TransManager (lambda (TransType TransCounter)

(if (counter? TransType) TransCounter (cons (add1 TransCounter) BODY )))]

[TransCounter 0]

…) … (let (result (TransManager t1 TransCounter)) (let ([TransCounter (car result)] [ProperResult (cdr result)])

…)))

This functional version of the program declares a variable for transaction counting in the same scope as the transaction manager procedure, which now takes the current value of the counter as an additional argument. Upon completion of the transaction, TransManager returns a pair whose first component is the increased counter value and whose second component is the proper result of the transaction. All calls to TransManager pass the current value of TransCounter as an extra argument. Finally, at every call site there is also some additional code to disassemble the result in the desired way.

The functional version offers many opportunities for code simplifications. Specifically, every call site for the transaction procedure could immediately update the counter if the transaction is a proper transaction, and could return the value of the counter if the transaction causes a check on the number of previous calls:

(let (… [TransManager (lambda (TransType) BODY )] [TransCounter 0] …)

… (let (TransCounter (add1 TransCounter)) (TransManager t1 ) …))

But, even after simplifying the functional version as much as possible, it always contains a large number of repeated occurrences of add1 expressions, one per call site for TransManager, distributed over the whole program.

The second example concerns the use of control operators. Imagine a large functional program consisting of several modules. The interfaces of these modules have fully formal specifications in the form of (variants of) parameter descriptions. Now suppose that because of some extension of the program’s requirements, one of the modules needs the capability to stop the execution of the (revised) program. In a functional setting, this task is accomplished by converting the relevant parts of the program into (simplified) continuation-passing style. Specifically, each function that (transitively) uses the critical module passes a functional abstraction of the rest of the computation to the critical module, and its call sites are in such a position that upon return, no further work needs to be done. It is thus up to the critical module to stop or to continue the execution of the rest of the program. If the former is necessary, the module discards the additional argument; otherwise, it invokes the argument on some intermediate result. This programming style, however, requires fundamental changes to the original, non-abortive program. First, the interface to the critical module must now indicate the possibility that the module could abort the program execution. Second, and more importantly, the code for every call site of a function with connections to the critical module must now satisfy special conditions. Again, as in the above example, there are alternatives, but for each of them, the lack of a non-expressible facility, this time the abort operation, causes the occurrence of programming patterns throughout the entire program.

Based on these examples and others with a similar flavor, we have come to believe that the major negative consequence of a lack of expressiveness is the abundance of programming patterns to make up for the missing, non-expressible constructs. Clearly, a more specific conjecture about this issue must address the question of which programs actually benefit from the additional expressive power of larger languages since not all of them do. A relatively naive answer would be that improved programs use non-expressible constructs in a sensible, observable manner. An example of a Scheme program that does not use assignments sensibly is a function whose only assignment statement occurs at procedure entry and affects the parameter. A more formal approach to the notion of “observable manner” could be the idea that a program with a sensible use of an additional feature must be transformable into a context that can witness operational distinctions between phrases in the restricted language. Despite the lack of a good definition for “sensible uses of constructs” or even for “programming patterns,” we still venture to formulate the following conjecture about the use of expressive programming languages.

Conciseness Conjecture. Programs in more expressive programming languages that use the additional facilities in a sensible manner contain fewer programming patterns than equivalent programs in less expressive languages.

The most disturbing consequence of programming patterns is that they are an obstacle to an understanding of programs for both human readers and programprocessing programs. In the above TransManager example, only a global program analysis can verify that the add1 expressions really count the number of transactions. Even worse there are two distinct explanations for a continuation-passing style subprogram in a call-by-name functional setting: it may either implement some sophisticated control structure, or it may implement a call-by-value protocol [34]. Only a thorough analysis of the details of the continuation-passing program fragment can reveal the true purpose behind the occurrence of the programming patterns. Thus, the main benefit of the use of expressive languages seems to be the ability to abstract from programming patterns with simple statements and to state the purpose of a program in the concisest possible manner.

6 Related Work

The earliest attempt at defining and comparing the expressive power of programming languages is the work on comparative schematology by Chandra, Hewitt, Manna, Paterson, and others in the early and mid seventies [6, 32]. Schematology studies programming languages with a simple set of control constructs, e.g., while-loop programs or recursion equations, and with uninterpreted constant and function symbols. As in predicate logic without arithmetic, it is possible to decide certain questions about such uninterpreted program schemas. Moreover, the languages are not universal, and it makes sense to compare the set of functions that are computable based on different sets of control constructs, or based on an interpretation of a subset of the function symbols as operations on data structures like stacks, arrays, queues. In the presence of full arithmetic, i.e., representations of integers with an addition and multiplication function, the approach can no longer compare the expressive power of programming languages since everything can be encoded and all functions become computable.

A second approach is due to Fortune et al [14]. Their basic observation is that statically typed languages without facilities for constructing diverging programs can only encode a subset of the total computable functions. For example, whereas the simply typed λ-calculus-language can define the elementary recursive functions, the second-order version of the calculus comprises the ϵ_{0} elementary recursive functions. Like schematology, this approach crucially relies on the fact that the languages under consideration are not universal. While these two approaches illuminate some of the issues about the expressiveness of data and type structures, their applicability to fullfledged programming languages is impossible because an equating of expressiveness with computational power is uninteresting from the programmer’s perspective.

Recently, Hoare [20] proposed classifying programming languages according to the equational and inequational laws that their programming constructs satisfy. He illustrates this idea with a collection of examples. The laws are based on denotational semantics, which are generally sound with respect to operational equivalences. Given our theorems that connect expressiveness with the validity of operational equivalences in programming languages, this approach seems to be a related attempt at formalizing or comparing the expressiveness of languages.

Williams [45] looks at a whole spectrum of formalization techniques for semantic conventions in formal systems and, in particular, programming languages. His work starts with ideas of applicative and definitional extensions of formal systems but also considers techniques that are more relevant in computational settings, e.g., compilation and interpretation. The goal of Williams’s research is a comparison of formalization techniques and not a study of the expressiveness of programming languages. Some of his results may be relevant for future extensions of our work.

A secondary piece of related work is the study of the full abstraction property of mathematical models [25, 31, 33] and the representability of functions in λ-calculi [3, 4]. In many cases, the natural denotational model of a programming language contains too many elements so that operationally equivalent phrases have different mathematical meanings. Since it is relatively easy to reverse-engineer a programming language from a model, the equality relation of models without the full abstraction property directly corresponds to the operational equivalence of a conservative extension. As a consequence, such models naturally lead to the discovery of non-expressible programming constructs. In the framework of λ-calculus languages, such facilities are multiple argument functions that do not require the values of all arguments to determine their result [33, 1]. Still, the study of full abstraction does not provide true insight into the expressive power of languages. On one hand, the discovery of new facilities directly depends on the choice of a model. For example, whereas a direct model of Λ_{n} requires the above-mentioned facility for exploiting deterministic parallelism, a continuation model leads to operations on continuations and to restrictions of such operations [39]. On the other hand, by Theorem 3.14 we also know that a change in the operational equivalence relation is only a sufficient but not a necessary condition for the nonexpressibility of a programming construct. In short, research on full abstraction is a valuable contribution to, but not a replacement for, the study of expressiveness (see Proposition 3.15).

7 Towards a Formal Programming Language Design Space

In the preceding sections we developed several ideas on a formal framework for comparing the expressive power of programming languages. Based on informal claims in the literature, we argued that

• the key to programming language comparisons is a restriction on the set of admissible translations between programming languages.

Specifically, we proposed that

• the translations between languages should preserve as much of a program’s structure as possible.

An application of this principle to conservative language extensions produced a number of criteria for deciding whether additional operators increase the expressive power or not. For a concrete example, we considered several language extensions of Pure Scheme, a simple functional programming language, and found that our formal expressiveness results are close to the intuitive ideas in the literature.

The most important criterion for comparing programming languages showed that an increase in expressive power may destroy semantic properties of the core language that programmers may have become accustomed to (Theorem 3.14). Among other things, this invalidation of operational laws through language extensions implies that there are now more distinctions to be considered for semantic analyses of expressions in the core language. On the other hand, the use of more expressive languages seems to facilitate the programming process by making programs more concise and abstract (Conciseness Conjecture). Put together, this result says that

• an increase in expressive power is related to a decrease of the set of “natural” (mathematically appealing) operational equivalences.

An interesting challenge is to find expressive extensions of languages whose additional facilities do not invalidate operational laws.^{16}

The current framework is only a first step towards a formal programming language design space. On one hand, we must investigate our comparison relation for arbitrary languages in more depth before we can judge its general usefulness. On the other hand, our set of restrictions on language translations is clearly not the only interesting basis for comparing programming languages. There is an entire spectrum of feasible restrictions that yield alternative notions of expressiveness, and these alternatives deserve exploration, too. Finally, we have not yet tackled the problem of deriving properties from expressiveness claims but expect to do so in the future. In the long run, we hope that some theory of language expressiveness develops into a formal theory of the programming language design space, and that such a theory can help a programmer in selecting the right set of constructs for solving a problem.

Acknowledgement. Dan Friedman directed my attention to the idea of expressiveness by insisting that an understanding of new programming constructs in terms of procedures or macro implementations is superior to an implementation based on interpreters. Conversations with Bruce Duba and Mitchell Wand provided the motivation for further work in this direction. Bob Harper pointed out the relationship to logic, which ultimately led to the current formalization. Tim Griffin’s remark that my original approach focused too much on macro expressiveness, redirected my efforts towards the broader framework of expressiveness of Section 3.1. Hans Boehm, Robert Cartwright, Dan Friedman, Robert Hieb, John Lamping, Scott Smith, Rebecca Selke, Carolyn Talcott, Mitchell Wand and numerous of my patient seminar students suggested many improvements in the presentation of the material. Thanks are also due to Carl Gunter (University of Pennsylvania), Peter Lee (Carnegie-Mellon University), and Carolyn Talcott (Stanford University) for giving me opportunities to expose my ideas to a wider audience before writing them up in this form. Finally, comments by members of the POPL’88 committee, and by the anonymous referees of ESOP’90 and of this special issue of Science of Computer Programming exposed weaknesses in early drafts.

16This is not to be confused with compiler annotations, which also preserve the operational equivalences but do not increase the expressive power of a language, e.g., futures for indicating opportunities for parallel evaluations [2, 19] and single-threaded destructive updates in functional languages [18].

8 References

1. Abramsky, S. The lazy λ-calculus. In Declarative Programming, D. Turner (ed). Addison Wesley, 1988, 65–116.

2. Baker, H.G. and C. Hewitt. The incremental garbage collection of processes. In Proceedings of the Symposium on Artificial Intelligence and Programming Languages. SIGPLAN Notices 12(8), 1977, 55-59.

3. Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics. Revised Edition. Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, 1984.

4. Berry, G. Séquentialité de l’evaluation formelle des λ-expressions. In Proc. 3rd International Colloquium on Programming, 1978.

5. Burris, S. and H. P. Sankappanaras. A Course in Universal Algebra. Springer Verlag, Berlin, 1981.

6. Chandra, A.K. and Z. Manna. The power of programming features. Journal of Computer Languages (Pergamon Press) 1, 1975, 219–232.

7. Church, A. A formulation of the simple theory of types. Journal of Symbolic Logic 5(1), 1940, 56–68.

8. Felleisen, M. The Calculi of Lambda-v-CS-Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. Ph.D. dissertation, Indiana University, 1987.

9. Felleisen, M. The theory and practice of first-class prompts. In Proc. 15th ACM Symposium on Principles of Programming Languages, 1988, 180–190.

10. Felleisen, M. and D.P. Friedman. Control operators, the SECD-machine, and the λ-calculus. In Formal Description of Programming Concepts III , edited by M. Wirsing. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986, 193–217.

11. Felleisen, M. and D.P. Friedman. A syntactic theory of sequential state. Theor. Comput. Sci. 69(3), 1989, 243–287. Preliminary version in: Proc. 14th ACM Symposium on Principles of Programming Languages, 1987, 314-325.

12. Felleisen, M. and R. Hieb. The revised report on the syntactic theories of sequential control and state. Technical Report 100, Rice University, June 1989. Accepted at TCS.

13. Felleisen, M., D.P. Friedman, E. Kohlbecker, and B. Duba. A syntactic theory of sequential control. Theor. Comput. Sci. 52(3), 1987, 205–237. Preliminary version in: Proc. Symposium on Logic in Computer Science, 1986, 131–141.

14. Fortune, S., D. Leivant, and M. O’Donnell. The expressiveness of simple and second-order type structures. J. ACM 30(1), 1980, 151–185.

15. Friedman, D.P. and D.S. Wise. Cons should not evaluate its arguments. In Automata, Languages and Programming, S. Michaelson and R. Milner (eds). Edinburgh Univ. Press, 257–284, 1976.

16. Goguen, J., J. Thatcher, and E. Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In Current Trends in Programming Methodology IV, edited by R. Yeh. Prentice-Hall, Englewood Cliffs, New Jersey, 1979, 80–149.

17. Griffin, T. Notational definition—A formal account. In Proc. Symposium on Logic in Computer Science, 1988, 372–383.

18. Guzmán, J.C. and P. Hudak. Single-threaded polymorphic lambda-calculus. In Proc. Symposium on Logic in Computer Science, 1990, 333–345.

19. Halstead, R. Multilisp: A language for concurrent symbolic computataion. ACM Trans. Program. Lang. Syst. 7(4), 1985, 501–538.

20. Hoare, C.A.R. The varieties of programming languages. In Proc. International Joint Conference on Theory and Practic of Software Development. Lecture Notes in Computer Science, Springer Verlag, Berlin, 1989, 1–18.

21. Kleene, S. C. Introduction to Metamathematics, Van Nostrand, New York, 1952.

22. Kohlbecker, E. Syntactic Extensions in the Programming Language Lisp. Ph.D. dissertation, Indiana University, 1986.

23. Landin, P.J. A λ-calculus approach. In Advances in Programming and Nonnumerical Computation, edited by L. Fox. Pergamon Press, New York, 1966, 97–141.

24. Landin, P.J. The next 700 programming languages. Commun. ACM 9(3), 1966, 157–166.

25. Meyer, A.R. Semantical Paradigms. In Proc. Symposium on Logic in Computer Science, 1988, 236–255.

26. Meyer, A.R. and J.R. Riecke. Continuations may be unreasonable. In Proc. 1988 Conference on Lisp and Functional Programming, 1988, 63–71.

27. Milner, R. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 1978, 348–375.

28. Milner, R., M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, Cambridge, Massachusetts and London, England, 1990.

29. Morris, J.H. Lambda-Calculus Models of Programming Languages. Ph.D. dissertation, MIT, 1968.

30. Naur, P. (Ed.). Revised report on the algorithmic language ALGOL 60. Commun. ACM 6(1), 1963, 1–17.

31. Ong, L C.-H. Fully abstract models of the lazy lambda-calculus. In Proc. 29th Symposium on Foundation of Computer Science, 1988, 368–376.

32. Paterson, M.S. and C.E. Hewitt. Comparative schematology. In Conf. Rec. ACM Conference on Concurrent Systems and Parallel Computation, 1970, 119–127.

33. Plotkin, G.D. LCF considered as a programming language. Theor. Comput. Sci. 5, 1977, 223–255.

34. Plotkin, G.D. Call-by-name, call-by-value, and the λ-calculus. Theor. Comput. Sci. 1, 1975, 125–159.

35. Rees, J. and W. Clinger (Eds.). The revised^{3} report on the algorithmic language Scheme. SIGPLAN Notices 21(12), 1986, 37–79.

36. Reynolds, J.C. GEDANKEN—A simple typeless language based on the principle of completeness and the reference concept. Commun. ACM 13(5), 1970, 308–319.

37. Reynolds, J.C. The essence of Algol. In Algorithmic Languages, edited by de Bakker and van Vliet. North-Holland, Amsterdam, 1981, 345–372.

38. Riecke, J.G. A complete and decidable proof system for call-by-value equalities. In Proc. 17th International Conference on Automata, Languages and Programming. Lecture Notes in Computer Science, 443. Springer Verlag, Berlin, 1990, 20–31.

39. Sitaram, D. and M. Felleisen. Reasoning with continuations II: Full abstraction for models of control. In Proc. 1990 ACM Conference on Lisp and Functional Programming, 1990, 161–175.

40. Steele, G.L., Jr. and G.J. Sussman. Lambda: The ultimate imperative. Memo 353, MIT AI Lab, 1976.

41. Sussman, G.J. and G.L. Steele Jr. Scheme: An interpreter for extended lambda calculus. Memo 349, MIT AI Lab, 1975.

42. Troelstra, A. S. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics 344. Springer-Verlag, Berlin, 1973.

43. Wand, M. Complete type inference for simple objects. In Proc. Symposium on Logic in Computer Science, 1987, 37–44.

44. Wand, M. A types-as-sets semantics for Milner-style polymorphism. In Proc. 11th Symposium on Principles of Programming Languages, 1984, 158–164.

45. Williams, J.G. On the formalization of semantic conventions. Draft version: September 1988. To appear in Journal of Symbolic logic, 1990.