Reasoning about Programs in Continuation-Passing Style

Amr Sabry Matthias Felleisen ^{∗}

Department of Computer Science Rice University Houston, TX 77251-1892

Abstract

Plotkin’s λ-value calculus is sound but incomplete for reasoning about βη-transformations on programs in continuation-passing style (CPS). To find a complete extension, we define a new, compactifying CPS transformation and an “inverse” mapping, un-CPS, both of which are interesting in their own right. Using the new CPS transformation, we can determine the precise language of CPS terms closed under βη-transformations. Using the un-CPS transformation, we can derive a set of axioms such that every equation between source programs is provable if and only if βη can prove the corresponding equation between CPS programs. The extended calculus is equivalent to an untyped variant of Moggi’s computational λ-calculus.

1 Compiling with CPS

Many modern compilers for higher-order functional languages [1, 13, 19, 20] utilize some variant of the Fischer-Reynolds continuation-passing style (CPS) transformation [10, 18]. Once a program is in continuation-passing style, these compilers usually perform code optimizations via local transformations. Typical examples of such optimizations are loop unrolling, procedure inlining, and partial evaluation.

In the terminology of the λ-calculus, optimizations generally correspond to (sequences of) β- and ηreductions. Hence, a natural question to ask is whether reductions on CPS programs correspond to known transformations of source programs. If so, optimizations of CPS programs could be understood and reported in terms of the original program as opposed to its rather complicated CPS version. In particular, compilers that do not use the CPS transformation, e.g., Chez Scheme [12] or Zinc [15], could benefit by implementing transformations of source programs that correspond to transformations of CPS programs.

Technically speaking, we are addressing the following question: which calculus can prove M = N for by-value expressions M and N , if cps(M) = cps(N) is provable in the (by-value or by-name) λ-calculus? As Plotkin [17] showed in 1974, the λ_{v}-calculus does not suffice. Thus we refine this question as follows:

Is there a set of axioms, A, that extend the call-by-value λ-calculus such that:

λ_{v}A ⊢ M = N iff λβη ⊢ cps(M) = cps(N).

Such a correspondence theorem would be similar to the correspondence theorems for the λ-calculus and combinatory logic [2: ch 7], and the λ_{v}-calculus and by-value combinatory logic [11]. In analogy to model theory, we call the left-to-right direction soundness and the right-to-left direction completeness since the CPS transformation is often taken as the definition of a callby-value semantics.

To derive A, we proceed in three steps:

1. First, we develop a CPS transformation that produces a canonical form of CPS programs. The new transformation also produces the smallest possible output of all known CPS transformations, without reducing any of the original (source) redexes.

2. Second, we develop an un-CPS transformation that maps canonical CPS programs and their derivations back to the original language. As Danvy and Lawall [3, 6] convincingly argue, this translation from CPS to direct terms is useful in its own right.

3. Finally, by studying the connection between the CPS and un-CPS transformations, we systematically derive A. The extended λ-value calculus is equivalent to an untyped variant of Moggi’s [16] computational λ-calculus.

The next section introduces the basic terminology and notation of the λ-calculus and its semantics. The third section is a short history of CPS transformations. In Section 4, we formalize the problem and outline our approach to the solution. Section 5 is about the CPS language and its properties. It also contains the definition of our new CPS transformation. Section 6 presents the “inverse” mapping and its exact relation to the CPS transformation. Our main results, the extension of the λ_{v}-calculus and its completeness, are the subject of Section 7. Finally, Section 8 discusses the relevance of the new calculus and future directions of research.

∗Both authors were supported in part by NSF grant CCR 89-17022 and by a Texas ATP grant 92-003604014.

To appear in:

1992 Conference on Lisp and Functional Programming

June 21–23, 1992

San Francisco, California

Due to space limitations, we only indicate the ideas behind major proof steps. For details, we refer the reader to our extended technical report (Rice TR 92-180 ).

2 Λ: Calculi & Semantics

The language of the pure lambda calculus, Λ [2], consists of variables, λ-abstractions, and applications. The set of terms, M, is generated inductively over an infinite set of variables, Vars:

M ::= V | (M M)  (Terms)
V ::= x | (λx.M)  (Values)
x ∈ Vars

A term is either a value, V, or an application. Values consist of variables, drawn from the set Vars, and λabstractions.

We adopt Barendregt’s [2: ch 2, 3] notation and terminology for this syntax. Thus, in the abstraction (λx.M), the variable x is bound in M . Variables that are not bound by a λ-abstraction are free; the set of free variables in a term M is F V (M). We identify terms modulo bound variables, and we assume that free and bound variables do not interfere in definitions or theorems. In short, we follow common practice and work with the quotient of Λ under α-equivalence. We write M ≡ N for α-equivalent terms M and N.

The expression M[x := N] is the result of the capturefree substitution of all free occurrences of x in M by N. For example, (λx.xz)[z := (λy.x)] ≡ (λu.u(λy.x)). A context, C, is a term with a “hole”, [ ], in the place of one subexpression. The operation of filling the context C with an expression M yields the term C[M], possibly capturing some free variables of M in the process. Thus, the result of filling (λx.x[ ]) with (λy.x) is (λx.x(λy.x)).

Calculi: A λ-calculus is an equational theory over Λ with a finite number of axiom schemas and inference rules. The most familiar axiom schemas are the following notions of reductions:

\begin{matrix}((λx.M) N) & ⟶ & M[x := N] & (β) \\ ((λx.M) V) & ⟶ & M[x := V] & (β_{v}) \\ λx.Mx & ⟶ & M  x ∉ F V (M) & (η) \\ λx.V x & ⟶ & V  x ∉ F V (V) & (η_{v}) \end{matrix}

The set of inference rules is identical for all λ-calculi. It extends the notions of reductions to an equivalence relation compatible with syntactic contexts:

M ⟶ N ⇒ C[M] = C[N]  (Comp)
M = M  (Ref )
M = L, L = N ⇒ M = N  (Trans)
M = N ⇒ N = M  (Sym)

