The Essence of Compiling with Continuations

Cormac Flanagan^{∗}  Amr Sabry^{∗}  Bruce F. Duba  Matthias Felleisen^{∗}

Department of Computer Science

Rice University Houston, TX 77251-1892

Abstract

In order to simplify the compilation process, many compilers for higher-order languages use the continuationpassing style (CPS) transformation in a first phase to generate an intermediate representation of the source program. The salient aspect of this intermediate form is that all procedures take an argument that represents the rest of the computation (the “continuation”). Since the naïve CPS transformation considerably increases the size of programs, CPS compilers perform reductions to produce a more compact intermediate representation. Although often implemented as a part of the CPS transformation, this step is conceptually a second phase. Finally, code generators for typical CPS compilers treat continuations specially in order to optimize the interpretation of continuation parameters.

A thorough analysis of the abstract machine for CPS terms shows that the actions of the code generator invert the naïve CPS translation step. Put differently, the combined effect of the three phases is equivalent to a source-to-source transformation that simulates the compaction phase. Thus, fully developed CPS compilers do not need to employ the CPS transformation but can achieve the same results with a simple source-level transformation.

1 Compiling with Continuations

A number of prominent compilers for applicative higherorder programming languages use the language of continuation-passing style (CPS) terms as their intermediate representation for programs [2, 14, 18, 19]. This strategy apparently offers two major advantages. First, Plotkin [16] showed that the λ-value calculus based on the β-value rule is an operational semantics for the source language, that the conventional full λ-calculus is a semantics for the intermediate language, and, most importantly, that the λ-calculus proves more equations between CPS terms than the λ_{v}-calculus does between corresponding terms of the source language. Translated into practice, a compiler can perform more transformations on the intermediate language than on the source language [2:4–5]. Second, the language of CPS terms is basically a stylized assembly language, for which it is easy to generate actual assembly programs for different machines [2, 13, 20]. In short, the CPS transformation provides an organizational principle that simplifies the construction of compilers.

To gain a better understanding of the role that the CPS transformation plays in the compilation process, we recently studied the precise connection between the λ_{v}-calculus for source terms and the λ-calculus for CPS terms. The result of this research [17] was an extended λ_{v}-calculus that precisely corresponds to the λ-calcu-lus of the intermediate CPS language and that is still semantically sound for the source language. The extended calculus includes a set of reductions, called the A-reductions, that simplify source terms in the same manner as realistic CPS transformations simplify the output of the naïve transformation. The effect of these reductions is to name all intermediate results and to merge code blocks across declarations and conditionals. Direct compilers typically perform these reductions on an ad hoc and incomplete basis.^{1}

The goal of the present paper is to show that the true purpose of using CPS terms as an intermediate representation is also achieved by using A-normal forms. We base our argument on a formal development of the abstract machine for the intermediate code of a CPS-based compiler. The development shows that this machine is identical to a machine for A-normal forms. Thus, the back end of an A-normal form compiler can employ the same code generation techniques that a CPS compiler uses. In short, A-normalization provides an organiza-

∗Supported in part by NSF grants CCR 89-17022 and CCR 91-22518 and Texas ATP grant 91-003604014.

To appear in:

1993 Conference on Programming Language Design and Implementation.

June 21–25, 1993 Albuquerque, New Mexico

1Personal communication: H. Boehm (also [4]), K. Dybvig, R. Hieb (April 92).

\begin{aligned}M & ::= & V \\ & & | (let (x M_{1}) M_{2}) \\ & & | (if0 M_{1} M_{2} M_{3}) \\ & & | (M M_{1} … M_{n}) \\ & & | (O M_{1} … M_{n}) \\ V & ::= & c | x | (λx_{1} … x_{n}.M) \end{aligned}

V ∈ Values
c ∈ Constants
x ∈ Variables
O ∈ Primitive Operations

Figure 1: Abstract Syntax of Core Scheme (CS)

tional principle for the construction of compilers that combines various stages of fully developed CPS compilers in one straightforward transformation.

The next section reviews the syntax and semantics of a typical higher-order applicative language. The following section analyses CPS compilers for this language. Section 4 introduces the A-reductions and describes Anormal form compilers. Section 5 proves the equivalence between A-normal form compilers and realistic CPS compilers. The benefits of using A-normal form terms as an intermediate representation for compilers is the topic of Section 6. The appendix includes a linear A-normalization algorithm.

2 Core Scheme

The source language is a simple higher-order applicative language. For our purposes, it suffices to consider the language of abstract syntax trees that is produced by the lexical and syntactic analysis module of the compiler: see Figure 1 for the context-free grammar of this language. The terms of the language are either values or non-values. Values include constants, variables, and procedures. Non-values include let-expressions (blocks), conditionals, function applications and primitive operations.^{2} The sets of constants and primitive procedures are intentionally unspecified. For our purposes, it is irrelevant whether the language is statically typed like ML or dynamically typed like Scheme.

The language Core Scheme has the following contextsensitive properties, which are assumed to be checked by the front-end of the compiler. In the procedure (λx_{1} … x_{n}.M) the parameters x_{1}, …, x_{n} are mutually distinct and bound in the body M. Similarly, the expression (let (x M_{1}) M_{2}) binds x in M_{2}. A variable that is not bound by a λ or a let is free; the set of free variables in a term M is F V (M). Like Barendregt [3:ch 2,3], we identify terms modulo bound variables and we assume that free and bound variables of distinct terms do not interfere in definitions or theorems.

The semantics of the language is a partial function from programs to answers. A program is a term with no free variables and an answer is a member of the syntactic category of constants. Following conventional tradition [1], we specify the operational semantics of Core Scheme with an abstract machine. The machine we use, the CEK machine [10], has three components: a control string C, an environment E that includes bindings for all free variables in C, and a continuation K that represents the “rest of the computation”.

The CEK machine changes state according to the transition function in Figure 2. For example, the state transition for the block (let (x M_{1}) M_{2}) starts the evaluation of M_{1} in the current environment E and modifies the continuation register to encode the rest of the computation ⟨lt x, M_{2}, E, K⟩. When the new continuation receives a value, it extends the environment with a value for x and proceeds with the evaluation of M_{2}. The remaining clauses have similarly intuitive explanations.

