9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # On the expressive power of programming languages

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 rst 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 rm 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.

1

Landin 24] was the rst 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 rst-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 classi cation 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:x74]. Troelstra 42:I.2] resumed this work and introduced further re nements 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 satis es 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 di er by a set of programming constructs, fc1; . . . ; cn g, 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 ci to the smaller language requires a global reorganization of the entire program. A rst 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" 2

semantic equivalence relations. We also discuss some attempts at generalizing the measure to a comparison relation for arbitrary programming languages. The next section brie y 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 speci cally, 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 brie y 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 De nitional Extensions

The theory of comparing formal systems is a peripheral topic in logical studies and nds 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 rst, 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 satis es certain well-formedness criteria. The set of theorems is the subset of the formulae that the formal system de nes 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 L0 is a formal system whose expressions are a superset of the expressions over L0, generated from a richer set of operators, and whose formulae and theorems restricted to the expressions of L0 are the formulae and theorems of L0: Fm(L) \ Exp(L0) = Fm(L0); Thm(L) \ Exp(L0) = Thm(L0). A conservative extension L is a de nitional extension of L0 if there is a mapping ' : Exp(L) ! Exp(L0) that satis es the following conditions: F1 '(f ) 2 Fm(L0) for each f 2 Fm(L); F2 '(f ) = f for all f 2 Fm(L0); F3 ' is homomorphic in all logical operators; 3

F4 L ` t if and only if L0 ` '(t); and F5 L ` t $ '(t).

Kleene referred to those symbols that generate the additional expressions of the extended formal system as eliminable . version of Condition 3, namely, F40 if L ` t then L0 ` '(t). Based on condition F5, it is possible to show that the two de nitions are equivalent, assuming the usual axioms for $ 21:x74]. As we shall discuss in several remarks below, this is not the case in the context of programming languages. Instead, condition F40 leads to a di erent but related notion of language expressiveness.

Remark 1 (Weak Expressibility). Kleene's original de nition contains a weaker

3 A Formal Theory of Expressiveness

As a rst 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 satis es 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. 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.

3.1 Expressibility

De nition 3.1. (Programming Language ) A programming language L consists of

4

a set of L-phrases, which is a set of freely generated abstract syntax trees (or terms ), based on a possibly in nite1 number of function symbols F; F1 ; . . . with arities a; a1; . . .; 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 . De nition 3.1 is an abstraction of the typical speci cations of many realistic programming languages. Most languages have a context-free syntax yet enforce additional context-sensitive constraints by recursive2 decision procedures. Examples of such constraints are scoping3 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 de nition 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 de nition is in many cases equivalent to a de nition that refers to the observable output of a program. For a consideration of languages with in nite output, e.g., through imperative output statements or through potentially in nite lists, the de nition needs some adjustments. Finally, the above de nition 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

We assume that there is enough structure on an in nite 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. 2 A notable exception is Scheme as de ned 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 de nition. 3 Although most languages impose lexical scoping, De nition 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 di erent de nition of expressibility and expressiveness.

1

5

Phrases Programs

e ::= x j v j (ee) v ::= ( v x:e) j ( n x:e)

(expressions) (values )

Semantics

e is a program if and only if fv(e) = ; where fv(e) is the set of free variables in e eval (e) holds if and only if e ?! v for some v

Evaluation Contexts Reduction Steps

E ::= j (( v x:e)E ) j (Ee)

( ) ( v)

E (( nx:e)e0) ?! E (e x=e0]) E (( v x:e)v) ?! E (e x=v]) where e x=e0 ] is the capture-free substituion of e0 for all free x in e

Figure 1: The programming language approach of equational restrictions, the de nition uses arbitrary recursive predicates for ltering 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 speci cally, the -phrases are generated from a set of variables (0ary constructors), fx; y; z; . . .g, 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 nx 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.

6

The operational semantics of re ects the semantics of realistic programming languages like Iswim, ML, and Scheme 34].4 The speci cation 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-byvalue 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 xed point operators, which facilitate the recursive de nition of functions: Yn = ( n f:( nx:f (xx))( nx:f (xx))) and Yv = ( v fx:( v g:gg)( v x:f ( v x:(gg)x))x): Two simple diverging programs are n = Yn ( n x:x) and v = Yv ( v xy:xy)( vx:x). To illustrate the impact of syntactic constraints on programs, we also de ne t, a typed variant of . t has the same set of phrases as but uses a type checking algorithm for ltering 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 de ning 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 de ne the notion of a conservative programming language extension.

De nition 3.2. (Conservative Extension & Restriction ) A programming language L is a conservative extension of a language L0 if the constructors of L0 are a subset of the constructors of L with the di erence being fF1; . . . ; Fn; . . .g, which are not constructors of L0;

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

4

7

Programs Types Type Assertion Type Inference

e is a program if and only if it is closed and ; ` e :

::= j ?!

A: Variables ?! Types ( nite functions) where A x= ](x) = A x= ](y) = A(y) (functional update) A x= ] ` e : 0 A ` v;n x:e : ?! 0 A ` e : 0 ?! ; A ` e0 : 0 A ` (ee0) :

A ` x : if A(x) = A ` Yn : ( ?! ) ?!