The underlying set of axioms completely identifies a theory. For example, β generates the theory λ, β_{v} generates the theory λ_{v}, and the union of β and η generates the theory λβη. In general, we write λA to refer to the theory generated by a set of axioms A. When a theory λA proves an equation M = N, we write λA ⊢ M = N. If the proof does not involve the inference rule Sym, we write λA ⊢ M ⟶ ⟶ N.

A notion of reduction R is Church-Rosser (CR) if λR ⊢ M = N implies that there exists a term L such that both M and N reduce to L, i.e., λR ⊢ M ⟶ ⟶ L and λR ⊢ N ⟶ ⟶ L. A term M is in R-normal form if there are no R-reductions starting with M.

Semantics: The semantics of the language Λ is a function, Eval, from programs to answers. A program is a term with no free variables and, in practical languages, an answer is a member of the syntactic category of values. Typically, Eval is defined via an abstract machine that manipulates abstract counterparts to machine stacks, stores, registers, etc. Examples are the SECD machine [14] and the CEK machine [7].

An equivalent method for specifying the semantics is based on the Curry-Feys Standard Reduction theorem [7, 17]. The Standard Reduction theorem defines a partial function, ⟼, from programs to programs that corresponds to a single evaluation step of an abstract machine for Λ.

A standard step (i) decomposes the program into a context E and a leftmost-outermost redex R (not inside an abstraction), and (ii) fills E with the contractum of R. The special contexts, E, are evaluation contexts and have the following definition for the call-by-value and call-by-name variants of Λ, respectively [7]:

\begin{aligned}E_{v} & ::= & [ ] | E_{v}[(V [ ])] | E_{v}[([ ] M)] \\ E_{n} & ::= & [ ] | E_{n}[([ ] M)] \end{aligned}

Conceptually, the hole of an evaluation context, [ ], points to the current instruction, which must be a β_{v} or β redex. The decomposition of M into E[(V N)] where (V N) is a redex means that the current instruction is (V N) and that the rest of the computation (the continuation! [7]) is E. Since, a call-by-name language never evaluates arguments, evaluation contexts do not include contexts of the shape E_{n}[(V [ ])].

Given evaluation contexts, the definitions of the standard reduction functions for call-by-value and call-by-name respectively are as follows:

\begin{matrix}E_{v}[((λx.M) V)] & ⟼_{v} & E_{v}[M[x := V]] \\ E_{n}[((λx.M) N)] & ⟼_{n} & E_{n}[M[x := N]] \end{matrix}

A complete evaluation applies the single-step functions repeatedly and either reaches an answer or diverges. The notation ⟼^{∗} denotes the reflexive, transitive closure of the function ⟼. The semantics of Λ is defined as follows:

Eval_{v}(M) = V iff M ⟼_{v}^{∗} V  (call-by-value)
Eval_{n}(M) = V iff M ⟼_{n}^{∗} V  (call-by-name)

For the definition of the semantics, η and η_{v} do not play any role. Their relevance for calculi is clarified in the next paragraph. Note: The syntax of the call-by-value language Λ can be redefined as follows:

Λ : M ::= V | E[(V V)]
Values : V ::= x | (λx.M)
EvCont : E ::= [ ] | E[(V [ ])] | E[([ ] M)]

We use both definitions of the syntax below.

Observational Equivalence: Not only do calculi define the semantics of Λ, but they are also useful for proving the correctness of some optimizations. Abstractly, an optimization of a program C[M] is the replacement of M by a “more efficient” expression N such that a programmer cannot distinguish the observational behavior of the programs C[M] and C[N]. The observational behavior of a program includes its termination behavior and its value when it terminates; it does not include execution speed. Formally, two expressions M and N are observationally equivalent, M ≅_{x} N (for x = v or x = n), if the following condition holds:

For all contexts C such that both C[M] and C[N] are programs, either both Eval_{x}(C[M]) and Eval_{x}(C[N]) are defined or both are undefined.

It is undecidable to determine whether two expressions are observationally equivalent. However, λ_{v} and λ are two typical (weak) examples of theories that are sound with respect to observational equivalence.

Theorem 2.1 (Plotkin) Let M, N ∈ Λ.

1. If λ_{v} ⊢ M = N then M ≅_{v} N.

2. If λ ⊢ M = N then M ≅_{n} N.

The soundness of extensions of λ and λ_{v} with η and η_{v}, respectively, depends on the circumstances. The axiom η_{v} is sound with respect to call-by-value observational equivalence for Λ. If we extend Λ with constants, η_{v} may be unsound. For an example, consider a dynamically typed language with numerals and a predicate integer?. The latter can distinguish 3 and λx.3 x, yet, the η_{v} axiom identifies the two terms. In a typed setting, η_{v} is generally sound, independent of the parameterpassing technique.

The axiom η, on the other hand, fails to be sound with respect to call-by-name observational equivalence even in a pure language. For example, if Ω is a diverging term, then (λx.Ωx) reduces to Ω but the two are clearly observationally distinct terms. Indeed, η is only sound in a typed language that does not permit the observation of the termination behavior of higher-type expressions.

3 The Origins and Practice of CPS

The idea of transforming programs to “continuationpassing style” appeared in the mid-sixties. For a few years, the transformation remained part of the folklore of computer science until Fischer and Reynolds codified it in 1972.

Fischer [10] studied two implementation strategies for Λ: a heap-based retention strategy, in which all variable bindings are retained until no longer needed, and a stack-based deletion strategy, in which variable bindings are destroyed when control leaves the procedure (or block) in which they were created. He concluded that

no real power is lost in restricting oneself to a deletion strategy implementation, for any program can be translated into an equivalent one which will work correctly under such an implementation [10: 104].

The translation is the following CPS transformation.

Definition 3.1. (Fischer CPS) Let k, m, n ∈ Vars be variables that do not occur in the argument to F.

\begin{aligned}F : Λ & → & Λ \\ F[[V]] & = & λk.k Ψ[[V]] \\ F[[MN]] & = & λk.F[[M]] (λm.F[[N]] λn.(m k) n) \\ Ψ[[x]] & = & x \\ Ψ[[λx.M]] & = & λk.λx.F[[M]] k \end{aligned}

