Math. Struct. in Comp. Science (1992), vol. 2, pp. 361–391. PREPRINT

Representing control: a study of the CPS transformation

O L I V I E R D A N V Y^{1}^{†} and A N D R Z E J F I L I N S K I^{2}

1 Department of Computing and Information Sciences, Kansas State University, Manhattan, Kansas 66506, USA. (danvy@cis.ksu.edu) 2 School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213, USA. (Andrzej.Filinski@cs.cmu.edu)

Received February 1991; Revised June 1992

This paper investigates the transformation of λ_{v} -terms into continuation-passing style (CPS). We show that by appropriate η-expansion of Fischer and Plotkin’s two-pass equational specification of the CPS transform, we can obtain a static and context-free separation of the result terms into “essential” and “administrative” constructs. Interpreting the former as syntax builders and the latter as directly executable code, we obtain a simple and efficient one-pass transformation algorithm, easily extended to conditional expressions, recursive definitions, and similar constructs. This new transformation algorithm leads to a simpler proof of Plotkin’s simulation and indifference results. We go on to show how CPS-based control operators similar to, but more general than, Scheme’s call/cc can be naturally accommodated by the new transformation algorithm. To demonstrate the expressive power of these operators, we use them to present an equivalent but even more concise formulation of the efficient CPS transformation algorithm. Finally, we relate the fundamental ideas underlying this derivation to similar concepts from other works on program manipulation; we derive a one-pass CPS transformation of λ_{n}-terms; and we outline some promising areas for future research.

1. Introduction and Motivation

The usual presentation of the continuation-passing style (CPS) transformation (Plotkin, 1975) is concise and simple, but tends to yield unreasonably large residual terms containing a lot of “administrative redexes.” While these redexes turn out to be relatively harmless from a theoretical perspective, they do require a special twist (the so-called “colontranslation”) for proving certain important properties of the transformation (Plotkin, 1975; Riecke, 1989; Murthy, 1990).

In practice, eliminating the administrative redexes is absolutely essential to obtain transformed terms of a manageable size. However, such a “post-reduction” pass is often

† This work was partly supported by NSF under grant CCR-9102625.

integrated with other, independent simplifications and optimization steps, and leads to relatively complex CPS transformers (Steele, 1978).

In the following, we will consider a systematization of the two-pass CPS transformation by focusing the attention on redexes that are introduced by the transformation itself, and by explicitly not reducing what would correspond to redexes in the source λ-term. Exploiting this distinction, we show that it is possible to perform all the administrative reductions “on the fly” in a single pass, without ever constructing the unreduced terms explicitly.

The CPS transformation permits a simple definition of generalized escape constructs like Scheme’s call/cc. Such operators are often perceived to eliminate the need for explicit CPS programs. However, sometimes the greater generality of “genuine” CPS is actually needed to express an algorithm (e.g., to implement backtracking (Mellish and Hardy, 1984).) Our investigation of the CPS transform leads naturally to the introduction of two new control operators, shift and reset, which allow the additional power of general CPS to be exploited in direct style programs. As an example, we will show how these operators permit us to express the efficient CPS transformation algorithm derived in this paper even more concisely.

Prerequisites

In the following, we will assume a basic familiarity with CPS and the λ_{v}-calculus, i.e., the applicative order λ-calculus that forms the core of languages such as Scheme (Clinger and Rees, 1991) and Standard ML (Milner et al., 1990).

For convenience in referring to individual applications, we will generally express them with an explicit operator @, writing @M N instead of the traditional simple juxtaposition M N. This is a purely syntactical variation: no change or refinement of semantics is implied by the @-notation.

As in Standard ML, but in contrast to Scheme, we will also assume a strict leftto-right evaluation order, i.e., that in an application @M N, M is evaluated before N. Where this distinction matters (i.e., when both M and N are potentially nonterminating or “escaping” terms), the evaluation order of Scheme programs will be considered fixed through a let or a similar construct. Note, however, that we adopt this convention only to simplify the presentation, not to advocate a general style of programming which depends implicitly on argument evaluation order.

Occasionally, we will use Reynolds’s notion of “serious” and “trivial” λ_{v}-terms (Reynolds, 1972). Evaluating a serious term might loop so this term must be transformed into CPS, whereas evaluating a trivial one cannot loop so this term does not need to be transformed.

