Reasoning about Programs in

Continuation-Passing Style

Amr Sabry Matthias Felleisen Department of Computer Science

Rice University Houston, TX 77251-1892

Technical Report (Rice TR 92-180 ).

A preliminary version of this paper appeared in

Lisp and Functional Programming June 22-24, 1992, San Francisco, California.

Copyright \begin{matrix}c \\ ◯ \end{matrix}1992 by Amr Sabry and Matthias Felleisen First Edition: May 28, 1992

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 βη-transfor-mations 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, 16, 24, 25] utilize some variant of the Fischer-Reynolds continuation-passing style (CPS) transformation [10, 23]. 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 [15] or Zinc [18], 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 [22] showed in 1974, the λ_{v}-calculus does not suffice. Thus we refine this question as follows:

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

Is there a set of axioms, A, that extends 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 [13]. 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 call-by-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 [21] 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. The last two sections present corollaries of our result. The first discusses the typed and untyped versions of the calculi and their soundness with respect to observational equivalence. The second is a correspondence between the extension of the λ_{v}-calculus and the CPS type structure.

2 Λ: Calculi and 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)  (Λ)
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). A term is closed if it has no free variables; the set of closed terms is denoted by Λ^{0}. 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 capture-free 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:

((λx.M) N) ⟶ M[x := N]  N : arbitrary  (β)
((λx.M) V) ⟶ M[x := V]  V : Value  (β_{v})
λx.Mx ⟶ M  x ∉ F V (M)  (η)
λx.V x ⟶ V  x ∉ F V (V)  (η_{v})

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]  for all contexts C  (Compatibility)
M = M  (Reflexivity)
M = L, L = N ⇒ M = N  (Transitivity)
M = N ⇒ N = M  (Symmetry)

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 Symmetry, 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 [17] and the CEK machine [7].