Reynolds [18] investigated definitional interpreters for higher-order languages. Among his goals was the desire to liberate the definition of a language from the parameter-passing technique of the defining language. He developed a constructive (but informal) method to transform an interpreter such that it becomes indifferent to whether the underlying parameter passing technique is call-by-value or call-by-name. His transformation is essentially the same transformation as Fischer’s F. Plotkin [17] later proved Reynolds’ ideas correct.

Theorem 3.2 (Plotkin [17]) Let M ∈ Λ.

Simulation: Ψ[[Eval_{v}(M)]] = Eval_{n}(F[[M]] (λx.x))

Indifference:

Eval_{n}(F[[M]] (λx.x)) = Eval_{v}(F[[M]] (λx.x))

The Simulation theorem shows that the evaluation of the CPS program produces correct outputs. The Indifference theorem establishes that this evaluation yields the same result under call-by-value and call-by-name.

The main disadvantage of the Fischer CPS transformation is the excessive number of redexes it introduces in the output. For example,

F[[((λx.x) (y y))]] = ; \begin{matrix}λk.((λk.k λk.λx.((λk.kx) k)) \\ (λm.((λk.((λk.ky) λm.λk.ky λn.(m k) n)) \\ (λn.(m k) n)))). \end{matrix}

Although the original term contains one λ-abstraction and no β_{v}-redexes, its CPS counterpart contains a large number of both. Plotkin [17] referred to the new redexes as administrative redexes because an evaluator must always reduce them before re-establishing β_{v}-redexes that were present in the source term.

From both a theoretical and a practical perspective, the presence of the administrative redexes is undesirable. On the theoretical side, they complicate reasoning about CPS programs. For example, Plotkin [17] finds it necessary to define an improved CPS transformation exclusively for the proof of Theorem 3.2 above. On the practical side, code generation phases in compilers favor smaller, i.e., more manageable, programs. Hence, “practical” CPS transformations [1, 5, 13, 19, 20] use special algorithms to minimize the size of their outputs.

In essence, all practical CPS transformations are conceptually equivalent to the following two-pass CPS transformation:^{1}

• First, “mark” the new λ-abstractions in the output of the Fischer CPS to identify administrative redexes, and then

• reduce all administrative redexes.

Source redexes should remain intact because unrestricted reductions could cause non-termination. The remainder of this section codifies these ideas in a simple manner.

Formally, the first pass of the two-pass CPS is the following modified Fischer CPS transformation.

Definition 3.3. (Modified Fischer CPS) Let k, m, n ∈ Vars be as in Definition 3.1.

\begin{aligned}F[[V]] & = & \overline{λ}k.k Ψ[[V]] \\ F[[MN]] & = & \overline{λ}k.F[[M]] (\overline{λ}m.F[[N]] \overline{λ}n.(m k) n) \\ Ψ[[x]] & = & x \\ Ψ[[λx.M]] & = & \overline{λ}k.λx.F[[M]] k \end{aligned}

An overline decorates λ-abstractions that were not present in the original term. An administrative reduction is simply one that involves decorated abstractions:

\begin{matrix}((\overline{λ}x.M) N) & ⟶ & M[x := N] & (\overline{β}) \\ (\overline{λ}x.Mx) & ⟶ & M x ∉ F V (M) & (\overline{η}) \end{matrix}

The complete definition of the two-pass CPS transformation, F2_{k}, is parametrized over a continuation k.

Definition 3.4. (Two-Pass CPS) F2_{k}[[M]] = P iff λ\overline{β}\overline{η} ⊢ (F[[M]] k) = P where P is in \overline{β}\overline{η}-normal form.

The following proposition establishes that F2_{k} is welldefined.

Proposition 3.5 F2_{k} is a total function.

Proof. By Lemma 3.7, \overline{β}\overline{η}-normal forms are unique. Therefore, the relation F2_{k} is a function. Moreover, by Lemma 3.6, all reductions paths starting at F[[M]] for M ∈ Λ terminate. Hence, F2_{k} is a total function.

Lemma 3.6 Let M ∈ Λ. If λ\overline{β}\overline{η} ⊢ F[[M]] ≡ M_{0} ⟶ M_{1} ⟶ M_{2} ⋯, then:

1. for all M_{i}, the bound variable of a \overline{λ}-abstraction occurs exactly once in the body,

2. for all i ≥ 0, M_{i+1} has one less \overline{λ}-abstraction than M_{i}, and

3. for some finite n, M_{n} is in \overline{β}\overline{η}-normal form.

Proof Sketch. The first claim is initially true by construction, and is preserved by \overline{β}\overline{η}-reductions. It implies that reductions cannot eliminate or duplicate subterms. Therefore, the second claim holds. The last claim follows by induction on the number of \overline{λ}-abstractions in F[[M]].

It remains to establish that if F[[M]] reduces to two normal forms P and Q, then P and Q are identical.

Lemma 3.7 Let P and Q be in \overline{β}\overline{η}-normal form. If λ\overline{β}\overline{η} ⊢ F[[M]] ⟶ ⟶ P and λ\overline{β}\overline{η} ⊢ F[[M]] ⟶ ⟶ Q, then P ≡ Q.

Proof. The proof is a consequence of the Church-Rosser theorem for βη [2].

The output of F2_{k} is extremely compact. For example, applying F2_{k} to (((λx.λy.x) a) b) yields the term:

M ≡^{df} ((λx.((λy.kx) b)) a)

For the same example, both Steele’s Rabbit transformation [20] and the Danvy/Filinski transformation [5] yield the term:^{2}

1See also Danvy and Filinski’s development of these ideas [5].

N ≡^{df} ((λk_{1}x.(k_{1} λk_{2}y.k_{2}x)) (λm.mkb) a).

In the term N, every procedure accepts its continuation at the same time it accepts its argument. Therefore, the management of all continuations in the term N must occur at run-time. Specifically, the evaluation of M requires two β-reductions:

M ⟶ ((λy.ka) b) ⟶ ka,

while the evaluation of N requires three (n-ary) βreductions:

N ⟶ ((λm.mkb) (λk_{2}y.k_{2}a))
⟶ ((λk_{2}y.k_{2}a) k b)
⟶ ka.