Finally, let us recall the main property of a CPS λ-term: the independence of its reduction order. Reducing a CPS term with the call-by-name (CBN) or with the callby-value (CBV) strategies yields the same evaluation steps (Reynolds, 1972; Plotkin,

[[x]] = λκ.@κx
[[λx.M]] = λκ.@κ(λx.[[M]])
[[@M N]] = λκ.@[[M]](λm.@[[N]](λn.@(@mn)κ))

Fig. 1. Fischer & Plotkin’s CPS transformation of λ_{v} -terms

Overview

The rest of this paper is organized as follows. Section 2 describes the stepwise derivation of a one-pass CPS transformer from Plotkin’s two-pass equational specification. Theorem 1 states that the one-pass transformer computes a result βη-equivalent to the original Fischer/Plotkin transformation. Section 3 investigates the reduction properties of the one-pass transformer. Theorem 2 captures Plotkin’s “Indifference” and “Simulation” theorems for the original CPS translation. Section 4 extends the one-pass transformer to handle conditional expressions, recursive definitions, etc. Section 5 introduces control operators and their CPS transformation. Using these control operators, it presents a onepass CPS transformer in direct style. Section 6 reviews related work on continuations and partial evaluation, and Section 7 concludes. An appendix reproduces the development of Section 2 on Plotkin’s CPS transformer for λ_{n}-terms.

2. Classical CPS transformation

Let us consider Fischer and Plotkin’s equational specification for transforming a λ_{v}- term into CPS (Fischer, 1972; Plotkin, 1975), as displayed in Figure 1. Source terms are represented between double brackets and κ is a fresh variable.

Taken literally, this translation yields many artificial “administrative” redexes that must be post-reduced in a second pass; only then do we obtain a result in what is commonly recognized as “continuation-passing style” (Steele, 1978). For example, translating

λf.λx.λy.@(@f y)x

results in

λk.@k (λf.λk.@k (λx.λk.@k (λy.λk. \begin{matrix}@ (λk.@(λk.@k f)(λm.@(λk.@k y)(λn.@(@mn)k))) \\ (λm.@(λk.@k x)(λn.@(@mn)k))))) \end{matrix}

whose post-reduction yields

λk.@k (λf.λk.@k (λx.λk.@k (λy.λk.@(@f y)(λm.@(@mx)k))))

Conversely, an overly enthusiastic post-reducer is likely to perform too many reductions, i.e., ones that would correspond to actual reductions in the source term. While this may be useful in its own right, it should not automatically be considered a part of the CPS transformation proper. In particular, excessive post-reduction can lead to uncontrolled “code duplication” in the result or, in the untyped case, even nontermination of the simplification.

In the following, we will, therefore, concentrate on integrating the first and the second passes subject to the two constraints: (1) a one-pass translation should not introduce any administrative redex; and (2) a one-pass translation should not perform any reduction that would correspond to reducing a source term.

Our derivation is simple. We analyze the original equational specification, identifying where redexes get built, independently of any actual source λ-term. When these redexes are “context-independent”, we reduce them at translation time. When they are “contextdependent”, we alter the translation with meaning-preserving transformations to make the construction of redexes context-independent. The goal of the game is to stage the CPS transformation into a “translation-time” part and a “run-time” part.

For precision and conciseness in the text, let us label the six lambdas and the six applications of this specification:

[[x]] = λ^{1}κ.@^{1}κx
[[λx.M]] = λ^{2}κ.@^{2}κ(λ^{3}x.[[M]])
[[@M N]] = λ^{4}κ.@^{3}[[M]](λ^{5}m.@^{4}[[N]](λ^{6}n.@^{5}(@^{6}mn)κ))

Our development is structured in three steps.

2.1. First step

As can be observed, the result of each elementary transformation (of a variable; of an abstraction; of an application) is an abstraction.

Question 1. Where can the abstractions λ^{1}, λ^{2}, and λ^{4} occur in the residual CPS term before post-reduction?

Answer – by cases: (a) as the body of λ^{3}; (b) as the first argument of @^{3}; (c) as the first argument of @^{4}. In cases (b) and (c) the translation is building a redex that can be simplified by β-reduction. In case (a) no simplification can take place immediately.

As a consequence, whether the abstractions λ^{1}, λ^{2}, and λ^{4} are post-reducible is contextdependent.

Question 2. Can we get rid of this dependence?

Answer – yes, by introducing one η-redex in the definitional translation of abstractions. This new redex will exhibit the continuation of the body:

[[λx.M]] = λ^{2}κ.@^{2}κ(λ^{3}x.λ^{7}k.@^{7}[[M]]k)

The new redex is safe (in the sense of preserving operational behavior under both CBN and CBV) because [[M]] is itself a λ-abstraction. (Expanding “@f a” to “λx.@(@f a)x” is not in general meaning-preserving, even if “@f a” has a functional type. Expanding “f” to “λx.@f x” or “λy.E” to “λx.@(λy.E)x” is safe.)

Remark: Such an η-expansion may be felt as a step backwards in optimizing the translation, since η-reduction is usually perceived as an actual optimization step. In fact, and as illustrated by this development, the premature optimization in the translation of λ-abstractions contributes to muddying the water in the translated terms.

Now let us repeat Question 1: Question 3. Where can the abstractions resulting from each elementary transformation occur in the residual term? Answer – by cases: (a) as the first argument of @^{7}; (b) as the first argument of @^{3}; (c) as the first argument of @^{4}.

Therefore, the translation is building a β-redex. This redex can be simplified unconditionally.

2.2. Second step

Since the three λ-abstractions λ^{1}, λ^{2}, and λ^{4} will be reduced at translation time, let us enumerate their possible arguments. Question 4. Which syntactic constructs can be denoted by κ in λ^{1}, λ^{2}, and λ^{4}? Answer – by cases: (a) the second argument of @^{7} is an identifier k; (b) the second argument of @^{3} is λ^{5}; (c) the second argument of @^{4} is λ^{6}.

Again, the situation is irregular: if the argument of these applications (i.e., the value denoted by κ) later gets applied, this application will be reducible in cases (b) and (c) only, i.e., in a context-dependent fashion. Question 5. Can we get rid of this dependence? Answer – yes, by introducing another η-redex in the translation of abstractions. This redex will exhibit the application of the continuation.

[[λx.M]] = λ^{2}κ.@^{2}κ(λ^{3}x.λ^{7}k.@^{7}[[M]](λ^{8}m.@^{8}k m))

Now let us repeat Question 4: Question 6. Which syntactic constructs can be denoted by κ? Answer – by cases (a) the second argument of @^{7} is λ^{8}; (b) the second argument of @^{3} is λ^{5}; (c) the second argument of @^{4} is λ^{6}.

Now the different occurrences of κ are ensured to denote λ-abstractions only.

2.3. Third step

Question 7. Where do these κ occur? Answer – by cases: (a) as the first argument of @^{1}; (b) as the first argument of @^{2};

(c) as the second argument of @^{5}. In cases (a) and (b), the translation is building a redex that can be simplified by β-reduction. In case (c) no simplification can take place immediately.

As a consequence, whether the application of a κ is post-reducible is context-dependent, since in case (c) κ does not occur in function position in an application. Question 8. Can we get rid of this dependence? Answer – yes, by introducing a last η-redex in the definitional translation of applications. The redex will exhibit sending the result of an application to the continuation.

[[@M N]] = λ^{4}κ.@^{3}[[M]](λ^{5}m.@^{4}[[N]](λ^{6}n.@^{5}(@^{6}mn)(λ^{9}a.@^{9}κa)))

Now let us repeat Question 7: Question 9. Where do the κ occur? Answer – by cases: (a) as the first argument of @^{1}; (b) as the first argument of @^{2}; (c) as the first argument of @^{9}.

As a consequence, because by construction the translation is building a λ-abstraction which is ensured to occur in function position in an application, we can classify these λ-abstractions and applications to be simplifiable unconditionally.

To summarize, let us overline the λ-abstractions and the applications that will be reduced unconditionally as a part of the translation. Since they exist only at translation time we refer to them as “static.”

[[x]] = \overline{λ^{1}}κ.\overline{@^{1}}κx
[[λx.M]] = \overline{λ^{2}}κ.\overline{@^{2}}κ(λ^{3}x.λ^{7}k.\overline{@^{7}}[[M]](\overline{λ^{8}}m.@^{8}k m))
[[@M N]] = \overline{λ^{4}}κ.\overline{@^{3}}[[M]](\overline{λ^{5}}m.\overline{@^{4}}[[N]](\overline{λ^{6}}n.@^{5}(@^{6}mn)(λ^{9}a.\overline{@^{9}}κa)))

2.4. Completing the transformation: the other syntactic constructions

We can also list the possible arguments of the κ: they are the second arguments of @^{1}, @^{2}, and @^{9}, i.e., (a) an identifier x; (b) λ^{3}; (c) an identifier a. These may be bound to m in λ^{5}, n in λ^{6}, and m in λ^{8}.

— In λ^{5}, m occurs as the first argument of @^{6}.

– If m is bound to x or a no simplification is possible.

– If m is bound to λ^{3} then a β-reduction is possible but it would correspond to a reduction in the original term; therefore we do not want to perform it. Thus @^{6} must be classified as irreducible and so is λ^{3} and thus λ^{7}.

— In λ^{6}, n occurs as the second argument of @^{6} which is irreducible.

— In λ^{8}, m occurs as the second argument of @^{8} that cannot be reduced since the first argument is the identifier k.

As a consequence, the first argument of @^{5} is irreducible and thus @^{5} is irreducible. As another consequence, the second argument of @^{5} must be irreducible.

To summarize, let us underline the abstractions and the applications that will be built unconditionally as a part of the translation. Since they are part of the transformed term, we refer to them as “dynamic.”

[[x]] = \overline{λ^{1}}κ.\overline{@^{1}}κx
[[λx.M]] = \overline{λ^{2}}κ.\overline{@^{2}}κ(\underline{λ^{3}}x.\underline{λ^{7}}k.\overline{@^{7}}[[M]](\overline{λ^{8}}m.\underline{@^{8}}k m))
[[@M N]] = \overline{λ^{4}}κ.\overline{@^{3}}[[M]](\overline{λ^{5}}m.\overline{@^{4}}[[N]](\overline{λ^{6}}n.\underline{@^{5}}(\underline{@^{6}}mn)(\underline{λ^{9}}a.\overline{@^{9}}κa)))

As a simple inspection of this two-level specification shows, the only application that could possibly be a dynamic β-redex (i.e., a redex in the resulting CPS term) is @^{6}. This happens if and only if m is bound to a dynamic λ, which again happens if and only if M is a λ-abstraction, so the source term contains a β-redex at this point. We do not want to reduce a dynamic β-redex because it would correspond to reducing a β-redex in the source term, which is not the job of the CPS transformation.

[[...]] : [syntax → syntax] → syntax
[[x]] = \overline{λ}κ.\overline{@}κx
[[λx.M]] = \overline{λ}κ.\overline{@}κ(\underline{λ}x.\underline{λ}k.\overline{@}[[M]](\overline{λ}m.\underline{@}k m))
[[@M N]] = \overline{λ}κ.\overline{@}[[M]](\overline{λ}m.\overline{@}[[N]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))

Fig. 2. One-pass CPS transformation of λ_{v} -terms

2.5. The complete transformation

To conclude, Figure 2 shows the final version of the transformer, without labels since they were only used for expository purposes. With its static/dynamic annotations, it can be read as a two-level specification à la Nielson and Nielson (Nielson and Nielson, 1988). Operationally, the overlined λ’s and @’s correspond to functional abstractions and applications in the translation program, while only the underlined occurrences represent abstract-syntax constructors. Transforming a λ-term into CPS amounts to representing contexts (i.e., λ-terms with a hole) as λ-abstractions. An empty context (e.g., top-level) is represented with the identity function. An arbitrary (“dynamic”) context is represented with some continuation k.

The result of transforming a term M into CPS in an empty context is given by

\overline{@}[[M]](\overline{λ}m.m)

whereas the result of transforming a term M into CPS in a dynamic context is given by

\underline{λ}k.\overline{@}[[M]](\overline{λ}m.\underline{@}k m)

As can be noticed, both initial contexts are represented with translation-time λabstractions, as dictated by the answer to Question 6. In the rest of this section, we refer to such translation-time λ-abstractions as static continuations.

This instrumented new translation yields terms without extraneous redexes, in one pass. The static/dynamic distinction aimed at defining all the administrative β-redexes. These administrative β-redexes are bound at translation time and therefore they do not occur in residual terms.

The above development is summarized in the following theorem. Theorem 1. This equational specification, i.e., \underline{λ}k.\overline{@}[[M]](\overline{λ}m.\underline{@}k m), computes a result βη-equivalent to the original Fischer/Plotkin transformation.

Proof. We started from Fischer & Plotkin’s specification and altered it in a meaningpreserving way, by introducing three η-redexes. We obtained a staged specification where static and dynamic constructs are not only distinct but context-independent. (Using Nielson and Nielson’s terminology (Nielson and Nielson, 1988; Nielson, 1989), our twolevel specification is “well-typed.”) We can now reduce away all the static β-redexes. Moreover, since the specification is compositional, a simple typing argument suffices to show that it is well-defined for all source terms, i.e., that the static reductions do in fact terminate. Only the static lambdas and applications matter; for the purpose of termination, the dynamic lambdas/applications are just uninterpreted constructors. And the static part of the transformation is simply typed, with a single base type “syntax”; the κ’s all have type “syntax → syntax” and the other static variables just have type “syntax”. In particular, given an initial continuation κ, \overline{@}[[M]]κ is a strongly normalizable term of type “syntax”. Thus, when interpreted as a functional program, the transformation always terminates (and in essentially linear time, since none of the static data is ever duplicated). Finally, no redexes of the original term are reduced: the “λx” of an abstraction in the source term is always translated into a dynamic “λx”, (i.e., a syntax constructor) in the corresponding CPS term, and hence is never reduced away. Observation 1. A λ_{v}-term and its CPS counterpart are related as follows:

— A variable is translated into itself.

— A λ-abstraction is translated into two λ-abstractions and one application.

— An application is translated into two applications and one λ-abstraction. This observation provides a simple correspondence between the size of a term and its

CPS counterpart. Moreover, since for all of the new λ-abstractions introduced by the translation, the abstracted variable occurs exactly once in the body, this relationship extends directly to the number of reduction steps performed during evaluation of the two terms (more about this in Section 3).

2.6. Tail-calls and η-redexes

While introducing η-redexes is crucial to avoid building β-redexes in residual terms, in one simple case it yields extra η-redexes in the transformed program. Not surprisingly this arises for tail-calls, as illustrated here:

\overline{@}[[λf.@f x]](\overline{λ}m.m) = λf.λk.@(@f x)(λa.@k a)

instead of λf.λk.@(@f x)k

Four straightforward possibilities come to the mind. We can leave these η-redexes where they are (which might be actually useful if the term is subjected to further transformation or if Observation 1 is used since tail-call optimizations change the number of reduction steps.) We can detect when a newly constructed λ-abstraction is actually an η-redex and simplify it at this time. We can instrument the translation with an inherited attribute identifying tail-call contexts, eliminating the dynamic tests on term structure entirely. Or equivalently we can duplicate the rules to account for tail-call contexts, as in Figure 3, and in a way reminiscent of Clinger’s double induction proof in his Scheme compiler (Clinger, 1984).

Rationale: The auxiliary translation [[...]]′ is used when the static continuation would have the form \overline{λ}m.\underline{@}k m; this avoids building an η-redex in the transformation of applications (hence the term “properly tail-recursive” (Steele, 1978)).

The result of transforming a term M into CPS in an empty context is still given by

\overline{@}[[M]](\overline{λ}m.m)

whereas the result of transforming a term M into CPS in a dynamic context is now simply

[[...]] : [syntax → syntax] → syntax
[[x]] = \overline{λ}κ.\overline{@}κx
[[λx.M]] = \overline{λ}κ.\overline{@}κ(\underline{λ}x.\underline{λ}k.\overline{@}[[M]]′ k)
[[@M N]] = \overline{λ}κ.\overline{@}[[M]](\overline{λ}m.\overline{@}[[N]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))
[[...]]′ : syntax → syntax
[[x]]′ = \overline{λ}k.\underline{@}k x
[[λx.M]]′ = \overline{λ}k.\underline{@}k (\underline{λ}x.\underline{λ}k.\overline{@}[[M]]′ k)
[[@M N]]′ = \overline{λ}k.\overline{@}[[M]](\overline{λ}m.\overline{@}[[N]](\overline{λ}n.\underline{@}(\underline{@}mn)k))

Fig. 3. One-pass, “properly tail-recursive” CPS transformation of λ_{v} -terms

\underline{λ}k.\overline{@}[[M]]′ k

By construction, this instrumented new translation yields terms without extraneous η-redexes, and of course with no β-redexes, in one completely syntax-directed pass. And since the only difference with the transformation in Figure 2 is the elimination of trivial η-redexes, the new translation preserves the statement of Theorem 1.

3. Reduction properties

We can now formulate results about the new CPS translation analogous to the ones for the original specification. Moreover, since we have eliminated all administrative redexes “once and for all”, the proofs become considerably simpler than for the unoptimized translation.

It may be worth quickly going over why administrative redexes raise problems in the original translation (Plotkin, 1975; Riecke, 1989). Ideally, the following implication would hold:

M →_{v} N ⇒ @[[M]](λx.x) →_{v}^{∗} @[[N]](λx.x)

Unfortunately, the administrative redexes get in the way of such a result. What really happens is the following: first, by a sequence of administrative reductions, @[[M]](λx.x) →_{v}^{∗} M′. Then M′ →_{v} N′, corresponding to the original redex. However, there is no reason to expect than N′ now reduces to @[[N]](λx.x); in fact, it would have to expand back to recreate the administrative redexes of the latter.

One therefore has to prove instead that the implication above holds “modulo administrative reductions”. This is formalized by the so-called “colon-translation” developed by Plotkin (Plotkin, 1975). For any term M and value K, one defines syntactically a term M : K and proves it equal to @[[M]]K with the first series of administrative reductions performed (i.e., corresponding to the term M′ above). One then proves that if M →_{v} N then M : K →_{v}^{∗} N : K. Finally, for every reduction sequence

M_{0} →_{v} M_{1} →_{v} ... →_{v} V where V is a non-functional value, one can take K = λx.x and get

@[[M_{0}]](λx.x) →_{v}^{∗} M_{0} : (λx.x) →_{v}^{∗} M_{1} : (λx.x) →_{v}^{∗} ... →_{v}^{∗} V : (λx.x) = @(λx.x)V →_{v} V

It is crucial to note that the colon-translation only removes enough redexes to “expose” the first real reduction. In particular, it never removes redexes within λ-abstractions. Nor does it have to, since it only acts as a proof technique, not a “code optimization” pass. In the new translation, on the other hand, we get a direct correspondence between reduction steps in the original and the translated term.

Remark: It does seem possible to modify the colon-translation to perform more administrative reductions at translation time (Griffin, 1990). Nevertheless, a practical translation (i.e., for a full language like Scheme) based on such an approach could be awkward because of the combinatorial explosion arising from translation-time distinctions between values and non-values in source terms.

Let us first observe a few elementary properties of the two-level translation. To simplify the presentation, we will generally treat α-equivalent dynamic terms as equal.

Definition 1. If V is a value (i.e., either a variable or an abstraction), we define

Ψ(V) = \overline{@}[[V]](\overline{λ}x.x)

(This differs from Plotkin’s Ψ in that the latter does not eliminate administrative redexes inside transformed λ-abstractions). It is immediate that Ψ(V) is itself a value. Lemma 1. If V is a value and P is not a value (i.e., an application), the following simple properties hold (where K is any term, that is, a term of type syntax and κ a static continuation, that is, a term of type syntax → syntax):

\overline{@}[[V]]κ = \overline{@}κ(Ψ(V))
\overline{@}[[V]]′ K = \underline{@}K (Ψ(V))
\overline{@}[[P]]κ = \overline{@}[[P]]′ (\underline{λ}a.\overline{@}κa)

Proof. Immediate in all cases.

Let us write substitution of N for x in M as M[x←N]. Now, we need to show that the static parts of the translation do not interfere with substitution.

Definition 2. We say that a variable x occurs free in a static continuation κ if for some M it occurs free in \overline{@}κM but not in M. κ is called schematic if for any terms M and N, and variable x not occurring free in κ,

(\overline{@}κM)[x←N] = \overline{@}κ(M[x←N])

(informally, this ensures that κ preserves the syntactic structure of its argument, and does not capture any free variables occurring in it).

One easily sees that any κ defined using only static abstraction, static application, and the syntax constructors (with any dynamic abstractions introducing only “new” variables) is schematic.

We can now formalize how substitution of arbitrary values for identifiers commutes with CPS-translation:

Lemma 2. Let M be a term, V a value, x a variable, and let κ be a schematic continuation and K any term. Then

\overline{@}[[M[x←V]]]κ = (\overline{@}[[M[x←x′]]]κ)[x′←Ψ(V)]
\overline{@}[[M[x←V]]]′ K = (\overline{@}[[M[x←x′]]]′ K)[x′←Ψ(V)]

where x′ is a new variable (the renaming is necessary to take care of the case when x occurs free in κ or K).

Proof. By induction on M. All cases are straightforward (let y ≠ x):

\overline{@}[[x[x←V]]]κ = \overline{@}[[V]]κ = \overline{@}κ(Ψ(V)) = \overline{@}κ(x′[x′←Ψ(V)])
= (\overline{@}κx′)[x′←Ψ(V)] = (\overline{@}[[x[x←x′]]]κ)[x′←Ψ(V)]
\overline{@}[[y[x←V]]]κ = \overline{@}[[y]]κ = (\overline{@}[[y[x←x′]]]κ)[x′←Ψ(V)]
\overline{@}[[(λx.M)[x←V]]]κ = (same as y[x←V])
\overline{@}[[(λy.M)[x←V]]]κ = \overline{@}[[λy.M[x←V]]]κ = \overline{@}κ(\underline{λ}y.\underline{λ}k.\overline{@}[[M[x←V]]]′ k)
= \overline{@}κ(\underline{λ}y.\underline{λ}k.(\overline{@}[[M[x←x′]]]′ k)[x′←Ψ(V)])
= (\overline{@}κ(\underline{λ}y.\underline{λ}k.\overline{@}[[M[x←x′]]]′ k))[x′←Ψ(V)]
= (\overline{@}[[λy.M[x←x′]]]κ)[x′←Ψ(V)]
= (\overline{@}[[(λy.M)[x←x′]]]κ)[x′←Ψ(V)]
\overline{@}[[(@M N)[x←V]]]κ = \overline{@}[[@(M[x←V])(N[x←V])]]κ
= \overline{@}[[M[x←V]]](\overline{λ}m.\overline{@}[[N[x←V]]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))
= (\overline{@}[[M[x←x′]]](\overline{λ}m.(\overline{@}[[N[x←x′]]](\overline{λ}n.
\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))[x′←Ψ(V)]))[x′←Ψ(V)]
= (\overline{@}[[M[x←x′]]](\overline{λ}m.\overline{@}[[N[x←x′]]](\overline{λ}n.
\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa))))[x′←Ψ(V)]
= (\overline{@}[[@(M[x←x′])(N[x←x′])]]κ)[x′←Ψ(V)]
= (\overline{@}[[(@M N)[x←x′]]]κ)[x′←Ψ(V)]