The relation ⟼^{∗} is the reflexive transitive closure of the transition function. The function γ constructs machine values from syntactic values and environments. The notation E(x) refers to an algorithm for looking up the value of x in the environment E. The operation E[x_{1} := V_{1}^{∗}, …, x_{n} := V_{n}^{∗}] extends the environment E such that subsequent lookups of x_{i} return the value V_{i}^{∗}. The object ⟨cl x_{1} … x_{n}, M, E⟩ is a closure, a record that contains the code for M and values for the free variables of (λx_{1} … x_{n}.M). The partial function δ abstracts the semantics of the primitive operations.

The CEK machine provides a model for designing direct compilers [6, 11, 15]. A compiler based on the CEK machine implements an efficient representation for environments, e.g., displays, and for continuations, e.g., a stack.^{3} The machine code produced by such a compiler realizes the abstract operations specified by the CEK machine by manipulating these concrete representations of environments and continuations.

2The language is overly simple but contains all ingredients that are necessary to generate our result for full ML or Scheme. In particular, the introduction of assignments, and even control operators, is orthogonal to the analysis of the CPS-based compilation strategy.

3The machine also characterizes compilers for first-order languages, e.g., Fortran. In this case, the creation and deletion of the environment and continuation components always follows a stack-like behavior. Hence the machine reduces to a traditional stack machine.

Semantics: Let M ∈ CS,

eval_{d}(M) = c if ⟨M, ∅, stop⟩ ⟼^{∗} ⟨stop, c⟩.

Data Specifications:

S ∈ State_{d} =  CS × Env_{d} × Cont_{d} | Cont_{d} × Value_{d}  (machine states)
E ∈ Env_{d} =  Variables ⟶ ∘ Value_{d}  (environments)
V^{∗} ∈ Value_{d} =  c | ⟨cl x_{1} … x_{n}, M, E⟩  (machine values)
K ∈ Cont_{d} =  stop | ⟨ap ⟨…, V^{∗}, •, M, …⟩, E, K⟩ | ⟨lt x, M, E, K⟩ (continuations)
| ⟨if M_{1}, M_{2}, E, K⟩ | ⟨pr O, ⟨…, V^{∗}, •, M, …⟩, E, K⟩

Transition Rules:

⟨V, E, K⟩ ⟼ ⟨K, γ(V, E)⟩
⟨(let (x M_{1}) M_{2}), E, K⟩ ⟼ ⟨M_{1}, E, ⟨lt x, M_{2}, E, K⟩⟩
⟨(if0 M_{1} M_{2} M_{3}), E, K⟩ ⟼ ⟨M_{1}, E, ⟨if M_{2}, M_{3}, E, K⟩⟩
⟨(M M_{1} … M_{n}), E, K⟩ ⟼ ⟨M, E, ⟨ap ⟨•, M_{1}, …, M_{n}⟩, E, K⟩⟩
⟨(O M_{1} M_{2} … M_{n}), E, K⟩ ⟼ ⟨M_{1}, E, ⟨pr O, ⟨•, M_{2}, …, M_{n}⟩, E, K⟩⟩
⟨⟨lt x, M, E, K⟩, V^{∗}⟩ ⟼ ⟨M, E[x := V^{∗}], K⟩
⟨⟨if M_{1}, M_{2}, E, K⟩, 0⟩ ⟼ ⟨M_{1}, E, K⟩
⟨⟨if M_{1}, M_{2}, E, K⟩, V^{∗}⟩ ⟼ ⟨M_{2}, E, K⟩ where V^{∗} ≠ 0
⟨⟨ap ⟨…, V_{i}^{∗}, •, M, …⟩, E, K⟩, V_{i+1}^{∗}⟩ ⟼ ⟨M, E, ⟨ap ⟨…, V_{i}^{∗}, V_{i+1}^{∗}, •, …⟩, E, K⟩⟩
⟨⟨ap V^{∗}, V_{1}^{∗}, …, •⟩, E, K⟩, V_{n}^{∗}⟩ ⟼ ⟨M′, E′[x_{1} := V_{1}^{∗}, …, x_{n} := V_{n}^{∗}], K⟩  if V^{∗} = ⟨cl x_{1} … x_{n}, M′, E′⟩
⟨⟨pr O, ⟨…, V_{i}^{∗}, •, M, …⟩, E, K⟩, V_{i+1}^{∗}⟩ ⟼ ⟨M, E, ⟨pr O, ⟨…, V_{i}^{∗}, V_{i+1}^{∗}, •, …⟩, E, K⟩⟩
⟨⟨pr O, ⟨V_{1}^{∗}, …, •⟩, E, K⟩, V_{n}^{∗}⟩ ⟼ ⟨K, δ(O, V_{1}^{∗}, …, V_{n}^{∗})⟩  if δ(O, V_{1}^{∗}, …, V_{n}^{∗}) is defined

Converting syntactic values to machine values:

γ(c, E) = c
γ(x, E) = E(x)
γ((λx_{1} … x_{n}.M), E) = ⟨cl x_{1} … x_{n}, M, E⟩

Figure 2: The CEK-machine

3 CPS Compilers

Several compilers map source terms to a CPS intermediate representation before generating machine code. The function F [12] in Figure 3 is the basis of CPS transformations used in various compilers [2, 14, 19]. It uses special λ-expressions or continuations to encode the rest of the computation, thus shifting the burden of maintaining control information from the abstract machine to the code. The notation (\overline{λ}x. · · ·) marks the administrative λ-expressions introduced by the CPS transformation. The primitive operation O′ used in the CPS language is equivalent to the operation O for the source language, except that O′ takes an extra continuation argument, which receives the result once it is computed.

The transformation F introduces a large number of administrative λ-expressions. For example, F maps the code segment

N =^{df} (+ (+ 2 2) (let (x 1) (f x)))

into the CPS term