An equivalent method for specifying the semantics is based on the Curry-Feys Standard Reduction theorem [7, 22]. 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} & ::= & [ ] | (V E_{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 (V E_{n}).

Given evaluation contexts, the definitions of the standard reduction functions for callby-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.

An important fact for the discussions below is that the syntax of the call-by-value language Λ can be redefined as follows:

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

The set of evaluation contexts has also the following equivalent definition:

E ::= [ ] | E[(V [ ])] | E[([ ] M)]  (EvCont)

We use all the definitions interchangeably. Moreover, we extend the notions of reductions to evaluation contexts by treating the hole as a placeholder for an arbitrary expression. For example, the reduction:

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

is a β-reduction; it is not a β_{v}-reduction.

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 parameter-passing 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 “continuation-passing style” appeared in the midsixties. 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 defined as follows.

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 [23] investigated definitional interpreters for higher-order languages. One of 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.^{1} Plotkin [22] later proved Reynolds’ ideas correct.

Theorem 3.2 (Plotkin [22]) 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 [22] 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 [22] 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, 16, 24, 25] use special algorithms to minimize the size of their outputs.

1In Reynolds’s transformation the continuation is the second argument to a procedure.

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

• 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 nontermination. 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, is the following.

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

The following proposition establishes that F2 is well-defined.

Proposition 3.5 F2 is a total function.

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

2See also the discussion of this idea by Danvy and Filinski [5].

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

It remains to establish that all \overline{β}\overline{η}-reduction paths terminate.

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

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

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

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

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

The evaluation of M requires two β-reductions:

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

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

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

Since the extra (administrative) reduction in the evaluation of N is completely predictable from the source term, the function F2 optimizes it away.

3This 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:

λk.((λ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:

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

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

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

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

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

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

4 Transforming CPS programs

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

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

Theorem 4.1 (Plotkin [22]) 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 is unknown. Moreover, the induced observational equivalence relations do not correspond.

Corollary 4.2 (Plotkin [22]) Let M, N ∈ Λ.

1. F[[M]] ≅_{n} F[[N]] implies M ≅_{v} N;

2. M ≅_{v} N does not imply F[[M]] ≅_{n} F[[N]].

In the second part of the corollary, the terms F[[M]] and F[[N]] fail to be observationally equivalent in contexts that manipulate the continuation in “non-standard” ways. We return to the observational equivalence relations and their correspondence in Section 8.

Our more immediate goal is to derive a set of axioms A such that:

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

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

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

By inspection, the left-hand side is:

F2[[((λx.xz) (λy.y))]].

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

λβη ⊢ F2[[((λa.((λx.xa) (λy.y))) z)]] = F2[[((λy.y) z)]] = λk.(((λk.λy.ky) k) z).

Assuming we choose ((λy.y) z) as the “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 (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 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 a redex ((λx.M) V) in an arbitrary continuation K:

((\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]])

via a number of \overline{β}\overline{η}-reductions. 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 of the redex [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 current continuation.

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_{i} ∈ Vars be variables that do not occur in the argument to C_{k}.^{4}

\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_{i}.C_{k}[[E[(u_{i} M)]]]) \end{aligned}

An informal examination of the above definition reveals that the function is not defined by structural recursion. Still, it is relatively easy to check that with an appropriate notion of “size”, the translation of every expression refers to the translation of a smaller expression. In particular, the size of E[(u_{i} M)] is smaller than the size of E[([ ] M)] because the empty context always replaces an application. The formal definition of “size” is as follows.

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.

As expected, the output of C_{k} is equivalent to the output of F2, which also proves that C_{k} is well-defined.

Proposition 5.3 Let M ∈ Λ. Then, F2[[M]] ≡ λk.C_{k}[[M]].

Proof. The essential steps in the proof are:

1. Define a natural extension of the modified Fischer transformation that accepts evaluation contexts: (Definition 5.4). Next, prove that:

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

2. Using the previous result, prove that:

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

4The CPS transformation C_{k} is related to the CPS transformation by Friedman, Wand, and Haynes [11:

ch 8], but differs significantly in several technical aspects.

3. The result follows because C_{k}[[M]] is in \overline{β}\overline{η}-normal form (Lemma 5.6) and \overline{β}\overline{η}-normal forms are unique (Lemma 3.6).

The extension of F that accepts evaluation contexts is as follows.

Definition 5.4. (Extension of the Fischer CPS) Let k, m, n ∈ Vars as in Definition 3.1:

\begin{aligned}F : EvCont & → & Λ \\ F[[[ ]]] & = & \overline{λ}k.k \\ F[[(V E)]] & = & \overline{λ}k.F[[V]] \overline{λ}m.F[[E]] \overline{λ}n.(m k) n \\ F[[(E M)]] & = & \overline{λ}k.F[[E]] \overline{λ}m.F[[M]] \overline{λ}n.(m k) n \end{aligned}

The following lemma establishes an important property of evaluation contexts. Intuitively, the evaluation of E[M] in a continuation K is identical to the evaluation of M in a continuation that combines E and K.

Lemma 5.5 Let M ∈ Λ, E ∈ EvCont. Then, λ\overline{β} ⊢ (F[[E[M]]] k) = (F[[M]] (F[[E]] k)).

Proof Idea. The proof is by induction on the structure of E.

It remains to establish that the output of F is provably equal to the output of C_{k} and that the latter is in \overline{β}\overline{η}-normal form.

Lemma 5.6 Let M ∈ Λ, E ∈ EvCont. Then,

1. λ\overline{β}\overline{η} ⊢ (F[[M]] k) = C_{k}[[M]] and λ\overline{β}\overline{η} ⊢ (F[[E]] k) = K_{k}[[E]];

2. C_{k}[[M]] and K_{k}[[E]] are in \overline{β}\overline{η}-normal form.

Proof. The proof is by induction on the size of G, where G is the argument to C_{k} or K_{k}. We proceed by case analysis on the possible inputs:

1. G ≡ V: then, λ\overline{β}\overline{η} ⊢ (F[[G]] k) = ((\overline{λ}k.k Ψ[[G]]) k) = (k Ψ[[G]]). By cases:

(a) G ≡ x: then (k Ψ[[G]]) ≡ (k x) ≡ C_{k}[[x]]. Moreover, C_{k}[[x]] is in \overline{β}\overline{η}-normal form.

(b) G ≡ λx.M: then (k Ψ[[G]]) ≡ (k \overline{λ}c.λx.F[[M]]c). By the inductive hypothesis λ\overline{β}\overline{η} ⊢ (F[[M]] c) = C_{c}[[M]] and C_{c}[[M]] is in \overline{β}\overline{η}-normal form. Therefore λ\overline{β}\overline{η} ⊢ (F[[λx.M]] k) = C_{k}[[λx.M]] and C_{k}[[λx.M]] is in \overline{β}\overline{η}-normal form.

2. G ≡ E[(x V)]: then λ\overline{β}\overline{η} ⊢ (F[[G]] k) = (F[[(x V)]] (F[[E]] k)) by Lemma 5.5. The latter term is provably equal to ((x F[[E]]k) Ψ[[V]]). There are two cases:

(a) V ∉ Vars: then |E| < |G|. By the inductive hypothesis, λ\overline{β}\overline{η} ⊢ F[[E]]k = K_{k}[[E]] and K_{k}[[E]] is in \overline{β}\overline{η}-normal form. By an argument similar to case 1, λ\overline{β}\overline{η} ⊢ Ψ[[V]] = Φ[[V]] and Φ[[V]] is in \overline{β}\overline{η}-normal form. Both results follow since

C_{k}[[G]] ≡ ((x K_{k}[[E]]) Φ[[V]]).

(b) V ∈ Vars: then |E| = |G| and the inductive hypothesis does not apply. By inlining the arguments in cases 4 to 7, λ\overline{β}\overline{η} ⊢ (F[[E]] k) = K_{k}[[E]] and K_{k}[[E]] is in \overline{β}\overline{η}-normal form. The result follows as in subcase (a).

3. G ≡ E[((λx.M) V)]: then λ\overline{β}\overline{η} ⊢ F[[G]]k = (F[[((λx.M) V)]] (F[[E]]k)) by Lemma 5.5. The latter expression is provably equal to ((λx.F[[E[M]]]k) Ψ[[V]]). The result follows by the inductive hypothesis and an argument similar to case 1.

4. G ≡ [ ]: then λ\overline{β}\overline{η} ⊢ (F[[G]] k) = ((\overline{λ}k.k) k) = k = K_{k}[[G]]. Moreover K_{k}[[G]] is in \overline{β}\overline{η}-normal form.

5. G ≡ E[(x [ ])]: then, λ\overline{β}\overline{η} ⊢ (F[[G]] k) = (F[[(x [ ])]] (F[[E]]k)) by Lemma 5.5. The latter expression is provably equal to (x F[[E]]k). The result follows by the inductive hypothesis.

6. G ≡ E[((λx.M) [ ])]: then λ\overline{β}\overline{η} ⊢ (F[[G]] k) = (λx.F[[E[M]]]k) and the result follows by the inductive hypothesis.

7. G ≡ E[([ ] M)]: then λ\overline{β}\overline{η} ⊢ (F[[G]] k) = (F[[([ ] M)]] (F[[E]]k)) by Lemma 5.5. The latter expression is provably equal to (\overline{λ}u.F[[M]] (u (F[[E]]k))). By another application of Lemma 5.5, we get (\overline{λ}u.(F[[E[(u M)]]] k)). By the inductive hypothesis, λ\overline{β}\overline{η} ⊢ (F[[E[(u M)]]] k) = C_{k}[[E[(u M)]]] and C_{k}[[E[(u M)]]] is in \overline{β}\overline{η}-normal form. Therefore, λ\overline{β}\overline{η} ⊢ (F[[G]] k) = K_{k}[[G]]. Moreover, by a simple case analysis, C_{k}[[E[(u M)]]] is never of the form (K u) for some term K. Therefore, no new \overline{η}-redex is created in \overline{λ}u.C_{k}[[E[(u M)]]] and the term in \overline{β}\overline{η}-normal form.

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

Besides its pragmatic significance, the new CPS transformation simplifies the definition of the set of CPS terms. Specifically, our universe of discourse consists only of the 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 function 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.7. (CPS grammar) Let x ∈ Vars\{k}:

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

Note: The special status reserved for the variable k ensures that the continuation parameter occurs exactly once in each abstraction λk.K. A program in CPS form is a closed term of the form ((λk.P) (λx.x)) where k is the special continuation paramter. When working with the quotient of the language under α-equivalence, the special status of k disappears. End Note

The following theorem establishes the equivalence of the two definitions of the set of CPS terms.

Theorem 5.8 S = cps(Λ).

Proof. The left to right inclusion is the subject of Lemma 5.9. Lemma 5.13 deals with the opposite direction.

Lemma 5.9 S ⊆ cps(Λ).

Proof. Let P ∈ S. From the definition of the set S, there exists an M ∈ Λ such that λβη ⊢ C_{k}[[M]] ⟶ ⟶ P in n steps where n ≥ 0. By induction on n, we prove that P ∈ cps(Λ).

• n = 0, then P ≡ C_{k}[[M]]. The result follows by Lemma 5.10.

• n = i + 1, then λβη ⊢ C_{k}[[M]] ⟶ ⟶ Q ⟶ P for some Q. By the inductive hypothesis, Q ∈ cps(Λ). Moreover, by Lemma 5.11, βη-reductions preserve the syntactic categories in the CPS language. Therefore, P ∈ cps(Λ).

Lemma 5.10 Let M ∈ Λ, E ∈ EvCont. Then, C_{k}[[M]] ∈ cps(Λ), K_{k}[[E]] ∈ cps(EvCont).

Proof Idea. The proof is by induction on the size of the argument to C_{k} or K_{k}. It follows the same strategy as the proof of Lemma 5.6.

It remains to establish that βη-reductions preserve the syntactic categories in the grammar of Definition 5.7. By inspection of the CPS grammar, the possible β- and η-reductions on CPS terms are as follows:

((λ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})

Therefore, for cps(Λ), β = β_{w} ∪ β_{k} and η = η_{w} ∪ η_{k}.

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

1. λβη ⊢ P_{1} ⟶ P_{2} implies P_{2} ∈ cps(Λ).

2. λβη ⊢ W_{1} ⟶ W_{2} implies W_{2} ∈ cps(Values).

3. λβη ⊢ K_{1} ⟶ K_{2} implies K_{2} ∈ cps(EvCont).

Proof. The proof is by induction on the structure of the terms:

1. Let P_{1} ∈ cps(Λ) and assume λβη ⊢ P_{1} ⟶ P_{2}. By definition, P_{1} must be of the form (K_{1} W_{1}) with K_{1} ∈ cps(EvCont) and W_{1} ∈ cps(Values). Three kinds of reductions are possible:

• λβη ⊢ (K_{1} W_{1}) ⟶ (K_{2} W_{1}) because K_{1} reduces to K_{2}. By the inductive hypothesis, K_{2} ∈ cps(EvCont) and therefore P_{2} ∈ cps(Λ).

• λβη ⊢ (K_{1} W_{1}) ⟶ (K_{1} W_{2}) because W_{1} reduces to W_{2}. The result follows also by the inductive hypothesis.

• λβη ⊢ ((λx.P) W_{1}) ⟶ P [x := W_{1}] because K_{1} ≡ (λx.P). By Lemma 5.12, P [x := W_{1}] ∈ cps(Λ).

2. Let W_{1} ∈ cps(Values) and assume λβη ⊢ W_{1} ⟶ W_{2}. There are two cases:

• W_{1} ≡ x which is impossible, and

• W_{1} ≡ λk.K_{1} where K_{1} ∈ cps(EvCont). Then, either:

– λβη ⊢ λk.K_{1} ⟶ λk.K_{2} because K_{1} reduces to K_{2}. The result follows by the inductive hypothesis.

– λβη ⊢ λk.W_{3}k ⟶ W_{3} because K_{1} ≡ (W_{3} k) and W_{3} ∈ cps(Values) by definition.

3. Let K_{1} ∈ cps(EvCont) and assume λβη ⊢ K_{1} ⟶ K_{2}. Then, either:

• K_{1} ≡ k which is impossible, or

• K_{1} ≡ λx.P_{1} and there are two cases:

– λβη ⊢ (λx.P_{1}) ⟶ (λx.P_{2}) because P_{1} reduces P_{2}. The result follows by the inductive hypothesis.

– λβη ⊢ (λx.Kx) ⟶ K because P_{1} ≡ Kx and K ∈ cps(EvCont) by definition.

• K_{1} ≡ (W K) and there are three cases:

– λβη ⊢ (W K) ⟶ (W_{1} K) because W reduces to W_{1} and the result follows by the inductive hypothesis.

– λβη ⊢ (W K) ⟶ (W K_{3}) because K reduces to K_{3} and the result follows also by induction.

– λβη ⊢ ((λk.K_{3}) K) ⟶ K_{3}[k := K] because W ≡ λk.K_{3}. The result follows by Lemma 5.12.

Finally, the grammar is also closed under the relevant substitutions.

Lemma 5.12 Let P ∈ cps(Λ), W ∈ cps(Values), K_{1}, K_{2} ∈ cps(EvCont). Then,

1. P [x := W] ∈ cps(Λ).

2. K_{1}[k := K_{2}] ∈ cps(EvCont).

Proof Idea. By induction on the structure of the terms P and K_{1}.

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

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

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. The proof proceeds by case analysis on the possible elements of cps(Λ) and cps(EvCont):

1. G ≡ (k W), then there are four cases:

(a) W ≡ x: take M = x.

(b) W ≡ λk.k: take M = λx.x.

(c) W ≡ λk.W_{1}K: let P_{1} ≡ ((W_{1}K) x), then P̃_{1} < G̃ because P_{1} has one less abstraction of the form λk.K than G. Therefore, by the inductive hypothesis, there exists an M_{1} such that λβη ⊢ C_{k}[[M_{1}]] ⟶ ⟶ P_{1}. Take M = λx.M_{1}.

(d) W ≡ λk.λx.P_{1}: by the inductive hypothesis, P_{1} is reachable from a term M_{1}. Take M = λx.M_{1}.

2. G ≡ ((x K) W): by the inductive hypothesis, K is reachable from an evaluation context E. By an argument similar to the the first case, W is reachable from a value V. Take M = E[(x V)].

3. G ≡ (((λk.K_{1}) K_{2}) W): by the inductive hypothesis, K_{2} is reachable from an evaluation context E_{2}. By repeating the argument for the first case, the values λk.K_{1} and W are reachable from V_{1} and V respectively. Take M = ((λx.((λy.E_{2}[(y x)]) V_{1})) V). Then,

C_{k}[[((λx.((λy.E_{2}[(y x)]) V_{1})) V)]]
≡ ((λx.((λy.((y K_{k}[[E_{2}]]) x)) Φ[[V_{1}]])) Φ[[V]])
⟶ ⟶ ((λx.((λy.((y K_{2}) x)) λk.K_{1})) W)  (induction)
⟶ ((λx.(((λk.K_{1}) K_{2}) x)) W)  (β)
⟶ (((λk.K_{1}) K_{2}) W)  (β)

4. G ≡ ((λx.P_{1}) W): by the inductive hypothesis, there exists an M_{1} that reaches P_{1}. By repeating the argument for the first case, there exists also a value V that reaches W. Take M = ((λx.M_{1}) V).

5. G ≡ k: take E = [ ].

6. G ≡ (x K_{1}): by the inductive hypothesis, there exists an E_{1} that reaches K_{1}. Take E = E_{1}[(x [ ])].

7. G ≡ ((λk.K_{1}) K_{2}): similarly to case 3, take E = ((λx.((λy.E_{2}[(y x)]) V_{1})) [ ]).

8. G ≡ (λx.P_{1}): take E = ((λx.M_{1}) [ ]) where M_{1} reaches P_{1} by the inductive hypothesis.

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})

\begin{aligned}C^{−1} : cps(Λ) & → & Λ \\ C^{−1}[[(K W)]] & = & K^{−1}[[K]][Φ^{−1}[[W]]] \end{aligned}

\begin{aligned}Φ^{−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]] \end{aligned}