Since the extra (administrative) reduction in the evaluation of N is completely predicable from the source term, the function F2_{k} optimizes it away.

4 Transforming CPS programs

With the elimination of all administrative redexes, we can turn our attention to “interesting” βη transformations on CPS programs.

Plotkin [17] was the first to offer some insights about the relation between reductions on source terms and CPS terms. In a comparative study of equational theories for call-by-value languages and call-by-name languages, he proved the following theorem.

Theorem 4.1 (Plotkin [17]) Let M, N ∈ Λ.

1. λ_{v} ⊢ M = N implies λ_{v} ⊢ F[[M]] = F[[N]];

2. λ_{v} ⊢ F[[M]] = F[[N]] does not imply λ_{v} ⊢ M = N;

3. λ_{v} ⊢ F[[M]] = F[[N]] iff λ ⊢ F[[M]] = F[[N]].

In short, β-reductions prove more equations on CPS terms than β_{v}-reductions prove on source terms. The effect of η-reductions on CPS terms is unknown. Our goal is to remedy this situation by deriving a set of reductions A such that:

λ_{v}A ⊢ M = N iff λβη ⊢ F2_{k}[[M]] = F2_{k}[[N]]

We illustrate some of the complications that this problem poses with a specific reduction on CPS terms:

((λx.((x k) z)) (λk.λy.ky)) ⟶ (((λk.λy.ky) k) z).

By inspection, the left-hand side is:

F2_{k}[[((λx.xz) (λy.y))]].

A quick glance at the right hand side reveals that it contains an administrative redex and hence cannot be F2_{k}[[M]] for any M ∈ Λ. The right hand side is, however, provably equal to a number of CPS terms;

\begin{aligned}λβη ⊢ & & F2_{k}[[((λa.((λx.xa) (λy.y))) z)]] \\ & = & F2_{k}[[((λy.y) z)]] \\ & = & (((λk.λy.ky) k) z). \end{aligned}

Assuming we choose ((λy.y) z) as the official “inverse” of the right hand side, then the CPS reduction corresponds to the following β_{v}-reduction:

((λx.xz) (λy.y)) ⟶ ((λy.y) z)

on source terms. The other choice corresponds to a β_{v}- expansion which is clearly undesirable.

Inspired by the above example, we proceed as follows:

1. We explicitly define the set of CPS terms. The definition relies on a one-pass CPS transformation equivalent to F2_{k} (Section 5).

2. We define an “inverse” CPS transformation and formalize its precise relationship to the CPS transformation (Section 6).

3. We derive the set A. For each notion of reduction P ⟶ Q on CPS terms, we apply the inverse transformation to P and Q and get the source terms M and N. If λ_{v} ⊢ M = N, then we are done. Otherwise, we add appropriate reductions to A (Section 7).

5 A compactifying CPS transformation and the CPS language

The one-pass CPS transformation should combine the modified Fischer transformation with the application of \overline{β}- and \overline{η}-reductions. An informal description of what these reductions accomplish will clarify the nature of such a function.

The most informative kind of administrative redexes appears in the translation of ((λx.M) V) in an arbitrary continuation K:

2This is slightly inaccurate. In both Steele’s Rabbit and the Danvy/Filinski CPS transformations, the continuation is the second parameter to a procedure. Thus, their output is actually:

((λxk_{1}.(k_{1} λyk_{2}.k_{2}x)) a (λm.mbk)).

Even though this term only contains source redexes, we could still optimize it by equational reasoning as the following derivation shows:

((λxk_{1}.(k_{1}λyk_{2}.k_{2}x)) a (λm.mbk))

⟶ ((λm.mbk) (λyk_{2}.k_{2}a))

⟶ ((λyk_{2}.k_{2}a) b k)

⟶ ka ⟵ ((λy.ka) b)

⟵ ((λx.((λy.kx) b)) a).

Indeed, the “net” effect of such transformations is that of performing administrative reductions only!

((\overline{λ}k.((\overline{λ}k.k (\overline{λ}k.λx.F[[M]] k))
(\overline{λ}m.((\overline{λ}k.k Ψ[[V]]) (\overline{λ}n.(mk)n)))))
K).

The expression reduces to:

(((\overline{λ}k.λx.F[[M]] k) K) Ψ[[V]]).

At this point, the following \overline{β}-reduction takes place:

(((\overline{λ}k.λx.F[[M]] k) K) Ψ[[V]]) ⟶ ((λx.F[[M]] K) Ψ[[V]])

i.e., the image of the abstraction absorbs the continuation of the application. For the source terms, this means that the body of an abstraction in application position absorbs the syntactic representation of the continuation, which is the evaluation context [7]. Thus, a program of the shape E[((λx.M) V)] where E represents K, must be translated as if it had been written as ((λx.E[M]) V).

Put differently, our CPS transformation “symbolically” evaluates redexes by lifting them to the root of the program. For applications of values to values inside of λ-abstractions, this means of course that it takes the evaluation contexts with respect to the closest λ, which will become the root of the program once the redex is discharged. The resulting transformation, C_{k}, is parametrized over a variable k that represents the continuation of the entire program.

Definition 5.1. (C_{k}, Φ, K_{k}) The CPS transformation uses three mutually recursive functions: C_{k} to transform terms, Φ to transform values, and K_{k} to transform evaluation contexts. Let k, u ∈ Vars be variables that do occur in the argument to C_{k}.

\begin{aligned}C_{k} : Λ & → & Λ \\ C_{k}[[V]] & = & (k Φ[[V]]) \\ C_{k}[[E[(x V)]]] & = & ((x K_{k}[[E]]) Φ[[V]]) \\ C_{k}[[E[((λx.M) V)]]] & = & ((λx.C_{k}[[E[M]]]) Φ[[V]]) \end{aligned}

\begin{aligned}Φ[[x]] & = & x \\ Φ[[λx.M]] & = & \overline{λ}k.λx.C_{k}[[M]] \\ K_{k}[[[ ]]] & = & k \\ K_{k}[[E[(x [ ])]]] & = & (x K_{k}[[E]]) \\ K_{k}[[E[((λx.M) [ ])]]] & = & (λx.C_{k}[[E[M]]]) \\ K_{k}[[E[([ ] M)]]] & = & (\overline{λ}u.C_{k}[[E[(u M)]]]) \end{aligned}