((\overline{λ}k_{2}. ((\overline{λ}k_{3}. (k_{3} 2))
(\overline{λ}t_{1}. ((\overline{λ}k_{4}. (k_{4} 2))
(\overline{λ}t_{2}. (+′ k_{2} t_{1} t_{2}))))))
(\overline{λ}t_{3}. ((\overline{λ}k_{5}.
((\overline{λ}k_{6}. (k_{6} 1))
(\overline{λ}t_{4}. (let (x t_{4})
((\overline{λ}k_{7}. ((\overline{λ}k_{8}. (k_{8} f ))
(\overline{λ}t_{5}. ((\overline{λ}k_{9}. (k_{9} x))
(\overline{λ}t_{6}. (t_{5} k_{7} t_{6}))))))
k_{5})))))
(\overline{λ}t_{7}. (+′ k t_{3} t_{7}))))))

By convention, we ignore the context (λk.[ ]) enclosing all CPS programs.

To decrease the number of administrative λabstractions, realistic CPS compilers include a simplification phase for compacting CPS terms [2:68–69, 14:5– 6, 19:49–51]. For an analysis of this simplification phase, its optimality, and how it can be combined with F, we refer the reader to Danvy and Filinski [9] and Sabry and Felleisen [17]. This phase simplifies administrative

F[[V]] = \overline{λ}k.(k Φ[[V]])
F[[(let (x M_{1}) M_{2})]] = \overline{λ}k.(F[[M_{1}]] \overline{λ}t.(let (x t) (F[[M_{2}]] k)))
F[[(if0 M_{1} M_{2} M_{3})]] = \overline{λ}k.(F[[M_{1}]] \overline{λ}t.(if0 t (F[[M_{2}]] k) (F[[M_{3}]] k)))
F[[(M M_{1} ⋯ M_{n})]] = \overline{λ}k.(F[[M]] \overline{λ}t.(F[[M_{1}]] \overline{λ}t_{1}. · · · (F[[M_{n}]] \overline{λ}t_{n}.(t k t_{1} … t_{n}))))
F[[(O M_{1} ⋯ M_{n})]] = \overline{λ}k.(F[[M_{1}]] \overline{λ}t_{1}. · · · (F[[M_{n}]] \overline{λ}t_{n}.(O′ k t_{1} … t_{n})))
Φ[[c]] = c
Φ[[x]] = x
Φ[[λx_{1} ⋯ x_{n}.M]] = λkx_{1} ⋯ x_{n}.F[[M]]

Figure 3: The CPS transformation F

redexes of the form ((\overline{λ}x.P) Q) according to the rule:

((\overline{λ}x.P) Q) ⟶ P [x := Q]  (\overline{β})

The term P [x := Q] is the result of the capture-free substitution of all free occurrences of x in P by Q; for example, (λx.xz)[z := (λy.x)] = (λu.u(λy.x)). Applying the reduction \overline{β} to all the administrative redexes in our previous example produces the following \overline{β}-normal form term:

cps(N ) = (+′ (\overline{λ}t_{1}. (let (x 1) (f (\overline{λ}t_{2}. (+′ k t_{1} t_{2})) x)))

2 2)

The reduction \overline{β} is strongly-normalizing on the language of CPS terms [17]. Hence, the simplification phase of a CPS compiler can remove all \overline{β}-redexes from the output of the translation F.^{4} After the simplification phase, we no longer need to distinguish between regular and administrative λ-expressions, and use the notation (λ. · · ·) for both classes of λ-expression. With this convention, the language of \overline{β}-normal forms, CPS(CS), is the following [17]:

P ::= (k W)  (return)
| (let (x W) P)  (bind)
| (if0 W P_{1} P_{2})  (branch)
| (W k W_{1} … W_{n})  (tail call)
| (W (λx.P) W_{1} … W_{n})  (call)
| (O′ k W_{1} … W_{n})  (prim-op)
| (O′ (λx.P) W_{1} … W_{n})  (prim-op)
W ::= c | x | (λkx_{1} … x_{n}.P)  (values)

Indeed, this language is typical of the intermediate representation used by CPS compilers [2, 14, 19].

Naïve CPS Compilers The abstract machine that characterizes the code generator of a naïve CPS compiler is the C_{cps}E machine. Since terms in CPS(CS) contain an encoding of control-flow information, the machine does not require a continuation component (K) to record the rest of the computation. Evaluation proceeds according to the state transition function in Figure 4. For example, the state transition for the tail call (W k W_{1} … W_{n}) computes a closure ⟨cl k′x_{1} … x_{n}, P′, E′⟩ corresponding to W, extends E′ with the values of k, W_{1}, …, W_{n} and starts the interpretation of P′.

Realistic CPS Compilers Although the C_{cps}E machine describes what a naïve CPS compiler would do, typical compilers deviate from this model in two regards.

First, the naïve abstract machine for CPS code represents the continuation as an ordinary closure. Yet, realistic CPS compilers “mark” the continuation closure as a special closure. For example, Shivers partitions procedures and continuations in order to improve the data flow analysis of CPS programs [18:sec 3.8.3]. Also, in both Orbit [14] and Rabbit [19], the allocation strategy of a closure changes if the closure is a continuation. Similarly, Appel [2:114–124] describes various techniques for closure allocation that treat the continuation closure in a special way.

In order to reflect these changes in the machine, we tag continuation closures with a special marker “ar” that describes them as activation records.

Second, the CPS representation of any user-defined procedure receives a continuation argument. However, Steele [19] modifies the CPS transformation with a “continuation variable hack” [19:94] that recognizes instances of CPS terms like ((λk_{1} · · · .P) k_{2} …) and transforms them to ((λ · · · .P [k_{1} := k_{2}]) …). This “optimization” eliminates “some of the register shuffling” [19:94] during the evaluation of the term. Appel [2] achieves the same effect without modifying the CPS transformation by letting the variables k_{1} and k_{2} share the same

4The CPS translation of a conditional expression contains two references to the continuation variable k. Thus, the \overline{β}- normalization phase can produce exponentially larger output.

Modifying the CPS algorithm to avoid duplicating k removes the potential for exponential growth. The rest of our technical development can be adapted mutatis mutandis.

Semantics: Let P ∈ CPS(CS),

eval_{n}(P) = c if ⟨P, ∅[k := ⟨cl x, (k x), ∅[k := stop]⟩]⟩ ⟼^{∗} ⟨(k x), ∅[x := c, k := stop]⟩.