The cases for the second equation are analogous.

Let us now recall the formal definition of the reduction strategies (Plotkin, 1975):

Definition 3. One-step by-value reduction is defined as follows:

@(λx.M)V →_{v} M[x←V]  \frac{M →_{v} M′}{@M N →_{v} @M′ N}  \frac{N →_{v} N′}{@V N →_{v} @V N′}

(where V is a value), and similarly one-step by-name reduction:

@(λx.M)N →_{n} M[x←N]  \frac{M →_{n} M′}{@M N →_{n} @M′ N}  \frac{N →_{n} N′}{@xN →_{n} @xN′}

We write M →_{a} N if both M →_{v} N and M →_{n} N. For any of the three reduction relations →, we use →^{+} and →^{∗} to refer to its transitive and reflexive-transitive closure, respectively. Lemma 3. Let M and N be terms such that M →_{v} N, and let κ be a schematic continuation. Then

\overline{@}[[M]]κ →a^{+} \overline{@}[[N]]κ

(in fact, in either two or three reductions).

Proof. By induction on the derivation of →_{v}:

— Base case: @(λx.M)V →_{v} M[x←V].

\overline{@}[[@(λx.M)V]]κ = \overline{@}[[λx.M]](\overline{λ}m.\overline{@}[[V]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))
= \overline{@}[[V]](\overline{λ}n.\underline{@}(\underline{@}(\underline{λ}x.\underline{λ}k.\overline{@}[[M]]′ k)n)(\underline{λ}a.\overline{@}κa))
= \underline{@}(\underline{@}(\underline{λ}x.\underline{λ}k.\overline{@}[[M]]′ k)(Ψ(V)))(\underline{λ}a.\overline{@}κa)
→_{a} \underline{@}(\underline{λ}k.(\overline{@}[[M]]′ k)[x←Ψ(V)])(\underline{λ}a.\overline{@}κa)
= \underline{@}(\underline{λ}k.(\overline{@}[[M[x←x′]]]′ k)[x′←Ψ(V)])(\underline{λ}a.\overline{@}κa)
= \underline{@}(\underline{λ}k.\overline{@}[[M[x←V]]]′ k)(\underline{λ}a.\overline{@}κa)
→_{a} \overline{@}[[M[x←V]]]′ (\underline{λ}a.\overline{@}κa)

Now the following two cases arise:

– M[x←V] is not a value. Then by Lemma 1, the last term is equal to \overline{@}[[M[x←V]]]κ, as required. The two reductions correspond to transferring the argument value and return continuation (if we use uncurried CPS translation, as in Section 4.3, only one reduction is needed).

– M[x←V] is a value. Then again Lemma 1 gives

\overline{@}[[M[x←V]]]′ (\underline{λ}a.\overline{@}κa) = \underline{@}(\underline{λ}a.\overline{@}κa)(Ψ(M[x←V]))
→_{a} \overline{@}κ(Ψ(M[x←V]))
= \overline{@}[[M[x←V]]]κ

The additional reduction in this case corresponds to an application of the return continuation to the value just computed.