An informal examination of the definition of C_{k} reveals that the translation of every expression refers to an expression of smaller “size”.

Definition 5.2. (Size) The size of a term M, |M|, is the number of variables in M (including binding occurrences). The size of a context E, |E|, is the number of variables in E (including binding occurrences) plus 2. (Because the empty context replaces a redex which has at least size 2, the size of the empty context is 2.)

Hence, the function C_{k} is well-defined.

Proposition 5.3 The function C_{k} is total.

Proof Sketch. The proof is by induction on the size of the argument to C_{k} or K_{k} and proceeds by cases on possible inputs to the two functions.

As expected the output of C_{k} does not contain any administrative redexes.

Lemma 5.4 If M ∈ Λ, C_{k}[[M]] is in \overline{β}\overline{η}-normal form.

Proof Sketch. By induction on the size of the argument to C_{k} or K_{k}.

Most importantly, the output of the new CPS transformation is equivalent to the output of F2_{k}.

Proposition 5.5 Let M ∈ Λ. Then,

λ\overline{β}\overline{η} ⊢ (F[[M]] k) ⟶ ⟶ C_{k}[[M]].

Proof Sketch. The essential steps in the proof are:

1. Define a natural extension of the modified Fischer transformation that acts on contexts such that F[[[ ]]] = \overline{λ}k.k.

2. By a simple induction on the structure of E, prove:

λ\overline{β} ⊢ (F[[E[M]]] k) = (F[[M]] (F[[E]] k)).

3. By induction on the size of M, prove that:

λ\overline{β}\overline{η} ⊢ (F[[M]] k) = C_{k}[[M]].

4. The result follows from the last claim because C_{k}[[M]] is in \overline{β}\overline{η}-normal form (Lemma 5.4) and \overline{β}\overline{η}- normal forms are unique (Lemma 3.7).

With the completion of the analysis of C_{k}, the decorating overlines become irrelevant. Therefore, in the remainder of the paper, we ignore the distinction between λ and \overline{λ}.

Next, we turn to the definition of our universe of discourse, the set of CPS terms. It must include all terms that contribute to the proofs of equations of the form:

λβη ⊢ C_{k}[[M]] = C_{k}[[N]].

Since βη is CR [2], it is sufficient to consider equations of the form:

λβη ⊢ C_{k}[[M]] ⟶ ⟶ P.

Hence, the interesting set of CPS terms is:

S ≡^{df} {P | ∃M ∈ Λ.λβη ⊢ C_{k}[[M]] ⟶ ⟶ P }.

The definition of the transformation C_{k} provides some insight about an inductive characterization of the set of CPS terms. According to the right hand sides of the equations in Definition 5.1 all terms in the CPS language are an application of a continuation to a value. Values are either variables or abstractions (continuation transformers). Continuations are either variables, or the result of the application of a value to a continuation, or a regular lambda abstraction. Therefore, we claim that S is generated by the following grammar.

Definition 5.6. (CPS grammar) Let x ∈ Vars\{k}:

cps(Λ) :  P ::= (K W)
cps(Values) :  W ::= x | (λk.K)
cps(EvCont) :  K ::= k | (W K) | (λx.P)

Note: The special status reserved for the variable k ensures that the continuation parameter occurs exactly once in each abstraction λk.K. When working with the quotient of the language under α-equivalence, the special status of k disappears.

The following theorem justifies the above claim by establishing the equivalence of the two definitions of the set of CPS terms.

Theorem 5.7 S = cps(Λ).

Proof. It is easy to prove that for M ∈ Λ, C_{k}[[M]] ∈ cps(Λ). The rest follows from Lemmas 5.8 and 5.9.

Since βη-reductions preserve the syntactic categories in the CPS language, the set S is a subset of cps(Λ).

Lemma 5.8 Let P_{1} ∈ cps(Λ), W_{1} ∈ cps(Values), and K_{1} ∈ cps(EvCont). Then,

• if λβη ⊢ P_{1} ⟶ P_{2} then P_{2} ∈ cps(Λ);

• if λβη ⊢ W_{1} ⟶ W_{2} then W_{2} ∈ cps(Values);

• if λβη ⊢ K_{1} ⟶ K_{2} then K_{2} ∈ cps(EvCont).

For the opposite implication, i.e., that cps(Λ) is a subset of S, it is sufficient that every P ∈ cps(Λ) is reachable from Λ via C_{k} and βη.

Lemma 5.9 For all P ∈ cps(Λ), there exists an M ∈ Λ such λβη ⊢ C_{k}[[M]] ⟶ ⟶ P.

Proof. The proof is by lexicographic induction on ⟨G̃, |G|⟩ where G is an element P of cps(Λ) or an element K of cps(EvCont), G̃ is the number of abstractions of the form λk.K in G, and |G| is the number of variables (including binding occurrences) in G.

6 An Inverse CPS Transformation

Based on the inductive definition of the CPS language, the specification of an “inverse” to the CPS transformation is almost straightforward: the source term corresponding to the application of a continuation K to a value W is simply E[V] where E is the evaluation context that syntactically represents the continuation K and V is the value that corresponds to W. The definition of the function C^{−1} (un-CPS) uses two auxiliary functions to translate continuations to evaluation contexts and values in the CPS language to values in the source language. Both definitions are straightforward.

Definition 6.1. (C^{−1}, Φ^{−1}, K^{−1})

C^{−1} : cps(Λ) → Λ
C^{−1}[[(K W)]] = K^{−1}[[K]][Φ^{−1}[[W]]]
Φ^{−1}[[x]] = x
Φ^{−1}[[(λk.k)]] = λx.x
Φ^{−1}[[(λk.W K)]] = λx.C^{−1}[[(W K) x]]
Φ^{−1}[[(λk.λx.P)]] = λx.C^{−1}[[P]]
K^{−1}[[k]] = [ ]
K^{−1}[[(x K)]] = K^{−1}[[K]][(x [ ])]
K^{−1}[[((λk.K_{1}) K_{2})]] = K^{−1}[[K_{1}[k := K_{2}]]]
K^{−1}[[(λx.P)]] = ((λx.C^{−1}[[P]]) [ ])