A ` Yv : (( ?! 0 ) ?! ( ?! 0 )) ?! ( ?! 0 )

Figure 2:

t

the set of L0-phrases is the full subset of L-phrases that do not contain any constructs in fF1; . . . ; Fn; . . .g; the set of L0-programs is the full subset of L-programs that do not contain any constructs in fF1; . . . ; Fn; . . .g; and the semantics of L0, eval L , is a restriction of L's semantics, i.e., for all L0programs P , eval L (P ) holds if and only if eval L(P ) holds. Conversely, L0 is a conservative restriction of L. To emphasize the constructors on which the restriction and extension di er, we write L0 = L n fF1; . . . ; Fn ; . . .g and L = L0 + fF1; . . . ; Fn; . . .g. 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 speci cation exist).

0 0

In our running example, the restricted language v is without call-by-name abstractions:

n

n

is without v -abstractions,

= n v;

v

= n n:

A restriction of the above evaluation process to v - and n-phrases yields a call-byvalue and a call-by-name semantics, respectively. The corresponding sublanguages of t are de ned similarly. 8

To enrich the set of examples, we add a let construct to . There is one binary let constructor for each variable x : letx : term term ?! term . Like x, letx binds its variable, namely in the second subexpression. The concrete syntax for letx(e; e0) (let x be e in e0): The semantics of + fletxg, or + let for short, requires an additional clause in the speci cation of evaluation contexts is

E ::= . . . j (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]):

(letv )

Otherwise the de nition 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 exibility, the new rule only requires that, at each occurrence of the abstracted variable, the named subexpression is typable with some type: A ` e : ; A ` e x=e0] : 0 A ` (let x be e in e0) : 0 t + let is polymorphic in the spirit of ML 27, 28, 43:43, 44]. Unlike -bound variv ables, let-bound variables can have several types. For example, x in (let x be ( y:y) in (xx)) conceptually assumes two di erent 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 exible. 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.

De nition 3.3. (Eliminability; Expressible Programming Constructs ) Let L be a programming language and let fF1; . . . ; Fn ; . . .g be a subset of its constructors such that L0 = LnfF1; . . . ; Fn; . . .g is a conservative restriction. The programming facilities F1 ; . . . ; Fn ; . . . are eliminable if there is a recursive mapping ' from L-phrases to L0 phrases that satis es the following conditions: 9

E1 '(e) is an L0-program for all L-programs e ; E2 '(F(e1; . . . ; ea)) = F('(e1); . . . ;0'(ea)) for all facilities F of L0 , 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 L0 can express the facilities F1; . . . ; Fn ; . . . with respect to L. We

0

omit the quali cation if the language universe is clear from the context. By abuse of notation, we write ' : L ?! L0.

Condition E2 in this de nition implies that the mapping ' is the identity on the language L0. 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.