\begin{aligned}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]]) [ ]) \end{aligned}

Intuitively, C^{−1}, Φ^{−1}, and K^{−1} are the “inverses” of C, Φ, and K respectively. 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. To facilitate proofs of subsequent theorems, we first show that the output of C^{−1} is a proper subset of Λ.

Definition 6.2. (Output of C^{−1})

M ::= E[V]  (Λ_{u})
V ::= x | (λx.M)  (Values_{u})
E ::= [ ] | ((λx.M) [ ]) | E[(x [ ])]  (EvCont_{u})

Lemma 6.3 Let P ∈ cps(Λ), K ∈ cps(EvCont). Then, C^{−1}[[P]] ∈ Λ_{u} and K^{−1}[[K]] ∈ EvCont_{u}.

Proof. The proof is by lexicogaphic induction on the number of abstractions of the form λk.K and the size of the terms (cpm. the proof of Lemma 5.13). It proceeds by case analysis on the possible inputs to C^{−1} and K^{−1}.

• P ≡ (K W), then C^{−1}[[P]] ≡ K^{−1}[[K]][Φ^{−1}[[W]]]. By induction, K^{−1}[[K]] ∈ EvCont_{u}. It remains to establish that Φ^{−1}[[W]] ∈ Values_{u}.

– W ≡ x, then Φ^{−1}[[W]] ≡ x ∈ Values_{u}.

– W ≡ λk.k, then Φ^{−1}[[W]] ≡ λx.x. Since x ≡ [ ][x], then λx.x ∈ Values_{u}.

– W ≡ λk.W K, then Φ^{−1}[[W]] ≡ λx.C^{−1}[[((W K) x)]]. Because the term ((W K) x) has one less abstraction of the form λk.K than W, the inductive hypothesis applies to it. Therefore, C^{−1}[[((W K) x)]] ∈ Λ_{u} which shows that Φ^{−1}[[W]] ∈ Values_{u}.

– W ≡ λk.λx.P, then Φ^{−1}[[W]] ≡ λx.C^{−1}[[P]], then the result follows by induction.

• K ≡ k, then K^{−1}[[K]] ≡ [ ] ∈ EvCont_{u}.

• K ≡ (x K_{1}), then K^{−1}[[K]] ≡ K^{−1}[[K_{1}]][(x [ ])]. The result is immediate because K^{−1}[[K_{1}]] ∈ EvCont_{u} by induction.

• K ≡ ((λk.K_{1}) K_{2}), then K^{−1}[[K]] ≡ K^{−1}[[K_{1}[k := K_{2}]]]. Because k occurs exactly once in K_{1}, then term K_{1}[k := K_{2}] has one less abstraction of the λk.K than ((λk.K_{1}) K_{2}). Therefore, K^{−1}[[K]] ∈ EvCont_{u} by the inductive hypothesis.

• K ≡ λx.P, then K^{−1}[[K]] ≡ ((λx.C^{−1}[[P]]) [ ]) and the result follows by induction.

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.^{5} 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.

5Danvy and Lawall [3, 6] define a direct style transformation mapping CPS programs into source terms.

The transformation is the inverse of the Danvy-Filinski CPS transformation [5]; it is only applicable to images of Λ terms. For example, let

M = ((λd.5) ((λx.xx) (λx.xx))).