— Inductive case 1: @M N →_{v} @M′ N because M →_{v} M′.

\overline{@}[[@M N]]κ = \overline{@}[[M]](\overline{λ}m.\overline{@}[[N]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))
→a^{+}  \overline{@}[[M′]](\overline{λ}m.\overline{@}[[N]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))
= \overline{@}[[@M′ N]]κ

— Inductive case 2: @V N →_{v} @V N′ because N →_{v} N′.

\overline{@}[[@V N]]κ = \overline{@}[[V]](\overline{λ}m.\overline{@}[[N]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))

= \overline{@}[[N]](\overline{λ}n.\underline{@}(\underline{@}(Ψ(V))n)(\underline{λ}a.\overline{@}κa))
→a^{+}  \overline{@}[[N′]](\overline{λ}n.\underline{@}(\underline{@}(Ψ(V))n)(\underline{λ}a.\overline{@}κa))
= \overline{@}[[V]](\overline{λ}m.\overline{@}[[N′]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))
= \overline{@}[[@V N′]]κ

If we restrict evaluation to closed terms, any term is either already a value or contains a redex. However, the results extend easily to open terms, with free variables treated as uninterpreted constants (i.e., with no associated δ-rules). In this case, there is a third possibility: evaluation may halt at a non-value term like @xy from which no further progress is possible.

Following Plotkin, we define: Definition 4. A (necessarily open) term S is said to be stuck under a given strategy if it is neither a value nor reducible by any of the reduction rules for that strategy. A quick inspection of Definition 3 shows that such terms must be of the following form (where V is a value and N is any term):

S_{v} ::= @xV | @S_{v} N | @V S_{v}  (for call-by-value)
S_{n} ::= @xV | @S_{n} N | @xS_{n}  (for call-by-name)

We note that every term stuck under CBN is also stuck under CBV. Lemma 4. Let M be any term and κ a static continuation. If M is stuck under CBV then \overline{@}[[M]]κ is stuck under any strategy.

Proof. By structural induction on the stuck term M. Base case, M = @xV:

\overline{@}[[@xV]]κ = \overline{@}[[x]](\overline{λ}m.\overline{@}[[V]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))
= \underline{@}(\underline{@}x(Ψ(V)))(\underline{λ}a.\overline{@}κa)

where the inner application, and hence the entire term, is stuck. Inductive case 1, M = @S N:

\overline{@}[[@S N]]κ = \overline{@}[[S]](\overline{λ}m.\overline{@}[[N]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))

which is stuck, by the induction hypothesis. Inductive case 2, M = @V S:

\overline{@}[[@V S]]κ = \overline{@}[[V]](\overline{λ}m.\overline{@}[[S]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))
= \overline{@}[[S]](\overline{λ}n.\underline{@}(\underline{@}(Ψ(V))n)(\underline{λ}a.\overline{@}κa))

which again is stuck by induction hypothesis.

Remark: In a statically-typed setting, the above problem does not occur: the typing rules ensure that a non-functional constant will never be applied to an argument. However, the argument extends easily to languages with the possibility of runtime errors (e.g., division by zero). A simple refinement of the proof shows that the CPS translation can even distinguish properly between different error conditions, i.e., if evaluation of the original program causes a specific error, so does evaluation of the CPS-transformed program.

We can now state the main result, analogous to Plotkin’s “Indifference” and “Simulation” theorems for the original CPS translation: Theorem 2. Let M be any λ-term (not necessarily closed) and V a value. If M →_{v}^{∗} V then \overline{@}[[M]](\overline{λ}x.x) →_{a}^{∗} \overline{@}[[V]](\overline{λ}x.x) = Ψ(V) (and in at most three times as many steps). In particular, if V is simply a free variable of M, the CPS translation of M also evaluates to Ψ(V) = V. Conversely, if M does not evaluate to a value under the call-by-value strategy, then for no strategy will \overline{@}[[M]](\overline{λ}x.x) evaluate to one.

Proof. The first part follows immediately from Lemma 3 applied to every step of the reduction. Conversely, any infinite value-reduction sequence starting from M gives rise to an infinite, strategy-independent reduction sequence starting from \overline{@}[[M]](\overline{λ}x.x). Finally, if the original reduction sequence stops at a CBV-stuck term S, the corresponding CPS reduction sequence ends in the term \overline{@}[[S]](\overline{λ}x.x) which is stuck under any strategy (Lemma 4).

4. Enriching the CPS transformation

This section investigates the translation of λ-terms as found in usual applicative-order functional languages and the problem of currying functions vs. tupling arguments.

4.1. CPS translation of extended and applied λ_{v}-terms

We now turn to translating λ_{v}-terms applied over constants and (pure) primitive operations and extended with conditional expressions, let and letrec expressions (restricting the values that are bound recursively to be functions). Such applied and extended λ-terms come straight from Scheme and Standard ML.

Following the line of Section 2, Figure 4 displays a one-pass equational specification of the CPS transformation. Primitive operations are treated differently from ordinary applications to simplify the equations. If a primitive operator q is to be passed as a functional value, it must be written with an explicit abstraction λx.q(x) — which can be done at syntax-analysis time. Again, the result of transforming a term M into CPS in an empty context is given by

\overline{@}[[M]](\overline{λ}m.m)

and the result of transforming M in a dynamic context is given by

\underline{λ}k.\overline{@}[[M]](\overline{λ}m.\underline{@}k m)

This instrumented new translation yields terms without extraneous redexes (if tail-calls are handled as in Section 2.6), in one pass. We obtained these equations by analyzing the binding times of the valuation functions of a continuation semantics of the λ_{v}-calculus, along the line of Section 2. The simulation and indifference properties of CPS-transformed terms generalize to the above translation, but with one exception: unless the primitive operations are also transformed into continuation-passing versions, there is no longer a direct correspondence between δ-reductions in the original and the CPS-transformed term. Thus, the optimized translation for primitives should only be used for “completely pure” operations (see also Section 6.2).

[[...]] : [syntax → syntax] → syntax
[[x]] = \overline{λ}κ.\overline{@}κx
[[λx.M]] = \overline{λ}κ.\overline{@}κ(\underline{λ}x.\underline{λ}k.\overline{@}[[M]](\overline{λ}m.\underline{@}k m))
[[@M N]] = \overline{λ}κ.\overline{@}[[M]](\overline{λ}m.\overline{@}[[N]](\overline{λ}n.\underline{@}(\underline{@}mn)(\underline{λ}a.\overline{@}κa)))
[[P →M, N]] = \overline{λ}κ.\overline{@}[[P]](\overline{λ}p.p \underline{→} \overline{@}[[M]]κ\underline{,} \overline{@}[[N]]κ)
[[q]] = \overline{λ}κ.\overline{@}κq
[[q(M)]] = \overline{λ}κ.\overline{@}[[M]](\overline{λ}m.\overline{@}κ(\underline{q}(m)))
[[q(M, N)]] = \overline{λ}κ.\overline{@}[[M]](\overline{λ}m.\overline{@}[[N]](\overline{λ}n.\overline{@}κ(\underline{q}(m, n))))
[[let x = N in M]] = \overline{λ}κ.\overline{@}[[N]](\overline{λ}n.\underline{let} x′ = n \underline{in} \overline{@}[[M[x←x′]]]κ)
[[letrec f = λx.N in M]] = \overline{λ}κ. \underline{letrec} f′ = \underline{λ}x.\underline{λ}k.\overline{@}[[N[f←f′]]](\overline{λ}n.\underline{@}k n)) \underline{in} \overline{@}[[M[f←f′]]]κ

Fig. 4. One-pass CPS transformation of extended and applied λ_{v} -terms

As always with non-trivial symbolic reductions in λ-calculus, we face the problem of name clashes. These can occur when a context is moved inside the scope of a binding construct, as illustrated in the following example:

\overline{@}([[λx.x + (let x = 3 in x)]])(\overline{λ}v.v) = λx.λk.let x′ = 3 in @k (x + x′)

Had we not renamed the x introduced by the let, we would have inadvertently captured a free variable of the static continuation κ. However, variables declared in λ-abstractions do not need to be renamed because contexts are never moved inside the scope of a λ-abstraction.

Let us also note that if the subterm N in the translation of a let-expression is a value (notably, an abstraction), the corresponding variable in the transformed term will also be let-bound (as opposed to λ-bound) to Ψ(N). Thus, the translation seems compatible with a restricted variant of ML-style polymorphism in which generalization can only be applied to values (Harper and Lillibridge, 1992).

4.2. On duplicating contexts

The CPS translation above duplicates contexts for each conditional expression:

[[P →M, N]] = \overline{λ}κ.\overline{@}[[P]](\overline{λ}p.p \underline{→} \overline{@}[[M]]κ\underline{,} \overline{@}[[N]]κ)

which increases the size of residual terms, as pointed out by Steele (Steele, 1978). For example, translating the direct style expression

@f ((x→y, z)→4, 5)

yields the more voluminous

λκ.x → \begin{matrix}(y →@(@f 4)(λv.@k v), @(@f 5)(λv.@k v)) , \\ (z →@(@f 4)(λv.@k v), @(@f 5)(λv.@k v)) \end{matrix}

and thus a bigger term to compile and correspondingly more object code to produce. For this reason, compiler writers usually refrain from duplicating contexts by introducing a dynamic let-expression to share the static continuation between the two branches of the conditional:

[[P →M, N]] = \overline{λ}κ. \begin{matrix}\underline{let} k = \underline{λ}a.\overline{@}κa \\ \underline{in} & \overline{@}[[P]](\overline{λ}p.p \underline{→} \overline{@}[[M]](\overline{λ}m.\underline{@}k m)\underline{,} \overline{@}[[N]](\overline{λ}n.\underline{@}k n)) \end{matrix}

where we have inserted the appropriate η-redexes, in the line of Section 2. This modification restores the linearity property of the static part of the translation, i.e., that bound variables of static λ-abstractions are used only once in their bodies, and thus maintains a linear relationship between the sizes of the original and transformed terms.

Because the let-expression introduces an explicit name for the context, each conditional branch de facto occurs in a dynamic context, just like the body of translated λ-abstractions. As in Section 2.6, we can use the special “tail-call” translation for these contexts:

[[P →M, N]] = \overline{λ}κ.\underline{let} k = \underline{λ}a.\overline{@}κa \underline{in} \overline{@}[[P]](\overline{λ}p.p \underline{→} \overline{@}[[M]]′ k\underline{,} \overline{@}[[N]]′ k)