takes on the following shape: F30. if eval L(e) holds then eval L ('(e)) holds, The intuition behind this de nition is that the translated phrase has at least as many capabilities as the original one. The terminology re ects our belief that any di erences 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.

0

Remark 2 (Weak Expressibility). By using an adaptation of Kleene's original Condition F40 (see Remark 1 in the previous section) instead of the third condition in the preceding de nition, we get a weak notion of expressibility. The revised condition

An alternative understanding of the above de nition 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 a ect 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 de nition of operational equivalence, we can characterize su cient conditions for the eliminability of programming constructs. A formal de nition of the operational equivalence relation relies on the auxiliary notion of a program context. 10

De nition 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 e1; . . . ; en are phrases in L, then the instance C (e1; . . . ; en) is a phrase in L that is like C ( 1; . . . ; n) except at occurrences of i where it contains the phrase ei: if C ( 1; . . . ; n ) = i then C (e1; . . . ; en) = ei, and if C ( 1; . . . ; n) = F(C1( 1; . . . ; n); . . . ; Ca( 1; . . . ; n)) for some F with arity a then C (e1; . . . ; en) = F(C1(e1; . . . ; en); . . . ; Ca(e1; . . . ; en)). An L-program context for a phrase e is a unary context, C ( ), such that C (e) is a program. For n, the context C0( ) = ( n xy: )( nx: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 de nition of operational equivalence compares the termination behavior of programs.5 De nition 3.5. (Operational Equivalence ) Let L be a programming language and let eval L be its operational semantics. The L-phrases e1 and e2 are operationally equivalent, e1 =L e2, if there are contexts that are program contexts for both e1 and e2, and if for all such contexts, C ( ), eval L(C (e1)) holds if and only if eval L(C (e2)) holds. With the above program context C0, it is possible, for example, to di erentiate the phrases x and y . Since n diverges, C0(x) = ( n xy:x)( nx:x) n terminates whereas C0(y) = ( n xy:y)( nx: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 nite sets of equations. It is sound but incomplete, i.e., if ; ` e = e0 then e = e0 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 speci cally, the term e1 operationally approximates e2, e1 @L e2, if for all program contexts, C ( ), for e1 and e2, eval L (C (e2)) holds if eval L(C (e1)) holds. | In conjunction with the above context C0, the program context C1( ) = ( n yx: )( nx:x) n shows that x and y do not approximate each other.

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

5

11

? ` ( v x:e)v = e x=v ] ? ` e = e0 ? ` v x:e = v x:e0 x 62 fv(?) ? ` (let x be v in e) = e x=v ]

?` e= ? ` e = e0 ? ` ee00 = e0 e00 ? ` (let x be

?`e = ? ` e = e0 ? ` e00 e = e00e0

in e) =

? ` e = e0 ? ` (let x be e in e00 ) = (let x be e0 in e00) x 62 fv(?) ? fe = e0 g ` e = e0 ?`e=e ? fe = g ` e1 = e2 ; ? fe = v g ` e1 = e2 for all v ? ` e1 = e2 ? ` e = e0 ? ` e0 = e ? ` e = e0; ? ` e0 = e00 ? ` e = e00

v + let

Figure 3: A Calculus for Operational Equivalence on

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 = L0 + fF1; . . . ; Fn; . . .g be0 a conservative extension of L0. If ' : L ?! L0 is homomorphic in all facilities of L and preserves program-ness, and if Fi (e1 ; . . . ; ea ) =L '(Fi (e1; . . . ; ea )) for all Fi and all L-expressions e1; . . . ; ea , then L0 can express the facilities F1; . . . ; Fn ; . . .. Proof. It su ces to show that condition E3 of De nition 3.3 holds for '. Assume that P is an L-program such that eval L(P ) holds. By the construction of P , there is

i i i

a context C ( 1; . . . ; n) such that

P = C (p1; . . . ; pn )

where p1, . . . , pn are the nite number of outermost occurrences of phrases constructed from some facilities in F1; . . . ; Fn ; . . .. Thus, C ( 1; p2; . . . ; pn ) is a program context for p1. It follows from the theorem's assumption that

eval L (C (p1; . . . ; pn )) holds if and only if eval L (C ('(p1); . . . ; pn )) holds:

12

Repeating this step n times proves that

eval L (C (p1; . . . ; pn )) holds if and only if eval L (C ('(p1); . . . ; '(pn))) holds:

But, since C does not contain any facilities in F1; . . . ; Fn; . . .,

C ('(p1); . . . ; '(pn )) = '(C (p1; . . . ; pn )) = '(P ):

Moreover, since L conservatively extends L0,

eval L(P ) holds if and only if eval L ('(P )) holds:

0

This completes the proof.

struct. 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 di erence 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 di erence is that in the typed case the translation must not only preserve the semantics but also the typability in order to preserve program-ness.

Remark 4 (Weak Expressibility). The theorem holds for weak expressibility even if we replace operational equivalence by operational approximation: If Fi(e1; . . . ; ea ) @L '(Fi(e1; . . . ; ea )), then the F1; . . . ; Fn; . . . are weakly eliminable. An application of this theorem shows that let is an example of an eliminable coni i

subexpression. The base case for e; e0 in v proceeds as follows. By the homomorphism constraint, '(e) = e and '(e0) = e0. By the laws in Figure 3, e = ` (let x be e in e0) = = ( x:e0)e and, for all values v , e = v ` (let x be e in e0) = e0 x=v] = ( x:e0)e;

6

Proposition 3.7 The constructor let is eliminable in call-by-value languages. (i ) v can express let with respect to v + let. (ii ) tv can express let with respect to tv + let. Proof. (i ) Set '(let x be e in e0) = ( v x:'(e0))'(e). To show that the two phrases are operationally equivalent we proceed by induction on the number of let's in the

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

13

(let x be e in e0) = +let ( x:e0)e: The induction step proceeds along the same line. (ii ) Set '(let x be e in e0) = (( v d:'(e0) x='(e)])'(e)) where d does not occur free in e or e0. To verify that this translation maps programs to programs, it su ces 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 xed set of type assumptions, '(e) has the same type as e . Assume e and e0 are let-free, and consider the typing of an instance of let:

and therefore,

A ` (let x be e in e0) :

0

for some A and 0. By the setup of the inference system, A ` e : for some and A ` e0 x=e] : 0. Since, by assumption, '(e) = e and '(e0) = e0, A ` '(e) : and A ` '(e0) x='(e)] : 0. The rest follows easily: A ` ( v d:'(e) x='(e0)]) : ?! 0 and also A ` ( v d:'(e) x='(e0)])'(e) : 0: The induction step requires a lemma that proves '(e) x='(e0)] has the same type as e x=e0] if '(e) and '(e0) have the same type as e and e0. 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 e0) = = ( d:e0 x=e]) = ( d:e0 x=e])e

and also, for all v ,