• 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) & x ∉ F V (E), E ≠ [ ] & (β_{lift}) \\ E[((M N) L)] & ⟶ & ((λx.E[(x L)]) (M N)) & x ∉ F V (E, L) & (β_{flat}) \end{matrix}

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.4 Let P ∈ cps(Λ). Then, C^{−1}[[P]] is in β_{lift}β_{flat}-normal form.

Proof. It suffices to show that all terms generated by the grammar in Definition 6.2 are in β_{lift}β_{flat}-normal form. The proof is by induction on the structure of the terms.

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

Then, according to Danvy/Filinski,

CPS(M) = ((λxk.xxk) (λxk.xxk) (λν.((λdk.k5) ν (λv.kv)))).

The latter expression reduces by two meaning-preserving β-reductions to:

((λxk.xxk) (λxk.xxk) (λν.k5))

which is still a diverging term. The direct style transformation cannot be applied to this term because in the continuation λν.k5, ν does not occur exactly once in k5. An extension of the direct style transformation that handles the above term fails to be an inverse of the Danvy/Filinski CPS transformation.

Theorem 6.5 Let M ∈ Λ, P ∈ cps(Λ), E ∈ EvCont, and K ∈ cps(EvCont). Then,

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

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

Proof. We prove the first claim by induction on the size of the argument to C_{k} or K_{k}. The proof proceeds by cases on the possible inputs to the two functions:

1. M ≡ V: then there are two sub-cases:

(a) V ≡ x: then x is identical to C^{−1}[[C_{k}[[x]]]].

(b) V ≡ λx.N: then by the inductive hypothesis λx.N reduces to λx.C^{−1}[[C_{k}[[N]]]] ≡ C^{−1}[[C_{k}[[λx.N]]]].

2. M ≡ E[(x V)]: then C^{−1}[[C_{k}[[M]]]] ≡ K^{−1}[[K_{k}[[E]]]][(x Φ^{−1}[[Φ[[V]]]])]. If V is not a variable, then |E| < |E[(x V)]|. Therefore, by the inductive hypothesis, E reduces to K^{−1}[[K_{k}[[E]]]], and by inlining the arguments for the first case, V reduces to Φ^{−1}[[Φ[[V]]]]. Otherwise, if V is a variable y, there are four cases:

(a) M ≡ (x y), then C^{−1}[[C_{k}[[M]]]] ≡ M.

(b) M ≡ E_{1}[(z (x y))], then C^{−1}[[C_{k}[[M]]]] ≡ K^{−1}[[K_{k}[[E_{1}]]]][(z (x y))] and the result follows by the inductive hypothesis.

(c) M ≡ E_{1}[((λz.L) (x y))], then C^{−1}[[C_{k}[[M]]]] ≡ ((λz.C^{−1}[[C_{k}[[E_{1}[L]]]]]) (x y)), and E_{1}[((λz.L) (x y))] reduces to ((λz.E_{1}[L]) (x y)) by a β_{lift}-reduction. The latter term reduces to ((λz.C^{−1}[[C_{k}[[E_{1}[L]]]]]) (x y)) by induction.

(d) M ≡ E_{1}[((x y) L)], then C^{−1}[[C_{k}[[M]]]] ≡ ((λu.C^{−1}[[C_{k}[[E_{1}[(u L)]]]]]) (x y)) and by a β_{flat}-reduction, E_{1}[((x y) L)] reduces to ((λu.E_{1}[(u L)]) (x y)), which in turn reduces to ((λu.C^{−1}[[C_{k}[[E_{1}[(u L)]]]]]) (x y)) by induction.

3. M ≡ E[((λx.N) V)]: then C^{−1}[[C_{k}[[M]]]] ≡ ((λx.C^{−1}[[C_{k}[[E[N]]]]]) Φ^{−1}[[Φ[[V]]]]), and E[((λx.N) V)] ⟶ ((λx.E[N]) V) by β_{lift}, which reduces to ((λx.C^{−1}[[C_{k}[[E[N]]]]]) V) by the inductive hypothesis. The result follows because V reduces to Φ^{−1}[[Φ[[V]]]] as in case 1.

4. E = [ ]: then K^{−1}[[K_{k}[[[ ]]]]] is identical to [ ].

5. E = E_{1}[(x [ ])]: then K^{−1}[[K_{k}[[E]]]] ≡ K^{−1}[[K_{k}[[E_{1}]]]][(x [ ])]. The result follows by the inductive hypothesis.

6. E = E_{1}[((λx.N) [ ])]: similar to case 3.

7. E = E_{1}[([ ] N)]: then K^{−1}[[K_{k}[[E]]]] ≡ ((λu.C^{−1}[[C_{k}[[E_{1}[(u N)]]]]]) [ ]). By a β_{flat}- reduction, E_{1}[([ ] N)] ⟶ ((λu.E_{1}[(u N)]) [ ]). By the inductive hypothesis, the latter term reduces to ((λu.C^{−1}[[C_{k}[[E_{1}[(u N)]]]]]) [ ]).

The proof of the second part differs slightly from the above. According to the grammar of Definition 6.2, cases 2d and 7 are impossible. Similarly, in cases 2c, 3 and 6 the surrounding context must be empty. Since these changes account for all the reductions from M to C^{−1}[[C_{k}[[M]]]], 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 naturally the inverse of C^{−1} on the subset of CPS terms that are images of source terms.

Theorem 6.6 Let P ∈ cps(Λ), M ∈ Λ, K ∈ cps(EvCont), and E ∈ EvCont. Then,

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

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

Proof Sketch. The proof of the first claim is similar to the proof of Lemma 5.13. We proceed by case analysis on the possible elements of cps(Λ) or cps(Evcont):

1. G ≡ (k W), then there are four cases:

(a) W ≡ x: Then (C_{k} ∘ C^{−1})[[G]] ≡ (k x) ≡ G.

(b) W ≡ λk.k: Then (C_{k} ∘ C^{−1})[[G]] ≡ (k λk.λx.kx), which reduces to G by an η-reduction.

(c) W ≡ λk.W_{1}K: Then (C_{k} ∘ C^{−1})[[G]] ≡ (k λk.λx.C_{k}[[C^{−1}[[((W_{1} K) x)]]]]) which is provably equal to (k λk.λx.((W_{1} K) x)) by the inductive hypothesis. The latter term reduces to G by an η-reduction.

(d) W ≡ λk.λx.P_{1}: Then (C_{k} ∘ C^{−1})[[G]] ≡ (k λk.λx.C_{k}[[C^{−1}[[P_{1}]]]]) and the result follows by the inductive hypothesis.

2. G ≡ ((x K) W): Then (C_{k} ∘ C^{−1})[[G]] = ((x K_{k}[[K^{−1}[[K]]]]) Φ[[Φ^{−1}[[W]]]]). By the inductive hypothesis λβη ⊢ K_{k}[[K^{−1}[[K]]]] = K and by argument similar the first case λβη ⊢ Φ[[Φ^{−1}[[W]]]] = W.

3. G ≡ (((λk.K_{1}) K_{2}) W): Then (C_{k} ∘ C^{−1})[[G]] ≡ (K_{k}[[K^{−1}[[K_{1}[k := K_{2}]]]]] Φ[[Φ^{−1}[[W]]]]). Because k occurs exactly once in K_{1}, then K_{1}[k := K_{2}] has one less abstraction of the form λk.K than ((λk.K_{1}) K_{2}). Therefore, by the inductive hypothesis, λβη ⊢ K_{k}[[K^{−1}[[K_{1}[k := K_{2}]]]]] = K_{1}[k := K_{2}]. By repeating the argument for the first case, Φ[[Φ^{−1}[[W]]]] and W are also provably equal. It follows that λβη ⊢ (K_{1}[k := K_{2}] W) = C_{k}[[C^{−1}[[(((λk.K_{1}) K_{2}) W)]]]]. The result follows by a β-reduction.