For example, the expression above is translated into

λk_{0}. let k_{1} = λv_{0}. \begin{matrix}let k_{2} = λv_{1}.@(@f v_{1})k_{0} \\ in & v_{0} →@k_{2} 4, @k_{2} 5 \end{matrix} in x→@k_{1} y, @k_{1} z

Still there is room left for further simplification, e.g., in the case of let-expressions. As revealed by a simple inspection of the equations, translating let-expressions whose headers are an application or a conditional expression will produce identity let expressions. These redundant let-expressions can be prevented at translation time:

[[let x = @N_{0} N_{1} in M]] = \overline{λ}κ.\overline{@}[[N_{0}]](\overline{λ}n_{0}.\overline{@}[[N_{1}]](\overline{λ}n_{1}.\underline{@}(\underline{@}n_{0} n_{1})(\underline{λ}x′.\overline{@}[[M[x←x′]]]κ)))

4.3. Currying vs. tupling

For practical applications of the CPS transformation algorithm described above, we need the slight refinement considered in this section.

In a call-by-name language, there is a one-to-one correspondence between curried and non-curried forms of multi-argument functions, but for call-by-value this property is lost: there may be several, non-equivalent ways of “currying” a function. For example, the curried form of the two-argument function

g = λ(a, b).(@f a) + b

can be written as either of the two terms:

g̃_{1} = λa.λb.(@f a) + b or g̃_{2} = λa.let x = @f a in λb.x + b

Both of these qualify as curried forms of g, in the sense that for any pair of values a and b,

@(@g̃_{1} a)b = @(@g̃_{2} a)b = @g (a, b)

but g̃_{1} and g̃_{2} behave differently if applied to only a single argument a for which f fails to terminate.

Since the CPS transform clearly needs to accommodate curried functions like g̃_{2} above, programs with “simple” curried functions appear unnecessarily complex. For example, curried addition

λa.λb.(a + b)

must be translated to the somewhat awkward

λa.λk.@k (λb.λk′.@k′ (a + b))

instead of the more natural

λa.λb.λk.@k (a + b)

The problem is that a higher-order type like τ_{1} → [τ_{2} → τ_{3}] does not make it clear whether the outermost function is “serious” or “trivial”, as in these two last examples. This can be solved by extending the source language with either a product type or a new “trivial function space” (restoring the equivalence between “trivially curried” and uncurried forms of functions).

Moreover, the result of translating a function of type

σ → τ

into CPS with “answer” type o, can itself be expressed in either “curried CPS”:

σ′ → [τ′ → o] → o

or “uncurried CPS:”

σ′ × [τ′ → o] → o

The functions resulting from the curried CPS transform can be easily checked to be always trivial (i.e., immediately return a closure), but this is not clear from their type. Thus, if we want to treat the transformation result itself as a call-by-value term, the uncurried form of the translation is more precise.

4.4. Multi-argument functions

For languages like Standard ML, which have an explicit product type for expressing functions of several arguments, we can essentially use the equations of Figure 4 directly. Multiple variables in λ-abstractions can be treated as syntactic sugar for projections from a single argument, and tuple construction becomes a new primitive operator. For a Scheme-like language, however, the “argument tuple” is not an autonomous entity, but is closely tied in with functional abstraction and application. We thus need to adjust the CPS equations of these two constructs slightly if we want an uncurried source-to-source transformation:

[[λ(x_{1}, ..., x_{n}).E]] = \overline{λ}κ.\overline{@}κ(\underline{λ}(x_{1}, ..., x_{n}, k).\overline{@}[[E]](\overline{λ}x.\underline{@}k x))
[[@E_{0} (E_{1}, ..., E_{n})]] = \overline{λ}κ. \begin{aligned}\overline{@} & [[E_{0}]] \\ & (\overline{λ}f.\overline{@}[[E_{1}]](\overline{λ}a_{1}. ...\overline{@}[[E_{n}]](\overline{λ}a_{n}.\underline{@}f (a_{1}, ..., a_{n}, \underline{λ}x.\overline{@}κx)))) \end{aligned}

More precisely, an argument list is translated as follows:

[[()]]^{∗} = \overline{λ}κ.\overline{@}κ()
[[E :: E^{∗}]]^{∗} = \overline{λ}κ.\overline{@}[[E]](\overline{λ}h.\overline{@}[[E^{∗}]]^{∗} (\overline{λ}t.\overline{@}κ(h \overline{::} t)))

and a full application as:

[[@E_{0} (E_{1}, ..., E_{n})]] = \overline{λ}κ.\overline{@}[[E_{0}]](\overline{λ}f.\overline{@}[[(E_{1}, ..., E_{n})]]^{∗} (\overline{λ}l.\underline{@}f (l \overline{⋄} [\underline{λ}x.\overline{@}κx])))

where ⋄ represents list concatenation.

Remark: To make the Scheme-style connection between lists and argument tuples even closer, we could put the continuation argument first in the argument list rather than last. This would allow us to translate “variadic procedures” such as

                       (lambda l (cdr l)) or (lambda (a b . l) b)

directly into

               (lambda (k . l) (k (cdr l))) and (lambda (k a b . l) (k b))

respectively. However, readability appears to suffer when the continuation argument, which is often large, must be followed by others in an application. Making continuations occur first is used sometimes to compile functional programs by program transformation (Fradet and Le Métayer, 1991). It is simple to write a one-pass CPS transformer where continuations precede values — just swap values and continuations in any of the specifications displayed in the figures.

5. Abstracting Control

So far we have been investigating how to perform the CPS transformation. This section explores properties and extensions of the transformation function.

5.1. Reynolds’s escape operator

Not every λ-calculus term is obtainable as a result of the CPS transformation. Some of the “unused” terms correspond to control operators in the source language. For example, the operator escape (interdefinable with Scheme’s call/cc) can be defined by the equation:

[[escape c in M]] = λκ.let c′ = λa.λκ′.@κa in @[[M[c←c′]]]κ

As a control operator, escape captures the current continuation and provides a representation of this current continuation as if it were a function in the source program. Applying this function to a value amounts to abandoning the current context of computation and passing this value to the captured continuation. For example, transforming the term

λf.escape c in 1 + (@f c)

into CPS in an empty context (and unfolding the let) yields

λf.λc.@(@f (λx.λk.@cx))(λv.@c(1 + v))

As can be observed in the equation above, escape duplicates the code for the current continuation. Along the lines of Section 4.2, this can be prevented by the following equation:

[[escape c in M]] = \overline{λ}κ.\underline{let} k = \underline{λ}a.\overline{@}κa \underline{in} \underline{let} c = \underline{λ}a.\underline{λ}k′.\underline{@}k a \underline{in} \overline{@}[[M]](\overline{λ}m.\underline{@}k m)

In the rest of this section, we shall waive concerns about such duplications of contexts.

5.2. Shift and reset

Let us note that even with escaping constructs, the result of the translation is in “ordinary” CPS form, i.e., with no nested function applications. This suggests that there is still a considerable amount of untapped expressive power in the CPS formalism, reflecting control structures whose translations are more general λ-terms. In particular, we can define the two operators shift and reset, conceptually serving as composition and identity for continuation functions:

[[shift c in M]] = λκ.let c = λa.λκ′.@κ′ (@κa) in @[[M]](λm.m)
[[⟨M⟩]] = λκ.@κ(@[[M]](λm.m))

Shift abstracts the current context as an ordinary, composable procedure (in contrast to the exceptional, non-composable procedures yielded by escape) and reset delimits the scope of such a context. Shift also differs from escape by not implicitly duplicating the current continuation (Felleisen’s C-operator introduced the behavior of not duplicating continuations (Felleisen et al., 1987b)).

For example,

1 + ⟨10 + shift c in @c(@c100)⟩ ⇒ 1 + (10 + (10 + 100)) ⇒ 121

With the fuller control over contexts afforded by these two operators, we can express in a functional style many control structures that would otherwise have required us to either rewrite the program extensively or introduce side effects. For example, let us consider a functional representation of “applicative” nondeterministic (in the sense of backtracking) programming, as embodied, e.g., in the programming language Icon (Griswold and Griswold, 1983).

Let us define a basic “nondeterministic choice” procedure:

flip = λ().shift c in @c tt ∨ @cff

When invoked, flip will “return” twice: once with each possible truth value. Here, we have specified that the final answer of the nondeterministic program should be true if either of these two return values causes the context to evaluate to true. For a canonical example, let φ be a boolean expression with free variables b_{1}, ..., b_{n}. To determine whether φ is satisfiable (i.e., whether there exists an assignment of truth values to the variables making the whole expression true), we can now simply evaluate the natural direct-style program

⟨let b_{1} = @flip () in … let b_{n} = @flip () in φ⟩

This approach to nondeterministic programming also easily handles irregular search structures, where further tests may depend on outcome of previous “guesses”, e.g., for simulating a nondeterministic finite automaton (Danvy and Filinski, 1990).

5.3. Control and prompt

While shift and reset are very similar to Felleisen’s operators control and prompt (Felleisen, 1988), there is a significant semantical difference between shift/reset and control/prompt: the context abstracted by shift is determined statically by the static program text, while control captures the context up to the nearest dynamically enclosing prompt.

The difference between shift and control is probably best displayed by the following two characteristic equations:

⟨@f (shift c in M)⟩ = ⟨let c = λx.⟨@f x⟩ in M⟩
⟨@f (control c in M)⟩ = ⟨let c = λx.@f x in M⟩

Now if f is bound to a procedure that itself abstracts control, the context it will capture with the shift semantics is still determined by the context where c is defined. On the other hand, with the control semantics, a control operator occurring in f will capture the context at the point where c is applied; in particular, it can capture part of M. (In the case where f is a simple procedure with no control effects, the effects of the two operators coincide.)

The shift/reset approach is based on viewing a program as computing a function expressed in CPS, i.e., on representing control with a function: the continuation. In contrast, prompt and control were introduced independently of CPS and therefore they admit no such simple static interpretation. Their two denotational descriptions introduce an algebra of control and lead to a representation of continuations as promptdelimited sequences of activation frames, and their composition as the concatenation of these sequences (Felleisen et al., 1988). Earlier on, prompts were specified with an operational description in terms of textual reductions (Felleisen, 1988). In general, these static vs. dynamic interpretations lead to different behaviors (Danvy, 1989).