Intuitively, C^{−1} is the “inverse” of C, Φ^{−1} is the “inverse” of Φ, and K^{−1} is the “inverse” of K. Moreover, C^{−1}, Φ^{−1}, and K^{−1} apply to the syntactic categories cps(Λ), cps(Values), and cps(EvCont) respectively and yield terms in the appropriate syntactic categories in the source language.

Lemma 6.2 C^{−1}[[P]] ∈ Λ, Φ^{−1}[[W]] ∈ Values, and K^{−1}[[K]] ∈ EvCont.

Proof Sketch. The proof is based on the same idea as the proof of Lemma 5.9.

For two distinct reasons, C^{−1} cannot be a complete inverse of C_{k}. First, some CPS terms are the image of more than one source term. Second, some CPS terms are not the image of any source term. The first fact is a property of the function C_{k} that reduces administrative redexes on the fly. The second one is due to the closure of the set of CPS terms under βη-reductions. We discuss each point in detail below.^{3}

The effect of administrative reductions: The function C_{k} incorporates the reduction of all administrative redexes from the output of the Fischer CPS. Hence, if F[[M]] and F[[N]] reduce to a common term by administrative reductions only, C_{k}[[M]] is identical to C_{k}[[N]]. The definition of the function C_{k} shows that, in two cases, different inputs are indeed mapped to the same output.

3Danvy and Lawall [3, 6] define a direct style transformation that maps CPS terms into source terms. To get an inverse of the Danvy/Filinski CPS [5], they have to restrict the domain of their direct style transformation to images of Λ terms. Hence, the Danvy-Lawall inverse is not applicable in situations that involve βη-transformations of CPS programs.

• The first equivalence is:

C_{k}[[E[((λx.M) N)]]] ≡ C_{k}[[((λx.E[M]) N)]].

The equation illustrates how the CPS transformation uses its knowledge about the continuation of an application. As indicated in Section 4, it “lifts” the application to top level and merges the continuation with the body of the application.

• The second equivalence is:

C_{k}[[E[((M N) L)]]] ≡ C_{k}[[((λx.E[(x L)]) (M N))]]

This equation captures another essential element of CPS transformations. According to folklore in the functional compiler-building community [4], the first aspect of a CPS transformation is to give the value of every application a name. In the above equation, the argument to C_{k} in the right hand side is a “flattened” version of the left hand side in which the nested application (M N) is factored out and given a name.

In summary, we define two reductions on Λ that capture the effect of the administrative reductions performed by C_{k}:

\begin{matrix}E[((λx.M) N)] & ⟶ & ((λx.E[M]) N) & (β_{lift}) \\ E[((M N) L)] & ⟶ & \begin{matrix}((λx.E[(x L)]) \\ (M N)) \end{matrix} & (β_{flat}) \end{matrix}

By the variable conventions, x ∉ F V (E, L) in the above reductions.

The reductions β_{lift} and β_{flat} define equivalence classes of source terms that map to the same CPS term. The function C^{−1} maps this CPS term to a particular representative of the equivalence class: the element in β_{lift}β_{flat}-normal form.

Lemma 6.3 Let P ∈ cps(Λ). Then, C^{−1}[[P]] is in β_{lift}β_{flat}-normal form.

Proof Sketch. The proof is by induction on the same lexicographic measure as the proof of Lemma 5.9.

It follows that C^{−1} is an inverse of C_{k} on the subset of source terms in β_{lift}β_{flat}-normal form.

Theorem 6.4 Let M ∈ Λ, P ∈ cps(Λ).

1. λβ_{lift}β_{flat} ⊢ M ⟶ ⟶ (C^{−1} ∘ C_{k})[[M]].

2. (C^{−1} ∘ C_{k})[[M]] ≡ M for M = C^{−1}[[P]].

The closure of the set of CPS terms under βηreductions: Because of arbitrary βη-reductions, the set of CPS terms includes terms that are not the image of any source term. For example, the following ηreduction generates such a term:

C_{k}[[λx.x]] = λk.λx.kx ⟶ λk.k The function C^{−1} (conceptually) coerces λk.k first to λk.λx.kx, i.e., C^{−1}[[λk.k]] = C^{−1}[[λk.λx.kx]] = λx.x.

Thus, P is generally not identical to (C_{k} ∘ C^{−1})[[P]]. However, C_{k} is the inverse of C^{−1} on the subset of CPS terms that are images of source terms.

Theorem 6.5 Let P ∈ cps(Λ), M ∈ Λ.

1. λβη ⊢ (C_{k} ∘ C^{−1})[[P]] = P.

2. (C_{k} ∘ C^{−1})[[P]] ≡ P for P = C_{k}[[M]].

Proof Sketch. The proof is by induction on the same lexicographic measure as the proof of Lemma 5.9.

7 Completeness and Soundness

Using the partial inverse of the CPS transformation, we can systematically derive a set of additional axioms A for λ_{v} such that λ_{v}A is complete for βη reasoning about CPS programs. Once we have the new axiom set, we prove its soundness in the second subsection. In the last subsection, we briefly discuss the connection to Moggi’s computational λ-calculus.

7.1 Completeness

By inspection of the inductive definition of the CPS language, the possible β- and η-reductions on CPS terms are as follows:

\begin{matrix}((λx.P) W) & ⟶ & P [x := W] & (β_{w}) \\ ((λk.K_{1}) K_{2}) & ⟶ & K_{1}[k := K_{2}] & (β_{k}) \\ (λk.W k) & ⟶ & W & (η_{w}) \\ (λx.Kx) & ⟶ & K x ∉ F V (K) & (η_{k}) \end{matrix}

Put differently, for cps(Λ), β = β_{w} ∪β_{k} and η = η_{w} ∪η_{k}. We outline the derivation of reductions corresponding to η_{k}. Let (λx.Kx) ⟶ K where x ∉ F V (K). Applying K^{−1} to both sides of the reduction, we get:

((λx.C^{−1}[[Kx]]) [ ]) ⟶ K^{−1}[[K]].