4. G ≡ ((λx.P_{1}) W): Then (C_{k} ∘ C^{−1})[[G]] ≡ ((λx.C_{k}[[C^{−1}[[P_{1}]]]]) Φ[[Φ^{−1}[[W]]]]). By the inductive hypothesis, λβη ⊢ P_{1} = C_{k}[[C^{−1}[[P_{1}]]]]. By the argument in case 1, λβη ⊢ W = Φ[[Φ^{−1}[[W]]]]. Therefore, λβη ⊢ ((λ.P_{1}) W) = ((λx.C_{k}[[C^{−1}[[P_{1}]]]]) Φ[[Φ^{−1}[[W]]]]).

5. G ≡ k: Then (K_{k} ∘ K^{−1})[[G]] ≡ G.

6. G ≡ (x K_{1}): Then (K_{k} ∘ K^{−1})[[G]] ≡ (x K_{k}[[K^{−1}[[K_{1}]]]]) and the result follows by the inductive hypothesis.

7. G ≡ ((λk.K_{1}) K_{2}): Then (K_{k} ∘ K^{−1})[[G]] ≡ K_{k}[[K^{−1}[[K_{1}[k := K_{2}]]]]] and this case is simliar to case 3.

8. G ≡ (λx.P_{1}): Then (K_{k} ∘ K^{−1})[[G]] ≡ (λx.C_{k}[[C^{−1}[[P_{1}]]]]) and the result follows by induction.

The proof of the second part is identical to the above but it excludes the cases that do not correspond to images of source terms. In particular, it excludes cases 1b and 1c because, in the image of a source term, the body of a λk.K abstraction must be of the form λx.P. Moreover, it excludes cases 3 and 7 because they contain the administrative redex ((λk.K_{1}) K_{2}).

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

As specified in Section 5, the possible β- and η-reductions on CPS terms are β_{w}, β_{k}, η_{w}, η_{k}. We first 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]]) [ ])  and  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)]  (β_{Ω})

• 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. The resulting set of source reductions, A, includes all the previously derived reductions and η_{v}: see Figure 1.

((λ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), 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}, β_{Ω}}

The Completeness Lemma summarizes the connection between the notions of reductions on cps(Λ) and the new reductions.

Lemma 7.1 (Completeness) Let P ∈ cps(Λ).

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

Proof. The proof of each case is distinct.

1. η_{k}-reduction: The proof is outlined at the beginning of the section.

2. β_{k}-reduction: By the definition of K^{−1}, K^{−1}[[((λk.K_{1}) K_{2})]] ≡ K^{−1}[[K_{1}[k := K_{2}]]].

3. η_{w}-reduction: Applying Φ^{−1} to both sides of the reduction, we get Φ^{−1}[[(λk.W k)]] ≡ (λx.C^{−1}[[((W k) x)]]) and Φ^{−1}[[W]]. The possible cases are:

• W ≡ z: then the reduction becomes the η_{v}-reduction: (λx.zx) ⟶ x.

• W ≡ λk.k: then both sides of the reduction are identical.

• W ≡ λk.W_{1}K: then again both sides of the reduction are identical.

• W ≡ λk.λz.P, then λx.((λz.C^{−1}[[P]]) x) ⟶ λz.C^{−1}[[P]] is an η_{v}-reduction.

4. β_{w}-reduction: Here, we need to show that:

λβ_{v}β_{lift}β_{id}β_{Ω} ⊢ C^{−1}[[((λx.P) W)]] ⟶ ⟶ C^{−1}[[P [x := W]]].

The left hand side of the reduction is equivalent to ((λx.C^{−1}[[P]]) Φ^{−1}[[W]]), which in turn reduces to C^{−1}[[P]][x := Φ^{−1}[[W]]] by a β_{v}-reduction. The latter term reduces to C^{−1}[[P [x := W]]] by the Substitution Lemma below.

In the above theorem, the proofs of the first three cases are complete. Only claim 4 requires the Substitution Lemma, which in turn refers back to Theorem 7.1 (case 1).

Lemma 7.2 (Substitution) Let P ∈ cps(Λ), W ∈ cps(Values), K ∈ cps(EvCont). Then,

1. λβ_{v}β_{lift}β_{id}β_{Ω} ⊢ C^{−1}[[P]][x := Φ^{−1}[[W]]] ⟶ ⟶ C^{−1}[[P [x := W]]].

2. λβ_{v}β_{lift}β_{id}β_{Ω} ⊢ K^{−1}[[K]][x := Φ^{−1}[[W]]] ⟶ ⟶ K^{−1}[[P [x := W]]].

Proof. The proof is by lexicographic induction on ⟨G̃, |G|⟩, i.e., the number of abstractions of the form λk.K and the size of the terms. The proof proceeds by cases on the arguments to C^{−1} and K^{−1}.

• P ≡ (K W_{1}): then, C^{−1}[[P]][x := Φ^{−1}[[W]]] ≡ K^{−1}[[K]][Φ^{−1}[[W_{1}]]] [x := Φ^{−1}[[W]]], which by the inductive hypothesis reduces to K^{−1}[[K[x := W]]][Φ^{−1}[[W_{1}]][x := Φ^{−1}[[W]]]]. It remains to establish that substitution commutes with Φ^{−1} as well. There are five cases:

1. W_{1} ≡ x: then Φ^{−1}[[x]][x := Φ^{−1}[[W]]] ≡ Φ^{−1}[[x[x := W]]].

2. W_{1} ≡ z and z ≢ x: then the result is immediate.

3. W_{1} ≡ λk.k: immediate since x is not free.

4. W_{1} ≡ λk.W_{2}k: then, Φ^{−1}[[W_{1}]][x := Φ^{−1}[[W]]] ≡ λz.C^{−1}[[((W_{2}K) z)]][x := Φ^{−1}[[W]]]. By induction, we get λz.C^{−1}[[(W_{2}K)[x := W] z]]. The latter term is identical to Φ^{−1}[[(λk.W_{2}K)[x := W]]] as desired.

5. W_{1} ≡ λk.λz.P_{1} (z ≢ x): then, Φ^{−1}[[W_{1}]][x := Φ^{−1}[[W]]] ≡ (λz.C^{−1}[[P]])[x := Φ^{−1}[[W]]]. By induction, we get λz.C^{−1}[[P [x := W]]] ≡ Φ^{−1}[[(λk.λz.P)[x := W]]].

• K ≡ k: then the claim is vacuously true because k ≠ x.

• K ≡ ((λk.K_{1}) K_{2}): here,

K^{−1}[[((λk.K_{1}) K_{2})]][x := Φ^{−1}[[W]]] ≡ K^{−1}[[K_{1}[k := K_{2}]]][x := Φ^{−1}[[W]]].

By induction, the latter term reduces to K^{−1}[[K_{1}[k := K_{2}][x := W]]], which is identical to K^{−1}[[((λk.K_{1}[x := W]) K_{2}[x := W])]].

• K ≡ λz.P_{1} (z ≢ x): K^{−1}[[λz.P_{1}]][x := Φ^{−1}[[W]]] ≡ ((λz.C^{−1}[[P]][x := Φ^{−1}[[W]]]) [ ]). By induction, ((λz.C^{−1}[[P [x := W]]]) [ ]) ≡ K^{−1}[[λz.P [x := W]]].

• K ≡ λx.P_{1}: immediate since x is not free.

• K ≡ (z K_{1}) and z ≢ x: this is a special case of the next clause.

• K ≡ (x K_{1}): then the left hand side is K^{−1}[[K_{1}]][x := Φ^{−1}[[W]]][(Φ^{−1}[[W]] [ ])]. By induction, the latter term reduces to K^{−1}[[K_{1}[x := W]]] [(Φ^{−1}[[W]] [ ])]. For readablity, let K′ ≡ K_{1}[x := W]. The goal is to prove that