In our framework, reset naturally is the direct style counterpart of initializing the continuation of a CPS λ-term with the identity function. Reset seems to be equivalent to prompt, but terms using control in general have no CPS counterpart.

5.4. CPS translation of terms that use shift and reset

Let us note that the definitions of shift and reset do not yield CPS terms (because continuations may be applied to non-values). Therefore the defining terms lose the important property of enforcing strict call-by-value evaluation ensured by proper CPS. However, we can restore that property by translating the defining (pure λ_{v}-calculus) terms once more into CPS, yielding a term in “meta-continuation passing style.” Here, the κ is treated as an ordinary functional parameter, while the proper evaluation order is ensured by a new continuation.

For example, and leaving the @-notation aside for readability, the following term occurring in an empty context

let f = λx.shift k in k(k(x))
in 1 + ⟨10 + f(100)⟩

gets CPS-transformed into

\begin{matrix}let f_{c} = λx.λk.k(k(x)) \\ in & 1 + (f_{c} 100 (λv.10 + v)) \end{matrix}

As can be noticed, this term is not in CPS because the call to f_{c} is not a tail-call and there is a nested call to k in the definition of f_{c}. But the second CPS transformation now gives a proper CPS term (with h as the continuation parameter):

\begin{matrix}let f_{cc} = λx.λk.λh.k x (λa.k a h) \\ in & f_{cc} 100 (λv.λh.h(10 + v)) (λa.1 + a) \end{matrix}

Remark: Iterating this construction leads to “extended CPS” and a whole hierarchy of control operators (Danvy and Filinski, 1990). This is the real forte of a CPS-based approach to advanced control structures: we obtain a natural notion of “levels” of control, allowing us to express, e.g., collections over all paths of a nondeterministic subcomputation, as defined in Section 5.2.

5.5. Translating control operations in one pass

Following a binding time analysis of the equations of Section 5.2 (as in Section 2), let us express the CPS transformation of control operations using two-level λ-terms:

[[escape c in M]] = \overline{λ}κ.\underline{let} c′ = \underline{λ}a.\underline{λ}κ′.\overline{@}κa \underline{in} \overline{@}[[M[c←c′]]]κ
[[shift c in M]] = \overline{λ}κ.\underline{let} c′ = \underline{λ}a.\underline{λ}κ′.\underline{@}κ′ (\overline{@}κa) \underline{in} \overline{@}[[M[c←c′]]](\overline{λ}m.m)
[[⟨M⟩]] = \overline{λ}κ.\overline{@}κ(\overline{@}[[M]](\overline{λ}m.m))

The CPS transformation now introduces let-expressions. These could be unfolded by substituting the control abstractions for the identifiers in the translated terms, as we first specified it (Danvy and Filinski, 1990):

[[escape c in M]] = \overline{λ}κ.(\overline{@}[[M[c←c′]]]κ)[c′←\underline{λ}a.\underline{λ}κ′.\overline{@}κa]
[[shift c in M]] = \overline{λ}κ.(\overline{@}[[M[c←c′]]](\overline{λ}m.m))[c′←\underline{λ}a.\underline{λ}κ′.\underline{@}κ′ (\overline{@}κa)]

However, these substitutions introduce residual β-redexes when control abstractions are applied within the scope of their declaration. For example,

\overline{@}[[λx.shift c in 1 + (@cx)]](\overline{λ}m.m) = λx.λc.@(@(λa.λk.1 + (@k a))x)c instead of the preferable λx.λc.1 + (@cx)

To keep this β-reduction at translation time, but again at the risk of duplicating contexts (as in shift c in (@c1) + (@c2)), we can distinguish between identifiers that are declared within a λ-abstraction and identifiers that are declared within a control abstraction. Unfortunately, this decision clutters the transformation, much in the same way as introducing “first-class” primitive operators (cf. Section 4.1). We adopt the same simple solution: at syntax-analysis time, occurrences of identifiers declared within a control abstraction are guaranteed to occur only in application position, which we single out by tagging this application with throw, as in Standard ML of New Jersey (Duba et al., 1991).

[[escape c in M]] = \overline{λ}κ.(\overline{@}[[M[c←c′]]]κ)[c′←\overline{λ}a.\overline{λ}κ′.\overline{@}κa]
[[shift c in M]] = \overline{λ}κ.(\overline{@}[[M[c←c′]]](\overline{λ}m.m))[c′←\overline{λ}a.\overline{λ}κ′.\overline{@}κ′ (\overline{@}κa)]
[[throw c M]] = \overline{λ}κ.\overline{@}[[M]](\overline{λ}m.\overline{@}(\overline{@}cm)κ)

To avoid dealing with substitutions over translated terms, we can introduce a translation-time environment mapping identifiers to a translation-time λ-abstraction if they are declared within a control abstraction. The following is the corresponding version of the CPS transformer, completed with the translation-time environment. The other equations are unchanged, except for the addition of an environment ρ passively transmitted everywhere.

env : var → syntax → [syntax → syntax] → syntax
[[[...]]] : env → [syntax → syntax] → syntax
[[[escape c in M]]] = \overline{λ}ρ.\overline{λ}κ.\overline{@}(\overline{@}[[[M[c←c′]]]][c′ \overline{↦} \overline{λ}a.\overline{λ}κ′.\overline{@}κa]ρ)κ
[[[shift c in M]]] = \overline{λ}ρ.\overline{λ}κ.\overline{@}(\overline{@}[[[M[c←c′]]]][c′ \overline{↦} \overline{λ}a.\overline{λ}κ′.\overline{@}κ′ (\overline{@}κa)]ρ)(\overline{λ}m.m)
[[[throw c M]]] = \overline{λ}ρ.\overline{λ}κ.\overline{@}(\overline{@}[[[M]]]ρ)(\overline{λ}m.\overline{@}(\overline{@}(\overline{@}ρc)m)κ)

Note how all the terms in the translation are static. All administrative reductions are performed at translation time, and no β-redexes are built for applications of control abstractions.

5.6. The problem of name clashes

Now only one problem remain: name clashes. These can occur when a control operator moves part of the context inside the scope of any binding construct, as illustrated in the following example:

\overline{@}(\overline{@}[[[λx.@f (escape c in λf.throw c f)]]]ρ_{0})(\overline{λ}v.v) = λx.λk.@k (λf′.λk′.@(@f f′)k)

The simplest solution is thus probably to systematically rename all bound variables.

5.7. Direct Transformation into CPS

We can view the CPS transformation of Section 4.1 as an applicative order program expressing the transformation algorithm. This program is expressed in a CPS-like style. This might lead one to believe that this program could be expressed more concisely using a “traditional” control operator like call/cc. Unfortunately, this is not quite possible because this program is not in CPS. Notably, in the translation of @M N the continuation application \overline{@}κa is a subterm of the syntax-constructor \underline{λ}a. · · ·. Conversely, in [[λx.M]], the continuation κ is applied to a potentially non-trivial term. Neither of these situations can arise from the translation of any conventional direct-style term (i.e., λ-calculus + escape). However, with shift/reset we can express exactly such behavior. Let us rewrite

[[x]] = x
[[λx.M]] = \underline{λ}x.\underline{λ}k.\overline{⟨}\underline{@}k [[M]]\overline{⟩}
[[@M N]] = \overline{shift} c \overline{in} \underline{@}(\underline{@}[[M]][[N]])(\underline{λ}a.\overline{@}ca)
[[P →M, N]] = \overline{shift} c \overline{in} [[P]] \underline{→} \overline{⟨}\overline{@}c[[M]]\overline{⟩}\underline{,} \overline{⟨}\overline{@}c[[N]]\overline{⟩}
[[q]] = q
[[q(M)]] = \underline{q}([[M]])
[[q(M, N)]] = \underline{q}([[M]], [[N]])
[[let x = N in M]] = \overline{shift} c \overline{in} \underline{let} x′ = [[N]] \underline{in} \overline{⟨}\overline{@}c[[M[x←x′]]]\overline{⟩}
[[letrec f = λx.N in M]] = \overline{shift} c \overline{in} \underline{letrec} f′ = \underline{λ}x.\underline{λ}k.\overline{⟨}\underline{@}k [[M[f←f′]]]\overline{⟩} \underline{in} \overline{⟨}\overline{@}c[[M[f←f′]]]\overline{⟩}
[[escape k in M]] = \overline{shift} c \overline{in} \underline{let} k′ = \underline{λ}v.\underline{λ}k′′.\overline{@}cv \underline{in} \overline{⟨}\overline{@}c[[M[k←k′]]]\overline{⟩}
[[shift k in M]] = \overline{shift} c \overline{in} \underline{let} k′ = \underline{λ}v.\underline{λ}k′′.\underline{@}k′′ (\overline{@}cv) \underline{in} \overline{⟨}[[M[k←k′]]]\overline{⟩}
[[⟨M⟩]] = \overline{⟨}[[M]]\overline{⟩}

Fig. 5. Direct-style, one-pass CPS transformation of λ_{v} -terms

the transformation equations using implicit continuations. The result is displayed in Figure 5.

The result of transforming a term M into CPS in an empty context is given by

\overline{⟨}[[M]]\overline{⟩}

Similarly, the result of transforming M in an arbitrary context is given by

\underline{λ}k.\overline{⟨}\underline{@}k [[M]]\overline{⟩}

The CPS counterpart of the applicative-order program expressing this transformation algorithm (using the equations of Section 4.1 and the first set of equations of Section 5.5) can be verified easily to coincide with the original translator. Thus, the two transformers yield textually the same output for a given input; only their internal organization differs.

This set of equations can be seen as a meta-circular compiler from a language with the new control operators into its purely functional subset. Alternatively (by omitting the equations for shift and reset), it translates terms of a Scheme-like language (i.e., λcalculus + escape) into standard CPS. Such a transformation has a practical interest for compiling, e.g., Scheme or Standard ML programs (Steele, 1978; Appel, 1992), and thus constitutes a significant example of using shift/reset: even the pure CPS translation is expressed naturally using the new control operators.