e = v ` (let x be e in e0) = e0 x=v] = ( d:e0 x=v])v = ( d:e0 x=e])e:

The rest is obvious. The converse of Theorem 3.6 does not hold. That is, the facilities F1; . . . ; Fn ; . . . may still be expressible in L0 even though the translation from L to L0 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 Fi(e1; . . . ; ea ) for some Fi 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.

i

Theorem 3.8 Let L = L0 + fF1;0. . . ; Fn ; . . .g be a conservative extension of L00. If for all mappings ' : L ?! L that are homomorphic in all facilities of L , Fi (e1 ; . . . ; ea ) =L '(Fi (e1 ; . . . ; ea )) for some L-expressions e1; . . . ; ea and Fi in F1; . . . ; Fn ; . . ., 6 and if there is a context C ( ) over L0 that witnesses this inequality, then L0 cannot

i i i

express the facilities F1; . . . ; Fn ; . . ..

14

Proof. Let ' : L ?! L0 be an arbitrary mapping that is homomorphic 0in all facilities of L0. Suppose '(Fi(e1; . . . ; ea )) = e and let C ( ) be the context over L that observes

i i i i

the operational di erence between e and Fi(e1; . . . ; ea ). Since ' is homomorphic over L0 , '(C (Fi(e1; . . . ; ea ))) = C ('(Fi(e1; . . . ; ea ))) = C (e): But, by assumption, eval L(C (Fi(e1; . . . ; ea ))) 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 L0 can possibly satisfy condition E3 of De nition 3.3 if the antecedent of the theorem holds, and that consequently the programming constructs F1; . . . ; Fn ; . . . cannot be eliminable. Based on this rst non-expressibility theorem, we can now prove that call-by-name cannot express call-by-value abstractions and vice versa.

i

0

Proposition 3.9 extends both

(i ) (ii )

n v

v

and

n.

cannot express cannot express

v n

with respect to . with respect to .

( 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 ?! e0 there is always an e00 such that e0 ?! e00; 2. it may uniformly converge to a value for all arguments, including n : for all expressions e there is a value ve such that ( n y:p)e ?! ve; 3. it may activate the argument for a rst time: ( n y:p)e ?! ee1 . . . ek for some e1; . . . ; ek. 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 ?! e0 then E (e) ?! E (e0). Let ( v x:e) be an abstraction in that converges upon application to some values. More speci cally, let e and v be in n and assume that for some value u, ( v x:e)v( nx: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 '( xv: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

7

Proof. 7 (i ) According to the semantics for n , the application of an abstraction

Improved by Carolyn Talcott.

15

translation cannot converge uniformly. Thus, let e1; . . . ; ek be the expressions such that

C ('( v x:e)) = '( v x:e)v( nx:x) ?! ( n y:p)v( nx:x) ?! ve1 . . . ek ( 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)e1 . . . ek ( n x:x) ?!

n e2 . . . ek ( 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:( nx:x)) and assume that ' is a structure-preserving translation. Clearly, eval(C ( nx:( nx:x))) holds, but, C ('(( n x:( nx:x)))) diverges. Hence, a structure-preserving translation cannot preserve operational equivalence, which proves the claim.

Remark 5 (Weak Expressibility). By Remark 4,

because v x:e @

n x:e.

n

can weakly express

v

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 = L0 + fF1; . . . ; Fn; . . .g be a conservative extension of L0. If0 for some Fi (e1 ; . . . ; ea ) there is a program context C over L0 but there is no e in L such that Fi (e1; . . . ; ea ) =L e, then L0 cannot express the facilities F1; . . . ; Fn; . . .

i i

Although the de nition of eliminable programming construct is a satisfactory rst 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: 16

3.2 Macro Expressibility

1. In a functional language with rst-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 ( xed) 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 abstractions8 in relation to the following de nition and its uses.

De nition 3.11. (Macro Eliminability; Macro Expressibility ) Let L be a programming language and let fF1; . . . ; Fn ; . . .g be a subset of its constructors such that L0 = L n fF1; . . . ; Fn ; . . .g is a conservative restriction. The programming facilities F1 ; . . . ; Fn ; . . . are macro eliminable if they are eliminable and if the eliminating mapping ' from L to L0 satis es the following, additional condition: E4 For each a -ary construct F 2 fF1; . . . ; Fn ; . . .g there exists an a -ary syntactic abstraction, A, over L0 such that

'(F(e1; . . . ; ea)) = A('(e1); . . . ; '(ea)):

We also say that L0 can macro-express the facilities F1; . . . ; Fn; . . . 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.120 Let L = L0 + fF1; . . . ; Fn ; . . .g be a 0conservative extension of L0. If ' : L ?! L is homomorphic in all facilities of L and preserves program-ness, and if there is a syntactic abstraction Ai for each Fi in F1; . . . ; Fn; . . . such that Fi (e1 ; . . . ; ea ) =L Ai ('(e1); . . . ; '(ea )) for all L-expressions e1; . . . ; ea , then L0 can

macro-express the facilities F1; . . . ; Fn; . . ..

i i i

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

8

17

what is needed to adapt the proof of Theorem 3.6 to the stronger conclusion. Moreover, the additional condition E4 permits a simpli cation of the theorem to a corollary that no longer makes any reference to the translating map. The corollary is used in Section 4.

i

Proof. It is easy to see that the additional condition in the antecedent is precisely

Corollary 3.13 Let L = L0 + fF1; . . . ; Fn; . . .g be a conservative extension of L0. If there is a syntactic abstraction Ai for each Fi in F1 ; . . . ; Fn; . . . so that Fi (e1; . . . ; ea ) =L Ai(e1; . . . ; ea ) for all L-expressions e1; . . . ; ea , then L0 can macro-express the facilities

F1 ; . . . ; Fn ; . . ..

i i

By Proposition 3.7, v can express let. A simple check of the proof reveals that the translation between the two languages satis es the antecedent of the corollary, and that therefore let is also macro-expressible. More importantly, however, the additional condition E4 in De nition 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 a ects existing operational equivalences.

Theorem 3.14 Let L1 = L0 + fF1; . . . ; Fn; . . .g be a conservative extension of L0. Let =0 and =1 be the operational equivalence relations of L0 and L1 , respectively. (i ) If the operational equivalence relation of L1 restricted to L0 expressions is not 6 equal to the operational equivalence relation of L0 , i.e., =0 = (=1 jL0 ), then L0 cannot macro-express the facilities F1 ; . . . ; Fn ; . . ..9 (ii ) The converse of (i ) does not hold. That is, there are cases where L0 cannot express some facilities F1 ; . . . ; Fn; . . ., even though the operational equivalence relation of L1 restricted to L0 is identical to the operational equivalence relation of L0, i.e., =0 = (=1 jL0 ). Proof. Let eval 0 and eval 1 be the respective evaluation predicates for L0 and L1. (i ) A di erence between the restricted operational equivalence relation of L1 and that of L0 implies that there are two phrases e and e0 in L0 and L1 such that either e =0 e0 and e =1 e0 or e =0 e0 and e =1 e0. For the rst case, let C ( ) be a context 6 6 over L1 that can di erentiate the two phrases e and e0. Let us say, without loss of

generality, that

eval 1 holds for C (e) but not for C (e0): Now, assume contrary to the claim in the theorem that L0 can express the facilities F1 ; . . . ; Fn ; . . .. Then, there is a mapping ' : L1 ?! L0 that satis es conditions E1

9

An 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.

18

termination behavior: eval 0('(C (e))) holds because eval 1(C (e)) holds and eval 0('(C (e0))) does not hold because eval 1 (C (e0)) does not hold. (y) By conditions E2 and E4, the programs '(C (e)) and '(C (e0)) can only di er in a nite number of occurrences of e and e0. In other words, there is a program context D( ) over L0 such that '(C (e)) = D(e) and '(C (e0)) = D(e0): for the proof, see the Translation Lemma below. Next, from the assumption e =0 e0, it follows that '(C (e)) = D(e) and '(C (e0)) = D(e0) have the same termination behavior in L0, i.e., eval 0 (D(e)) holds if and only if eval 0(D(e0 )) holds: But this contradicts the above fact (y) that '(C (e)) = D(e) converges and '(C (e0)) = D(e0) diverges, which concludes the rst case. For the second case, assume e 6=0 e0 and e =1 e0. This assumption actually implies that there are no contexts over L0 that complete both e and e0 to programs. () For otherwise, there must be a context C ( ) such that eval 0(C (e)) holds while eval 0 (C (e0)) does not. Since L1 is a conservative extension of L0 , eval 1(C (e)) holds, eval 1 (C (e0)) does not, and therefore contrary to the assumption, e 6=1 e0. Now again, assume contrary to the claim of the theorem that L0 can express the additional facilities in L1 via an appropriate translation ' : L1 ?! L0. Since e and e0 are operationally equivalent in L1, there must be a context C ( ) over L1 such that eval 1 (C (e)) and eval 1(C (e0)). By assumption, eval 0('(C (e))) and eval 0('(C (e0))). 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 (e0)) = D(e0). 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 nish the proof of claim (i), we must nally show that a homomorphic function preserves the structure of a program. Translation Lemma. Let ' : L1 ?! L0 be a translation that satis es Conditions (0) through (3) in De nitions 3.3 and 3.11. Let C ( ) be a context over L1. Then, there is a context D( ) over L0 such that '(C (e)) = D(e) and '(C (e0)) = D(e0). Proof. The proof is an induction on the structure of C ( ). The only interesting case is the following. Say, C ( ) = F(C1( ); . . . ; Ca( )) for some F in F1; . . . ; Fn; . . .. Then, '(F(C1(e); . . . ; Ca(e)) = A('(C1(e)); . . . ; '(Ca(e))) 19

C (e) and C (e0) have counterparts in L0, '(C (e)) and '(C (e0)), that have the same

through E4 of De nitions 3.3 and 3.11. By conditions E1 and E3, the programs

and

The proof of the Translation Lemma nishes 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 ts 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 xed point operator, whose types are either base types or arrow types. Because of the type system, it is impossible to de ne 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 rst 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 rst claim is derived from a theorem by Ong 31: Thm. 4.1.1],10 based on the preceding meta-theorem. Consider the phrases x( ny: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) = x(x(YK) )(YK): The operational reasoning for a veri cation of this equivalence is as follows. No matter which argument the procedure x evaluates rst, the expression (YK) eventually appears in the hole of the evaluation context, which leads to an immediate termination of the program evaluation.

n

'(F(C1(e0); . . . ; Ca(e0)) = A('(C1(e0)); . . . ; '(Ca(e0))) for some xed syntactic abstraction A over L0 by condition E4. By inductive hypothesis, there are contexts Di ( ), for 1 i a, such that '(Ci(e)) = Di(e) and '(Ci(e0)) = Di(e0). But then D( ) = A(D1( ); . . . ; Da( )) is the context corresponding to C ( ). The other cases are similar but easier. lemma

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

10

20

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 a ect the rest of the program. Thus, the context

setting, the two are operationally equivalent:

v f:(f ( v x:x))

C ( ) = ( n x: )( v x:( n y:y)) can distinguish between the two phrases: C (x( ny: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

=

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 di erentiate the two with the context

C ( ) = ( v x:( ny:x)):

The context applies a phrase to a function that returns the value of the rst 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 = 6 = . 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.

n

For a second application of Theorem 3.14, we show that the polymorphic let construct of tv is not macro-expressible in t. On one hand, this lemma con rms 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

t v

cannot macro-express let with respect to

t + let. v

21

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 tv program context for the two expressions, and the two programs cannot be operationally equivalent: ((gx)(ff ))) 6= ( v d:((gx)(ff )))(gx) Still their dynamic behavior is the same. The di erence between the two programs is that the second computes the application of g to x twice, throwing away the rst 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 )) = +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 di erentiate 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.

t t

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 rst 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 xes 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. 22

De nition 3.17. ((Macro) Expressiveness ) Let L0 and L1 be conservative language restrictions of L. L1 is at least as (macro-) expressive as L0 with respect to L if L1 contains or can (macro-) express a set of L-constructs whenever L0 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 L0, L1,0 L2 be conservative restrictions of L, and let L be a conservative restriction of L . (i ) L0 is less expressive than L0 with respect to to L. (ii ) If L0 is less expressive than L1 with respect to L and L1 is less expressive than L2 with respect to L, then L0 is less expressive than L2 with respect to L. (iii ) If L0 is less expressive than L1 with respect to L, then L0 is less expressive than L1 with respect to L0. Proof. The proof is an easy calculation, verifying the conditions based on the above

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

sions of the languages.

Theorem 3.19 Expressiveness relationships are not invariant under uniform extenProof. For a simple example, consider , n, and v , and recall that the two sub-

languages 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 rst value. The formal speci cation requires an extension of the set of evaluation contexts to E ::= . . . j (begin E e) and an additional reduction clause: E (begin v e) ?! E (e): Now, n +fbeging 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 e1 e2) is (macro-) expressible as ( v xy:y)e1e2 in v . Thus, in the extended setting n + fbeging is more expressive than v + fbeging. 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. 23

The example in the preceding theorem formalizes Algol 60's de nition of call-byvalue 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 de ne 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 speci c language universes for speci c conservative language restrictions: they often have no validity in other contexts!

Syntax

c ::= f ::= v ::=

Semantics

cjf j (lambda (x . . .) e) e ::= v jx j (e e . . .)

0 j 1 j ?1 j 2 j ?2 j 0? j 1+ j 1? j + j ?

...

(numerals) (numeric functions ) (constants) (abstractions ) (values ) (variables ) (applications )

Evaluation Contexts Reduction Steps

eval (e) holds i e ?! v for some v

E ::= j (v . . . E e . . .)

E ((fv . . .)) ?! E ( (f; v; . . .)) if (f; v; . . .) is de ned E (((lambda (x1 . . . xn ) e) v1 . . . vn )) ?! E (e x1=v1; . . . ; xn =vn])

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 6= 0

Figure 4: Pure Scheme

4 The Structure of Idealized Scheme

Pure Scheme is a simple functional programming language. It has multi-ary, call-byvalue 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 speci es the behavior of

24

constants in Pure Scheme and its extensions. Typically, the constants include integers, characters, booleans, and some appropriate functions; Figure 4 contains the appropriate de nition 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 speci cation of Pure Scheme, based on a reduction semantics in the style of the previous section. Scheme programs satisfy two contextsensitive de nitions: 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 in nite 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 unde ned, 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 re ect 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 di erent control operators, one for stopping the execution of a program and another for handling the general ow of control. The third subsection shows how imperative assignments add expressive power to the core language. Finally, the last

Although this is common practice in semantic considerations, a more realistic speci cation 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.

11

25

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. 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

4.1 Local Control and Dynamic Types

E ::= . . . j (Bif E e e);

the following two additional reduction rules characterize the behavior of truth-value based Bif: E (Bif 1 et ef ) ?! E (et) (Bif :true) E (Bif 0 et ef ) ?! E (ef ): (Bif :false) If the test value in a Bif-expression is neither 0 nor 1, the evaluation of the program is unde ned, 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. 26

Remark 8 (Weak Expressibility). An extension of Pure Scheme with Bif and

(Bif true 1 2); and map to the same image, namely (Bif t 1 2);

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

A(t; '(e1); '(e2))

for some xed syntactic abstraction A. But it is then impossible that the translation preserves program behavior because the rst 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 di erently, 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 di er accordingly from (Bif.true) and (Bif.false): (Lif v et ef ) ?! et for v 6= 0 (Lif :v) (Lif 0 et ef ) ?! ef : (Lif :nil) Proposition 4.2 Pure Scheme cannot macro-express Lif. 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:

Proof Sketch. For readability, we carry out the proof in PS(Bif ). Since Bif is

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 rst 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 27

(3) use its argument in the procedure position of an application. For the evaluation of C ( ) to reach , the procedure must return two di erent 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 rst test position. In short, either the evaluation of C diverges at the rst 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) 6=Lif 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 su ces 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 e ectively 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 );

(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. 28 where

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 modi ed context invokes p on 1: C 0( ) = (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 0 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 0(1) =Lif C 0( ), yet, with int? in the language, this is no longer the case: C 0(1) 6=int? C 0( ). 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 ::= . . . j (call=cc e) j (abort e)

(continuation captures ) (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

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 ow 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 speci es the syntax and a simple reduction semantics of Pure 29

4.2 Non-Local Control

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 example12 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 rst expression with these contexts evaluates to 0, the second expression diverges in the same contexts: (lambda (f ) ((f 0) )) 6=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

This 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 di erently, 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 speci ed as a part of the language standards!

12

30

Proposition 4.6 The control constructs abort and call/cc cannot express each

other: (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 rst 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 di er 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 rst 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) 6=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 nd 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 (e0)) for some e0, 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 (e0 ) then either (1) e0 is a value, or (2) e0 contains a stuck redex, or (3) there is an e00 such that E (e0) ?! E (e00) and E (e00) satis es the above condition. Since an expression over PS(call/cc) does not contain any abort expression, it vacuously satis es the antecedent of the auxiliary claim. Hence, it either diverges or it returns a value and cannot be interchanged with an abort expression without e ect 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). 31

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 L1 = L0 + fF1; . . . ; Fn; . . .g be a conservative restriction of L0. Let =0 and =1 be the operational equivalence relations of L0 and L1,

respectively. (ii ) The converse of (i ) does not hold. That is, there are cases where L0 cannot express some facilities F1 ; . . . ; Fn; . . ., even though the operational equivalence relation of L1 restricted to L0 is identical to the operational equivalence relation of L0, i.e., =0 = (=1 jL0 ).

Proof. By the preceding proposition we know that PS(call/cc) cannot express abort. To nish 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 jPS (call=cc)); the other direction is obvious. Assume that e 6=c+a e0. We prove that e 6=c e0. Suppose there is a context C that can distinguish e and e0 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 e1); . . . ; (abort en)):

Now let a be a variable that does not occur in C , and let the context C 0(e) be de ned as follows: C 0( ) = ((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 0(e)) holds. First, the program C 0 evaluates to an intermediate program with a few administrative steps:

C 0(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 ei), and therefore 32

D (e , ((lambda (x ) (abort (x ))) (lambda () e 1 )), . . ., ((lambda (x ) (abort (x ))) (lambda () e n )))

terminates if and only if D (e , (abort e1), . . ., (abort en)) = C (e ) terminates. The same analysis holds for the program C (e0), and we have thus shown that the context C 0( ) distinguishes e and e0: e6=c e0.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 di erent 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 nal 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 identi er 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

((lambda (d) (f 0)) (f 0)) =ps (f 0):

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 rst subexpression is discarded, the expression is operationally equivalent to (f 0): The veri cation 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) )))) );

The transformation of C (e) into C (e0 ) 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.

14

33

Additional Syntax

e ::= . . . j (set! x e) j (letrec ( x v] . . .) e)

(assignments) (recursive de nitions)

Extended Semantics

eval (e) holds i e ?! v or (letrec () e) ?! (letrec (. . .) v ) for some v

Additional Evaluation Contexts

E ::= . . . j (set! x E )

Additional Reduction Steps (letrec (. . .) E ((fv . . .))) ?! (letrec (. . .) E ( (f; v; . . .)))

(letrec (. . .) E ((lambda (x1 . . .) e) v1 . . .)) ?! (letrec (. . . x v ] . . .) E (x)) ?! (letrec (. . . x u] . . .) E ((set! x v )) ?! (letrec ( x v ] . . .) E ((letrec ( y u] . . .) e))) ?!

provided (f; v; . . .) is de ned (letrec (. . . xi vi ] . . .) E (e xj =vj ; . . .])) if the xi ; . . . are assignable and the xj ; . . . are not assignable (letrec (. . . x v ] . . .) E (v )) (letrec (. . . x v ] . . .) E (v )) (letrec ( x v ] . . . y u] . . .) E (e))

Figure 6: Pure Scheme with state which declares a procedure f . Upon the rst application, the procedure modi es 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)) 6=set! (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 o er data constructors, say cons, that do not evaluate their arguments 15]. It is a widely held 34

belief that such provisions are super uous in the presence of higher-order procedural abstractions.

Evaluation Contexts

E ::= j (u . . . E e . . .)

where u = v n fcons$g

Additional Reduction Steps

E ((cons$ e1 e2) 1) ?! E (e1) E ((cons$ e1 e2) 2) ?! E (e2)

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 di erent conservative extensions of Pure Scheme, each of which incorporates a di erent form of a callby-name constructor. The rst extension, PS(lazy), provides the constructor as a rst-class function: v ::= . . . j cons$ (call-by-name cons) j (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 rst. The non-evaluating constructor is no longer a rst-class function but is only available in rst-order form: v ::= . . . j (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 ))) 35

It is easy to check that the corresponding translation satis es 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 de nition of an expressible construct, programs in a less expressive language generally have a globally di erent 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 rst 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 rst 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

This 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].

15

36

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. A program in Pure Scheme|or any other functional language without assignments| must realize the counting of transactions in a di erent 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 rst 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 o ers many opportunities for code simpli cations. 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. 37

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 speci cations 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 (simpli ed) continuation-passing style. Speci cally, 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 avor, 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 speci c conjecture about this issue must address the question of which programs actually bene t 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 a ects 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 de nition 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 38

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 bene t 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 de ning 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 di erent 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 de ne 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 fulledged 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 39

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 de nitional 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 di erent 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 su cient 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. Speci cally, we proposed that the translations between languages should preserve as much of a program's structure as possible. 40

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 nd expressive extensions of languages whose additional facilities do not invalidate operational laws.16 The current framework is only a rst 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. siveness 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 Gri n's remark that my original approach focused too much on macro expressiveness, redirected my e orts towards the broader framework of expressiveness of Section 3.1. Hans Boehm, Robert

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].

Acknowledgement. Dan Friedman directed my attention to the idea of expres-

41

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.

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 Arti cial 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. NorthHolland, Amsterdam, 1984. 4. Berry, G. Sequentialite 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 rst-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. 42

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 speci cation, correctness, and implementation of abstract data types. In Current Trends in Programming Methodology IV, edited by R. Yeh. Prentice-Hall, Englewood Cli s, New Jersey, 1979, 80{149. 17. Griffin, T. Notational de nition|A formal account. In Proc. Symposium on Logic in Computer Science , 1988, 372{383. 18. Guzman, 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. 43

28. Milner, R., M. Tofte, and R. Harper. The De nition 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 revised3 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. 44

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

45

- On the expressive power of logic programming languages with sets
- On the expressive power of three-valued and four-valued languages
- On the expressive power of graphical query languages
- On the expressive power of a language for programming coordination media
- On the power of database update languages
- On the Kolmogorov expressive power of boolean query languages
- On the expressive power of planar perfect matching and permanents of bounded treewidth matr
- On the expressive power of temporal logic
- On the expressive power of semijoin queries
- On the expressive power of pure OCL

更多相关文章：
**
***On* *the* *expressive* *power* *of* logic *programming* *languages* with ....pdf

*On* *the* *expressive* *power* *of* logic *programming* *languages* with sets_专业资料。Several recent papers [Kup87a] [Kup87b] [BNR*87] have proposed adding sets ...**
***On* *the* *Expressive* *Power* *of* *Programming* *Languages*.unkown

*On* *the* *Expressive* *Power* *of* *Programming* *Languages* Matthias Felleisen* Department *of* Computer Science Rice University Houston, TX 77251-1892 Abstract *The* ...**
***On* *the* *Expressive* *Power* *of* Logic *Programming* *Languages* with ....unkown

*On* *the* *Expressive* *Power* *of* Logic *Programming* *Languages* with Sets Gabriel M. Kuper IBM T. J. Watson Research Laboratory Yorktown Heights, New York 1 ...**
***On* *the* *Expressive* *Power* *of* Concurrent Constraint *Programming* ....unkown

BRICS Basic Research in Computer Science*On* *the* *Expressive* *Power* *of* Concurrent Constraint *Programming* *Languages* Mogens Nielsen Catuscia Palamidessi Frank D. ...**
...***of* informal claims *on* *the* *expressive* *power* *of* *programming* ....unkown

B. Jones Revised March 1991 Abstract Felleisen, M.,*On* *the* *expressive* *power* *of* *programming* *languages*, Science *of* Computer *Program- ming* 17 (1991) X-75...**
***On* *the* *Expressive* *Power* *of* Temporal Concurrent Constraint ....unkown

*On* *the* *Expressive* *Power* *of* Temporal Concurrent Constraint *Programming* *Languages* Mogens Nielsen BRICS Dept. *of* Computer Science, University *of* Aarhus mn@...**
***On* *the* *Expressive* *Power* *of* Logic *Programming* *Languages* with ....unkown

*On* *the* *Expressive* *Power* *of* Logic *Programming* *Languages* with Sets Gabnel M Kuper IBM T J Watson Research Laboratory Yorktown Heights, New York 1 ...**
...Combining Functional and Logic ***Programming* *Languages* ....unkown

3 p. 17 Complexity and*Expressive* *Power* *of* Disjunctive Logic *Programming* p. 23 Combining Functional and Logic *Programming* *Languages* p. 43 Signed Logic ...**
***On* *the* *Expressive* *Power* *of* Temporal Concurrent Constraint ....unkown

Electronic Notes in Theoretical Computer Science www.elsevier.com/locate/entcs*On* *the* *Expressive* *Power* *of* Temporal Concurrent Constraint *Programming* *Languages* (...**
***On* *the* *Expressive* *Power* *of* a *Language* for *Programming* ....unkown

*On* *the* *Expressive* *Power* *of* a *Language* for *Programming* Coordination Media Enrico Denti Antonio Natali LIA - Laboratorio d'Informatica Avanzata DEIS - ...**
***On* *the* *expressive* *power* *of* a *language* for *programming* ....unkown

and author profiles for this publication at: http://www.researchgate.net/publication/221001265*On* *the* *expressive* *power* *of* a *language* for *programming* ...**
***Expressive* *Power* *of* specification *Languages*.pdf

For example, all general-purpose*programming* *languages* have *the* same *expressive* *power*, and hence *the* choice between them is not signi cant. However, there...**
***On* *the* *expressive* *power* *of* a *language* for *programming* ....unkown

and author profiles for this publication at: http://www.researchgate.net/publication/221001265*On* *the* *expressive* *power* *of* a *language* for *programming* ...**
***On* *the* *expressive* *power* *of* graphical query *languages*.pdf

*On* *the* *expressive* *power* *of* graphical query *languages*_专业资料。In this paper...In Section 5 we deal with *the* class *of* *programming* queries. Finally, ...**
***On* *Expressive* *Power* *of* Second Order Propositional *Program* ....pdf

*On* *Expressive* *Power* *of* Second Order Propositional *Program* Logics_专业资料。We examine *expressive* *power* *of* second order propositional *program* logics: logic 2M ...**
...and ***the* Abstractive *Power* *of* *Programming* *Languages*.pdf

References Fell91] Matthias Felleisen, \*On* *the* *Expressive* *Power* *of* *Programming* *Languages*", Science *of* Computer *Programming* 17 nos. 1{3 (December 1991) ...**
***On* *the* *expressive* *power* *of* semijoin queries.pdf

*On* *the* *expressive* *power* *of* semijoin queries_专业资料。*The* semijoin algebra ...Modal *languages* and bounded fragments *of* predicate logic. Journal *of* ...**
***The* *Expressive* *Power* *of* Side Effects in Prolog J.A. Makowsky ....pdf

influence*of* side effects in Logic *Programming*. ...Ullman. Introduction to Automata Theory, *Languages* ...*The* *Expressive* *Power* *of* Side E ects in Prolog ...**
...several ontologies to enhance ***the* *expressive* *power* *of* ....pdf

enhance*the* *expressive* *power* *of* queries_专业资料。...General Terms Standardization, *Languages* Keywords ... D SOFTWARE D.0 D.1 GENERAL *PROGRAMMING* ...**
***On* *expressive* and model checking *power* *of* propositional ....pdf

*On* *expressive* and model checking *power* *of* propositional *program* logics_专业资料。Abstract. We examine when a model checker for a propositional *program* logic ... 更多相关标签：

BRICS Basic Research in Computer Science

B. Jones Revised March 1991 Abstract Felleisen, M.,

3 p. 17 Complexity and

Electronic Notes in Theoretical Computer Science www.elsevier.com/locate/entcs

and author profiles for this publication at: http://www.researchgate.net/publication/221001265

For example, all general-purpose

and author profiles for this publication at: http://www.researchgate.net/publication/221001265

References Fell91] Matthias Felleisen, \

influence

enhance