K^{−1}[[K′]][(Φ^{−1}[[W]] [ ])] reduces to K^{−1}[[(W K′)]].

We proceed by cases of W:

1. W ≡ y: then K^{−1}[[K′]][(y [ ])] ≡ K^{−1}[[(y K′)]].

2. W ≡ λk.k: then, K^{−1}[[K′]][((λx.x) [ ])] reduces to K^{−1}[[K′]] by an β_{id}-reduction. The latter term is identical to K^{−1}[[((λk.k) K′)]].

3. W ≡ λk.W_{3}K: then, the left hand side K^{−1}[[K′]][((λy.C^{−1}[[((W_{3}K) y)]]) [ ])] ≡ K^{−1}[[K′]][K^{−1}[[(λy.((W_{3}K) y))]]]. By the first case in Lemma 7.1, this reduces to K^{−1}[[K′]][K^{−1}[[(W_{3}K)]]]. Moreover, by Lemma 7.3, the latter term reduces to K^{−1}[[(W_{3}K)[k := K′]]], which is identical to K^{−1}[[((λk.W_{3}K) K′)]].

4. W ≡ λk.λy.P_{2}: then by a β_{lift}-reduction, K^{−1}[[K′]][((λz.C^{−1}[[P_{2}]]) [ ])] reduces to ((λz.K^{−1}[[K′]][C^{−1}[[P_{2}]]]) [ ]). By Lemma 7.3, the latter term reduces to ((λz.C^{−1}[[P_{2}[k := K′]]]) [ ]) ≡ K^{−1}[[λz.P_{2}[k := K′]]] ≡ K^{−1}[[((λk.λz.P_{2}) K′)]].

Lemma 7.3 (Continuation) Let K, K_{1}, K_{2} ∈ cps(EvCont), P ∈ cps(Λ). Then,

1. λβ_{lift} ⊢ K^{−1}[[K]][C^{−1}[[P]]] ⟶ ⟶ C^{−1}[[P [k := K]]]

2. λβ_{lift} ⊢ K^{−1}[[K_{2}]][K^{−1}[[K_{1}]]] ⟶ ⟶ K^{−1}[[K_{1}[k := K_{2}]]]

Proof. The proof is by induction on the number of abstractions of the λk.K and the size of P or K_{1}. It proceeds by case analysis on the possible elements of cps(Λ) and cps(EvCont).

• P ≡ (K_{3} W), then K^{−1}[[K]][C^{−1}[[P]]] ≡ K^{−1}[[K]][K^{−1}[[K_{3}]][Φ^{−1}[[W]]]]. By the inductive hypothesis, λβ_{lift} ⊢ K^{−1}[[K]][K^{−1}[[K_{3}]]] ⟶ ⟶ K^{−1}[[K_{3}[k := K]]]. Therefore, λβ_{lift} ⊢ K^{−1}[[K]][C^{−1}[[P]]] ⟶ ⟶ K^{−1}[[K_{3}[k := K]]][Φ^{−1}[[W]]]. The latter term is identical to K^{−1}[[(K_{3} W)[k := K]]] since k is never free in W.

• K_{1} ≡ k: then both sides are identical to K^{−1}[[K_{2}]].

• K_{1} ≡ (x K_{3}), then K^{−1}[[K_{2}]][K^{−1}[[K_{3}]][(x [ ])]] reduces to K^{−1}[[K_{3}[k := K_{2}]]][(x [ ])] by induction. The latter term is identical to K^{−1}[[(x K_{3}[k := K_{2}])]].

• K_{1} ≡ ((λk.K_{3}) K_{4}), then K^{−1}[[K_{2}]][K^{−1}[[K_{3}[k := K_{4}]]]] reduces to K^{−1}[[K_{3}[k := K_{4}][k := K_{2}]]] by induction. This term is identical to K^{−1}[[K_{3}[k := K_{4}[k := K_{2}]]]], which in turn is identical to K^{−1}[[((λk.K_{3}) K_{4})[k := K_{2}]]].

• K_{1} ≡ λx.P: then, K^{−1}[[K_{2}]][((λx.C^{−1}[[P]]) [ ])] reduces to ((λx.K^{−1}[[K_{2}]][C^{−1}[[P]]]) [ ]) by a β_{lift}-reduction. By induction, this term reduces to

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

The Completeness Theorem is a direct consequence of the above results.

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

Proof. By pasting together the proofs of the Completeness Lemma.

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, λβη ⊢ C_{k}[[M]] = C_{k}[[N]]. In fact, we can prove the stronger results of the following lemma.

Lemma 7.5 (Soundness) Let M ∈ Λ.

1. If λβ_{v} ⊢ M ⟶ N then λβ  ⊢ C_{k}[[M]] ⟶ ⟶ C_{k}[[N]]
2. If λη_{v} ⊢ M ⟶ N then λη_{w}η_{k} ⊢ C_{k}[[M]] ⟶ ⟶ C_{k}[[N]]
3. If λβ_{lift} ⊢ M ⟶ N then  C_{k}[[M]] ≡ C_{k}[[N]]
4. If λβ_{flat} ⊢ M ⟶ N then  C_{k}[[M]] ≡ C_{k}[[N]]
5. If λβ_{id} ⊢ M ⟶ N then λη_{k}  ⊢ C_{k}[[M]] ⟶ ⟶ C_{k}[[M]]
6. If λβ_{Ω} ⊢ M ⟶ N then λη_{k}  ⊢ C_{k}[[M]] ⟶ ⟶ C_{k}[[N]]

Proof. The cases for β_{lift} and β_{flat} are immediate from the definition of the function C_{k}. We present only the proof for β_{v}-reductions in Lemma 7.6. The other proofs are similar.

Lemma 7.6 (β_{v}) λβ ⊢ C_{k}[[((λx.M) V)]] ⟶ ⟶ C_{k}[[M[x := V]]].

Proof. By definition of C_{k},

C_{k}[[((λx.M) V)]] ≡ ((λx.C_{k}[[M]]) Φ[[V]]).

The latter term reduces to C_{k}[[M]][x := Φ[[V]]]. It remains to establish that substitution commutes with C_{k}, i.e.,

1. λβ ⊢ C_{k}[[M]][x := Φ[[V]]] ⟶ ⟶ C_{k}[[M[x := V]]].

2. λβ ⊢ K_{k}[[E]][x := Φ[[V]]] ⟶ ⟶ K_{k}[[E[x := V]]].

The proof is by induction on the size of the argument to C_{k} or K_{k}. Except for one case, the inductive hypothesis applies immediately. The interesting case occurs when M ≡ E[(x U)]:

C_{k}[[E[(x U)]]][x := Φ[[V]]] ≡ ((x K_{k}[[E]]) Φ[[U]])[x := Φ[[V]]]
⟶ ((Φ[[V]] K_{k}[[E]][x := Φ[[V]]]) Φ[[U]][x := Φ[[V]]])
⟶ ⟶ ((Φ[[V]] K_{k}[[E[x := V]]]) Φ[[U[x := V]]])

The last line follows by cases on E if U is a variable. Otherwise, it follows by the inductive hypothesis. For readability, let E′ ≡ E[x := V] and U′ ≡ U[x := V]. The goal is to prove that:

((Φ[[V]] K_{k}[[E′]]) Φ[[U′]]) ⟶ ⟶ C_{k}[[E′[(V U′)]]]

We proceed by cases of V:

• V ≡ z, then both sides are identical.

• V ≡ λz.L, then by a β-reduction,

(((λk.λz.C_{k}[[L]]) K_{k}[[E′]]) Φ[[U′]]) ⟶ ((λz.C_{k}[[L]][k := K_{k}[[E′]]]) Φ[[U′]]).