As with all meta-circular definitions, we need to bootstrap it. If we have an interpreter for a language with shift/reset, we can use it to execute the translator on itself, obtaining a CPS transformer written in pure λ-calculus. On the other hand, we can get an interpretive semantics for the extended language by translating a trivial (i.e., defining shift in terms of shift, etc.) self-interpreter into extended CPS (Danvy and Filinski, 1990). This correspondence helps to ensure consistency between the two methods of language definition.

6. Related Work

6.1. CPS transformation

Two other works have independently employed CPS translations similar to the one presented here. The first one is Appel’s CPS transformer in the Standard ML of New Jersey compiler (Appel, 1992). The second one is Wand’s combinator-based compilation technique (Wand, 1991). But neither motivate their transformer, e.g., as we do in Section 2, nor extend it to control operators or normal order, as we do in Sections 5 and 7.

As revealed in the source code of the SML/NJ compiler, the CPS transformer operates in one pass by keeping a translation time continuation, based on η-redexes identical to those in Section 2. However, in contrast to our work, the goal is not to aim at the “exact” continuation-passing counterparts of source programs but to simplify them as much as possible, even if some of the simplifications correspond to source reductions. Still no particular care is taken to avoid building extraneous η-redexes, such as those pointed out in Section 4.2. Instead, the compiler relies on a powerful and blind simplifier of CPS terms that processes both these redexes and what corresponds to source reductions. It would be interesting to measure whether and how much our more precise CPS transformer relieves the simplifier.

Similarly, devising a particular representation of run time procedures and their application (instead of our \underline{λ} and \underline{@}), Wand also compiles programs based on a CPS transformer with the same η-redexes as in Section 2, but again without motivating them.

Today Sabry and Felleisen are also investigating the CPS transformation in one pass, and Lawall and the first author are investigating the inverse “Direct Style” transformation (Danvy, 1992; Danvy and Lawall, 1992; Sabry and Felleisen, 1992).

6.2. Primitive operators

Most CPS-based compilers (Steele, 1978; Appel, 1992; Wand, 1991) and program analyzers (Shivers, 1991) also use continuation-passing forms of even the primitive operators. However, the practical justification of such a “radical CPS” transform is not completely clear. In particular, the oft-quoted advantage of having explicit names for all subexpressions can be realized equally well with let-expressions. Clearly, side-effecting operators need to be tied down by explicit conversion to continuation-passing variants. However, expressing “trivial computations” like tuple construction/destruction or arithmetic in CPS introduces unnecessary sequentialization and obscures the fact that such computations can be rearranged or even eliminated or duplicated without affecting the meaning of the program.

Remark: A possible problem here concerns primitive operators like division that can signal error conditions, but are otherwise “pure”. Clearly, the translation should preserve any exception-raising behavior of the original program, and not compromise the order-of-evaluation independence of CPS terms. On the other hand, going to full CPS for such almost-functional operators may still be overkill, for the reasons outlined above. However, it often seems possible to factor the original operator into two aspects: the control behavior (the process of computation, possibly error-raising) to be expressed in CPS and the pure (and hence freely rearrangable) function computed, in which case we actually get the best of both worlds.

6.3. Control operators

From Reynolds’s escape to call/cc in Scheme, control operators are nicely introduced within the CPS transformation (Reynolds, 1972; Felleisen et al., 1986). However, because CPS appears to constrain expressive power, Felleisen and others have successively proposed new control operators to compose continuations (Felleisen et al., 1987a) and to limit their extent (Felleisen, 1988). As later shown by Sitaram and Felleisen (Sitaram and Felleisen, 1990), inclusion of control delimiters is also necessary to obtain fully abstract models of control for CPS models with escape. The motivation for shift and reset was somewhat different: rather than devising new theories, new models, and new representations of control, we have set out to explore CPS more thoroughly. In particular, shift and reset are introduced together as representing composition and identity on continuation functions respectively; proper CPS form is restored by iterating the CPS transformation (Danvy and Filinski, 1990).

6.4. Partial evaluation

Partial evaluation (or more accurately: program specialization (Jones et al., 1989)) makes heavy use of binding time information to process the static and the dynamic semantics of source programs (Consel and Danvy, 1991a), as we do here. Recent works by Bondorf and the first author emphasize the issues of code duplication and termination properties (Bondorf and Danvy, 1991), and use the technique of enumerating finitary constructs (Bondorf, 1991), as we do in Sections 2 and 4.2. The latter is also central to Shivers’s work on higher-order flow analysis (Shivers, 1991). All these concepts were pervasive in our derivation of a one-pass CPS transformer. In particular, the notion of a two-level λcalculus as advocated in Nielson and Nielson’s TML (Nielson and Nielson, 1988) proves useful to develop and to express new CPS transformations that distinguish properly between translation-time and run-time constructs.

With respect to partial evaluation, this development illustrates the connection between a CPS transformer and a λ-calculus interpreter expressed in CPS. The former is a twolevel version of the latter.

Moreover, our derivation illustrates a new trend in partial evaluation: using CPS to improve binding time properties of source programs, leading to better specialization (Consel and Danvy, 1991b). Work is going on to further automate the process.

7. Conclusion and Issues

As proven constructively in this paper, transforming λ-terms into CPS can be expressed in one pass by moving administrative redexes to translation time in a context-free way. While the actual transformation algorithm seems to have been independently discovered

[[x]] = x
[[λx.M]] = λκ.@κ(λx.[[M]])
[[@M N]] = λκ.@[[M]](λm.@(@m[[N]])κ)

Fig. 6. Plotkin’s CPS transformation of λ_{n}-terms

several times in slightly different forms, we believe that ours is the first systematic derivation and analysis of its correctness and properties. The translation is easily extended to the usual constructs of applicative order functional languages and also to account for control operators. And using two control operators shift and reset derived naturally from the CPS formalism, the translation can be formulated even more concisely and directly.

The role of continuations in programming language design and implementation has long been dominated by pragmatic concerns. In the last few years, however, the subject has seen renewed theoretical interest, especially with the introduction of concepts and methods from mathematical logic and category theory, e.g., (Griffin, 1990; Murthy, 1990; Filinski, 1992). We believe that any investigation of advanced control structures based on the CPS transform will be able to pick up and integrate such developments more directly than a free-standing approach derived from more intuitively “desirable” operational behavior could. And in fact, recent developments seem to support this conviction (Murthy, 1992).

Moreover, there is a close relationship between computational monads (Moggi, 1989) and “generalized CPS”, as suggested in “Abstracting Control” (Danvy and Filinski, 1990) and properly formalized by Wadler (Wadler, 1992). Effectively, this implies that CPS-based control operators like shift and reset can by themselves uniformly express a rich class of computational behaviors, including partiality, nondeterminism, and state. It seems natural to take this as another indication that both the theoretical and practical significance of functional representations of control will only grow stronger in the years to come.

Appendix: call by name

Let us consider Plotkin’s equational specification for transforming a λ_{n}-term into CPS (Plotkin, 1975), as displayed in Figure 6. We want to apply the method of Section 2 to stage the CPS_{n}-transformation.

Again, taken literally, this translation yields artificial redexes that must be postreduced in a second pass, although the size explosion is not as drastic as for call-by-value. For example, translating

λf.λx.λy.@(@f y)x

yields

λk.@k (λf.λk.@k (λx.λk.@k (λy.λk.@(λk.@f (λm.@(@my)k))(λm.@(@mx)k))))

[[...]] : [syntax → syntax] → syntax
[[x]] = \overline{λ}κ.\underline{@}x(\underline{λ}a.\overline{@}κa)
[[λx.M]] = \overline{λ}κ.\overline{@}κ(\underline{λ}x.\underline{λ}k.\overline{@}[[M]](\overline{λ}m.\underline{@}k m))
[[@M N]] = \overline{λ}κ.\overline{@}[[M]](\overline{λ}m.\underline{@}(\underline{@}m(\underline{λ}k.\overline{@}[[N]](\overline{λ}n.\underline{@}k n)))(\underline{λ}a.\overline{@}κa))

Fig. 7. One-pass CPS transformation of λ_{n}-terms

whose post-reduction yields

λk.@k (λf.λk.@k (λx.λk.@k (λy.λk.@f (λm.@(@my)(λm.@(@mx)k)))))

This CPS counterpart of the λ_{n}-term can be equally evaluated using call-by-name or call-by-value. As a simple consequence, the continuation can be implemented as a strict function without altering the meaning of the original λ_{n}-term.

Can we subject the original specification to the same treatment as in Section 2 and get a one-pass CPS transformer? The answer is yes but the resulting transformation shows less immediate success. The original specification can be transformed into the one in Figure 7 which does not build any β-redex.

The result of transforming a term M into CPS in an empty context is then given by

\overline{@}[[M]](\overline{λ}m.m)

Again, this specification, viewed as an applicative order program, can be re-expressed using shift and reset.

However this new CPS translation suffers from a deficiency, as pinpointed by the following observation. Observation 2. A λ_{n}-term and its CPS counterpart are related as follows:

— A variable is translated into one application and one λ-abstraction.

— A λ-abstraction is translated into two λ-abstractions and one application.

— An application is translated into three applications and two λ-abstractions. Whereas the two last points also hold for Plotkin’s specification, the first point reveals that the new translation actually produces more redexes! However, the new specification only produces more η-redexes, which are not nearly as hard to get rid of as the β-redexes produced by the original translation, as outlined now.

η-redexes are only constructed in tail-contexts, for identifiers occurring as λ-abstraction bodies, and as arguments of functions (this corresponds to the ALGOL 60 situation of “suspending a suspension”). As in Section 2.6, they can eliminated at translation time by duplicating the rules (cf. Figure 8).

Rationale: The auxiliary translation [[M]]′′ is used for the special case \underline{λ}k.\overline{@}[[M]](\overline{λ}m.\underline{@}k m), thereby avoiding the construction of extraneous η-redexes.

The result of transforming a term M into CPS in an empty context is then given by

\overline{@}[[M]](\overline{λ}m.m)

whereas the result of transforming a term M into CPS in a dynamic context is given by

[[...]] : [syntax → syntax] → syntax
[[x]] = \overline{λ}κ.\underline{@}x(\underline{λ}a.\overline{@}κa)
[[λx.M]] = \overline{λ}κ.\overline{@}κ(\underline{λ}x.[[M]]′′)
[[@M N]] = \overline{λ}κ.\overline{@}[[M]](\overline{λ}m.\underline{@}(\underline{@}m[[N]]′′)(\underline{λ}a.\overline{@}κa))
[[...]]′′ : syntax
[[x]]′′ = x
[[λx.M]]′′ = \underline{λ}k.\underline{@}k (\underline{λ}x.[[M]]′′)
[[@M N]]′′ = \underline{λ}k.\overline{@}[[M]](\overline{λ}m.\underline{@}(\underline{@}m[[N]]′′)k)