To understand how the left hand side could reduce to the right hand side, we proceed by case analysis on K:

• K ≡ k: The reduction becomes:

((λx.x) [ ]) ⟶ [ ].

Since the empty context generally stands for an arbitrary expression, A should therefore contain the reduction:

((λx.x) M) ⟶ M  (β_{id})

• K ≡ (y K_{1}): The reduction becomes:

((λx.K^{−1}[[K_{1}]][(y x)]) [ ]) ⟶ K^{−1}[[K_{1}]][(y [ ])].

By a similar argument as above, we must add the following reduction to A:

((λx.E[(y x)]) M) ⟶ E[(y M)]  (β_{Ω})

((λx.M) V) ⟶ M[x := V]  (β_{v})
(λx.V x) ⟶ V  x ∉ F V (V)  (η_{v})
E[((λx.M) N)] ⟶ ((λx.E[M]) N)  x ∉ F V (E)  (β_{lift})
E[((M N) L)] ⟶ ((λx.E[(x L)]) (M N))  x ∉ F V (E, L)  (β_{flat})
((λx.x) M) ⟶ M  (β_{id})
((λx.E[(y x)]) M) ⟶ E[(y M)]  x ∉ F V (E[y])  (β_{Ω})

Figure 1: Source Reductions: A ≡^{df} {η_{v}, β_{lift}, β_{flat}, β_{id}, β_{Ω}}

• K ≡ ((λk.K_{1}) K_{2}): The reduction becomes:

((λx.C^{−1}[[K_{1}[k := K_{2}] x]]) [ ]) ⟶ K^{−1}[[K_{1}[k := K_{2}]]].

Since the term (K_{1}[k := K_{2}] x) has one less λk.K abstraction than K, the inductive hypothesis provides an appropriate equivalence.

• K ≡ λy.P: By an β_{v}-reduction, the left hand side ((λx.((λy.C^{−1}[[P]]) x)) [ ]) reduces to ((λx.C^{−1}[[P]][y := x]) [ ]), which is identical to the right hand side.

The cases for the other reductions on CPS terms are similar but with more complicated proofs. The resulting set of source reductions, A, includes all the previously derived reductions and η_{v}: see Figure 1.

Figure 2 summarizes the source reductions corresponding to each CPS reduction. A β_{w}-reduction corresponds essentially to a β_{v}-reduction on source terms. Similarly, an η_{w}-reduction corresponds to η_{v}. However, the reduction of a β_{w} redex might create some administrative redexes for the management of continuations. The reductions of these redexes correspond to β_{lift}β_{id}β_{Ω}-reductions on source terms.

By pasting together the proofs of the lemmas corresponding to each reduction, we get the following completeness theorem.

Theorem 7.1 (Completeness) If λβη ⊢ P ⟶ ⟶ Q then λ_{v}A ⊢ C^{−1}[[P]] ⟶ ⟶ C^{−1}[[Q]].

7.2 Soundness

The set of source reductions in Figure 1 is sound with respect to the equational theory over CPS terms. In other words, for a source reduction M ⟶ N, we have λβη ⊢ C_{k}[[M]] = C_{k}[[N]]. In fact, we can prove the stronger results of Figure 3. The Soundness theorem is a direct consequence of these results.

Theorem 7.2 (Soundness) If λ_{v}A ⊢ M ⟶ ⟶ N then λβη ⊢ C_{k}[[M]] ⟶ ⟶ C_{k}[[N]].

7.3 Correspondence

Unfortunately, if C_{k}[[M]] reduces to C_{k}[[N]], it is not necessarily the case that M reduces to N. A proof that C_{k}[[M]] reduces to C_{k}[[N]] in the CPS calculus translates to a proof that C^{−1}[[C_{k}[[M]]]] reduces to C^{−1}[[C_{k}[[N]]]] in the source calculus. Unless N is in β_{lift}β_{flat}-normal form, the latter proof does not imply that M ⟶ ⟶ N. Still, M is always provably equal to N.

Theorem 7.3 (Correspondence) The calculi λβη and λ_{v}A are equivalent in the following sense:

1. λ_{v}A ⊢ M = (C^{−1} ∘ C_{k})[[M]].

2. λβη ⊢ P = (C_{k} ∘ C^{−1})[[P]].

3. λ_{v}A ⊢ M = N iff λβη ⊢ C_{k}[[M]] = C_{k}[[N]].

4. λβη ⊢ P = Q iff λ_{v}A ⊢ C^{−1}[[P]] = C^{−1}[[Q]].

Note: Other CPS transformations. The correspondence theorem does not depend on any specific aspects of C_{k} or F. Rather the result is valid for any CPS transformation cps that satisfies the following condition for M ∈ Λ:

λβη ⊢ F[[M]] = cps(M).

7.4 The computational λ-calculus

The calculus λ_{v}A is equivalent to an untyped variant of Moggi’s computational λ-calculus λ_{c} [16]. Specifically, we ignore the types of expressions, eliminate product and computational expressions, re-interpret Moggi’s let-expression as the usual abbreviation for a λ-application, and apply his let-axioms to the expanded expressions. The basic reductions of our variant of λ_{c} are β_{v}, η_{v}, β_{id} plus the additional reductions of Figure 4.

We prove the equivalence of our calculus and λ_{c} by showing how each calculus proves the reductions of the other. First, there is a set of common rules: β_{v}, η_{v}, and β_{id}. Moreover, Comp is an instance of β_{lift} and let.1 an instance of β_{flat}. Finally, let.2 is simply an η_{v} expansion. This establishes one direction of the equivalence. For the reverse direction, it is sufficient to show that λ_{c} proves β_{lift}, β_{flat}, and β_{Ω} for the cases when E is empty, E ≡ (V [ ]), and E ≡ ([ ] M).

If λβ_{w} ⊢ P ⟶ Q then λβ_{v}β_{lift}β_{id}β_{Ω} ⊢ C^{−1}[[P]] ⟶ ⟶ C^{−1}[[Q]]
If λβ_{k} ⊢ P ⟶ Q then  C^{−1}[[P]] ≡ C^{−1}[[Q]]
If λη_{w} ⊢ P ⟶ Q then λη_{v}  ⊢ C^{−1}[[P]] ⟶ ⟶ C^{−1}[[Q]]
If λη_{k} ⊢ P ⟶ Q then λβ_{v}β_{id}β_{Ω}  ⊢ C^{−1}[[P]] ⟶ ⟶ C^{−1}[[Q]]