Data Specifications:

S_{n} ∈ State_{n} = CPS(CS) × Env_{n}  (machine states)
E ∈ Env_{n} = Variables ⟶ ∘ Value_{n}  (environments)
W^{∗} ∈ Value_{n} = c | ⟨cl kx_{1} … x_{n}, P, E⟩ | ⟨cl x, P, E⟩ | stop (machine values)

Transition Rules:

⟨(k W), E⟩ ⟼ ⟨P′, E′[x := μ(W, E)]⟩ where E(k) = ⟨cl x, P′, E′⟩
⟨(let (x W) P), E⟩ ⟼ ⟨P, E[x := μ(W, E)]⟩
⟨(if0 W P_{1} P_{2}), E⟩ ⟼ ⟨P_{1}, E⟩ where μ(W, E) = 0
or ⟨P_{2}, E⟩ where μ(W, E) ≠ 0
⟨(W k W_{1} … W_{n}), E⟩ ⟼ ⟨P′, E′[k′ := E(k), x_{1} := W_{1}^{∗}, …, x_{n} := W_{n}^{∗}]⟩
where μ(W, E) = ⟨cl k′x_{1} … x_{n}, P′, E′⟩ and for 1 ≤ i ≤ n, W_{i}^{∗} = μ(W_{i}, E)
⟨(W (λx.P) W_{1} … W_{n}), E⟩ ⟼ ⟨P′, E′[k′ := ⟨cl x, P, E⟩, x_{1} := W_{1}^{∗}, …, x_{n} := W_{n}^{∗}]⟩
where μ(W, E) = ⟨cl k′x_{1} … x_{n}, P′, E′⟩ and for 1 ≤ i ≤ n, W_{i}^{∗} = μ(W_{i}, E)
⟨(O′ k W_{1} … W_{n}), E⟩ ⟼ ⟨P′, E′[x := δ_{c}(O′, W_{1}^{∗}, …, W_{n}^{∗})]⟩  if δ_{c}(O′, W_{1}^{∗}, …, W_{n}^{∗}) is defined,
where E(k) = ⟨cl x, P′, E′⟩ and for 1 ≤ i ≤ n, W_{i}^{∗} = μ(W_{i}, E)
⟨(O′ (λx.P) W_{1} … W_{n}), E⟩ ⟼ ⟨P, E[x := δ_{c}(O′, W_{1}^{∗}, …, W_{n}^{∗})]⟩  if δ_{c}(O′, W_{1}^{∗}, …, W_{n}^{∗}) is defined,
and for 1 ≤ i ≤ n, W_{i}^{∗} = μ(W_{i}, E)

Converting syntactic values to machine values:

μ(c, E) = c
μ(x, E) = E(x)
μ((λkx_{1} … x_{n}.P), E) = ⟨cl kx_{1} … x_{n}, P, E⟩

Figure 4: The naïve CPS abstract machine: the C_{cps}E machine.

register during the procedure call.

In terms of the CPS abstract machine, the optimization corresponds to a modification of the operation E′[k′ := E(k), x_{1} := W_{1}^{∗}, …, x_{n} := W_{n}^{∗}] to E′[x_{1} := W_{1}^{∗}, …, x_{n} := W_{n}^{∗}] such that E and E′ share the binding of k. In order to make the sharing explicit, we split the environment into two components: a component E^{k} that includes the binding for the continuation, and a component E^{−} that includes the rest of the bindings, and treat each component independently. This optimization relies on the fact that every control string has exactly one free continuation variable, which implies that the corresponding value can be held in a special register.^{5}

Performing these modifications on the naïve abstract machine produces the realistic CPS abstract machine in Figure 5. The new C_{cps}EK machine extracts the information regarding the continuation from the CPS terms and manages the continuation in an optimized way. For example, the state transition for the tail call (W k W_{1} … W_{n}) evaluates W to a closure ⟨cl kx_{1} … x_{n}, P′, E_{1}^{−}⟩, extends E_{1}^{−} with the values of W_{1}, …, W_{n} and starts the execution of P′. In particular, there is no need to extend E_{1}^{−} with the value of k as this value remains in the environment component E^{k}.

4 A-Normal Form Compilers

A close inspection of the C_{cps}EK machine reveals that the control strings often contain redundant information considering the way instructions are executed. First, a return instruction, i.e., the transition ⟼ _{c}^{(1)}, dispatches on the term (k W), which informs the machine that the “return address” is denoted by the value of the variable k. The machine ignores this information since a return instruction automatically uses the value of register E^{k} as the “return address”. Second, the call instructions, i.e., transitions ⟼ _{c}^{(4)} and ⟼ _{c}^{(5)}, invoke closures that expect, among other arguments, a continuation k. Again, the machine ignores the continuation parameter in the closures and manipulate the “global” register E^{k} instead.

5This fact also holds in the presence of control operators as there is always one identifiable current continuation.

eval_{c}(P) = c if ⟨P, ∅, ⟨ar x, (k x), ∅, stop⟩⟩ ⟼_{c}^{∗} ⟨(k x), ∅[x := c], stop⟩.

Data Specifications:

S_{c} ∈ State_{c} = CPS(CS) × Env_{c} × Cont_{c} (machine states)
E^{−} ∈ Env_{c} = Variables ⟶ ∘ Value_{c}  (environments)
W^{∗} ∈ Value_{c} = c | ⟨cl kx_{1} … x_{n}, P, E^{−}⟩ (machine values)
E^{k} ∈ Cont_{c} = stop | ⟨ar x, P, E^{−}, E^{k}⟩  (continuations)

Transition Rules:

⟨(k W), E^{−}, E^{k}⟩ ⟼ _{c}^{(1)} ⟨P′, E_{1}^{−}[x := μ(W, E^{−})], E_{1}^{k}⟩  where E^{k} = ⟨ar x, P′, E_{1}^{−}, E_{1}^{k}⟩
⟨(let (x W) P), E^{−}, E^{k}⟩ ⟼ _{c}^{(2)} ⟨P, E^{−}[x := μ(W, E^{−})], E^{k}⟩
⟨(if0 W P_{1} P_{2}), E^{−}, E^{k}⟩ ⟼ _{c}^{(3)} ⟨P_{1}, E^{−}, E^{k}⟩ where μ(W, E^{−}) = 0
or ⟨P_{2}, E^{−}, E^{k}⟩ where μ(W, E^{−}) ≠ 0
⟨(W k W_{1} … W_{n}), E^{−}, E^{k}⟩ ⟼ _{c}^{(4)} ⟨P′, E_{1}^{−}[x_{1} := W_{1}^{∗}, …, x_{n} := W_{n}^{∗}], E^{k}⟩
where μ(W, E^{−}) = ⟨cl k′x_{1} … x_{n}, P′, E_{1}^{−}⟩ and for 1 ≤ i ≤ n, W_{i}^{∗} = μ(W_{i}, E^{−})
⟨(W (λx.P) W_{1} … W_{n}), E^{−}, E^{k}⟩ ⟼ _{c}^{(5)} ⟨P′, E_{1}^{−}[x_{1} := W_{1}^{∗}, …, x_{n} := W_{n}^{∗}], ⟨ar x, P, E^{−}, E^{k}⟩⟩
where μ(W, E^{−}) = ⟨cl k′x_{1} … x_{n}, P′, E_{1}^{−}⟩ and for 1 ≤ i ≤ n, W_{i}^{∗} = μ(W_{i}, E^{−})
⟨(O′ k W_{1} … W_{n}), E^{−}, E^{k}⟩ ⟼ _{c}^{(6)} ⟨P′, E_{1}^{−}[x := δ_{c}(O′, W_{1}^{∗}, …, W_{n}^{∗})], E_{1}^{k}⟩  if δ_{c}(O′, W_{1}^{∗}, …, W_{n}^{∗}) is defined,
where E^{k} = ⟨ar x, P′, E_{1}^{−}, E_{1}^{k}⟩ and for 1 ≤ i ≤ n, W_{i}^{∗} = μ(W_{i}, E^{−})
⟨(O′ (λx.P) W_{1} … W_{n}), E^{−}, E^{k}⟩ ⟼ _{c}^{(7)} ⟨P, E^{−}[x := δ_{c}(O′, W_{1}^{∗}, …, W_{n}^{∗})], E^{k}⟩  if δ_{c}(O′, W_{1}^{∗}, …, W_{n}^{∗}) is defined,
and for 1 ≤ i ≤ n, W_{i}^{∗} = μ(W_{i}, E^{−})

Figure 5: The realistic CPS abstract machine: the C_{cps}EK machine.

Undoing CPS The crucial insight is that the elimination of the redundant information from the C_{cps}EK machine corresponds to an inverse CPS transformation [7, 17] on the intermediate code. The function U in Figure 6 realizes such an inverse [17]. The inverse transformation formalizes our intuition about the redundancies in the C_{cps}EK machine. It eliminates the variable k from return instructions as well as the parameter k from procedures. The latter change implies that continuations are not passed as arguments in function calls but rather become contexts surrounding the calls. For example, the code segment cps(N) in Section 3 becomes:

A(N ) = (let (t_{1} (+ 2 2))

(let (x 1)

(let (t_{2} (f x))

(+ t_{1} t_{2}))))

Based on the above argument, it appears that CPS compilers perform a sequence of three steps:

[figure: A; CPS(CS ); CPS; \overline{β}-normalization; un-CPS; CS; •; •; •; •; A(CS )]

The diagram naturally suggests a direct translation A that combines the effects of the three phases. The identification of the translation A requires a theorem relating \overline{β}-reductions on CPS terms to reductions on the source language. This correspondence of reductions was the subject of our previous paper [17]. The resulting set of source reductions, the A-reductions, is in Figure 7.^{6} Since the A-reductions are strongly normalizing, we can characterize the translation A as any function that applies the A-reductions to a source term until it reaches a normal form [17:Theorem 6.4].

The definition of the A-reductions refers to the concept of evaluation contexts. An evaluation context is a term with a “hole” (denoted by [ ]) in the place of one subterm. The location of the hole points to the next

6Danvy [8] and Weise [21] also recognize that the compaction of CPS terms can be expressed in the source language, but do not explore this topic systematically.

The inverse CPS transformation:

U : CPS(CS) → A(CS)
U[[(k W)]] = Ψ[[W]]
U[[(let (x W) P)]] = (let (x Ψ[[W]]) U[[P]])
U[[(if0 W P_{1} P_{2})]] = (if0 Ψ[[W]] U[[P_{1}]] U[[P_{2}]])
U[[(W k W_{1} … W_{n})]] = (Ψ[[W]] Ψ[[W_{1}]] … Ψ[[W_{n}]])
U[[(W (λx.P) W_{1} … W_{n})]] = (let (x (Ψ[[W]] Ψ[[W_{1}]] … Ψ[[W_{n}]])) U[[P]])
U[[(O′ k W_{1} … W_{n})]] = (O Ψ[[W_{1}]] … Ψ[[W_{n}]])
U[[(O′ (λx.P) W_{1} … W_{n})]] = (let (x (O Ψ[[W_{1}]] … Ψ[[W_{n}]])) U[[P]])
Ψ : W → V
Ψ[[c]] = c
Ψ[[x]] = x
Ψ[[λkx_{1} … x_{n}.P]] = λx_{1} … x_{n}.U[[M]]

The language A(CS) :

M ::= V  (return)
| (let (x V) M)  (bind)
| (if0 V M M)  (branch)
| (V V_{1} … V_{n})  (tail call)
| (let (x (V V_{1} … V_{n})) M)  (call)
| (O V_{1} … V_{n})  (prim-op)
| (let (x (O V_{1} … V_{n})) M)  (prim-op)
V ::= c | x | (λx_{1} … x_{n}.M)  (values)

Figure 6: The inverse CPS transformation and its output

Evaluation Contexts:

E ::= [ ] | (let (x E) M) | (if0 E M M) | (F V ⋯ V E M ⋯ M)  where F = V or F = O

The A-reductions:

E[(let (x M) N)] ⟶ (let (x M) E[N]) where E ≠ [ ], x ∉ F V (E)  (A_{1})
E[(if0 V M_{1} M_{2})] ⟶ (if0 V E[M_{1}] E[M_{2}]) where E ≠ [ ]  (A_{2})
E[(F V_{1} … V_{n})] ⟶ (let (t (F V_{1} … V_{n})) E[t])  (A_{3})