By Lemma 7.7, the latter term reduces to ((λz.C_{k}[[E′[L]]]) Φ[[U′]]), which is identical to C_{k}[[E′[((λz.L) U′)]]].

Lemma 7.7 (Context) Let M ∈ Λ, E, E_{1} ∈ EvCont. Then,

λβ ⊢ C_{k}[[M]][k := K_{k}[[E]]] ⟶ ⟶ C_{k}[[E[M]]] and λβ ⊢ K_{k}[[E_{1}]][k := K_{k}[[E]]] ⟶ ⟶ K_{k}[[E[E_{1}]]]

.

Proof Idea. The proof is by induction on the size of M or E_{1}.

The Soundness theorem is a direct consequence of these results.

Theorem 7.8 (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]], M does not reduce to N unless N is in β_{lift}β_{flat}- normal form. Figure 2 summarizes the relationship between proofs on either side. The dotted lines correspond to the application of C_{k} or C^{−1}. The solid lines represent sequences of reductions.

[figure: βη; A; β_{lift}β_{flat}; β_{lift}β_{flat}; C_{k}[[N]]; C_{k}[[M]]; (C^{−1} ∘ C_{k})[[N]]; (C^{−1} ∘ C_{k})[[M]]; N; M]

Figure 2: The correspondence Theorem.

Although the functions C_{k} and C^{−1} do not always preserve reductions, they preserve equality.

Theorem 7.9 (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).

End Note

7.4 The computational λ-calculus

The calculus λ_{v}A is equivalent to an untyped variant of Moggi’s computational λ-cal-culus λ_{c} [21]. Specifically, if 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, then the basic reductions of λ_{c} are β_{v}, η_{v}, β_{id} plus the additional reductions of Figure 3.