Figure 2: The Completeness Lemma

If λβ_{v}  ⊢ M ⟶ N then λβ  ⊢ C_{k}[[M]] ⟶ ⟶ C_{k}[[N]]
If λη_{v}  ⊢ M ⟶ N then λη_{w}η_{k} ⊢ C_{k}[[M]] ⟶ ⟶ C_{k}[[N]]
If λβ_{lift} ⊢ M ⟶ N then  C_{k}[[M]] ≡ C_{k}[[N]]
If λβ_{flat} ⊢ M ⟶ N then  C_{k}[[M]] ≡ C_{k}[[N]]
If λβ_{id} ⊢ M ⟶ N then λη_{k}  ⊢ C_{k}[[M]] ⟶ ⟶ C_{k}[[M]]
If λβ_{Ω} ⊢ M ⟶ N then λη_{k}  ⊢ C_{k}[[M]] ⟶ ⟶ C_{k}[[N]]

Figure 3: The Soundness Lemma

((λx_{2}.M) ((λx_{1}.M_{2}) M_{1})) ⟶ ((λx_{1}.((λx_{2}.M) M_{2})) M_{1})  (Comp)
((M N) L) ⟶ ((λx.x L) (M N))  (let.1)
(V (M N)) ⟶ ((λx.V x) (M N))  (let.2)

Figure 4: Additional Reductions for the Computational λ-calculus

Based on the above argument, the correspondence of the calculi yields the following reformulation of the Correspondence theorem.

Theorem 7.3′ (Correspondence (Reformulation)) The calculi λβη and λ_{c} are equivalent in the sense of Theorem 7.3.

8 Conclusion and Future Research

The interest in calculi is motivated by their soundness with respect to observational equivalence (see Section 2). Therefore, the natural question is whether our extension is sound with respect to the call-by-value observational equivalence relation. Moggi [16] proves the result in a typed setting. It follows that our extension is sound for reasoning about typed CPS programs, for example in a language like (full) ML.

For dynamically typed languages like Lisp or Scheme, the λ_{c}-calculus is unsound since it includes the axiom η_{v} (See Section 2). As all other axioms are sound with respect to call-by-value observational equivalence, the relevant reductions for untyped languages are:

A^{−} ≡^{df} {β_{lift}, β_{flat}, β_{id}, β_{Ω}}.

By the Completeness and Soundness lemmas (Figures 2 and 3 respectively) the corresponding CPS calculus is λβη_{k}.

Theorem 7.3′′ (Correspondence (Untyped))

The calculi λβη_{k} and λ_{v}A^{−} are equivalent in the sense of Theorem 7.3.

In summary, our extensions of the λ_{v}-calculus result in an equational theory over Λ that is sound with respect to the call-by-value observational equivalence, and corresponds to λβη (or λβη_{k}) over CPS terms. Moreover, the result extends to languages with ground constants and primitive functions and languages with imperative assignment procedures for data structures.

For languages with Scheme-like control operators, our extension of λ_{v}-calculus is still sound with respect to observational equivalence. However, the correspondence theorem fails since operators like call/cc manipulate their continuation in non-standard ways. To re-establish the correspondence theorem for such languages, we need to find an extension for the λ-control calculus [8, 9] that corresponds to λβη on CPS terms.

References

1. Appel, A. and T. Jim. Continuation-passing, closure-passing style. In Proc. 16th ACM Symposium on Principles of Programming Languages, 1982, 293–302.

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

3. Danvy, O. Back to direct style. In 4th Proc. European Symposium on Programming. Springer Lecture Notes in Computer Science, 582. Springer Verlag, Berlin, 1992, 130–150.

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

5. Danvy, O. and A. Filinski. Representing control: A study of the CPS transformation. Tech. Rpt. CIS-91-2. Kansas State University, 1991.

6. Danvy, O. and J. Lawall. Back to direct style II: First-class continuations. In Proc. 1992 ACM Conference on Lisp and Functional Programming, 1992, this volume.

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

8. Felleisen, M. and R. Hieb. The revised report on the syntactic theories of sequential control and state. Technical Report 100, Rice University, June 1989. Theor. Comput. Sci., 1991, to appear.

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

10. Fischer, M.J. Lambda calculus schemata. In Proc. ACM Conference on Proving Assertions About Programs, SIGPLAN Notices 7(1), 1972, 104–109.

11. Gateley, J. and B.F. Duba. Call-by-value combinatory logic and the lambda-value calculus. In Proc. 1991 Workshop on Mathematical Foundations of Programming Semantics. Lecture Notes in Computer Science 517, to appear.

12. Hieb R., R. K. Dybvig, and C. Bruggeman. Representing control in the presence of first-class continuations. In Proceedings of the SIGPLAN ’90 Conference on Programming Language Design and Implementation, June 1990, 66–77.

13. Kranz, D., et al. ORBIT: An optimizing compiler for Scheme. In Proc. SIGPLAN 1986 Symposium on Compiler Construction, SIGPLAN Notices 21(7), 1986, 219–233.

14. Landin, P.J. The mechanical evaluation of expressions. Comput. J. 6(4), 1964, 308–320.

15. Leroy, X. The Zinc experiement. Technical Report 117. INRIA, 1990.

16. Moggi, E. Computational lambda-calculus and monads. In Proc. Symposium on Logic in Computer Science, 1989, 14–23. Also appeared as: LFCS Report ECS-LFCS-88-66, University of Edinburgh, 1988.

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

18. Reynolds, J.C. Definitional interpreters for higher-order programming languages. In Proc. ACM Annual Conference, 1972, 717–740.

19. Shivers, O. Control-flow Analysis of Higher-Order Languages or Taming Lambda. Ph.D. dissertation, Carnegie-Mellon University, 1991.

20. Steele, G.L., Jr. RABBIT: A compiler for SCHEME. Memo 474, MIT AI Lab, 1978.