Fig. 8. One-pass, “properly tail-recursive” CPS transformation of λ_{n}-terms

[[M]]′′

By construction, this instrumented new translation yields terms without β-redexes, in one pass.

7.1. Continuations first

Making continuations occur first introduces a new opportunity for extraneous η-redexes in residual CPS terms. The result of transforming a term can occur (1) in function position where the argument is a static lambda that will be applied to a static continuation; (2) in function position where the argument is a static lambda that will be applied to a dynamic continuation; and (3) not in function position. These cases can be handled by a suitable series of tests on intermediate result or again by duplicating the rules as in Figure 9. Notice how [[...]] terms correspond to case (1), [[...]]′ terms correspond to case (2), and [[...]]′′ terms correspond to case (3). This suggests that a Clinger-style compiler for λ_{n}-terms would be proven using a triple induction hypothesis (Clinger, 1984).

As usual, the result of transforming a term M into CPS in an empty context is then given by

\overline{@}[[M]](\overline{λ}m.m)

whereas the result of transforming a term M into CPS in a dynamic context is given by

\underline{λ}k.\overline{@}[[M]]′ k

or better, by

[[M]]′′

This final translation yields terms without β-redexes nor new η-redexes, in one pass.

Acknowledgements

We are grateful to the editor and the three referees. Thanks are also due to Karoline Malmkjær and Dave Schmidt for their patience and to Chet Murthy for his enthusiasm.

Representing Control 29

[[...]] : [syntax → syntax] → syntax
[[x]] = \overline{λ}κ.\underline{@}x(\underline{λ}a.\overline{@}κa)
[[λx.M]] = \overline{λ}κ.\overline{@}κ(\underline{λ}k.\underline{λ}x.\overline{@}[[M]]′ k)
[[@M N]] = \overline{λ}κ.\overline{@}[[M]](\overline{λ}m.\underline{@}(\underline{@}m(\underline{λ}a.\overline{@}κa))[[N]]′′)
[[...]]′ : syntax → syntax
[[x]]′ = \overline{λ}k.\underline{@}xk
[[λx.M]]′ = \overline{λ}k.\underline{@}k (\underline{λ}k.\underline{λ}x.\overline{@}[[M]]′ k)
[[@M N]]′ = \overline{λ}k.\overline{@}[[M]](\overline{λ}m.\underline{@}(\underline{@}mk)[[N]]′′)
[[...]]′′ : syntax
[[x]]′′ = x
[[λx.M]]′′ = \underline{λ}k.\underline{@}k (\underline{λ}k.\underline{λ}x.\overline{@}[[M]]′ k)
[[@M N]]′′ = \underline{λ}k.\overline{@}[[M]](\overline{λ}m.\underline{@}(\underline{@}mk)[[N]]′′)

Fig. 9. One-pass, “properly tail-recursive” CPS transformation of λ_{n}-terms with continuations first

References

Appel, A. W. (1992). Compiling with Continuations. Cambridge University Press. Bondorf, A. (1991). Automatic autoprojection of higher-order recursive equations. Science of

Computer Programming, 17:3–34. Bondorf, A. and Danvy, O. (1991). Automatic autoprojection of recursive equations with global

variables and abstract data types. Science of Computer Programming, 16:151–195. Clinger, W. (1984). The Scheme 311 compiler, an exercise in Denotational Semantics. In

Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming, pages 356–364, Austin, Texas.

Clinger, W. and Rees, J., editors (1991). Revised^{4} report on the algorithmic language Scheme.

LISP Pointers, IV(3):1–55. Consel, C. and Danvy, O. (1991a). Static and dynamic semantics processing. In (POPL, 1991),

pages 14–24. Consel, C. and Danvy, O. (1991b). For a better support of static data flow. In Proceedings of

the Fifth ACM Conference on Functional Programming and Computer Architecture, number 523 in Lecture Notes in Computer Science, pages 496–519, Cambridge, Massachusetts.

Danvy, O. (1989). Programming with tighter control. Special issue of the BIGRE journal:

Putting Scheme to Work, (65):10–29. Danvy, O. (1992). Back to direct style. In Krieg-Brückner, B., editor, Proceedings of the Fourth

European Symposium on Programming, number 582 in Lecture Notes in Computer Science, pages 130–150, Rennes, France.

Danvy, O. and Filinski, A. (1990). Abstracting control. In (LFP, 1990), pages 151–160.

O. Danvy and A. Filinski 30

Danvy, O. and Lawall, J. L. (1992). Back to direct style II: First-class continuations. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, San Francisco, California.

Danvy, O. and Talcott, C. L., editors (1992). Proceedings of the ACM SIGPLAN Workshop on

Continuations, San Francisco, California. Technical report, Stanford University. Duba, B. F., Harper, R., and MacQueen, D. (1991). Typing first-class continuations in ML. In

(POPL, 1991), pages 163–173. Felleisen, M. (1988). The theory and practice of first-class prompts. In Proceedings of the

Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 180–190, San Diego, California.

Felleisen, M., Friedman, D. P., Duba, B., and Merrill, J. (1987a). Beyond continuations. Tech-

nical Report 216, Computer Science Department, Indiana University, Bloomington, Indiana. Felleisen, M., Friedman, D. P., Kohlbecker, E., and Duba, B. (1986). Reasoning with continua-

tions. In Proceedings of the First Symposium on Logic in Computer Science, pages 131–141, Cambridge, Massachusetts. IEEE.

Felleisen, M., Friedman, D. P., Kohlbecker, E., and Duba, B. (1987b). A syntactic theory of

sequential control. Theoretical Computer Science, 52(3):205–237. Felleisen, M., Wand, M., Friedman, D. P., and Duba, B. F. (1988). Abstract continuations: A

mathematical semantics for handling full functional jumps. In Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pages 52–62, Snowbird, Utah.

Filinski, A. (1992). Linear continuations. In (POPL, 1992), pages 27–38. Fischer, M. J. (1972). Lambda calculus schemata. In Proceedings of the ACM Conference

on Proving Assertions about Programs, pages 104–109. SIGPLAN Notices, Vol. 7, No 1 and SIGACT News, No 14.

Fradet, P. and Le Métayer, D. (1991). Compilation of functional languages by program trans-

formation. ACM Transactions on Programming Languages and Systems, 13:21–51. Griffin, T. G. (1990). A formulae-as-types notion of control. In Proceedings of the Seventeenth

Annual ACM Symposium on Principles of Programming Languages, pages 47–58, San Francisco, California. ACM Press.

Griswold, R. E. and Griswold, M. T. (1983). The Icon Programming Language. Prentice-Hall. Harper, B. and Lillibridge, M. (1992). Polymorphic type assignment and CPS conversion. In

(Danvy and Talcott, 1992). Jones, N. D., Sestoft, P., and Søndergaard, H. (1989). MIX: A self-applicable partial evaluator

for experiments in compiler generation. LISP and Symbolic Computation, 2(1):9–50. LFP (1990). Proceedings of the 1990 ACM Conference on Lisp and Functional Programming,

Nice, France. LFP (1992). Proceedings of the 1992 ACM Conference on Lisp and Functional Programming,

San Francisco, California. Mellish, C. and Hardy, S. (1984). Integrating Prolog in the POPLOG environment. In Campbell,

J. A., editor, Implementations of PROLOG, pages 147–162. Ellis Horwood. Milner, R., Tofte, M., and Harper, R. (1990). The Definition of Standard ML. The MIT Press. Moggi, E. (1989). Computational lambda-calculus and monads. In Proceedings of the Fourth

Annual Symposium on Logic in Computer Science, pages 14–23, Pacific Grove, California. IEEE.

Murthy, C. R. (1990). Extracting Constructive Content from Classical Proofs. PhD thesis,

Department of Computer Science, Cornell University. Murthy, C. R. (1992). Control operators, hierarchies, and pseudo-classical type systems: A-

translation at work. In (Danvy and Talcott, 1992).

Representing Control 31

Nielson, F. (1989). Two-level semantics and abstract interpretation. Theoretical Computer

Science, 69(2):117–242. Nielson, F. and Nielson, H. R. (1988). Two-level semantics and code generation. Theoretical

Computer Science, 56(1):59–133. Plotkin, G. D. (1975). Call-by-name, call-by-value and the λ-calculus. Theoretical Computer

Science, 1:125–159. POPL (1991). Proceedings of the Eighteenth Annual ACM Symposium on Principles of Pro-

gramming Languages, Orlando, Florida. ACM Press. POPL (1992). Proceedings of the Nineteenth Annual ACM Symposium on Principles of Pro-

gramming Languages, Albuquerque, New Mexico. ACM Press. Reynolds, J. C. (1972). Definitional interpreters for higher-order programming languages. In

Proceedings of 25th ACM National Conference, pages 717–740, Boston. Riecke, J. G. (1989). Should a function continue? Master’s thesis, Department of Electrical

Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, Massachusetts.

Sabry, A. and Felleisen, M. (1992). Reasoning about programs in continuation-passing style. In

(LFP, 1992). Shivers, O. (1991). The semantics of Scheme control-flow analysis. In Hudak, P. and Jones,

N. D., editors, Symposium on Partial Evaluation and Semantics-Based Program Manipulation, SIGPLAN Notices, Vol. 26, No 9, pages 190–198, New Haven, Connecticut. ACM, ACM Press.

Sitaram, D. and Felleisen, M. (1990). Reasoning with continuations II: Full abstraction for

models of control. In (LFP, 1990), pages 161–175. Steele Jr., G. L. (1978). Rabbit: A compiler for Scheme. Technical Report AI-TR-474, Artificial

Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts. Wadler, P. (1992). The essence of functional programming. In (POPL, 1992), pages 1–14. Wand, M. (1991). Correctness of procedure representations in higher-order assembly language.

In Brookes, S., Main, M., Melton, A., Mislove, M., and Schmidt, D., editors, Mathematical Foundations of Programming Semantics, volume 598 of Lecture Notes in Computer Science, pages 294–311, Pittsburgh, Pennsylvania. 7th International Conference.