((λ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 3: Additional Reductions for the Computational λ-calculus

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

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

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

8 Observational Equivalence

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 [21] proves the result for a typed setting.

In a dynamically typed language, the soundness of the λ_{c}-calculus with respect to the call-by-value observational equivalence relation depends on the particular language extensions. For example, the axiom η_{v} is unsound in languages like Lisp or Scheme as argued in Section 2. It is still possible to prove the soundness of the λ_{c}-calculus for pure dynamically typed languages, i.e., languages with no constants.

Theorem 8.1 Let M, N ∈ Λ. If λ_{v}A ⊢ M = N then M ≅_{v} N.

Proof. Let C be a context such that C[M], C[N] ∈ Λ^{0}. Assume λ_{v}A ⊢ M = N and eval_{v}(C[M]) is defined. The goal is to show that eval_{v}(C[N]) is also defined.

It follows from the assumptions that λ_{v}A ⊢ C[M] = C[N] by Compatiblity. Therefore,

λβη ⊢ C_{k}[[C[M]]] = C_{k}[[C[N]]]  (1)

by Theorem 7.9. Also by the assumptions and the definition of eval_{v}, λ_{v} ⊢ C[M] = V for some value V. Hence,

λβη ⊢ C_{k}[[C[M]]] = C_{k}[[V]]  (2)

by Theorem 7.9. From (1) and (2), we deduce that λβη ⊢ C_{k}[[C[N]]] = C_{k}[[V]] = (k Φ[[V]]). The Church-Rosser Theorem implies the existence of a term P such that:

\begin{aligned}λβη & ⊢ & C_{k}[[C[N]]] ⟶ ⟶ P \\ λβη & ⊢ & (k Φ[[V]]) ⟶ ⟶ P \end{aligned}

Obviously, all the reductions starting from the term (k Φ[[V]]) must occur inside Φ[[V]]. Since reductions preserve the syntactic categories in the CPS language, P must be of the form (k W) for some W. Therefore, λβη ⊢ C_{k}[[C[N]]] ⟶ ⟶ (k W), and hence

λβη ⊢ C_{k}[[C[N]]][k := λx.x] ⟶ ⟶ ((λx.x) W) ⟶ W

Lemma 8.2 implies that eval_{n}((F[[C[N]]] λx.x)) is defined. Thus, eval_{v}(C[N]) is defined by Theorem 3.2.

Lemma 8.2 Let M ∈ Λ^{0}. If λβη ⊢ C_{k}[[M]][k := λx.x] ⟶ ⟶ W, then eval_{n}(F[[M]] λx.x) is defined.

Proof. Assume λβη ⊢ C_{k}[[M]][k := λx.x] ⟶ ⟶ W, then by Lemma 5.6,

λβη ⊢ (F[[M]] λx.x) ⟶ ⟶ ((λk.C_{k}[[M]]) λx.x) ⟶ C_{k}[[M]][k := λx.x] ⟶ ⟶ W

By the Postponement Lemma [2: 15], we also have:

(F[[M]] λx.x) ⟶ ⟶_{β} L ⟶ ⟶_{η} W for some term L

Since M is a closed term, W cannot be a variable; it must a λ-abstraction. Any η-expansion starting from a λ-abstraction will also result in a λ-abstraction. Therefore, L is a value:

(F[[M]] λx.x) ⟶ ⟶_{β} W′

By the Standard Reduction theorem [22], if a term reduces to a value, then it standardreduces to a value. Therefore, eval_{n}(F[[M]] λx.x) is defined.

As pointed out in Section 4, M ≅_{v} N does not imply that C_{k}[[M]] ≅_{n} C_{k}[[N]]. For example, if

\begin{matrix}M & =^{df} & λy.λx.x (y x) \\ N & =^{df} & λy.λx.x (y λz.xz) \end{matrix}

then, M ≅_{v} N [22]. On the other hand,

\begin{aligned}C_{k}[[M]] & = & (k λk.λy.(k λk.λx.((y (x k)) x))), \\ C_{k}[[N]] & = & (k λk.λy.(k λk.λx.((y (x k)) (λk.λz.((x k) z))))), \end{aligned}

and the context

D =^{df} \begin{matrix}((λk.[ ]) \\ (λa.((a (λb.((b (λx.x)) λd.Ω))) \\ (λk.λm.m (λx.x))))) \end{matrix}

differentiates the two expressions. Since the context D includes a term (λk.λm.(m λx.x)) that ignores its continuation, there is no context C ∈ Λ such that C_{k}[[C[M]]] = D[C_{k}[[M]]].

This result prompted Meyer and Riecke [19] to deduce that “continuations may be unreasonable”. However, a restriction of D to range over contexts in the language cps(Λ) results in a notion of observational equivalence that coincides with the call-by-value observational equivalence.

Definition 8.3. (≅_{cps(Λ)}: CPS observational equivalence) Two terms P, Q are observationally equivalent, P ≅_{cps(Λ)} Q, iff for all contexts D such that ((λk.D[P]) (λx.x)), ((λk.D[Q]) (λx.x)) are programs in CPS form, then either both of eval_{n}((λk.D[P]) λx.x) and eval_{n}((λk.D[Q]) λx.x) are defined or both are undefined.

Theorem 8.4 Let M, N ∈ Λ. Then, M ≅_{v} N iff C_{k}[[M]] ≅_{cps(Λ)} C_{k}[[N]]

Proof. Assume C_{k}[[M]] ≅_{c̸ps(Λ)} C_{k}[[N]], then there exists a context D such that D[C_{k}[[M]]], D[C_{k}[[N]]] ∈ cps(Λ) and the evaluation of one of the programs terminates while the other diverges. Without loss of generality, assume eval_{n}((λk.D[C_{k}[[M]]]) λx.x) is defined and eval_{n}((λk.D[C_{k}[[N]]]) λx.x) is undefined. By the definition of eval_{n}, we get:

\begin{matrix}λβ ⊢ ((λk.D[C_{k}[[M]]]) λx.x) = W \\ λβ ⊬ ((λk.D[C_{k}[[N]]]) λx.x) = W′ for any W′ \end{matrix}

By Lemma 8.5, there exists a context C ∈ Λ such that:

\begin{matrix}λβη ⊢ ((λk.C_{k}[[C[M]]]) λx.x) = W \\ λβη ⊬ ((λk.C_{k}[[C[N]]]) λx.x) = W′ for any W′ \end{matrix}

By Lemma 8.2 and Theorem 3.2, eval_{v}(C[M]) is defined and eval_{v}(C[N]) is undefined. Therefore, M ≅_{v̸} N. The reverse implication is straightforward.

Lemma 8.5 Let M, N ∈ Λ, D[C_{k}[[M]]], D[C_{k}[[N]]] ∈ cps(Λ). Then, there exists a context C such that λβη ⊢ C_{k}[[C[M]]] = D[C_{k}[[M]]] and λβη ⊢ C_{k}[[C[N]]] = D[C_{k}[[N]]].

Proof. Since D[C_{k}[[M]]], D[C_{k}[[N]]] ∈ cps(Λ), they are valid arguments to C^{−1}. It suffices to show that the function C^{−1} is a homomorphism when restricted to inputs of the form C_{k}[[M]] for some M ∈ Λ. By cases:

1. C^{−1}[[(K W)]] = K^{−1}[[K]][Φ^{−1}[[W]]].
2. Φ^{−1}[[x]] = x.
3. Φ^{−1}[[(λk.k)]] = λx.x.
4. Φ^{−1}[[(λk.W K)]] = λx.C^{−1}[[(W K) x]].
5. Φ^{−1}[[(λk.λx.P)]] = λx.C^{−1}[[P]].
6. K^{−1}[[k]] = [ ].
7. K^{−1}[[(x K)]] = K^{−1}[[K]][(x [ ])].
8. K^{−1}[[((λk.K_{1}) K_{2})]] = K^{−1}[[K_{1}[k := K_{2}]]].
9. K^{−1}[[(λx.P)]] = ((λx.C^{−1}[[P]]) [ ]).

The function is homomorphic is all cases except cases 4 and 8. Both are impossible if the input is of the form C_{k}[[M]] for some M ∈ Λ.

9 Typed CPS Models

Friedman [12] investigates the connection between the typed βη-calculus and the functionals of finite type. Two convertible λ-terms define the same functional of finite type, and two non-convertible λ-terms define different functionals. Technically, λβη is sound and complete with respect to the full type structure.

The Correspondence Theorem suggests the existence of a similar completeness theorem for the λ_{c}-calculus and the CPS type structure [20, 14]. We prove this theorem after briefly reviewing the full type structure and the CPS type structure as denotational models for the call-by-value λ-calculus.

Full Type Structure

The set of types for the simply typed λ-calculus is

t ::= o | t → t

where o denotes the observable base type. The denotations of types are as follows. Let B be an infinite set of elements of type o. Then, the full type pre-structure over B consists of a nonempty set D^{t} for each type t:

\begin{aligned}D^{o} & = & B \\ D^{t_{1}→t_{2}} & = & D^{t_{1}} ⇒ D^{t_{2}} \end{aligned}

The term language of the simply typed λ-calculus is the subset of Λ to which we can assign simple types as follows. Every variable has a fixed type t. If M is of type t → s and N is of type t, then (M N) is of type s. Finally, if x is of type t and M is of type s, then λx.M has type t → s. The full type structure, P_{B}, over B consists of a full type pre-structure and a meaning function P such that:

Env : Vars ⇒ ∪_{t}D^{t}  such that for ρ ∈ Env, ρ(x^{t}) ∈ D^{t}
P[[x]]ρ = ρ(x)
P[[λx.M]]ρ = \underline{λ}a.P[[M]]ρ[x/a]
P[[MN]]ρ = P[[M]]ρ(P[[N]]ρ)

The notation A ⇒ B represents the set of functions from A to B and \underline{λ}a. · · · denotes the function f such that f(a) = · · ·. Also, P_{B} ⊧ M = N means that for all environments ρ, P[[M]]ρ = P[[N]]ρ. Based on this definition, we can formulate the completeness theorem.

Theorem 9.1 (Friedman [12]) Let M, N ∈ Λ. Then, λβη ⊢ M = N iff P_{B} ⊧ M = N.

Since F[[M]] ∈ Λ, the theorem implies the following corollary.

Corollary 9.2 Let M, N ∈ Λ. Then λ_{c} ⊢ M = N iff λβη ⊢ F[[M]] = F[[N]] iff P_{B} ⊧ F[[M]] = F[[N]].

CPS Type Structure

Meyer and Wand [20] establish that the type of a Λ term may be related in a straightforward manner to the type of its CPS transform. The set of types becomes:^{6}

s ::= o | (s → a) → (s → a)

where a denotes a distinguished type of answers. The CPS type structure, S_{B}, over some infinite base set B and an infinite set of answers A, consists of a nonempty set D^{s} for each type and a meaning function such that:

\begin{aligned}D^{o} & = & B \\ D^{(s_{1}→a)→s_{2}→a} & = & (D^{s_{1}} ⇒ A) ⇒ D^{s_{2}} ⇒ A \end{aligned}

and

S : Λ × Env × Continuation ⇒ A
Env : Vars ⇒ ∪_{s}D^{s}  such that for ρ ∈ Env, ρ(x^{s}) ∈ D^{s}
Continuation : ∪_{s}D^{s} ⇒ A
S[[x]]ρκ = κ(ρ(x))
S[[λx.M]]ρκ = κ \underline{λ}c.\underline{λ}a.S[[M]]ρ[x/a]c
S[[MN]]ρκ = S[[M]]ρ(\underline{λ}a.S[[N]]ρ(\underline{λ}b.((a κ) b)))

6Meyer and Wand assume that the continuation is the second argument to a procedure. This means that their set of types is actually:

s ::= o | s → (s → a) → a.

Not surprisingly, the meaning of a term M in the CPS model is directly related to the meaning of F[[M]] in the direct model.

Lemma 9.3 Let M ∈ Λ. (P[[F[[M]]]]ρ κ) = S[[M]]ρκ.

Proof Idea. The proof is by induction on M.

This lemma implies that S_{B} and P_{B} satisfy theorems that are related via the Fischer-cps transformation.

Lemma 9.4 Let M, N ∈ Λ. Then, P_{B} ⊧ F[[M]] = F[[N]] iff S_{B} ⊧ M = N.

Proof. The proposition follows from Lemma 9.3.

It follows that the λ_{c}-calculus is sound and complete with respect to the CPS type structure.

Theorem 9.5 Let M, N ∈ Λ. Then, λ_{c} ⊢ M = N iff S_{B} ⊧ M = N.

Proof. The theorem is a direct consequence of Lemma 9.4 and Corollary 9.2.

10 Conclusion and Future Research

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 λβη over CPS terms. Thus far, we have also determined that 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. L. 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., 1992, to appear.

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

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

11. Friedman, D.P., M. Wand, and C.T. Haynes. Essentials of Programming Languages. The MIT Press, Cambridge, Mass., 1992.

12. Friedman, H. Equality between functionals. In Logic Colloquium’73, Rohit Parikh (Ed.), Lecture Notes in Mathematics 453, Springer Verlag, Berlin, 1973, 22–37.

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

14. Harper, R. and M. Lillibridge. Polymorphic type assignment and cps conversion. Tech. Rpt. CMU-CS-92-122. Carnegie Mellon University. 1992. Preliminary version in: Proc. Workshop on Continuations: CW92 . Technical Report CS-92-1426. Stanford University, 1992, 13–22.

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

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

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

18. Leroy, X. The Zinc experiment. Technical Report 117. INRIA, 1990.

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

20. Meyer, A.R. and M. Wand. Continuation semantics in typed lambda-calculi. Proc. Workshop Logics of Programs, Lecture Notes in Computer Science 193, Springer-Verlag, Heidelberg, 1985, 219–224.

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

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

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

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

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