where F = V or F = O, E ≠ E′[(let (z [ ]) M)], E ≠ [ ], t ∉ F V (E)

Figure 7: Evaluation contexts and the set of A-reductions

subexpression to be evaluated according to the CEK semantics. For example, in an expression (let (x M_{1}) M_{2}), the next reducible expression must occur within M_{1}, hence the definition of evaluation contexts includes the clause (let (x E) M).

The A-reductions transform programs in a natural and intuitive manner. The first two reductions merge code segments across declarations and conditionals. The last reduction lifts redexes out of evaluation contexts and names intermediate results. Using evaluation contexts and the A-reductions, we can

Semantics: Let M ∈ A(CS),

eval_{a}(M) = c if ⟨M, ∅, ⟨ar x, x, ∅, stop⟩⟩ ⟼_{a}^{∗} ⟨x, ∅[x := c], stop⟩.

Data Specifications:

S_{a} ∈ State_{a} = A(CS) × Env_{a} × Cont_{a} (machine states)
E ∈ Env_{a} = Variables ⟶ ∘ Value_{a}  (environments)
V^{∗} ∈ Value_{a} = c | ⟨cl x_{1} … x_{n}, M, E⟩ (machine values)
K ∈ Cont_{a} = stop | ⟨ar x, M, E, K⟩  (continuations)

Transition Rules:

⟨V, E, K⟩ ⟼ _{a}^{(1)} ⟨M′, E′[x := γ(V, E)], K′⟩  where K = ⟨ar x, M′, E′, K′⟩
⟨(let (x V) M), E, K⟩ ⟼ _{a}^{(2)} ⟨M, E[x := γ(V, E)], K⟩
⟨(if0 V M_{1} M_{2}), E, K⟩ ⟼ _{a}^{(3)} ⟨M_{1}, E, K⟩ where γ(V, E) = 0
or ⟨M_{2}, E, K⟩ where γ(V, E) ≠ 0
⟨(V V_{1} … V_{n}), E, K⟩ ⟼ _{a}^{(4)} ⟨M′, E′[x_{1} := V_{1}^{∗}, …, x_{n} := V_{n}^{∗}], K⟩

where γ(V, E) = ⟨cl x_{1} … x_{n}, M′, E′⟩ and for 1 ≤ i ≤ n, V_{i}^{∗} = γ(V_{i}, E)

⟨(let (x (V V_{1} … V_{n})) M), E, K⟩ ⟼ _{a}^{(5)} ⟨M′, E′[x_{1} := V_{1}^{∗}, …, x_{n} := V_{n}^{∗}], ⟨ar x, M, E, K⟩⟩

where γ(V, E) = ⟨cl x_{1} … x_{n}, M′, E′⟩ and for 1 ≤ i ≤ n, V_{i}^{∗} = γ(V_{i}, E)

⟨(O V_{1} … V_{n}), E, K⟩ ⟼ _{a}^{(6)} ⟨M′, E′[x := δ(O, V_{1}^{∗}, …, V_{n}^{∗})], K′⟩  if δ(O, V_{1}^{∗}, …, V_{n}^{∗}) is defined,

where K = ⟨ar x, M′, E′, K′⟩ and for 1 ≤ i ≤ n, V_{i}^{∗} = γ(V_{i}, E)

⟨(let (x (O V_{1} … V_{n})) M), E, K⟩ ⟼ _{a}^{(7)} ⟨M, E[x := δ(O, V_{1}^{∗}, …, V_{n}^{∗})], K⟩  if δ(O, V_{1}^{∗}, …, V_{n}^{∗}) is defined,

and for 1 ≤ i ≤ n, V_{i}^{∗} = γ(V_{i}, E)

Figure 8: The C_{a}EK machine

rewrite our sample code segment N in Section 3 as follows. For clarity, we surround the reducible term with a box:

N = (+ (+ 2 2) (let (x 1) (f x)))

⟶ (let (t_{1} (+ 2 2))

(+ t_{1} (let (x 1) (f x))) )

(A_{3})

⟶ (let (t_{1} (+ 2 2))

(let (x 1)

(+ t_{1} (f x)) ))

(A_{1})

⟶ (let (t_{1} (+ 2 2))

(let (x 1)

(let (t_{2} (f x)) (+ t_{1} t_{2}))))

(A_{3})

The appendix includes a linear algorithm that maps Core Scheme terms to their normal form with respect to the A-reductions.

Compilers In order to establish that the Areductions generate the actual intermediate code of CPS compilers, we design an abstract machine for the language of A-normal forms, the C_{a}EK machine, and prove that this machine is “equivalent” to the CPS machine in Figure 5.

The C_{a}EK machine is a CEK machine specialized to the subset of Core Scheme in A-normal form (Figure 6). The machine (see Figure 8) has only two kinds of continuations: the continuation stop, and continuations of the form ⟨ar x, M, E, K⟩. Unlike the CEK machine, the C_{a}EK machine only needs to build a continuation for the evaluation of a non-tail function call. For example, the transition rule for the tail call (V V_{1} … V_{n}) evaluates V to a closure ⟨cl x_{1} … x_{n}, M′, E′⟩, extends the environment E′ with the values of V_{1}, …, V_{n} and continues with the execution of M′. The continuation component remains in the register K. By comparison, the CEK machine would build a seperate continuation for the evaluation of each sub-expression V, V_{1}, …, V_{n}.

5 Equivalence of Compilation Strategies

A comparison of Figures 5 and 8 suggests a close relationship between the C_{cps}EK machine and the C_{a}EK machine. In fact, the two machines are identical modulo the syntax of the control strings, as corresponding state transitions on the two machines perform the same abstract operations. Currently, the transition rules for these machines are defined using pattern matching on the syntax of terms. Once we reformulate these rules using predicates and selectors for abstract syntax, we can see the correspondence more clearly.

For example, we can abstract the transition rules ⟼ _{a}^{(5)} and ⟼ _{c}^{(5)} from the term syntax as the higher-order functional T_{5}:

T_{5}[call-var, call-body, call?, call-args, call-fn] =

⟨C, E, K⟩ ⟼ ⋯  if call?(C)

where

x = call-var(C)
M = call-body(C)
V = call-fn(C)
V_{1}, …, V_{n} = call-args(C)

The arguments to T_{5} are abstract-syntax functions for manipulating terms in a syntax-independent manner. Applying T_{5} to the appropriate functions produces either the transition rule ⟼ _{a}^{(5)} of the C_{a}EK machine or the rule ⟼ _{c}^{(5)} of the C_{cps}EK machine, i.e.,

⟼ _{a}^{(5)} = T_{5}[A-call-var, …, A-call-fn]
⟼ _{c}^{(5)} = T_{5}[cps-call-var, …, cps-call-fn]

Suitable definitions of the syntax-functions for the language A(CS) are:

A-call-var[[(let (x (V V_{1} … V_{n})) M)]] = x
A-call-body[[(let (x (V V_{1} … V_{n})) M)]] = M
…
A-call-fn[[(let (x (V V_{1} … V_{n})) M)]] = V

Definitions for the language CPS(CS) follow a similar pattern:

cps-call-var[[(W (λx.P) W_{1} … W_{n})]] = x
cps-call-body[[(W (λx.P) W_{1} … W_{n})]] = P
…
cps-call-fn[[(W (λx.P) W_{1} … W_{n})]] = W

In the same manner, we can abstract each pair of transition rules ⟼ _{a}^{(n)} and ⟼ _{c}^{(n)} as a higher-order functional T_{n}.

Let S_{a} and S_{c} be abstract-syntax functions appropriate for A-normal forms and CPS terms, respectively. Then the following theorem characterizes the relationship between the two transition functions.

Theorem 5.1 (Machine Equivalence) For 1 ≤ n ≤ 7, ⟼ _{a}^{(n)} = T_{n}[S_{a}] and ⟼ _{c}^{(n)} = T_{n}[S_{c}].

The theorem states that the transition functions of the C_{a}EK and C_{cps}EK machines are identical modulo syntax. However, in order to show that the evaluation of an A-normal form term M and its CPS counterpart on the respective machines produces exactly the same behavior, we also need to prove that there exists a bijection M between machine states that commutes with the transition rules.

Definition 5.2. (M, R, V, and K)

M : State_{c} ⟶ State_{a}

M(⟨P, E^{−}, E^{k}⟩) = ⟨U[[P]], R(E^{−}), K(E^{k})⟩

R : Env_{c} ⟶ Env_{a}

R(E^{−}) = E where E(x) = V(E^{−}(x))

V : Value_{c} ⟶ Value_{a}

V(c) = c

V(⟨cl kx_{1} … x_{n}, P, E^{−}⟩) =

⟨cl x_{1} … x_{n}, U[[P]], R(E^{−})⟩
K : Cont_{c} ⟶ Cont_{a}

K(stop) = stop

K(⟨ar x, P, E^{−}, E^{k}⟩) =

⟨ar x, U[[P]], R(E^{−}), K(E^{k})⟩

Intuitively, the function M maps C_{cps}EK machine states to C_{a}EK machine states, and R, V and K perform a similar mapping for environments, machine values and continuations respectively. We can now formalize the previously stated requirement that O and O′ behave in the same manner.

Requirement For all W_{1}^{∗}, …, W_{n}^{∗} ∈ Value_{c},

V(δ_{c}(O′, W_{1}^{∗}, …, W_{n}^{∗})) = δ(O, V(W_{1}^{∗}), …, V(W_{n}^{∗})).

The function M commutes with the state transition functions.

Theorem 5.3 (Commutativity Theorem)

Let S ∈ State_{c}: S ⟼ _{c}^{(n)} S′ if and only if M(S) ⟼ _{a}^{(n)} M(S′).

[figure: ^{⟼ {(n) \atop c}}; ⟼ _{a}^{(n)}; M; M(S); S; S′; M(S′); M]

Proof: The inverse CPS transformations U is bijective [17]. Hence by structural induction, the functions M, R, V and K are also bijective. The proof proceeds by case analysis on the transition rules.

Intuitively, the evaluation of a CPS term P on the C_{cps}EK machine proceeds in the same fashion as the evaluation of U[[P]] on the C_{a}EK machine. Together with the machine equivalence theorem, this implies that both machines perform the same sequence of abstract operations, and hence compilers based on these abstract machines can produce identical code for the same input. The A-normal form compiler achieves its goal in fewer passes.

6 A-Normal Forms as an Intermediate Language

Our analysis suggests that the language of A-normal forms is a good intermediate representation for compilers. Indeed, most direct compilers use transformations similar to the A-reductions on an ad hoc and incomplete basis. It is therefore natural to modify such compilers to perform a complete A-normalization phase, and analyze the effects. We have conducted such an experiment with the non-optimizing, direct compiler CAML Light [15]. This compiler translates ML programs into bytecode via a λ-calculus based intermediate language, and then interprets this bytecode. By performing A-normalization on the intermediate language and rewriting the interpreter as a C_{a}EK machine, we achieved speedups of between 50% and 100% for each of a dozen small benchmarks. Naturally, we expect the speedups to be smaller when modifying an optimizing compiler.

A major advantage of using a CPS-based intermediate representation is that many optimizations can be expressed as sequences of β and η reductions. For example, CPS compilers can transform the non-tail call (W (λx.kx) W_{1} … W_{n}) to the tail-recursive call (W k W_{1} … W_{n}) using an η-reduction on the continuation [2]. An identical transformation [17] on the language of A-normal forms is the reduction β_{id}:

(let (x (V V_{1} … V_{n})) x) ⟶ (V V_{1} … V_{n}),

where V, V_{1}, …, V_{n} are the A-normal forms corresponding to W, W_{1}, …, W_{n} respectively. Every other optimization on CPS terms that corresponds to a sequence of βη-reductions is also expressible on A-normal form terms [17].

The A-reductions also expose optimization opportunities by merging code segments across block declarations and conditionals. In particular, partial evaluators rely on the A-reductions to improve their specialization phase [5]. For example, the addition operation and the constant 0 are apparently unrelated in the following term:

(add1 (let (x (f 5)) 0))

The A-normalization phase produces:

(let (x (f 5)) (add1 0)),

which specializes to (let (x (f 5)) 1).

In summary, compilation with A-normal forms characterizes the critical aspects of the CPS transformation relevant to compilation. Moreover, it formulates these aspects in a way that direct compilers can easily use. Thus, our result should lead to improvements for both traditional compilation strategies.

A Linear A-Normalization

The linear A-normalization algorithm in Figure 9 is written in Scheme extended with a special form match, which performs pattern matching on the syntax of program terms. It employs a programming technique for CPS algorithms pioneered by Danvy and Filinski [9]. To prevent possible exponential growth in code size, the algorithm avoids duplicating the evaluation context enclosing a conditional expression. We assume the frontend uniquely renames all variables, which implies that the condition x ∉ F V (E) of the reduction A_{1} holds.

Acknowledgments We thank Olivier Danvy, Preston Briggs, and Keith Cooper for comments on an early version of the paper.

References

[1] Aho, A., Sethi, R., and Ullman, J. Compilers—Principles, Techniques, and Tools. Addison-Wesley, Reading, Mass., 1985.

[2] Appel, A. Compiling with Continuations. Cambridge University Press, 1992.

[3] Barendregt, H. The Lambda Calculus: Its Syntax and Semantics, revised ed. Studies in Logic and the Foundations of Mathematics 103. North-Holland, 1984.

[4] Boehm, H.-J., and Demers, A. Implementing Russel. In Proceedings of the ACM SIG-PLAN 1986 Symposium on Compiler Construction (1986), vol. 21(7), Sigplan Notices, pp. 186–195.

[5] Bondorf, A. Improving binding times without explicit CPS-conversion. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming (1992), pp. 1–10.

[6] Clinger, W. The Scheme 311 compiler: An exercise in denotational semantics. In Proceedings of the 1984 ACM Conference on Lisp and Functional Programming (1984), pp. 356–364.

[7] Danvy, O. Back to direct style. In Proceedings of the 4th European Symposium on Programming (Rennes, 1992), Lecture Notes in Computer Science, 582, Springer Verlag, pp. 130–150.

[8] Danvy, O. Three steps for the CPS transformation. Tech. Rep. CIS-92-2, Kansas State University, 1992.

[9] Danvy, O., and Filinski, A. Representing control: A study of the CPS transformation. Mathematical Structures in Computer Science, 4 (1992), 361–391.

(define normalize-term (lambda (M ) (normalize M (lambda (x) x))))

(define normalize

(lambda (M k)

(match M [‘(lambda ,params ,body) (k ‘(lambda ,params ,(normalize-term body)))] [‘(let (,x ,M_{1}) ,M_{2}) (normalize M_{1} (lambda (N_{1}) ‘(let (,x ,N_{1}) ,(normalize M_{2} k))))] [‘(if0 ,M_{1} ,M_{2} ,M_{3}) (normalize-name M_{1} (lambda (t) (k ‘(if0 ,t ,(normalize-term M_{2}) ,(normalize-term M_{3})))))]

[‘(,Fn . ,M^{∗}) (if (PrimOp? Fn)

(normalize-name^{∗} M^{∗} (lambda (t^{∗}) (k ‘(,Fn . ,t^{∗}))))

(normalize-name Fn (lambda (t) (normalize-name^{∗} M^{∗} (lambda (t^{∗}) (k ‘(,t . ,t^{∗})))))))]

[V (k V )])))

(define normalize-name

(lambda (M k) (normalize M (lambda (N ) (if (Value? N ) (k N ) (let ([t (newvar)]) ‘(let (,t ,N ) ,(k t))))))))

(define normalize-name^{∗}

(lambda (M^{∗} k)

(if (null? M^{∗})

(k ’())

(normalize-name (car M^{∗}) (lambda (t) (normalize-name^{∗} (cdr M^{∗}) (lambda (t^{∗}) (k ‘(,t . ,t^{∗})))))))))

Figure 9: A linear-time A-normalization algorithm

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

[11] Fessenden, C., Clinger, W., Friedman, D. P., and Haynes, C. T. Scheme 311 version 4 reference manual. Computer Science Technical Report 137, Indiana University, Bloomington, Indiana, Feb. 1983.

[12] Fischer, M. Lambda calculus schemata. In Proceedings of the ACM Conference on Proving Assertions About Programs (1972), vol. 7(1), Sigplan Notices, pp. 104–109.

[13] Kelsey, R., and Hudak, P. Realistic compilation by program transformation. In Conference Record of the 16th Annual ACM Symposium on Principles of Programming Languages (Austin, TX, Jan. 1989), pp. 281–292.

[14] Kranz, D., Kelsey, R., Rees, J., Hudak, P., Philbin, J., and Adams, N. Orbit: An optimizing compiler for Scheme. In Proceedings of the ACM SIGPLAN 1986 Symposium on Compiler Construction (1986), vol. 21(7), Sigplan Notices, pp. 219–233.

[15] Leroy, X. The Zinc experiment: An economical implementation of the ML language. Tech. Rep. 117, INRIA, 1990.

[16] Plotkin, G. Call-by-name, call-by-value, and the λ-calculus. Theoretical Computer Science 1 (1975), 125–159.

[17] Sabry, A., and Felleisen, M. Reasoning about programs in continuation-passing style. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming (1992), pp. 288–298. Technical Report 92-180, Rice University.

[18] Shivers, O. Control-Flow Analysis of Higher-Order Languages or Taming Lambda. PhD thesis, Carnegie-Mellon University, 1991.

[19] Steele, G. L. RABBIT: A compiler for Scheme. MIT AI Memo 474, Massachusetts Institute of Technology, Cambridge, Mass., May 1978.

[20] Wand, M. Correctness of procedure representations in higher-order assembly language. In Proceedings of the 1991 Conference on the Mathematical Foundations of Programing Semantics (1992), S. Brookes, Ed., vol. 598 of Lecture Notes in Computer Science, Springer Verlag, pp. 294–311.

[21] Weise, D. Advanced compiling techniques. Course Notes at Stanford University, 1990.