LISP AND SYMBOLIC COMPUTATION: An International Journal, ?, ??–??, 1993 \begin{matrix}c \\ ◯ \end{matrix} 1993 Kluwer Academic Publishers – Manufactured in The Netherlands

Reasoning about Programs in Continuation-Passing Style^{∗}

AMR SABRY† (sabry@cs.rice.edu)

MATTHIAS FELLEISEN† (matthias@cs.rice.edu) Department of Computer Science, Rice University, Houston, TX 77251-1892

Keywords: λ-calculus, λ_{v}-calculus, continuation-passing style, CPS transformations, inverse CPS transformations, λ_{v}-C-calculus, IOCC

Abstract. Plotkin’s λ_{v}-calculus for call-by-value programs is weaker than the λβηcalculus for the same programs in continuation-passing style (CPS). To identify the callby-value axioms that correspond to βη on CPS terms, we define a new CPS transformation and an inverse mapping, both of which are interesting in their own right. Using the new CPS transformation, we determine the precise language of CPS terms closed under βη-transformations, as well as the call-by-value axioms that correspond to the so-called administrative βη-reductions on CPS terms. Using the inverse mapping, we map the remaining β and η equalities on CPS terms to axioms on call-by-value terms. On the pure (constant free) set of Λ-terms, the resulting set of axioms is equivalent to Moggi’s computational λ-calculus. If the call-by-value language includes the control operators abort and call-with-current-continuation, the axioms are equivalent to an extension of Felleisen et al.’s λ_{v}-C-calculus and to the equational subtheory of Talcott’s logic IOCC.

Contents

1 Compiling with and without Continuations 4

2 Λ: Calculi and Semantics 7

3 The Origins and Practice of CPS 10 3.1 The Original Encoding . . . . . . . . . . . . . . . . . . . . . 10 3.2 The Universe of CPS Terms . . . . . . . . . . . . . . . . . . 11

4 A Compacting CPS Transformation 13

∗This article is a revised and extended version of the conference paper with the same title [42]. The technical report of the same title contains additional material.

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

4.1 The Two-Pass CPS Transformation . . . . . . . . . . . . . . 13 4.2 The CPS Transformation C_{k} . . . . . . . . . . . . . . . . . . 15 4.3 Administrative Source Reductions: The A-Reductions … 17 4.4 The CPS Language . . . . . . . . . . . . . . . . . . . . . . . 18

5 A CPS Inverse 20 5.1 The Transformation C^{−1} . . . . . . . . . . . . . . . . . . . . 20 5.2 Composing C_{k} and C^{−1} . . . . . . . . . . . . . . . . . . . . . 21

6 Equational Correspondence for the Pure Language 22 6.1 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . 23 6.2 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 6.3 Equational Correspondence . . . . . . . . . . . . . . . . . . 25

7 Non-Local Control Operators 27 7.1 The Extended Language and its Semantics . . . . . . . . . 27 7.2 The CPS Language and the Inverse Translation . . . . . . . 29 7.3 Equational Correspondence . . . . . . . . . . . . . . . . . . 32

8 A Realistic Language 33 8.1 Core Scheme: CS . . . . . . . . . . . . . . . . . . . . . . . . 33 8.2 The CPS Language: CS_{k} . . . . . . . . . . . . . . . . . . . 35 8.3 Equational Correspondence . . . . . . . . . . . . . . . . . . 36

9 Summary of the Results 38

10 Example: Coroutines from Continuations 40 10.1 The Original Program . . . . . . . . . . . . . . . . . . . . . 40 10.2 Simplifying the Program . . . . . . . . . . . . . . . . . . . . 42

11 Conclusion and Future Research 48

A Proofs 48

List of Definitions

1 Equational Correspondence . . . . . . . . . . . . . . . . . . 8 2 Fischer CPS Transformation (F) . . . . . . . . . . . . . . . 11 3 Administrative CPS Reductions (\overline{β} and \overline{η}) . . . . . . . . . . 12 4 CPS Transformation (F2) . . . . . . . . . . . . . . . . . . . 13 5 CPS Transformation (C_{k}) . . . . . . . . . . . . . . . . . . . 16 6 Size of Terms and Evaluation Contexts . . . . . . . . . . . . 17 7 A-Reductions (β_{lift} and β_{flat}) . . . . . . . . . . . . . . . . . 18 8 CPS Language cps(Λ) . . . . . . . . . . . . . . . . . . . . . 18 9 Inverse CPS Transformation (C^{−1}) . . . . . . . . . . . . . . 20 10 A-Normal Forms (Λ_{a}) . . . . . . . . . . . . . . . . . . . . . 21 11 CPS Transformation with Control Operators (C_{k}) . . . . . . 28 12 CPS Language cps(Λ + callcc + A) . . . . . . . . . . . . . . 29 13 Inverse CPS Transformation with Control Operators (C^{−1}) 29

List of Figures

1 Coroutines from Continuations. . . . . . . . . . . . . . . . . 6 2 Source Reductions: X =^{df} {η_{v}, β_{lift}, β_{flat}, β_{id}, β_{Ω}}. . . . . . . . 23 3 The Correspondence of Reduction Steps. . . . . . . . . . . . 26 4 The Axioms C: {C_{current}, C_{elim}, C_{lift}, C_{abort}, C_{tail}, Abort}… 31 5 Additional Axioms F for CS. . . . . . . . . . . . . . . . . . 34 6 Additional Axioms F_{k} for CS_{k}. . . . . . . . . . . . . . . . . 36 7 The Theory λCS. . . . . . . . . . . . . . . . . . . . . . . . . 39 8 The Theory λCS_{k}. . . . . . . . . . . . . . . . . . . . . . . . 40 9 Pseudo Coroutine Code. . . . . . . . . . . . . . . . . . . . . 41

1. Compiling with and without Continuations

Many compilers for higher-order applicative languages use the continuationpassing style (CPS) transformation [21, 41] to generate an intermediate representation [3, 30, 43, 46]. The CPS intermediate language has the following desirable properties:

• The language consists only of basic primitive operations and procedure applications whose semantics is independent of the parameter evaluation technique [39, 41]; many optimizations are therefore sequences of β- and η-reductions [2, 43, 46].

• It exposes the control flow of the program; complicated control facilities in the source language, e.g., exception handlers and call-with-current-continuation [40], are translated to simple procedures that manipulate their continuation arguments in non-standard ways [41, 47].

• It constitutes an abstract assembly language whose standard reduction sequence mimics the behavior of typical target machines [2, 3, 24, 29, 49].

The CPS transformation is a global transformation that affects every subexpression in a program. It restructures programs to the extent that many of their original aspects are unrecognizable. The transformation might even obscure the analysis of optimizations that rely on execution paths having matching call/return pairs [Private Communication, Hans Boehm, October 1992]. For these reasons and others, a fair number of compilers (usually called direct compilers) do not rely on the CPS intermediate representation [5, 6, 28, 32].

The choice of compilation strategy would not be significant if both classes of compilers performed the same optimizations. However for the important class of optimizations that is expressible in the framework of the λ-cal-culus, CPS compilers have an advantage. While CPS compilers can use the full λ-calculus reductions to perform optimizations, direct compilers can apparently only rely on weaker calculi like the λ_{v}-calculus [39] and the λ_{v}-C-calculus [18, 19]. Naturally we ask: what optimizations do CPS compilers perform that are not also performed by direct compilers? Or in technical terms, what set of call-by-value axioms corresponds to βη-reductions on CPS terms. With such a set, CPS compilers could report optimizations in terms of the original program, and direct compilers could benefit by performing all the optimizations that correspond to βη-reductions on CPS programs.

The main technical result of this paper is the identification of axioms for call-by-value languages that correspond to βηδ-reductions on CPS programs.^{1} In order to simplify the technical exposition, we first focus on a pure, constant-free call-by-value language. Specifically, we strengthen Plotkin’s Translation Theorem (cf. Theorem 1) by identifying an axiom set X such that:

λβ_{v}X ⊢ M = N  if and only if  λβη ⊢ cps(M) = cps(N).

Our strategy for the identification of the axioms X consists of three steps:

1. First, we develop a new CPS transformation that produces a canonical form of CPS programs. The new transformation provides a simple characterization of a CPS language that is closed under βη-reductions. It also identifies a subset A of the call-by-value axioms X.

2. Second, we develop an “inverse” transformation that maps canonical CPS programs back to the original language. As Danvy and Lawall [11, 14] convincingly argue, this translation from CPS to direct terms is useful in its own right.

3. Finally, by studying the connection between the CPS transformation and the inverse mapping, we systematically derive the remaining axioms in the set X. The resulting calculus is a variant of Moggi’s untyped computational λ-calculus [36].

A complete treatment of the relationship between programs and their CPS transforms must also analyze a language with control operators since these are the language facilities for which continuations were conceived [34, 37, 41, 47]. To this end, we extend our language with two typical control operators expressible in the CPS framework: abort and call-with-current-continuation. These operators suffice to express a wide variety of control abstractions such as error exits, jumps, intelligent backtracking, coroutines, and exception handling [23, 27].^{2}

1For call-by-name languages, the reductions βη are valid in both the source language and the CPS language and the CPS translation does not create any new opportunities for equational reasoning [39, page 153].

2The CPS framework can also express a control delimiting facility [44], e.g., prompt [15]. However, we do not include prompt in our language for two reasons. First, current language implementations do not include such facilities. Second, the CPS translation of prompt generates expressions that are no longer independent of the timing of parameter evaluation [12, 20]. As a consequence, we can associate two different semantics with the CPS language: a call-by-value semantics which is the classic semantics for control delimiters [13, 15], and a call-by-name semantics which yields a lazy prompt. The first semantics is incompatible with the βη-reductions we use for the CPS language and, at this point, there seems to be little practical motivation to pursue the analysis of the lazy prompt.

The addition of abort and call-with-current-continuation extends the set of CPS programs and generates a new set of program equivalences that are provable using β- and η-reductions. In order to re-establish the correspondence between the source and CPS calculi, we extend both the CPS transformation and its inverse and proceed in the same way as for the pure language. The resulting calculus includes the reductions of the λ_{v}-C-calculus [18, 19] and is equivalent to the equational subtheory of the logic IOCC (Impredicative theory of Operations, Control abstractions, and Classes) [48].

Finally, since Lisp and similar languages include more facilities than just procedures and control operators, we consider the language Core Scheme, which also includes constants, conditionals, and assignments. We develop a theory for reasoning about Core Scheme that proves all the equations that hold in the CPS framework. To illustrate the power of the theory, we optimize a Scheme program that implements a coroutine facility using first-class continuations. The left program in Figure 1, due to Haynes,

(define make-coroutine

(lambda (f )

(callcc

(lambda (maker)

(let ([LCS ’any])

(let ([resume

(lambda (dest val) (callcc (lambda (k)

(set! LCS k) (dest val))))])

(f resume

(resume maker

(lambda (v) (LCS v)))) (error "fell off end")))))))

(define make-coroutine

(lambda (f )

(letrec ([LCS

(lambda (x)

(f (lambda (dest val)

(callcc

(lambda (k) (set! LCS k) (dest val))))

x) (error "fell off end"))])

(lambda (v) (LCS v)))))

Figure 1: Coroutines from Continuations.

Friedman, and Wand [27], is the result of clear and well-understood design steps but is far more complicated than necessary. The initialization part of the coroutine is non-trivial: it involves capturing a continuation and an artificial use of the procedure resume that assigns the proper value to the local control state (LCS). The second program, a variant of the first according to folklore, avoids the clumsy initialization phase and immediately returns a closure. Using our new set of axioms, we can rewrite the left program to the second. The derivation is subject of Section 10.

The next section introduces the basic terminology and notation of the λ-calculus and its semantics. Sections 3 to 6 are dedicated to the pure call-by-value language. Section 3 includes a short history of CPS transformations that motivates the ideas that lead to our new CPS transformation in Section 4. The inverse mapping is the subject of Section 5. In Section 6, we identify the complete set of axioms X and prove its completeness with respect to β- and η-reductions on CPS terms. Section 7 extends the result to a language that includes the non-local control operators abort and callwith-current-continuation. Section 8 deals with the addition of constants, assignments, and conditionals. Finally, we conclude with a brief discussion of the theoretical and practical implications of our work and future directions of research. The appendix includes the tedious but straightforward portions of the proofs.

2. Λ: Calculi and Semantics

The language Λ is a pure (constant-free) functional language. The set of terms is generated inductively over an infinite set of variables Vars; it includes values and applications. Values consist of variables and λabstractions, applications are juxtapositions of terms:

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

We adopt Barendregt’s [4, chapters 2, 3] notation and terminology for Λ’s 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. 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 term M[x := N] is the result of the capture-free substitution of all free occurrences of x in M by N, e.g., (λx.xz)[z := (λy.x)] ≡ (λu.u(λy.x)). A context C is a term with a “hole”, [ ], in the place of one subterm. The operation of filling the context C with a term M yields the term C[M], possibly capturing some free variables of M in the process, e.g., the result of filling (λx.x[ ]) with (λy.x) is (λx.x(λy.x)). The variables that may be captured when filling a context C are called the trapped variables of C and are denoted by trap(C).

Calculi

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

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

A reduction may also be applied to a context C_{1} yielding another context C_{2}. In that case, the holes in both contexts are treated as placeholders to an arbitrary term. We only use such reductions when the sets of trapped variables in both contexts are empty (cf. evaluation contexts below).

The set of inference rules is identical for all λ-calculi. It extends some notions of reduction 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 λX to refer to the theory generated by a set of axioms X. When a theory λX proves an equation M = N, we write λX ⊢ M = N. If the proof does not use the inference rule (Symmetry), we write λX ⊢ 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.

Many of the results in the paper relate the calculi for different languages. To provide a uniform terminology for the relationships between such systems, we introduce the concept of “equational correspondence”.

Definition 1 (Equational Correspondence) Let S and T be two languages with calculi λX_{S} and λX_{T} respectively. Also let f : S → T be a translation from S to T , and g : T → S be a translation from T to S. Finally let s, s_{1}, s_{2} ∈ S and t, t_{1}, t_{2} ∈ T . Then the calculus λX_{S} equationally corresponds to the calculus λX_{T} if the following four conditions hold:

1. λX_{S} ⊢ s = (g ∘ f)(s).

2. λX_{T} ⊢ t = (f ∘ g)(t).

3. λX_{S} ⊢ s_{1} = s_{2} if and only if λX_{T} ⊢ f(s_{1}) = f(s_{2}).

4. λX_{T} ⊢ t_{1} = t_{2} if and only if λX_{S} ⊢ g(t_{1}) = g(t_{2}).

The above correspondence is similar to the correspondence between the λ-calculus and combinatory logic [4, 10]. In the third clause, the left-to-right implication refers to the soundness of the calculus λX_{S}, and the rightto-left implication refers the completeness of the calculus λX_{S} (relative to λX_{T}, f, and g).

Semantics

The semantics of the language Λ is a (partial) 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 hardware stacks, stores, registers, etc. Examples are the SECD machine [31] and the CEK machine [16].

An equivalent method for specifying the semantics is based on the Curry-Feys Standard Reduction Theorem [16, 39]. 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 special context E and a leftmost-outermost redex R (not inside an abstraction), and (ii) fills E with the contractum of R. The special contexts are evaluation contexts and have the following definition for the call-by-value and call-by-name variants of Λ, respectively [16]:

\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, is E [16]. For a call-by-value language, the syntax of the terms can therefore be reformulated as follows:

M ::= V | E_{v}[(V V)]  (Λ)
V ::= x | (λx.M)  (Values)
E_{v} ::= [ ] | (V E_{v}) | (E_{v} M)  (EvCont)

A similar definition exists for the call-by-name language except that arguments are not evaluated before a function call, i.e., evaluation contexts do not include contexts of the shape (V E_{n}).

Using 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 relation ⟼. The semantics of Λ is defined as follows:

eval_{v}(M) = V if and only if M ⟼_{v}^{∗} V  (call-by-value)
eval_{n}(M) = V if and only if M ⟼_{n}^{∗} V  (call-by-name)

3. The Origins and Practice of CPS

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

The first subsection briefly reviews the original encoding of the CPS transformation. In the second subsection, we analyze the universe of CPS terms and the so-called administrative CPS reductions.

3.1. The Original Encoding

Fischer [21] 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 [21, page 104].

3The origin of the concept of “continuation” can be traced back to A. van Wijngaarden [45] who defined a source to source transformation that eliminates jumps (goto instructions) from a program in favor of procedures that never return.

The translation he refers to is the Fischer CPS transformation.

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

F : Λ → Λ
F[[V]] = λk.(k F_{v}[[V]])
F[[MN]] = λk.(F[[M]] (λm.(F[[N]] λn.((m k) n))))
F_{v} : Values → Λ
F_{v}[[x]] = x
F_{v}[[λx.M]] = λk.λx.(F[[M]] k)

Reynolds [41] 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 method to transform an interpreter such that it becomes indifferent to whether the underlying parameter passing technique is callby-value or call-by-name. His transformation is essentially the same transformation as Fischer’s.^{4} Plotkin [39] later proved Reynolds’s ideas correct.

Theorem 1 (Plotkin [39]) Let M ∈ Λ.

Simulation: F_{v}[[eval_{v}(M)]] = eval_{v}(F[[M]] (λx.x))
Indifference: eval_{n}(F[[M]] (λx.x)) = eval_{v}(F[[M]] (λx.x))
Translation: If λβ_{v} ⊢ M = N then λβ ⊢ F[[M]] = F[[N]]. The

implication is not reversible. Also, λβ_{v} ⊢ F[[M]] = F[[N]] if and only if λβ ⊢ F[[M]] = F[[N]].

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 Translation Theorem establishes the soundness and incompleteness of λβ_{v} for reasoning about CPS programs.

3.2. The Universe of CPS Terms

Since we are interested in the analysis of βη-equality on CPS terms, our universe of discourse consists of all terms that contribute to the proofs of equations like:

λβη ⊢ F[[M]] = F[[N]].

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

Because the notion of reduction βη is CR [4], it suffices to consider equations of the form:

λβη ⊢ F[[M]] ⟶ ⟶ P.

Hence, the universe of discourse for CPS terms is the set:

{P | ∃M ∈ Λ. λβη ⊢ F[[M]] ⟶ ⟶ P }.

Unfortunately, this set includes a large of terms that have no counterpart in the source language. For example, the source reduction:

((λx.x) y) ⟶ y

corresponds to the following derivation on CPS terms:

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

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

The derivation mostly consists of reductions that do not correspond to reductions of source terms.

The “new” reductions on CPS terms are known as administrative reductions [39]. In order to give a precise definition of these new reductions, we modify the Fischer CPS transformation by overlining all λ-abstractions that are introduced during the translation. The reduction of any of these overlined λ-abstractions constitutes an administrative reduction.

Definition 3 (F, \overline{β}, \overline{η}) Let k, m, n ∈ Vars be variables that do not occur in the argument to F.

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

\begin{aligned}F_{v} : Values & → & Λ \\ F_{v}[[x]] & = & x \\ F_{v}[[λx.M]] & = & \overline{λ}k.λx.(F[[M]] k) \end{aligned}

A β- or η-reduction is an administrative reduction if it involves overlined abstractions:

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

To simplify the derivation of the source reductions that correspond to βη on CPS terms, we split the problem in two parts: finding source reductions that correspond to administrative CPS reductions (Section 4), and finding source reductions that correspond to proper CPS reductions (Sections 5 and 6).

4. A Compacting CPS Transformation

To identify all the source reductions that correspond to the CPS administrative reductions at once, we define a compacting CPS transformation that performs the administrative reductions in the output of F and produces terms in \overline{β}\overline{η}-normal form.

The first subsection formally defines the process of eliminating the administrative reductions from the output of F and analyzes the connection between the elimination process and the evaluation of CPS programs. The second subsection includes a new compacting CPS transformation that illuminates the effect of administrative reductions. Subsection 3 includes the source reductions that correspond to the elimination of the administrative CPS reductions. Finally, the last subsection includes the definition of a simplified universe of CPS terms based on the new CPS transformation.

4.1. The Two-Pass CPS Transformation

The relation F2 combines the Fischer CPS transformation with the elimination of the administrative reductions.

Definition 4 (F2) Let M ∈ Λ, then F2[[M]] = P if and only if λ\overline{β}\overline{η} ⊢ F[[M]] = P and P is in \overline{β}\overline{η}-normal form.

Each source term is related by F2 to exactly one CPS term in \overline{β}\overline{η}-normal form.

Proposition 2 The relation F2 is a total function from Λ to Λ.

Proof: ^{5} It is sufficient to show that F[[M]] has a unique \overline{β}\overline{η}-normal form. The \overline{β}-reductions starting with F[[M]] are a special kind of reductions called developments [4, section 11.2]. It follows that F[[M]] has a unique \overline{β}-normal form [4, corollary 11.2.24]. Moreover, a Λterm has a β-normal form if and only it has a βη-normal form [4, corollary 15.1.5]. It follows that F[[M]] has a unique \overline{β}\overline{η}-normal form.

In other words, the function F2 specifies a CPS transformation that produces terms without any administrative redexes.^{6}

The proposition also establishes that administrative reductions can be performed in any order without affecting the result. A quick look at their effect on standard reduction sequences is particularly illuminating.

According to Plotkin [39], the standard reduction sequence of a source program relates to the standard reduction sequence of its CPS counterpart as described in the following diagram:

[figure: •; M; ⟼_{v}; •; N; ⟼_{v}; •; L; .; .; .; .; F[[M]]K; •; F[[N]]K; •; F[[L]]K; •; •; •; •; M : K; N : K; L : K; .; .; .; .; .; .]

5Improved by Robert Harper.

6The function F2 eliminates more administrative than other CPS transformations [3, 13, 30, 43, 46]. For example, applying F2 to (((λx.λy.x) a) b) yields λk.((λx.((λy.kx) b)) a). For the same example, both Steele’s Rabbit transformation [46] and the Danvy/Filinski transformation [13] yield the term:

λ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 without eliminating source redexes:

λβη ⊢ λ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).

The term M : K is the result of eliminating all the administrative reductions before the first (in a standard reduction sequence) proper reduction in (F[[M]] K). The solid lines represent the reduction of source redexes; the dashed lines correspond to the reduction of administrative redexes.

By Plotkin’s analysis, the role of the administrative reductions is to locate the next source redex in a standard reduction sequence, and to restructure the CPS program such that this redex occurs at the top level. For example, in the term:

M =^{df} ((λy.y) ((λx.x) z)),

the first redex in a standard reduction sequence is ((λx.x) z). After CPS conversion and the elimination of all administrative reductions, we get:

P =^{df} (F2[[M]] (λa.a)) = ((λx.((λy.((λa.a) y)) x)) z),

where the redex ((λx. · · ·) z) occurs at the top level.

Although the action of “lifting” the redex ((λx. · · ·) z) to the top level happens naturally in the CPS framework, it does not require an explicit CPS conversion, i.e., we can rewrite the original program as follows:

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

This example suggests that administrative CPS reductions are naturally expressible in the source language. We investigate the exact nature of these source reductions in the next subsection.

4.2. The CPS Transformation C_{k}

By specifying the function F2 in a new and original way that illuminates the effect of administrative reductions on the reduction of source and CPS terms, we can directly identify two notions of reduction on source terms that perform the same task as administrative reductions.

The key insights that are necessary to derive the new CPS transformation are the following:

• The evaluation context is a syntactic representation of the continuation (cf. Section 2).

• The first redex in a standard reduction sequence always occurs inside the evaluation context (cf. Section 2).

• Administrative reductions “lift” the redex that occurs inside the evaluation context to the top level (cf. Section 4.1).

Based on these insights, we develop the new compacting CPS transformation C_{k}. The transformation relies on the following definition of the set of evaluation contexts, which is more suitable for the following definition:

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

The definition generates the same set as the one in Section 2.

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

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]])
Φ : Values → Λ
Φ[[x]] = x
Φ[[λx.M]] = \overline{λ}k.λx.C_{k}[[M]]
K_{k} : EvCont → Λ
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)]]])

The transformation of a complete program M is λk.C_{k}[[M]]. The function C_{k} is parametrized over a variable k that represents the current continuation. The CPS transform of values is straightforward. The translation of E[(x V)] generates a term in which the unknown procedure x is applied to the continuation K_{k}[[E]] and the result applied to the argument Φ[[V]]. The CPS transform of E[((λx.M) V)] conceptually lifts the redex outside the evaluation context producing ((λx.E[M]) V) and then converts the resulting term to CPS. The first three cases in the translation of evaluation contexts to continuations have the same intuitive explanation. In the last case E[([ ] M)], the term in function position is the result of an intermediate computation. The CPS transformation gives the intermediate result a fresh name u_{i} and proceeds with the translation of a simpler term.

7The CPS transformation C_{k} is, in spirit, similar to the CPS transformation by Friedman, Wand, and Haynes [24, chapter 8], but differs significantly in its formal part.

While C_{k}, Φ and K_{k} are not defined by structural induction, it is relatively easy to check that the functions are well-defined using an appropriate notion of “size”.

Definition 6 (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.

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. Also, the size of (λx.M) is greater than the size of M by 1.

The following proposition verifies that the outputs of C_{k} and F2 are identical. As a consequence, the result also establishes that C_{k} is a total function.

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

Proof: By the definition of F2, it suffices to establish the following statements:

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

• C_{k}[[M]] is in \overline{β}\overline{η}-normal form.

• (F[[M]] k) has a unique \overline{β}\overline{η}-normal form.

The last claim follows from Proposition 2. The proofs of the first two claims are in the Appendix (Page 48).

4.3. Administrative Source Reductions: The A-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. (Proposition 11 verifies that there are indeed only two such cases.)

Lemma 4 (β_{lift}, β_{flat}) Let M, N, L ∈ Λ, E ∈ EvCont, and z ∈ Vars:

C_{k}[[E[((λx.M) N)]]] ≡ C_{k}[[((λx.E[M]) N)]] where x ∉ F V (E)
C_{k}[[((z M) L)]] ≡ C_{k}[[((λu.uL) (z M))]] where u ∉ F V (L)

Proof: The proof of the first claim is straightforward. The proof of the second claim^{8} is in the Appendix (Page 50). The identity in the second statement holds modulo the decorating overlines above administrative λ-abstractions.

To characterize these effects of the C_{k}-translation, we introduce two reductions on Λ that capture the effect of the administrative reductions.

Definition 7 (A-reductions, β_{lift}, β_{flat}) The set of axioms A contains two reductions:

E[((λx.M) N)] ⟶ ((λx.E[M]) N)  (β_{lift})
where E ≠ [ ] and x ∉ F V (E)
((z M) L) ⟶ ((λu.(u L)) (z M))  (β_{flat})
where u ∉ F V (L)

As Lemma 4 shows, the A-reductions define equivalence classes of source terms that map to the same CPS term.

At this point, the decorating overlines above the special λ-abstractions become irrelevant. In the remainder of the paper, we ignore the distinction between λ and \overline{λ}.

4.4. The CPS Language

Using the equivalence of the functions F2 and C_{k}, we can specify the universe of CPS terms as follows:

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

ignoring the outermost binding of the continuation.

The context-free grammar that generates the set S can be directly derived from the right hand sides of the equations in Definition 5. According to the definition, all terms in the CPS language are an application of a continuation to a value. Values are either variables or abstractions that transform continuations. Continuations are either variables, or the result of the application of a value to a continuation, or an abstraction that transforms a value to an answer.

8The earlier version of the paper [42] erroneously included an arbitrary term M in place of the variable z.

Definition 8 (CPS grammar, CPS program, cps(Λ)) Let K-Vars = {k} be a set of continuation variables such that Vars ∩ K-Vars = ∅.

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

The special status reserved for the variable k ensures that the continuation parameter occurs exactly once in the body of 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 parameter. When working with the quotient of the language under α-equivalence, the special status of the name “k” disappears but the linearity constraint remains.

The following theorem establishes that the two definitions of CPS terms define the same language.

Theorem 5 S = cps(Λ).

Proof: For the left to right inclusion, it suffices to show that the output of C_{k} is a subset of cps(Λ), and that the latter language is closed under βη-reductions. We omit the proof of the first claim. The second claim follows from the Subject Reduction Lemma (Lemma 6). For the opposite implication, i.e., cps(Λ) ⊆ S, it suffices to show that for all P ∈ cps(Λ), there exists M ∈ Λ such that λβη ⊢ C_{k}[[M]]⟶ ⟶P. The proof of this auxiliary claim is in the Appendix (Page 51).

To complete the proof of the theorem, we need to establish that βηreductions on cps(Λ) preserve the syntactic categories of the terms.

Lemma 6 (Subject Reduction) Let P_{1} ∈ cps(Λ), W_{1} ∈ cps(Values) and 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: See Appendix (Page 52).

The above lemma implies that βη-reductions on CPS terms can be naturally characterized as reductions that apply to continuations and reductions that apply to values.

Corollary 7 The reductions β and η on cps(Λ) can be decomposed into reductions that apply to values (β_{w} and η_{w}) and reductions that apply to continuations (β_{k} and η_{k}):

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

5. A CPS Inverse

In order to map the CPS reductions β_{w}, β_{k}, η_{w}, and η_{k} to reductions on the source language, we define a mapping from cps(Λ) to Λ. After presenting the new transformation in the first subsection, we study its connection to the CPS transformation in the second subsection.

5.1. The Transformation C^{−1}

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 (K W) is E[V] where E is the evaluation context that syntactically represents the continuation K, and V is the value that corresponds to W.

Definition 9 (C^{−1}, Φ^{−1}, K^{−1}) Let P ∈ cps(Λ), W ∈ cps(Values), and K, K_{1}, K_{2} ∈ cps(EvCont):

C^{−1} : cps(Λ) → Λ
C^{−1}[[(K W)]] = K^{−1}[[K]][Φ^{−1}[[W]]]
Φ^{−1} : cps(Values) → Values
Φ^{−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} : cps(EvCont) → EvCont
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]]) [ ])

The correctness of the function C^{−1} is subject of the following theorem. The first part of the theorem establishes that the composition of C^{−1} and C_{k} respects βη-equality. The second part of the theorem establishes the stronger property that, when restricted to images of Λ terms, the composition of C^{−1} and C_{k} yields the identity function.

Theorem 8 Let P ∈ cps(Λ), K ∈ cps(EvCont). Then,

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

2. (C_{k} ∘ C^{−1})[[P]] ≡ P and (K_{k} ∘ K^{−1})[[K]] ≡ K if there exists M ∈ Λ and E ∈ EvCont such that P = C_{k}[[M]] and K = K_{k}[[E]].

Proof: See Appendix (Page 54).

5.2. Composing C_{k} and C^{−1}

The compacting CPS transformation C_{k} maps all the members of Aequivalence classes to the same CPS term (cf. Section 4.3). Our inverse CPS transformation maps this CPS term back to a particular element of the equivalence class, the element in β_{lift}β_{flat}-normal form. In order to establish this result, we first define a subset of Λ in β_{lift}β_{flat}-normal form.

Definition 10 (Λ_{a}) The language Λ_{a} is a subset of Λ that only includes terms in β_{lift}β_{flat}-normal form.

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

We omit the simple inductive proof that the elements of the language are actually in β_{lift}β_{flat}-normal form.

The range of the function C^{−1} is included in Λ_{a}, i.e., any output of C^{−1} is in β_{lift}β_{flat}-normal form.

Lemma 9 Let P ∈ cps(Λ) and K ∈ cps(EvCont), then C^{−1}[[P]] ∈ Λ_{a} and K^{−1}[[K]] ∈ EvCont_{a}.

Proof: See Appendix (Page 55).

With the help of this lemma, we can now specify the precise relation between the CPS transformation and its inverse. The effect of composing the CPS transformation with its inverse is to reduce terms to β_{lift}β_{flat}- normal form. Naturally, if a term is already in β_{lift}β_{flat}-normal form, then the composition yields the identity function.

Theorem 10 Let M ∈ Λ, then:

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

2. (C^{−1} ∘C_{k})[[M]] ≡ M if there exists P ∈ cps(Λ) such that M = C^{−1}[[P]].

Proof: See Appendix (Page 56).

Put differently, the theorem asserts that the reductions β_{lift}β_{flat} capture all possible equivalences introduced by administrative reductions. If the CPS transforms of M and N are related by those administrative reductions that C_{k} eliminates, then it must be the case that M and N are related by the axioms β_{lift}β_{flat}.

Proposition 11 If C_{k}[[M]] ≡ C_{k}[[N]], then λβ_{lift}β_{flat} ⊢ M = N.

Proof: Assume C_{k}[[M]] ≡ C_{k}[[N]] ≡ P. The function C^{−1} maps P, the CPS transform of M or N, to a source term L. By Theorem 10, both M and N reduce to L by β_{lift}β_{flat}-reductions. It follows that λβ_{lift}β_{flat} ⊢ M = N.

6. Equational Correspondence for the Pure Language

Using the partial inverse of the CPS transformation, we can systematically derive a set of additional axioms B for λβ_{v} such that X = A ∪ B, i.e., such that λβ_{v}AB 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 correspondence of the calculi.

6.1. Completeness

As specified in Corollary 7, the possible β- and η-reductions on CPS terms are β_{w}, β_{k}, η_{w}, and η_{k}. To illustrate our technique, 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 term, the extended set of axioms 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 in the first case, we must add the following reduction to the set B:

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

• K = ((λk.K_{1}) K_{2}) or K = λy.P: these cases do not introduce any new reductions.

The cases for the other reductions on CPS terms are similar. The resulting set of source reductions X includes all the previously derived reductions and η_{v}: see Figure 2. The equational theory generated by the full set of

((λ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})
((z M) L) ⟶ ((λu.(u L)) (z M)) u ∉ F V (L) (β_{flat})
((λx.x) M) ⟶ M  (β_{id})
((λx.E[(y x)]) M) ⟶ E[(y M)]  x ∉ F V (E[y])  (β_{Ω})

Figure 2: Source Reductions: X =^{df} {η_{v}, β_{lift}, β_{flat}, β_{id}, β_{Ω}}.

axioms λβ_{v}X corresponds to Moggi’s untyped computational λ-calculus as it appeared in his original Edinburgh LFCS Technical Report [36].

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

Lemma 12 (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 independent from the proofs of other cases.

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 the left hand side, we get the term Φ^{−1}[[(λk.W k)]] which is equivalent to (λx.C^{−1}[[((W k) x)]]). We show that the latter term reduces to Φ^{−1}[[W]] by cases:

• 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: λx.((λz.C^{−1}[[P]]) x) ⟶ λz.C^{−1}[[P]] is an η_{v}-reduction.

4. β_{w}-reduction: See Appendix (Page 57).

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

Theorem 13 (Completeness) Let P ∈ cps(Λ). If λβη ⊢ P ⟶ ⟶ Q then λβ_{v}X ⊢ C^{−1}[[P]] ⟶ ⟶ C^{−1}[[Q]].

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

6.2. Soundness

The set of source reductions in Figure 2 is sound with respect to the equational theory over CPS terms. In fact, we can prove the following stronger results on the correspondence of reduction steps.

Lemma 14 (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}[[N]].

6. If λβ_{Ω} ⊢ M ⟶ N then λη_{k} ⊢ C_{k}[[M]] ⟶ ⟶ C_{k}[[N]].

Proof: The proofs for β_{lift} and β_{flat} are in Lemma 4. The proof for β_{v}-reductions is in the Appendix (Page 60). The other proofs are similar.

The Soundness Theorem summarizes the results of this subsection.

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

Proof: By pasting the proofs of the Soundness Lemma.

6.3. Equational Correspondence

The Completeness and Soundness Theorems in the previous sections are formulated in the most precise way. In particular, the theorems relate reduction steps in one calculus to reduction steps in the other calculus. Together with Theorems 8 and 10 about the composition of the CPS transformation and its inverse, they imply the results of Figure 3. In the figure, the dotted lines correspond to the application of C_{k} or C^{−1}. The solid lines represent sequences of reductions.

The correspondence of reduction steps reveals the close relation between source terms in A-normal form and CPS terms. Unfortunately, this correspondence of reduction steps relies crucially on the properties of the functions C_{k} and C^{−1}, and does not appear to hold for arbitrary CPS transformation and their inverses.

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

Figure 3: The Correspondence of Reduction Steps.

In contrast, the correspondence of equalities in the source and CPS calculi holds for any transformations cps and uncps that satisfy the following equations:

\begin{matrix}λβη & ⊢ & cps(M) = C_{k}[[M]] \\ λβ_{v}X & ⊢ & uncps(P) = C^{−1}[[P]] \end{matrix} (†)

For such transformations, it is straightforward to deduce variants of Theorems 8, 10, 15, and 13 that relate equalities in one calculus to equalities in the other calculus. The combination of the four theorems implies an equational correspondence in the sense of Definition 1.

Theorem 16 (Equational Correspondence) The theory λβ_{v}X equationally corresponds to the theory λβη for any cps and uncps functions satisfying (†).

The formulation of the calculus λβ_{v}X based on the six axioms in Figure 2 is only necessary for the correspondence of reduction steps. For the equational correspondence, there is no reason to distinguish between the reductions β_{flat}, β_{id}, and β_{Ω} as we can summarize the three reductions with the following axiom:

((λx.E[x]) M) = E[M]  x ∉ F V (E)  (β′_{Ω})

We will use the axiom (β′_{Ω}) in the remainder of the paper.

7. Non-Local Control Operators

After establishing the Equational Correspondence Theorem for pure callby-value languages, we turn our attention to languages with control operators. Specifically, we investigate the addition of the control operators abort (A) and call-with-current-continuation (callcc). Informally, A permits the programmer to ignore the rest of a computation and return the value of a subexpression as the result of the entire program, while callcc provides the programmer with a procedural abstraction of the rest of the computation. Because the two operators manipulate the global control state of the program, their CPS transforms are procedures that manipulate the continuation in non-standard ways. As a consequence, the CPS language includes new terms and the first Equational Correspondence Theorem no longer applies. In the remainder of the section, we formalize these ideas and conclude with a version of the Equational Correspondence Theorem for the extended language. The development of the section follows the development of Sections 4 to 6 with one exception. None of the intermediate results is concerned with mapping the reductions of one calculus to the reductions of the other. Rather the intermediate results only relate the equalities of one calculus to the equalities of the other. At this point, it is an open question whether the results can be re-established for reductions (as opposed to equalities).^{9}

7.1. The Extended Language and its Semantics

The extension of the source language with the functional constants callcc and A results in the language Λ + callcc + A:

\begin{aligned}M & ::= & V | E[(V V)] \\ V & ::= & x | (λx.M) | callcc | A \\ E & ::= & [ ] | (V E) | (E M) \end{aligned}

Instead of providing a formal semantics for callcc and A in terms of standard reductions, we follow the more traditional route and immediately specify the translation of these values into CPS form and use this translation as their formal semantics.^{10} The extensions to C_{k} (or F) consist of two additional clauses to the function Φ (or F_{v}) [8]:

9Griffin [26] established that, in the presence of control operators similar to A and callcc, standard reductions on source terms correspond to standard reductions on CPS terms. His result does not imply that an arbitrary sequence of reductions in either calculus correspond to another sequence of reductions in the other calculus.

Φ[[callcc]] = (λk.λu.((u k) λd.k))
Φ[[A]] = (λk.λx.x)

The CPS transform of callcc is a procedure that expects a continuation k and an argument u. The non-standard manipulation of the continuation is manifest in the second argument to u, which is a procedural abstraction of the continuation. Similarly, the CPS transform of A is a procedure that expects a continuation k and an argument x. The procedure ignores its continuation argument (k) and immediately returns its value argument (x). The non-use of k is again a non-standard manipulation of the continuation. Given the CPS transformation, the formal semantics of the source language is:

eval_{v}(M) = V if and only if eval_{n}((λk.C_{k}[[M]]) λx.x) = Φ[[V]].

In order to simplify the following discussions (and proofs), we use a CPS transformation that is less compacting but more suited for the analysis than the one in Definition 5.

Definition 11 (C_{k} with Control Operators) Let k, u_{i} ∈ Vars be variables that do not occur in the argument to C_{k}.

C_{k}[[V]] = (k Φ[[V]])
C_{k}[[E[(V_{1} V_{2})]]] = ((Φ[[V_{1}]] K_{k}[[E]]) Φ[[V_{2}]])
Φ[[x]] = x
Φ[[λx.M]] = λk.λx.C_{k}[[M]]
Φ[[callcc]] = λk.λu.((u k) λd.k)
Φ[[A]] = λk.λx.x
K_{k}[[[ ]]] = k
K_{k}[[E[(V [ ])]]] = (Φ[[V]] K_{k}[[E]])
K_{k}[[E[([ ] M)]]] = λf.C_{k}[[E[(f M)]]]

10Felleisen et al. [16, 18, 19] and Talcott [48] use alternative definitions that do not rely on the CPS transformation.

Besides the extensions to callcc and A, the transformation differs from the function in Definition 5 in the following aspect. The new function translates expressions of the form E[(V M)] uniformly for all values V. By not including a special clause for each kind of value, the CPS transformation may produce terms with administrative redexes. However, the presence of these administrative redexes is irrelevant since it does not affect the set of reachable CPS terms, and we are no longer concerned with mapping the reductions of one calculus to the reductions of the other calculus.

7.2. The CPS Language and the Inverse Translation

The closure of the output of C_{k} under βη-reductions yields an extension of the CPS language of Definition 8.

Definition 12 (CPS grammar cps(Λ + callcc + A)) The extended CPS terms are generated by the following grammar:

P ::= W | (K W)  (cps(Λ + callcc + A) = Answers)
W ::= x | (λk.K)  (Values)
K ::= k | (λx.P) | (W K)  (Continuations)
x ∈ Vars
k ∈ K-Vars = {k_{1}, k_{2}, …} and K-Vars ∩ Vars = ∅

A comparison with Definition 8 explains how the addition of callcc and A affects the set of reachable CPS terms and thus, how it affects the semantics. Intuitively, callcc permits the programmer to “label” arbitrary points in the program. Thus more than one continuation can potentially be lexically visible at any point during the execution of the program. The extended CPS language accommodates this fact by providing an infinite set of continuation variables instead of a singleton. The addition of A permits the programmer to ignore the current continuation by returning a value as the answer of the entire program. This extension is reflected in the CPS language by extending the syntactic category of answers to include values directly. An equivalent way to understand the effect of A is that A ignores the current continuation and uses the initial continuation (λx.x) instead. We therefore may extend the syntactic category of continuations with an “initial continuation” (λx.x). Because, our CPS language is closed under βη-reductions, the addition of the initial continuation results in programs of the shape P = ((λx.x) W) ⟶ W and thus extends the syntactic category of answers with values.

The inverse CPS transformation mapping the extended CPS language to Λ + callcc + A is the following.

Definition 13 Let P ∈ cps(Λ + callcc + A). Let W and K be values and continuations in the same language:

C^{−1}[[W]] = (A Φ^{−1}[[W]])
C^{−1}[[(K W)]] = K^{−1}[[K]][Φ^{−1}[[W]]]
Φ^{−1}[[x]] = x
Φ^{−1}[[λk.K]] = λz.callcc λk.K^{−1}[[K]][z]
K^{−1}[[k]] = (k [ ])
K^{−1}[[(W K)]] = K^{−1}[[K]][(Φ^{−1}[[W]] [ ])]
K^{−1}[[λx.P]] = ((λx.C^{−1}[[P]]) [ ])

The transformation differs from the function in Definition 9 in several aspects. First, the inverse of an answer W is a term that aborts with the value Φ^{−1}[[W]]. Second, a binding of a continuation k in the CPS language corresponds to a capture of the continuation k in the source language. Finally, every continuation is explicitly invoked. The last two changes exploit an idea due to Danvy and Lawall [14].^{11}

The discovery of the call-by-value axioms that correspond to βη-reduc-tions on CPS terms proceeds in the same manner as for the pure language. The resulting axioms consist of the axioms X for the pure language and the control specific axioms in Figure 4. The new axioms have the following intuitive explanation. The first axiom shows that the current continuation is always implicitly applied. The axiom C_{elim} is a garbage-collection rule: continuations captured but not used can be collected. The axiom C_{lift} characterizes the capture of continuations via callcc while the axiom C_{abort} shows that continuations abort their context upon invocation. The last callcc axiom implies that the continuation of an application is indistinguishable from the continuation of the body.^{12} The operator A eliminates evaluation contexts.

The set of axioms C_{current}, C_{elim}, C_{lift}, C_{abort} and Abort constitute the control-specific axioms of the λ_{v}-C-calculus [18, 19]. The full theory λβ_{v}XC

11Danvy and Lawall [14] perform a counting analysis to determine whether a continuation is used in a non-standard way and include a callcc only when necessary. This analysis is unnecessary for our purposes. The outputs of our inverse transformation are provably equal to their outputs (in our axiom system), thus achieving the same effect without the counting analysis.

12… and a good implementation would use the same continuation: we can also interpret this law as imposing tail-call optimization on faithful implementations.

(callcc λk.kM) = (callcc λk.M)  (C_{current})
(callcc λd.M) = M d ∉ F V (M) (C_{elim})
E[(callcc M)] = callcc λk.E[(M (λf.(k E[f])))]  (C_{lift})
k, f ∉ F V (E, M)
callcc λk.C[E[(k M)]] = callcc λk.C[(k M)]  k ∈ F V (C[k])  (C_{abort})
(callcc λk.((λx.M) N)) = ((λx.(callcc λk.M)) N)  k ∉ F V (N)  (C_{tail})
E[(A M)] = (A M)  (Abort)

Figure 4: The Axioms C: {C_{current}, C_{elim}, C_{lift}, C_{abort}, C_{tail}, Abort}.

corresponds to the restriction of the theory IOCC [48] to the language Λ + callcc + A.

The relationship of C_{k} to the function C^{−1} is subject of two lemmas. The first lemma establishes that a CPS term P is βη-equal to (C_{k} ∘ C^{−1})[[P]] if it contains no free continuation variables, e.g., P ≡ x. The lemma proves a more general result that accounts for terms with free variables. The generalization is necessary for CPS terms like P ≡ (k_{1} x) or P ≡ (k_{1} (λd.k_{2})).

Lemma 17 Let P ∈ cps(Λ + callcc + A) and K be a continuation, and W be a value in the same language. Also, let k_{1}, …, k_{n} be the free continuation variables in these terms, and k ∉ {k_{1}, …, k_{n}}. Then,

1. λβη ⊢ (C_{k} ∘ C^{−1})[[P]][k_{1} := (λd.k_{1}), …, k_{n} := (λd.k_{n})] = P.

2. λβη ⊢ (K_{k} ∘ K^{−1})[[K]][k_{1} := (λd.k_{1}), …, k_{n} := (λd.k_{n})] = K.

3. λβη ⊢ (Φ ∘ Φ^{−1})[[W]][k_{1} := (λd.k_{1}), …, k_{n} := (λd.k_{n})] = W.

Proof: See Appendix (Page 61).

The second lemma relates the terms M and (C^{−1} ∘ C_{k})[[M]] via the axioms X for the pure language and the control-specific axioms C in Figure 4.

Lemma 18 Let M ∈ Λ + callcc + A, E be an evaluation context in the same language, and k a variable that is not free in either. Then,

• λβ_{v}XC ⊢ (C^{−1} ∘ C_{k})[[M]] = (k M)

• λβ_{v}XC ⊢ (K^{−1} ∘ K_{k})[[E]] = (k E)

Proof: See Appendix (Page 62).

7.3. Equational Correspondence

We establish that the calculus λβ_{v}XC proves all the equations that βη can prove on CPS terms. The key lemma is the following Completeness Lemma.

Lemma 19 Let P ∈ cps(Λ + callcc + A), and let k_{1} … k_{n} be the free continuation variables in P. Then, λβη ⊢ P = Q implies that:

λβ_{v}XC ⊢ callcc λk_{1}…. callcc λk_{n}.C^{−1}[[P]] =

callcc λk_{1}…. callcc λk_{n}.C^{−1}[[Q]].

Proof: We consider each notion of reduction separately.

1. The reduction is: ((λx.P) W) ⟶ P [x := W]. The proof of this case is in the Appendix (Page 64).

2. The reduction is: (λk.W k) ⟶ W where k is not free in W. We can apply Φ^{−1} or C^{−1} to both sides of the equation since W can be an answer or a value.

• W is an answer. Then,

C^{−1}[[(λk.W k)]] = (A λz.callcc λk.K^{−1}[[k]][(Φ^{−1}[[W]] z)])
= (A λz.Φ^{−1}[[W]] z)
= (A Φ^{−1}[[W]])

• W is a value. Then

Φ^{−1}[[λk.W k]] ≡ λz.callcc λk.K^{−1}[[k]][(Φ^{−1}[[W]] z)]

and a similar argument as in the preceding subcase applies.

3. The reduction is: (λx.Kx) ⟶ K where x is not free in K. Then K^{−1}[[λx.Kx]] ≡ ((λx.K^{−1}[[K]][x]) [ ]) is equal to K^{−1}[[K]] by β′_{Ω}.

4. The reduction is: ((λk.K_{1}) K_{2}) ⟶ K_{1}[k := K_{2}]. The proof is in the Appendix (Page 65).

The soundness of the new axioms is the subject of the following lemma.

Lemma 20 Let M, N ∈ Λ + callcc + A, then λβ_{v}XC ⊢ M = N implies that λβη ⊢ C_{k}[[M]] = C_{k}[[N]].

The above lemmas imply that the calculi λβ_{v}XC and λβη satisfy an Equational Correspondence Theorem.

Theorem 21 (Equational Correspondence) The theory λβ_{v}XC equationally corresponds to the theory λβη for any cps and uncps functions satisfying (†).

8. A Realistic Language

To be useful, a Correspondence Theorem should hold in the presence of programming languages constructs such as conditionals, constants, and mutable data objects. To address this issue, we consider a small, but typical subset of Scheme, Core Scheme, that we define in the first subsection. The second subsection introduces the CPS language for Core Scheme. Unlike in previous sections, the CPS language cannot be a subset of Λ, and as a result, the CPS equational theory includes more axioms than just β and η. Finally, in the last subsection we discuss how the different constructs affect the Correspondence Theorems. The development in the section includes enough details so that it can be adapted to the reader’s favorite language.

8.1. Core Scheme: CS

Core Scheme’s basic constants include numerals and booleans; functional constants include operations to manipulate the basic constants, e.g., addition, as well as operations to create, access, and update data-structures, e.g., lists, reference cells. The formal definition extends the grammar in Section 7.1:

M ::= … | E[(if V M M)] | E[(O V)] | E[(O V V)]
V ::= … | c
E ::= … | (if E M M) | (O E) | (O E M) | (O V E)
c ::= true | false | ^{⌈}n^{⌉}
O ::= integer? | add1 | / | ref | deref | setref!
n ∈ ℕ

Informally, integer? recognizes integers, add1 denotes the increment function, / is the integer division operator, ref creates a reference cell, deref returns the contents of a reference cell, and setref! updates the contents of its first argument (a reference cell) with the value of its second argument.

The set of axioms F in Figure 5 specifies the semantics of the new constructs. For convenience, we write ρ{(x_{1}, V_{1}), …, (x_{n}, V_{n})}.M as an abbreviation for:

(…((λx_{1}. · · · λx_{n}.(begin (setref! x_{1} V_{1}) … (setref! x_{n} V_{n}) M))

(ref 0)) … (ref 0)) where (begin M_{1} … M_{n}) is itself an abbreviation for:

(… ((λx_{1}. · · · λx_{n}.x_{n}) M_{1}) … M_{n})

(if true M N) = M  (If_{t})
(if false M N) = N  (If_{f})
(add1 ^{⌈}n^{⌉}) = ^{⌈}n + 1^{⌉}  (Add)
(/ ^{⌈}n^{⌉} ^{⌈}m^{⌉}) = ^{⌈}n/m^{⌉} m ≠ 0 (Div)
(/ ^{⌈}n^{⌉} ^{⌈}0^{⌉}) = (A ^{⌈}5^{⌉})  (Div_{e})
(integer? ^{⌈}n^{⌉}) = true  (Int_{t})
(integer? V) = false  V ≠ ^{⌈}n^{⌉}  (Int_{f})
(ref V) = ρ{(x, V)}.x  x ∉ F V (V)  (ref )
ρθ ∪ {(x, V)}.E[(deref x)] = ρθ ∪ {(x, V)}.E[V]  (deref )
ρθ ∪ {(x, V_{1})}.E[(setref! x V_{2})] = ρθ ∪ {(x, V_{2})}.E[V_{2}]  (setref )
ρθ_{1}.ρθ_{2}.M = ρθ_{1} ∪ θ_{2}.M  (ref_{∪})

Figure 5: Additional Axioms F for CS.

The first three sets of axioms are straightforward; the last set specifies the semantics of reference cells [9, 33].

The combination of the equational theory λβ_{v}XC with the new axioms F results in an inconsistent equational system due to η_{v}. For example, using η_{v}, we can show that for any two terms M and N:

M = (if true M N)  (If_{t})
= (if (integer? ^{⌈}0^{⌉}) M N)  (Int_{t})
= (if (integer? (λx.(^{⌈}0^{⌉} x))) M N)  (η_{v})
= (if false M N)  (Int_{f})
= N  (If_{f})

To avoid the consistency problem, we restrict the equational theory for the source language by eliminating η_{v}.

8.2. The CPS Language: CS_{k}

Given our extensions to the source language, the CPS language cannot be a subset of Λ unless the CPS transformation encodes all new constructs in the source language using procedures. Since such an encoding is not a proper CPS transformation, the CPS language must include constructs that correspond to the extensions of the source language.

The set of CPS terms extends the language in Definition 12 with the following additional clauses:

P ::= … | (if W P P) | (O_{k} K W) | (O_{k} K W W)
W ::= … | c
K ::= …
c ::= true | false | ^{⌈}n^{⌉}
O_{k} ::= integer?_{k} | add1_{k} | /_{k} | ref_{k} | deref_{k} | setref!_{k}

The semantics of the new constructs in the CPS language matches the semantics of the corresponding constructs in the source language. The set of axioms F_{k} in Figure 6 specifies this semantics precisely. For convenience, we also use ρ{(x_{1}, W_{1}), …, (x_{n}, W_{n})}.P as an abbreviation for:

(ref_{k} (λx_{1}. · · · (ref_{k} (λx_{n}.(setref!_{k} (λd. · · · (setref!_{k} (λd.P)
x_{n} W_{n}))
x_{1} W_{1}))

0))

0)

where d is not free in any of the x_{i}, W_{i} or P.

The CPS language includes a constant O_{k} for every functional constant O in the source language. The main difference between O_{k} and O is that the former takes an additional continuation argument that receives the result of the primitive application (if any). Thus, (O_{k} K W) is essentially equivalent to (K (O W)). We do not use the latter term because, contrary to the spirit of CPS translation (cf. Theorem 1), its evaluation is sensitive to the parameter-passing technique. For example, the evaluation of ((λd.^{⌈}8^{⌉}) (/ ^{⌈}1^{⌉} ^{⌈}0^{⌉})) yields an error (^{⌈}5^{⌉}) under call-by-value and yields ⌈8^{⌉} under call-by-name. Similarly, assuming that x is a reference cell whose contents is ^{⌈}1^{⌉}, the evaluation of the term:

ρ{(x,^{⌈}1^{⌉})}.((λd.(deref x)) (setref! x ^{⌈}2^{⌉}))

yields ^{⌈}2^{⌉} under call-by-value and yields ^{⌈}1^{⌉} under call-by-name.

(if true P Q) = P  (Ifk_{t})
(if false P Q) = Q  (Ifk_{f})
(add1_{k} K ^{⌈}n^{⌉}) = (K ^{⌈}n + 1^{⌉})  (Addk)
(/_{k} K ^{⌈}n^{⌉} ^{⌈}m^{⌉}) = (K ^{⌈}n/m^{⌉}) m ≠ 0 (Divk)
(/_{k} K ^{⌈}n^{⌉} ^{⌈}0^{⌉}) = ^{⌈}5^{⌉}  (Divk_{e})
(integer?_{k} K ^{⌈}n^{⌉}) = (K true)  (Intk_{t})
(integer?_{k} K W) = (K false) W ≠ ^{⌈}n^{⌉}  (Intf_{t})
(ref_{k} K W) = ρ{(x, W)}.(K x)  (refk)
x ∉ F V (W)
ρθ ∪ {(x, W)}.(deref_{k} K x) = ρθ ∪ {(x, W)}.(K W)  (derefk)
ρθ ∪ {(x, W_{1})}.(setref!_{k} K x W_{2}) = ρθ ∪ {(x, W_{2})}.(K W_{2})  (setrefk)
ρθ_{1}.ρθ_{2}.P = ρθ_{1} ∪ θ_{2}.P  (refk_{∪})

Figure 6: Additional Axioms F_{k} for CS_{k}.

8.3. Equational Correspondence

After setting the basic framework, we can define two translations, a CPS transformation and an inverse, between the languages CS and CS_{k}.

The CPS transformation of the new constructs in CS is the following:

C_{k}[[E[(if V M N)]]] = (if Φ[[V]] C_{k}[[E[M]]] C_{k}[[E[N]]])
C_{k}[[E[(O V)]]] = (O_{k} K_{k}[[E]] Φ[[V]])
C_{k}[[E[(O V_{1} V_{2})]]] = (O_{k} K_{k}[[E]] Φ[[V_{1}]] Φ[[V_{2}]])

\begin{aligned}Φ[[c]] & = & c \\ K_{k}[[E[(if [ ] M N)]]] & = & (λu.C_{k}[[E[(if u M N)]]]) \\ K_{k}[[E[(O [ ])]]] & = & (λu.C_{k}[[E[(O u)]]]) \\ K_{k}[[E[(O [ ] M)]]] & = & (λu.C_{k}[[E[(O u M)]]]) \\ K_{k}[[E[(O V [ ])]]] & = & (λu.C_{k}[[E[(O V u)]]]) \end{aligned}

The clause for conditionals duplicates the evaluation context E in both branches of the conditional expression. This duplication is due to two factors:^{13}

1. First, the Fischer CPS transformation for conditionals duplicates the continuation variable k:

F[[(if M N L)]] = λk.F[[M]] (λu.(if u F[[N]]k F[[L]]k)).

2. Second, the transformation C_{k} eliminates all the administrative redexes from the output of the Fischer CPS transformation.

The extensions to the CPS language result in simple extensions to the inverse CPS transformation:

C^{−1}[[(if W P_{1} P_{2})]] = (if Φ^{−1}[[W]] C^{−1}[[P_{1}]] C^{−1}[[P_{2}]])
C^{−1}[[(O_{k} K W)]] = K^{−1}[[K]][(O Φ^{−1}[[W]])]
C^{−1}[[(O_{k} K W_{1} W_{2})]] = K^{−1}[[K]][(O Φ^{−1}[[W_{1}]] Φ^{−1}[[W_{2}]])]
Φ^{−1}[[c]] = c

In order to establish the correspondence between the source and CPS calculi, we need to prove results similar to Lemma 17, Lemma 18, Lemma 19, and Lemma 20. The previous results cannot be extended immediately since we must eliminate η_{v} from the call-by-value equational theory. Furthermore, both the source and CPS equational theories include additional axioms for constants and conditionals (F and F_{k} respectively).

By revisiting the proofs of the four lemmas, we establish the following:

• The proof of Lemma 17 does not rely on η_{w}.

• The proof of Lemma 18 only uses a restricted version of η_{v} on continuations, A, and callcc:

(callcc (λk.C[(λx.kx)])) = (callcc (λk.C[k]))  (η_{v}_{1})
k ∉ trap(C)
(λx.callcc λk.xk) = callcc  (η_{v}_{2})
(λx.Ax) = A  (η_{v}_{3})

13Alternative translations that do not cause this exponential increase in the size of the code are:

C_{k}[[E[(if V M N)]]] = ((λk.(if Φ[[V]] C_{k}[[M]] C_{k}[[N]])) K_{k}[[E]])

or ((if Φ[[V]] (λk.C_{k}[[M]]) (λk.C_{k}[[N]])) K_{k}[[E]]).

The first translation is used by compilers [46] but also duplicates the entire evaluation context once we close the language under βη-reductions. The second translation relies on Allison’s [1] CPS translation that keeps the local transfer of control independent of the continuation.

The proof also requires the introduction of the following axiom for conditionals:

E[(if M N L)] = (if M E[N] E[L])  (If_{lift})

The axiom is introduced by the compacting phase of the CPS transformation and is thus an administrative call-by-value reduction (cf. Definition 7).

• The proof of Lemma 19 shows that η_{v}-reductions occur in the source language only as a result of η_{w}-reductions on CPS terms.

• The proof of Lemma 20 shows that η_{w}-reductions on CPS terms occur only as a result of η_{v}-reductions on source terms.

As a consequence, the complete equational theory for Core Scheme λCS with respect to its CPS language consists of all the previously derived axioms except η_{v}; the corresponding CPS equational theory consists of the axioms βηF excluding η_{w}.

9. Summary of the Results

The full equational theories for CS and CS_{k} are in Figures 7 and 8. The correspondences between the different axiom systems for the sublanguages in the previous sections are summarized in the following table.

Language  Call-by-Value Theory CPS Theory η_{v}/η_{w} Typed

Λ  X^{−}  βη_{k}  √  √

Λ + callcc + A  X^{−}C′  βη_{k}  √  √

CS  X^{−}C′F^{+}  βη_{k}F_{k}

CS^{T}  X^{−}C′F^{+}  βη_{k}F_{k}  √

The Axioms X^{−}:

((λx.M) V) = M[x := V]  (β_{v})
((λx.E[x]) M) = E[M]  (β′_{Ω})
E[((λx.M) N)] = ((λx.E[M]) N)  (β_{lift})

The Axioms C′:

E[(callcc M)] = callcc λk.E[(M (λf.(k E[f])))] (C_{lift})
(callcc λk.((λx.M) N)) = ((λx.(callcc λk.M)) N)  (C_{tail})
(callcc λk.kM) = (callcc λk.M)  (C_{current})
(callcc λd.M) = M  (C_{elim})
callcc λk.C[E[(k M)]] = callcc λk.C[(k M)]  (C_{abort})
E[(A M)] = (A M)  (Abort)
(callcc (λk.C[(λx.kx)])) = (callcc (λk.C[k]))  (η_{v}_{1})
(λx.callcc λk.xk) = callcc  (η_{v}_{2})
(λx.Ax) = A  (η_{v}_{3})

The Axioms F^{+}:

(if true M N) = M  (If_{t})
(if false M N) = N  (If_{f})
E[(if M N L)] = (if M E[N] E[L])  (If_{lift})
(add1 ^{⌈}n^{⌉}) = ^{⌈}n + 1^{⌉}  (Add)
(/ ^{⌈}n^{⌉} ^{⌈}m^{⌉}) = ^{⌈}n/m^{⌉} m ≠ 0 (Div)
(/ ^{⌈}n^{⌉} ^{⌈}0^{⌉}) = ^{⌈}5^{⌉}  (Div_{e})
(integer? ^{⌈}n^{⌉}) = true  (Int_{t})
(integer? V) = false  V ≠ ^{⌈}n^{⌉}  (Int_{f})
(ref V) = ρ{(x, V)}.x  x ∉ F V (V)  (ref )
ρθ ∪ {(x, V)}.E[(deref x)] = ρθ ∪ {(x, V)}.E[V]  (deref )
ρθ ∪ {(x, V_{1})}.E[(setref! x V_{2})] = ρθ ∪ {(x, V_{2})}.E[V_{2}]  (setref )
ρθ_{1}.ρθ_{2}.M = ρθ_{1} ∪ θ_{2}.M  (ref_{∪})

Figure 7: The Theory λCS.

The left column gives the name of the source language. The language CS^{T} is a simply typed variant of CS. The next two columns list the call-by-value axioms and the corresponding CPS axioms. The names of the axioms refer to the definitions in Figures 7 and 8. The column η_{v}/η_{w} includes a check mark if it is possible to extend the theories with η_{v} and η_{w}, respectively. The rightmost column includes a check mark if the correspondence holds for the simply typed variant of the language.

For the simply typed languages, our calculi are also “semantically complete” with respect to denotational CPS models [35]. The result is a consequence of the completeness of the λ-calculus with respect to the full type structure [42].

The Axioms βη_{k}:

((λx.P) W) = P [x := W]  (β_{w})
((λk.K_{1}) K_{2}) = K_{1}[k := K_{2}]  (β_{k})
(λx.Kx) = K  (η_{k})

The Axioms F_{k}:

(if true P Q) = P  (Ifk_{t})
(if false P Q) = Q  (Ifk_{f})
(add1_{k} K ^{⌈}n^{⌉}) = (K ^{⌈}n + 1^{⌉}) n ∈ ℕ  (Addk)
(/_{k} K ^{⌈}n^{⌉} ^{⌈}m^{⌉}) = (K ^{⌈}n/m^{⌉})m ≠ 0  (Divk)
(/_{k} K ^{⌈}n^{⌉} ^{⌈}0^{⌉}) = ^{⌈}5^{⌉}  (Divk_{e})
(integer?_{k} K ^{⌈}n^{⌉}) = (K true)  (Intk_{t})
(integer?_{k} K W) = (K false) W ≠ ^{⌈}n^{⌉}  (Intk_{f})
(ref_{k} K W) = ρ{(x, W)}.(K x)  (refk)
x ∉ F V (W)
ρθ ∪ {(x, W)}.(deref_{k} K x) = ρθ ∪ {(x, W)}.(K W) (derefk)
ρθ ∪ {(x, W_{1})}.(setref!_{k} K x W_{2})] = ρθ ∪ {(x, W_{2})}.(K W_{2}) (setrefk)
ρθ_{1}.ρθ_{2}.P = ρθ_{1} ∪ θ_{2}.P  (refk_{∪})

Figure 8: The Theory λCS_{k}.

10. Example: Coroutines from Continuations

The equational theory of Core Scheme λCS provides a basis for the semantic manipulation of programs by programmers and programming tools alike. For example, programmers may use the theory to evaluate programs in a symbolic manner, to prove the equivalence of two programs, or to simplify a program by a series of meaning-preserving transformations. The first subsection includes an intuitive explanation of a program that implements coroutines using first-class continuations and the second subsection includes a simplification phase based on the CS axioms.

10.1. The Original Program

For convenience, we use a superset of Core Scheme that includes assignments to variables via set!, and various other syntactic extensions [40]:

error =^{df} A
(let ([x M]) N) =^{df} ((λx.N) M)
(begin M N) =^{df} ((λd.N) M)  where d ∉ F V (N)

(λx.MN) =^{df} (λx.(begin M N))
(letrec ([x (λy.M)]) N)

=^{df}
(let ([x ’any])
(begin (set! x (λy.M)) N))

The original definition of coroutines using first-class continuations is the following [27]:

(define make-coroutine

(lambda (f )

(callcc (lambda (maker)

(let ([LCS ’any])

(let ([resume (lambda (dest val)
(callcc (lambda (k)

(set! LCS k) (dest val))))])

(f resume (resume maker (lambda (v) (LCS v)))) (error "fell off end")))))))

Intuitively, the procedure make-coroutine accepts an argument that contains the programmer’s coroutine code. For example, the pseudocode in Figure 9 implements one player in a hypothetical game.

(define Player-1-Code

(let ([Board (make-board)])

(lambda (resume his-first-shot)

(letrec ([loop (lambda (his-shot)
(if (his-shot-is-fatal?)

(I-lost-the-game)

(loop (resume Player-2 (compute-my-shot)))))])

(loop his-first-shot)))))

(define Player-1 (make-coroutine Player-1-Code))

Figure 9: Pseudo Coroutine Code.

The procedure resume handles the transfer of control from one coroutine to the other. As the definition of make-coroutine shows, resume takes two arguments: a destination that denotes the coroutine to be resumed and a value to be passed to the resumed coroutine. Before actually resuming the destination, resume saves the current continuation in the local control state LCS of the active coroutine, which makes it possible to resume the current coroutine later in the execution.

10.2. Simplifying the Program

The transformation of the program proceeds by applying one of the axioms of the λCS-calculus at each step. For clarity, the redex is surrounded by a box. During the transformation, set! is treated as a free variable. Alternatively, we could use the axioms of the λ_{v}-S-calculus [17], but for this example, they are superfluous.

(define make-coroutine (lambda (f )

(callcc (lambda (maker) (let ([LCS ’any]) (let ([resume (lambda (dest val) (callcc (lambda (k) (set! LCS k) (dest val))))]) (f resume (resume maker (lambda (v) (LCS v)))) (error "fell off end"))))) ))

by two uses of (C_{tail})

= (define make-coroutine

(lambda (f ) (let ([LCS ’any])

(let ([resume (lambda (dest val) (callcc (lambda (k) (set! LCS k) (dest val))))]) (callcc (lambda (maker) (f resume (resume maker (lambda (v) (LCS v)))) (error "fell off end")))) )))

by three uses of (β_{v})

= (define make-coroutine

(lambda (f )

(let ([LCS ’any])

(let ([resume (lambda (dest val)
(callcc (lambda (k)

(set! LCS k) (dest val))))])

(callcc (lambda (maker)

(f resume (callcc (lambda (k) (set! LCS k) (maker (lambda (v) (LCS v)))))) (error "fell off end") ))))))

by (C_{lift})

= (define make-coroutine

(lambda (f )

(let ([LCS ’any])

(let ([resume (lambda (dest val)
(callcc (lambda (k)

(set! LCS k) (dest val))))])

(callcc

(lambda (maker)

(callcc

(lambda (kk)

(f resume ((lambda (k)

(set! LCS k) (maker (lambda (v) (LCS v)))) (lambda (x)

(kk (begin (f resume x) (error "fell off end"))) )))

(error "fell off end")))))))))

by (β_{lift}) applied to the expansion of begin

= (define make-coroutine

(lambda (f )

(let ([LCS ’any])

(let ([resume (lambda (dest val)
(callcc (lambda (k)

(set! LCS k) (dest val))))])

(callcc

(lambda (maker)

(callcc

(lambda (kk)

(f resume ((lambda (k)

(set! LCS k) (maker (lambda (v) (LCS v)))) (lambda (x)

(begin (f resume x)

(kk (error "fell off end")) ))))

(error "fell off end")))))))))

by (Abort)

= (define make-coroutine

(lambda (f )

(let ([LCS ’any])

(let ([resume (lambda (dest val)
(callcc (lambda (k)

(set! LCS k) (dest val))))])

(callcc (lambda (maker)

(callcc (lambda (kk) (f resume ((lambda (k) (set! LCS k) (maker (lambda (v) (LCS v)))) (lambda (x) (begin (f resume x) (error "fell off end"))))) (error "fell off end"))) ))))))

by (C_{elim})

= (define make-coroutine

(lambda (f )

(let ([LCS ’any])

(let ([resume (lambda (dest val)
(callcc (lambda (k)

(set! LCS k) (dest val))))])

(callcc (lambda (maker)
(f resume

((lambda (k) (set! LCS k) (maker (lambda (v) (LCS v)))) (lambda (x) (begin (f resume x) (error "fell off end")))) )))))))

by (β_{v})

= (define make-coroutine

(lambda (f )

(let ([LCS ’any])

(let ([resume (lambda (dest val)
(callcc (lambda (k)

(set! LCS k) (dest val))))])

(callcc

(lambda (maker)

(f resume

(begin (set! LCS (lambda (x) (begin (f resume x) (error "fell off end")))) (maker (lambda (v) (LCS v)))) )))))))

by (β_{lift})

= (define make-coroutine

(lambda (f )

(let ([LCS ’any])

(let ([resume (lambda (dest val)
(callcc (lambda (k)

(set! LCS k) (dest val))))])

(callcc (lambda (maker)

(f resume (maker (begin (set! LCS (lambda (x) (begin (f resume x) (error "fell off end")))) (lambda (v) (LCS v))))) ))))))

by (C_{abort})

= (define make-coroutine

(lambda (f )

(let ([LCS ’any])

(let ([resume (lambda (dest val)
(callcc (lambda (k)

(set! LCS k) (dest val))))])

(callcc (lambda (maker) (maker (begin (set! LCS (lambda (x) (begin (f resume x) (error "fell off end")))) (lambda (v) (LCS v)))))) ))))

by (C_{current}) and (C_{elim})

= (define make-coroutine

(lambda (f ) (let ([LCS ’any])

(let ([resume (lambda (dest val) (callcc (lambda (k) (set! LCS k) (dest val))))]) (begin (set! LCS (lambda (x) (begin (f resume x) (error "fell off end")))) (lambda (v) (LCS v)))) )))

by (β_{v})

= (define make-coroutine

(lambda (f )

(let ([LCS ’any])

(begin (set! LCS (lambda (x)
(begin (f (lambda (dest val)

(callcc

(lambda (k) (set! LCS k) (dest val))))

x) (error "fell off end"))))

(lambda (v) (LCS v))))))

by the letrec macro definition

= (define make-coroutine

(lambda (f )

(letrec ([LCS (lambda (x)
(begin (f (lambda (dest val)
(callcc (lambda (k)

(set! LCS k) (dest val))))

x) (error "fell off end")))])

(lambda (v) (LCS v)))))

11. Conclusion and Future Research

The Equational Correspondence Theorems establish that equational reasoning about call-by-value programs can be as powerful as reasoning about their CPS counterparts.

Consequently, any CPS-based programming tool that performs sequences of βη-reductions can be substituted by an equivalent tool that does not require an explicit conversion to CPS. The applications to compilers, partial evaluators, and other transformation systems are numerous. For example, direct compilers like Chez Scheme [28] or Zinc [32] can benefit by including the reductions CS in their basic repertoire of optimizations. Similarly, partial evaluators that use transformations like β_{lift} and β′_{Ω} produce residual programs of better quality [7]. Finally, the set of axioms CS could be the base of an expression simplifier (for compilers and other tools) extending that of Galbiati and Talcott [25].

Our result questions the practice of transforming programs to CPS in order to simplify and improve code generators, partial evaluators, data flow analyzers, and other tools. In fact, we have established that the code generators of typical CPS compilers perform an implicit inverse CPS transformation, and that the true intermediate representation of a typical CPS compiler is the subset of source terms in β_{lift}β_{flat}-normal form [22]. Furthermore, although the literature contains claims that the CPS framework improves the accuracy of data flow analyzers [38], we conjecture that the observed improvements are orthogonal to the “passing of continuations” but are rather side-effects of the axioms CS. We are currently investigating the relationship between the CPS transformation and the precision of data flow analysis.

Acknowledgments

We thank Carolyn Talcott for her outstanding efforts on behalf of this paper, which go far beyond the ordinary duties of an editor. The Scheme code was typeset using Dorai Sitaram’s SLaTEX. The referees’s comments improved the presentation of the results.

A. Proofs

Proof of the auxiliary claims in Proposition 3 (Page 17). Let M ∈ Λ:

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

• C_{k}[[M]] is in \overline{β}\overline{η}-normal form.

Proof: The proof is by induction on the size of the argument to C_{k}. Since the transformation of a term by C_{k} refers to evaluation contexts, we extend the Fischer CPS transformation to accept evaluation contexts and strengthen the inductive hypothesis to take evaluation contexts into account. The extension of the Fischer CPS transformation is the following:

\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 extended function satisfies the following property which we state without proof:

• λ\overline{β} ⊢ (F[[E[M]]] K) = (F[[M]] (F[[E]] K))

• λ\overline{β} ⊢ (F[[E[E′]]] K) = (F[[E′]] (F[[E]] K)).

We can now prove the following statements by induction on the size of G, where G is the argument to C_{k} or K_{k}:

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

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

The proof proceeds by case analysis on the possible inputs to the functions C_{k} or K_{k}:

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

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

(b) V = λx.M: then (k F_{v}[[V]]) ≡ (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. The result follows since C_{k}[[V]] ≡ (k \overline{λ}c.λx.C_{k}[[M]]).

2. G = E[(x V)]: then,

λ\overline{β}\overline{η} ⊢ (F[[G]] k) = (F[[(x V)]] (F[[E]] k)) = ((x F[[E]]k) F_{v}[[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{η} ⊢ F_{v}[[V]] = Φ[[V]], and Φ[[V]] is in \overline{β}\overline{η}-normal form. The result follows 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,

\begin{aligned}λ\overline{β}\overline{η} ⊢ F[[G]]k & = & (F[[((λx.M) V)]] (F[[E]]k)) \\ & = & ((λx.F[[E[M]]]k) F_{v}[[V]]). \end{aligned}

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)) = (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))
= (\overline{λ}u.F[[M]] (u (F[[E]]k)))
= (\overline{λ}u.(F[[E[(u M)]]] k)).

The size of E[(u M)] is smaller than the size of E[([ ] M)] by 1. The inductive hypothesis implies λ\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]]. 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 is in \overline{β}\overline{η}-normal form.

Proof of the second claim in Lemma 4 (Page 17). Let M, L ∈ Λ, E ∈ EvCont, and z ∈ Vars:

C_{k}[[((z M) L)]] ≡ C_{k}[[((λu.uL) (z M))]] where u ∉ F V (L)
K_{k}[[((z E) L)]] ≡ K_{k}[[((λu.uL) (z E))]] where u ∉ F V (L)

Proof: The proof is by induction on the size of M and E and proceeds by cases:

1. M = V, then C_{k}[[((z V) L)]] is identical to:

((z K_{k}[[([ ] L)]]) Φ[[V]]) ≡ ((z \overline{λ}u.C_{k}[[(u L)]]) Φ[[V]]).

The right hand side C_{k}[[((λu.uL) (z V))]] is:

((z K_{k}[[((λu.uL) [ ])]]) Φ[[V]]) ≡ ((z (λu.C_{k}[[(uL)]])) Φ[[V]]).

The two sides of the equation differ by the overline above the abstraction λu. The terms are identical because the abstraction λu cannot be part of an administrative \overline{η} redex in the first term.

2. M = E[(y V)], then C_{k}[[((z E[(y V)]) L)]]

≡ ((y K_{k}[[((z E) L)]]) Φ[[V]])
≡ ((y K_{k}[[((λu.uL) (z E))]]) Φ[[V]]) (induction)

3. M = E[((λx.N) V)], then C_{k}[[((z E[((λx.N) V)]) L)]]

≡ ((λx.C_{k}[[((z E[N]) L)]]) Φ[[V]])
≡ ((λx.C_{k}[[((λu.uL) (z E[N]))]]) Φ[[V]]) (induction)

4. E = [ ], then K_{k}[[((z [ ]) L)]] ≡ (z K_{k}[[([ ] L)]]) ≡ (z \overline{λ}u.C_{k}[[(uL)]]). The right hand side is (z λu.C_{k}[[(uL)]]). The result follows because the overline does not create an administrative redex.

5. E = E_{1}[(x [ ])], then K_{k}[[((z E_{1}[(x [ ])]) L)]]

≡ (x K_{k}[[((z E_{1}) L)]])
≡ (x K_{k}[[((λu.uL) (z E_{1}))]]) (induction)

6. E = E_{1}[((λx.N) [ ])], then K_{k}[[((z E_{1}[((λx.N) [ ])]) L)]]

≡ (λx.C_{k}[[((z E_{1}[N]) L)]])
≡ (λx.C_{k}[[((λu.uL) (z E_{1}[N]))]]) (induction)

7. E = E_{1}[([ ] N)], then K_{k}[[((z E_{1}[([ ] N)]) L)]]

≡ \overline{λ}f.C_{k}[[((z E_{1}[(f N)]) L)]]
≡ \overline{λ}f.C_{k}[[((λu.uL) (z E_{1}[(f N)]))]] (induction)

Proof of the auxiliary claim in Theorem 5 (Page 19).

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

• For all K ∈ cps(EvCont), there exists E ∈ EvCont such that λβη ⊢ 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 size of G. The proof proceeds by case analysis on the possible elements of cps(Λ) and cps(EvCont):

1. G = (k W): 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 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. Let M be the following term ((λx.((λy.E_{2}[(y x)]) V_{1})) V). Then C_{k}[[M]]

≡ ((λ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 also exists 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 to be the evaluation context ((λ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 induction.

Proof of Lemma 6 (Page 19). Let P_{1} ∈ cps(Λ), W_{1} ∈ cps(Values) and 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 P_{1}, W_{1} and K_{1}.

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} ⟶ 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} ⟶ W_{2}. The result follows by the inductive hypothesis.

• λβη ⊢ ((λx.P) W_{1}) ⟶ P [x := W_{1}] because K_{1} = (λx.P). By a simple inductive argument, the substitution preserves the syntactic category.

2. Let W_{1} ∈ cps(Values) and assume λβη ⊢ W_{1} ⟶ W_{2}. The term W_{1} cannot be a variable, thus W_{1} = λk.K_{1} where K_{1} ∈ cps(EvCont). Either:

• λβη ⊢ λk.K_{1} ⟶ λk.K_{2} because K_{1} ⟶ 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}. The term K_{1} cannot be a variable, thus there are two cases:

• K_{1} = λx.P_{1} and there are two subcases:

– λβη ⊢ (λx.P_{1}) ⟶ (λx.P_{2}) because P_{1} ⟶ 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 ⟶ W_{1} and the result follows by the inductive hypothesis.

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

– λβη ⊢ ((λk.K_{3}) K) ⟶ K_{3}[k := K] because W = λk.K_{3}. By an inductive argument, the substitution preserves the syntactic category.

Proof of Theorem 8 (Page 21). Let P ∈ cps(Λ), K ∈ cps(EvCont). Then,

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

2. (C_{k} ∘ C^{−1})[[P]] ≡ P and (K_{k} ∘ K^{−1})[[K]] ≡ K if there exists M ∈ Λ and E ∈ EvCont such that P = C_{k}[[M]] and K = K_{k}[[E]].

Proof: The proof of the first claim is by lexicographic induction on the number of abstractions of the form λk.K and the size of the G where G is an element 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) = (k λk.k).

(c) W = λk.W_{1}K: Then,

(C_{k} ∘ C^{−1})[[G]] ≡ (k λk.λx.(C_{k} ∘ C^{−1})[[((W_{1} K) x)]])
= (k λk.λx.((W_{1} K) x))

(induction)

= (k λk.(W_{1} K)).

(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 an argument similar to case 1, λβη ⊢ (Φ ∘ Φ^{−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]])
= (K_{1}[k := K_{2}] (Φ ∘ Φ^{−1})[[W]])

(induction)

= (K_{1}[k := K_{2}] W)  (similar to case 1)
= (((λk.K_{1}) K_{2}) W)  (β)

4. G = ((λx.P_{1}) W): Then,

(C_{k} ∘ C^{−1})[[G]] ≡ ((λx.(C_{k} ∘ C^{−1})[[P_{1}]]) (Φ ∘ Φ^{−1})[[W]])
= ((λx.P_{1}) (Φ ∘ Φ^{−1})[[W]])  (induction)
= ((λx.P_{1}) W)  (similar to case 1)

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 similar 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}) and hence are not the image of any source term.

Proof of Lemma 9 (Page 22). Let P ∈ cps(Λ) and K ∈ cps(EvCont), then, C^{−1}[[P]] ∈ Λ_{a} and K^{−1}[[K]] ∈ EvCont_{a}.

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

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

(a) W = x, then Φ^{−1}[[W]] ≡ x ∈ Values_{a}.

(b) W = λk.k, then Φ^{−1}[[W]] ≡ λx.x ∈ Values_{a}.

(c) 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)]] ∈ Λ_{a} which shows that the term Φ^{−1}[[W]] ∈ Values_{a}.

(d) W = λk.λx.P, then Φ^{−1}[[W]] ≡ λx.C^{−1}[[P]], and the result follows by induction.

2. K = k, then K^{−1}[[K]] ≡ [ ] ∈ EvCont_{a}.

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

4. 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_{a} by the inductive hypothesis.

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

Proof of Theorem 10 (Page 22). Let M ∈ Λ, then:

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

2. (C^{−1}∘C_{k})[[M]] ≡ M if there exists P ∈ cps(Λ) such that M = C^{−1}[[P]].

Proof: In order to prove the first claim, we strengthen the statement as follows.

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

The proof is by induction on the size of M or E and proceeds by cases:

1. M = V: then there are two subcases:

(a) V = x: then (C^{−1} ∘ C_{k})[[x]] ≡ x.

(b) V = λx.N: then,

λx.N ⟶ ⟶ λx.(C^{−1} ∘ C_{k})[[N]]  (induction)
≡ (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]])].

There are two cases:

(a) V ∉ V ars, then |E| < |E[(x V)]| and the inductive hypothesis applies, i.e., E[(x V)] ⟶ ⟶ (K^{−1} ∘ K_{k})[[E]][(x V)]. The result follows because V ⟶ ⟶ (Φ^{−1} ∘ Φ)[[V]] as in case 1.

(b) V = y ∈ V ars, then there are four cases depending on the structure of E: i. M = (x y), then (C^{−1} ∘ C_{k})[[M]] ≡ M. ii. M = E_{1}[(z (x y))], then the result follows by induction. iii. M = E_{1}[((λz.L) (x y))], then,

M ⟶ ((λz.E_{1}[L]) (x y))  (β_{lift})
⟶ ⟶ ((λz.(C^{−1} ∘ C_{k})[[E_{1}[L]]]) (x y))
≡ (C^{−1} ∘ C_{k})[[M]].

iv. M = E_{1}[((x y) L)], then

M ⟶ E_{1}[((λu.(u L)) (x y))]  (β_{flat})
⟶ ((λu.E_{1}[(u L)]) (x y))  (β_{lift})
⟶ ⟶ ((λu.(C^{−1} ∘ C_{k})[[E_{1}[(u L)]]]) (x y))
≡ (C^{−1} ∘ C_{k})[[M]].

3. M = E_{1}[((λx.N) V)]: then

(C^{−1} ∘ C_{k})[[M]] ≡ ((λx.(C^{−1} ∘ C_{k})[[E_{1}[N]]]) (Φ^{−1} ∘ Φ)[[V]]).

The left hand side M:

⟶ ((λx.E_{1}[N]) V)  (β_{lift})
⟶ ⟶ ((λx.(C^{−1} ∘ C_{k})[[E_{1}[N]]]) V)
⟶ ⟶ ((λx.(C^{−1} ∘ C_{k})[[E_{1}[N]]]) (Φ^{−1} ∘ Φ)[[V]]).

4. E = [ ]: then (K^{−1} ∘ K_{k})[[[ ]]][(x L)] ≡ (x L).

5. E = E_{1}[(z [ ])]: then we want to show that E_{1}[(z (x L))] ⟶ ⟶ (K^{−1} ∘ K_{k})[[E_{1}[(z [ ])]]][(x L)] ≡ (K^{−1} ∘ K_{k})[[E_{1}]][(z (x L))]. The result is immediate since the inductive hypothesis applies to E_{1}.

6. E = E_{1}[((λz.N) [ ])]: then, E_{1}[((λz.N) (x L))]

⟶ ⟶ ((λz.E_{1}[N]) (x L))  (β_{lift})
⟶ ⟶ ((λz.(C^{−1} ∘ C_{k})[[E_{1}[N]]]) (x L))  (induction)
⟶ ⟶ (K^{−1} ∘ K_{k})[[E_{1}[((λz.N) [ ])]]][(x L)].

7. E = E_{1}[([ ] N)]: then, E_{1}[((x L) N)]

⟶ ⟶ E_{1}[((λu.uN) (x L))]  (β_{flat})
⟶ ⟶ ((λu.E_{1}[(u N)]) (x L))  (β_{lift})
⟶ ⟶ ((λu.(C^{−1} ∘ C_{k})[[E_{1}[(u N)]]]) (x L)) (induction)
⟶ ⟶ (K^{−1} ∘ K_{k})[[E_{1}[([ ] N)]]][(x L)].

The proof of the second claim proceeds as above but is restricted to terms of the form C^{−1}[[P]] for some P ∈ cps(Λ). By the grammar in Definition 10, the context E_{1} in cases 2b(iii), 3, and 6 must be empty. Also cases 2b(iv) and 7 are impossible. Since these cases account for all the reductions, it follows that M is identical to (C^{−1} ∘ C_{k})[[M]].

Proof of case 4 in Lemma 12 (Page 24). Let P ∈ cps(Λ), and W ∈ cps(Values), then:

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

Proof:

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

The first three steps are straightforward; the last step requires an appropriate proof. We prove the following claims:

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}[[K[x := W]]].

The proof relies on an auxiliary claim that we state and prove after the main proof. The main 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}:

1. P = (K W_{1}): then C^{−1}[[P]][x := Φ^{−1}[[W]]]

\begin{matrix}≡ & K^{−1}[[K]][Φ^{−1}[[W_{1}]]] [x := Φ^{−1}[[W]]] \\ ⟶ ⟶ & K^{−1}[[K[x := W]]][Φ^{−1}[[W_{1}]][x := Φ^{−1}[[W]]]]. \end{matrix}

It remains to establish that substitution commutes with Φ^{−1} as well. There are five cases:

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

(b) W_{1} = z and z ≠ x: the result is immediate.

(c) W_{1} = λk.k: immediate since x is not free.

(d) W_{1} = λk.W_{2}k: then Φ^{−1}[[W_{1}]][x := Φ^{−1}[[W]]]

\begin{matrix}≡ & λz.C^{−1}[[((W_{2}K) z)]][x := Φ^{−1}[[W]]] \\ ⟶ ⟶ & λz.C^{−1}[[(W_{2}K)[x := W] z]] \\ ≡ & Φ^{−1}[[(λk.W_{2}K)[x := W]]]. \end{matrix}

(e) W_{1} = λk.λz.P_{1} (z ≠ x): then Φ^{−1}[[W_{1}]][x := Φ^{−1}[[W]]]

≡  (λz.C^{−1}[[P]])[x := Φ^{−1}[[W]]]
≡  (λz.C^{−1}[[P]][x := Φ^{−1}[[W]]])
⟶ ⟶ λz.C^{−1}[[P [x := W]]]  (induction)
≡  Φ^{−1}[[(λk.λz.P)[x := W]]]

2. K = k: then the claim is vacuously true because k ≠ x.

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

\begin{matrix}≡ & K^{−1}[[K_{1}[k := K_{2}]]][x := Φ^{−1}[[W]]] \\ ⟶ ⟶ & K^{−1}[[K_{1}[k := K_{2}][x := W]]] \\ ≡ & K^{−1}[[((λk.K_{1}[x := W]) K_{2}[x := W])]]. \end{matrix}

4. K = λz.P_{1} (z ≠ x): then K^{−1}[[λz.P_{1}]][x := Φ^{−1}[[W]]]

\begin{matrix}≡ & ((λz.C^{−1}[[P]][x := Φ^{−1}[[W]]]) [ ]) \\ ⟶ ⟶ & ((λz.C^{−1}[[P [x := W]]]) [ ]) \\ ≡ & K^{−1}[[λz.P [x := W]]]. \end{matrix}

5. K = λx.P_{1}: immediate since x is not free.

6. K = (z K_{1}) and z ≠ x: this is a special case of the next clause.

7. K = (x K_{1}): then K^{−1}[[(x K_{1})]][x := Φ^{−1}[[W]]]

\begin{matrix}≡ & K^{−1}[[K_{1}]][(x [ ])][x := Φ^{−1}[[W]]] \\ ≡ & K^{−1}[[K_{1}]][x := Φ^{−1}[[W]]][(Φ^{−1}[[W]] [ ])] \\ ⟶ ⟶ & K^{−1}[[K_{1}[x := W]]] [(Φ^{−1}[[W]] [ ])]. \end{matrix}

For readability, 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:

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

(b) W = λk.k: then,

\begin{aligned}K^{−1}[[K′]][((λx.x) [ ])] & ⟶ & K^{−1}[[K′]] & (β_{id}) \\ & ≡ & K^{−1}[[((λk.k) K′)]] \end{aligned}

(c) W = λk.W_{3}K: then, K^{−1}[[K′]][((λy.C^{−1}[[((W_{3}K) y)]]) [ ])]

≡  K^{−1}[[K′]][K^{−1}[[(λy.((W_{3}K) y))]]]
⟶ ⟶ K^{−1}[[K′]][K^{−1}[[(W_{3}K)]]]  (case 1 (Lem. 12))
⟶ ⟶ K^{−1}[[(W_{3}K)[k := K′]]]  (aux. claim)
≡  K^{−1}[[((λk.W_{3}K) K′)]].

(d) W = λk.λz.P_{2}: then K^{−1}[[K′]][((λz.C^{−1}[[P_{2}]]) [ ])]

⟶ ((λz.K^{−1}[[K′]][C^{−1}[[P_{2}]]]) [ ]) (β_{lift})
⟶ ⟶ ((λz.C^{−1}[[P_{2}[k := K′]]]) [ ]) (aux. claim)
≡  K^{−1}[[λz.P_{2}[k := K′]]]
≡  K^{−1}[[((λk.λz.P_{2}) K′)]].

Auxiliary Claim: Let P ∈ cps(Λ), and let K, K_{1}, K_{2} ∈ cps(EvCont), 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}]]] The proof of the auxiliary claim 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):

1. P = (K_{3} W), then K^{−1}[[K]][C^{−1}[[P]]]

\begin{matrix}≡ & K^{−1}[[K]][K^{−1}[[K_{3}]][Φ^{−1}[[W]]]] \\ ⟶ ⟶ & K^{−1}[[K_{3}[k := K]]][Φ^{−1}[[W]]] \\ ≡ & K^{−1}[[(K_{3} W)[k := K]]]. \end{matrix}

The last equivalence holds because k is never free in W.

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

3. K_{1} = (x K_{3}), then K^{−1}[[K_{2}]][K^{−1}[[K_{3}]][(x [ ])]]

\begin{matrix}⟶ ⟶ & K^{−1}[[K_{3}[k := K_{2}]]][(x [ ])] \\ ≡ & K^{−1}[[(x K_{3}[k := K_{2}])]]. \end{matrix}

4. K_{1} = ((λk.K_{3}) K_{4}), then K^{−1}[[K_{2}]][K^{−1}[[K_{3}[k := K_{4}]]]]

\begin{matrix}⟶ ⟶ & K^{−1}[[K_{3}[k := K_{4}][k := K_{2}]]] \\ ≡ & K^{−1}[[K_{3}[k := K_{4}[k := K_{2}]]]] \\ ≡ & K^{−1}[[((λk.K_{3}) K_{4})[k := K_{2}]]]. \end{matrix}

5. K_{1} = λx.P: then, K^{−1}[[K_{2}]][((λx.C^{−1}[[P]]) [ ])]

\begin{matrix}⟶ & ((λx.K^{−1}[[K_{2}]][C^{−1}[[P]]]) [ ])(β_{lift}) \\ ⟶ ⟶ & ((λx.C^{−1}[[P [k := K_{2}]]]) [ ]) \\ ≡ & K^{−1}[[(λx.P)[k := K_{2}]]]. \end{matrix}

Proof of case 1 in Lemma 14 (Page 25). Let M ∈ Λ, and V ∈ Values:

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

Proof: The main proof uses the following result that we state without proof.

\begin{matrix}λβ ⊢ C_{k}[[M]][k := K_{k}[[E]]] & ⟶ ⟶ & C_{k}[[E[M]]] \\ λβ ⊢ K_{k}[[E_{1}]][k := K_{k}[[E]]] & ⟶ ⟶ & K_{k}[[E[E_{1}]]] \end{matrix}

For the main proof, we have 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)]. The left hand side 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:

1. V = z, then both sides are identical.

2. V = λz.L. Then, (((λk.λz.C_{k}[[L]]) K_{k}[[E′]]) Φ[[U′]])

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

Proof of Lemma 17 (Page 31). Let P ∈ cps(Λ + callcc + A) and K be a continuation, and W be a value in the same language. Also, let k_{1}, …, k_{n} be the free continuation variables in these terms, and k ∉ {k_{1}, …, k_{n}}. Then,

1. λβη ⊢ (C_{k} ∘ C^{−1})[[P]][k_{1} := (λd.k_{1}), …, k_{n} := (λd.k_{n})] = P.

2. λβη ⊢ (K_{k} ∘ K^{−1})[[K]][k_{1} := (λd.k_{1}), …, k_{n} := (λd.k_{n})] = K.

3. λβη ⊢ (Φ ∘ Φ^{−1})[[W]][k_{1} := (λd.k_{1}), …, k_{n} := (λd.k_{n})] = W.

Proof: The proof is by lexicographic induction on the number of abstractions of the form λk.K and the size of the terms. We proceed by cases:

1. P = x, then

(C_{k} ∘ C^{−1})[[P]] ≡  C_{k}[[(A x)]]
≡  (((λk.λx.x) k) x)
⟶ ⟶ x  (β twice)

2. P = λk.K, then

(C_{k} ∘ C^{−1})[[P]] ≡  C_{k}[[(A Φ^{−1}[[λk.K]])]]
=  (((λk.λx.x) k) (Φ ∘ Φ^{−1})[[λk.K]])
⟶ ⟶ (Φ ∘ Φ^{−1})[[λk.K]]

The result follows by inlining the last case in the proof.

3. P = (K W), then (C_{k} ∘ C^{−1})[[(K W)]] ≡ C_{k}[[K^{−1}[[K]][Φ^{−1}[[W]]]]] and by cases on K:

(a) K = k′, then C_{k}[[(k′ Φ^{−1}[[W]])]] ≡ ((k′ k) (Φ∘Φ^{−1})[[W]]). By substituting every free continuation variable (in particular substituting k′ by (λd.k′)) and using the inductive hypothesis, we get (k′ W).

(b) K = λx.P′, then (C_{k} ∘ C^{−1})[[P]]

\begin{matrix}= & C_{k}[[((λx.C^{−1}[[P′]]) Φ^{−1}[[W]])]] \\ = & ((λx.(C_{k} ∘ C^{−1})[[P′]]) (Φ ∘ Φ^{−1})[[W]]) \end{matrix}

The result follows by the inductive hypothesis.

(c) K = W′K′, then (C_{k} ∘ C^{−1})[[P]]

\begin{matrix}≡ & (C_{k} ∘ C^{−1})[[((W′K′) W)]] \\ ≡ & (((Φ ∘ Φ^{−1})[[W′]] (K_{k} ∘ K^{−1})[[K′]]) (Φ ∘ Φ^{−1})[[W]]) \end{matrix}

The result follows by the inductive hypothesis.

4. K = k′, λx.P or W K. The cases are similar to the preceding three cases.

5. W = x, then (Φ ∘ Φ^{−1})[[x]] ≡ x.

6. W = λk.K, then (Φ ∘ Φ^{−1})[[λk.K]]

= Φ[[λz.callcc λk.K^{−1}[[K]][z]]]
= λk′.λz.(((λk′′.λu.(u k′′) (λd.k′′)) k′) Φ[[λk.K^{−1}[[K]][z]]])
= λk′.λz.((λu.(u k′) (λd.k′)) Φ[[λk.K^{−1}[[K]][z]]])
= λk′.λz.((λu.(u k′) (λd.k′)) (λk′′.λk.C_{k′′}[[C^{−1}[[(K z)]]]]))
= λk′.λz.C_{k′′}[[C^{−1}[[(K z)]]]][k′′ := k′][k := λd.k′]
= λk′.λz.C_{k′}[[C^{−1}[[(K z)]]]][k := λd.k′]
= λk.λz.C_{k}[[C^{−1}[[(K z)]]]][k := λd.k]

By substituting the remaining free continuation variables and using the inductive hypothesis (the term (K z) has one less abstraction than λk.K), we get λk.λz.Kz which is equal to λk.K.

Proof of Lemma 18 (Page 31). Let M ∈ Λ + callcc + A, and E be an evaluation context in the same language, and k a variable that is not free in either. Then, • λβ_{v}XC ⊢ (C^{−1} ∘ C_{k})[[M]] = (k M)

• λβ_{v}XC ⊢ (K^{−1} ∘ K_{k})[[E]] = (k E)

Proof: By induction on the size of the terms. We proceed by cases:

1. M = V, then (C^{−1}∘C_{k})[[V]] ≡ C^{−1}[[(k Φ[[V]])]] ≡ (k (Φ^{−1}∘Φ)[[V]]). By cases, we show that (Φ^{−1} ∘ Φ)[[V]] = V.

(a) V = x, then (Φ^{−1} ∘ Φ)[[x]] ≡ x.

(b) V = λx.N, then

(Φ^{−1} ∘ Φ)[[V]] ≡ Φ^{−1}[[λk.λx.C_{k}[[N]]]]
≡ λz.callcc λk.((λx.(C^{−1} ∘ C_{k})[[N]]) z)
= λz.callcc λk.((λx.(k N)) z)

(induction)

= λz.callcc λk.k ((λx.N) z)  (β_{lift})
= λz.((λx.N) z)

(C_{current} and C_{elim})

= λx.N  (β_{v})

(c) V = callcc, then (Φ^{−1} ∘ Φ)[[V]]

≡ Φ^{−1}[[λk.λu.(u k) λd.k]]
≡ λz.callcc λk.((λu.(k (u λf.callcc λd.(k f)))) z)
= λz.callcc λk.((λu.(k (u λf.(k f)))) z) (C_{elim})
= λz.callcc λk.((λu.(k (u k))) z)  (η_{v})
= λz.callcc λk.(k (z k))  (β_{v})
= λz.callcc λk.(z k)  (C_{current})
= callcc  (η_{v} twice)

(d) V = A, then

(Φ^{−1} ∘ Φ)[[V]] ≡ Φ^{−1}[[λk.λx.x]]
= λz.callcc λk.((λx.A x) z)
= λz.((λx.A x) z)  (C_{elim})
= (λz.A z)  (β_{v})
= A  (η_{v})

2. M = E[(V_{1} V_{2})], then (C^{−1} ∘ C_{k})[[M]]

= C^{−1}[[((Φ[[V_{1}]] K_{k}[[E]]) Φ[[V_{2}]])]]
= K^{−1}[[(Φ[[V_{1}]] K_{k}[[E]])]][(Φ^{−1} ∘ Φ)[[V_{2}]]]
= (K^{−1} ∘ K_{k})[[E]][((Φ^{−1} ∘ Φ)[[V_{1}]] (Φ^{−1} ∘ Φ)[[V_{2}]])]

The result follows by the inductive hypothesis and a repetition of the argument in case 1.

3. E = [ ], then (K^{−1} ∘ K_{k})[[E]] ≡ K^{−1}[[k]] ≡ (k [ ]).

4. E = E_{1}[(V [ ])], then (K^{−1} ∘ K_{k})[[E]]

\begin{matrix}= & (K^{−1} ∘ K_{k})[[E_{1}[(V [ ])]]] \\ = & (K^{−1} ∘ K_{k})[[E_{1}]][((Φ^{−1} ∘ Φ)[[V]] [ ])] \end{matrix}

The result follows by the inductive hypothesis and a repetition of the argument in case 1.

5. E = E_{1}[([ ] M)], then

(K^{−1} ∘ K_{k})[[E]] ≡ (K^{−1} ∘ K_{k})[[E_{1}[([ ] M)]]]
≡ ((λf.(C^{−1} ∘ C_{k})[[E_{1}[(f M)]]]) [ ])
= ((λf.(k E_{1}[(f M)])) [ ])  (induction)
= (k E_{1}[([ ] M)])  (β′_{Ω})

Proof of case 1 in Lemma 19 (Page 32). Let k_{1} … k_{n} be the free continuation variables in P and W. Then,

λβ_{v}XC ⊢ callcc λk_{1}…. callcc λk_{n}.C^{−1}[[((λx.P) W)]] = callcc λk_{1}…. callcc λk_{n}.C^{−1}[[P [x := W]]]

Proof: Applying C^{−1} to ((λx.P) W) yields:

K^{−1}[[(λx.P)]][Φ^{−1}[[W]]] ≡ ((λx.C^{−1}[[P]]) Φ^{−1}[[W]]).

By β_{v}, we get C^{−1}[[P]][x := Φ^{−1}[[W]]]. It remains to show that C^{−1} commutes with the substitution. We prove the following statements by induction on the structure of the terms:

• C^{−1}[[P]][x := Φ^{−1}[[W]]] ≡ C^{−1}[[P [x := W]]].

• Φ^{−1}[[W′]][x := Φ^{−1}[[W]]] ≡ Φ^{−1}[[W′[x := W]]].

• K^{−1}[[K]][x := Φ^{−1}[[W]]] ≡ K^{−1}[[K[x := W]]].

1. P = y, then C^{−1}[[y]][x := Φ^{−1}[[W]]] ≡ (A y) ≡ C^{−1}[[y[x := W]]].

2. P = x, then

C^{−1}[[x]][x := Φ^{−1}[[W]]] ≡ (A Φ^{−1}[[W]]) ≡ C^{−1}[[x[x := W]]]

3. P = λk.K, then C^{−1}[[λk.K]][x := Φ^{−1}[[W]]]

≡ (A Φ^{−1}[[λk.K]][x := Φ^{−1}[[W]]])
≡ (A Φ^{−1}[[λk.K[x := W]]])  (similar to case 7)
≡ C^{−1}[[λk.K[x := W]]]

4. P = (K′ W′), then C^{−1}[[P]][x := Φ^{−1}[[W]]]

≡ K^{−1}[[K′]][x := Φ^{−1}[[W]]][Φ^{−1}[[W′]][x := Φ^{−1}[[W]]]]
≡ K^{−1}[[K′[x := W]]][Φ^{−1}[[W′[x := W]]]]  (induction)
≡ C^{−1}[[(K′ W′)[x := W]]]

5. W′ = x, then

Φ^{−1}[[W′]][x := Φ^{−1}[[W]]] ≡ Φ^{−1}[[W]] ≡ Φ^{−1}[[x[x := W]]]

6. W′ = y, then Φ^{−1}[[y]][x := Φ^{−1}[[W]]] ≡ y ≡ Φ^{−1}[[y[x := W]]].

7. W′ = λk.K, then Φ^{−1}[[W′]][x := Φ^{−1}[[W]]]

≡ λz.callcc λk.K^{−1}[[K]][x := Φ^{−1}[[W]]][z]
≡ λz.callcc λk.K^{−1}[[K[x := W]]][z]  (induction)
≡ Φ^{−1}[[λk.K[x := W]]]

8. K = k, then K^{−1}[[k]][x := Φ^{−1}[[W]]] ≡ (k [ ]) ≡ K^{−1}[[k[x := W]]].

9. K = λy.P, then

K^{−1}[[λy.P]][x := Φ^{−1}[[W]]] ≡ ((λy.C^{−1}[[P]][x := Φ^{−1}[[W]]]) [ ])

The result follows by induction.

10. K = W′K′, then the result follows also by a straightforward application of the inductive hypothesis.

Proof of case 4 in Lemma 19 (Page 32). Let k_{1} … k_{n} be the free continuation variables in ((λk.K_{1}) K_{2}). Then,

λβ_{v}XC ⊢ callcc λk_{1}…. callcc λk_{n}.K^{−1}[[((λk.K_{1}) K_{2})]] = callcc λk_{1}…. callcc λk_{n}.K^{−1}[[K_{1}[k := K_{2}]]]

Proof: Let D be a context callcc λk_{1}…. callcc λk_{n}.C[ ] where C is an arbitrary context, then it suffices to prove:

λβ_{v}XC ⊢ D[K^{−1}[[((λk.K_{1}) K_{2})]]] = D[K^{−1}[[K_{1}[k := K_{2}]]]]

The left hand side D[K^{−1}[[((λk.K_{1}) K_{2})]]]

\begin{matrix}≡ & D[K^{−1}[[K_{2}]][(Φ^{−1}[[λk.K_{1}]] [ ])]] \\ = & D[K^{−1}[[K_{2}]][((λz.callcc λk.K^{−1}[[K_{1}]][z]) [ ])]] \end{matrix}

It remains to prove the following statements by induction on the structure of P, W, and K_{1}.

λβ_{v}XC ⊢ D[C^{−1}[[P [k := K_{2}]]]] = D[K^{−1}[[K_{2}]][callcc λk.C^{−1}[[P]]]] λβ_{v}XC ⊢ D[Φ^{−1}[[W [k := K_{2}]]]] = D[Φ^{−1}[[W]][k := λf.K^{−1}[[K_{2}]][f]]] λβ_{v}XC ⊢ D[K^{−1}[[K_{1}[k := K_{2}]]]] =

D[K^{−1}[[K_{2}]][((λz.callcc λk.K^{−1}[[K_{1}]][z]) [ ])]] The main proof relies on the following auxiliary claim that we state without proof. Let K be a continuation in cps(Λ + callcc + A) with free continuation variables k_{1}, …, k_{n}, then either:

\begin{aligned}λβ_{v}XC ⊢ K^{−1}[[K]] & = & (A E) \\ or λβ_{v}XC ⊢ K^{−1}[[K]] & = & (k_{i} E) 1 ≤ i ≤ n \end{aligned}

The auxiliary claim implies that for any evaluation context E:

D[E[K^{−1}[[K]][M]]] = D[K^{−1}[[K]][M]].

The latter result implies that D[K^{−1}[[K]][callcc λk.K^{−1}[[K′]][M]]]

= D[callcc λk′.K^{−1}[[K]][((λk.K^{−1}[[K′]][M]) λf.(k′ K^{−1}[[K]][f]))]]
= D[callcc λk′.K^{−1}[[K]][((λk.K^{−1}[[K′]][M]) λf.K^{−1}[[K]][f])]]
= D[K^{−1}[[K]][((λk.K^{−1}[[K′]][M]) λf.K^{−1}[[K]][f])]]
= D[K^{−1}[[K]][K^{−1}[[K′]][((λk.M) λf.K^{−1}[[K]][f])]]]
= D[K^{−1}[[K′]][((λk.M) λf.K^{−1}[[K]][f])]]
= D[((λk.K^{−1}[[K′]][M]) λf.K^{−1}[[K]][f])]

The main proof proceeds by case analysis:

1. P = x, then:

D[K^{−1}[[K_{2}]][callcc λk.A x]] = D[K^{−1}[[K_{2}]][A x]]
= D[(A x)]
= D[C^{−1}[[x]]]

2. P = λk′.K′. The left hand side:

D[C^{−1}[[λk′.K′[k := K_{2}]]]]

= D[(A Φ^{−1}[[λk′.K′[k := K_{2}]]])]
= D[(A λz.callcc λk′.K^{−1}[[K_{2}]][callcc λk.K^{−1}[[K′]][z]])]
= D[(A λz.callcc λk′.((λk.K^{−1}[[K′]][z]) λf.K^{−1}[[K_{2}]][f]))]

(auxiliary claim)

= D[(A λz.callcc λk′.K^{−1}[[K′]][z])[k := λf.K^{−1}[[K_{2}]][f]]]
= D[((λk.(A λz.callcc λk′.K^{−1}[[K′]][z])) (λf.K^{−1}[[K_{2}]][f]))]
= D[K^{−1}[[K_{2}]][callcc λk.(A λz.callcc λk′.K^{−1}[[K′]][z])]]

(auxiliary claim)

= D[K^{−1}[[K_{2}]][callcc λk.C^{−1}[[λk′.K′]]]]

3. P = (K W). The left hand side D[C^{−1}[[(K W)[k := K_{2}]]]]

= D[K^{−1}[[K[k := K_{2}]]][Φ^{−1}[[W [k := K_{2}]]]]]
= \begin{matrix}D[K^{−1}[[K_{2}]][callcc λk. \\ K^{−1}[[K]][Φ^{−1}[[W]][k := λf.K^{−1}[[K_{2}]][f]]]]] \end{matrix}
= \begin{matrix}D[((λk.K^{−1}[[K]][Φ^{−1}[[W]][k := λf.K^{−1}[[K_{2}]][f]]]) \\ (λf.K^{−1}[[K_{2}]][f]))] \end{matrix}
= D[K^{−1}[[K]][Φ^{−1}[[W]]][k := λf.K^{−1}[[K_{2}]][f]]]
= D[K^{−1}[[K_{2}]][callcc λk.K^{−1}[[K]][Φ^{−1}[[W]]]]]

4. W = x, then the result is immediate.

5. W = λk′.K, then Φ^{−1}[[λk′.K[k := K_{2}]]]

= D[λz.callcc λk′.K^{−1}[[K[k := K_{2}]]][z]]
= D[λz.callcc λk′.K^{−1}[[K_{2}]][callcc λk.K^{−1}[[K]][z]]]
= D[λz.callcc λk′.K^{−1}[[K]][z][k := λf.K^{−1}[[K_{2}]][f]]]

6. K_{1} = k′, then:

D[K^{−1}[[K_{2}]][callcc λk.(k′ [ ])]] = D[K^{−1}[[K_{2}]][(k′ [ ])]]
= D[(k′ [ ])]
= D[K^{−1}[[k′]]]

7. K_{1} = k, then D[K^{−1}[[K_{2}]][callcc λk.(k [ ])]] = D[K^{−1}[[K_{2}]]].

8. K_{1} = λx.P, then D[K^{−1}[[λx.P [k := K_{2}]]]]

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

9. K_{1} = W′K′, then the left hand side:

D[K^{−1}[[W′K′[k := K_{2}]]]]
= D[K^{−1}[[K′[k := K_{2}]]][(Φ^{−1}[[W′[k := K_{2}]]] [ ])]]
= \begin{matrix}D[K^{−1}[[K_{2}]][callcc λk. \\ K^{−1}[[K′]][(Φ^{−1}[[W′]][k := λf.K^{−1}[[K_{2}]][f]] \\ [ ])]]] \end{matrix}

= D[K^{−1}[[K′]][(Φ^{−1}[[W′]] [ ])][k := λf.K^{−1}[[K_{2}]][f]]]
= D[K^{−1}[[K_{2}]][callcc λk.K^{−1}[[K′]][(Φ^{−1}[[W′]] [ ])]]]

References

1. Allison, L. A Practical Introduction to Denotational Semantics. Volume 23 of Cambridge Computer Science Texts, Cambridge University Press (1986).

2. Appel, A. Compiling with Continuations. Cambridge University Press (1992).

3. Appel, A. and Jim, T. Continuation-passing, closure-passing style. In Conference Record of the 16th ACM Symposium on Principles of Programming Languages (1989) 293–302.

4. Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, revised edition (1984).

5. Bartley, D. H. and Jensen, J. C. The implementation of PC Scheme. In Proceedings of the ACM Conference on Lisp and Functional Programming (1986) 86–93.

6. Boehm, H.-J. and Demers, A. Implementing Russel. In Proceedings of the ACM Sigplan Symposium on Compiler Construction, Sigplan Notices, 21, 7 (1986) 186–195.

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

8. Clinger, W., Friedman, D., and Wand, M. A scheme for a higher-level semantic algebra. In Reynolds, J. and Nivat, M., editors, Algebraic Methods in Semantics, Cambridge University Press (1985) 237–250.

9. Crank, E. and Felleisen, M. Parameter-passing and the lambda calculus. In Conference Record of the 18th ACM Symposium on Principles of Programming Languages (1991) 233–244.

10. Curry, H. B. and Feys, R. Combinatory Logic, Volume I. North-Holland, Amsterdam (1958).

11. Danvy, O. Back to direct style. Science of Computer Programming (1993). To appear. Preliminary version in: Proceedings of the 4th European Symposium on Programming, 1992. Lecture Notes in Computer Science, 582, Springer Verlag.

12. Danvy, O. and Filinski, A. Abstracting control. In Proceedings of the ACM Conference on Lisp and Functional Programming (1990) 151–160.

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

14. Danvy, O. and Lawall, J. Back to direct style II: First-class continuations. In Proceedings of the ACM Conference on Lisp and Functional Programming (1992) 299–310.

15. Felleisen, M. The theory and practice of first-class prompts. In Conference Record of the 15th ACM Symposium on Principles of Programming Languages (1988) 180–190.

16. Felleisen, M. and Friedman, D. P. Control operators, the SECDmachine, and the λ-calculus. In Wirsing, M., editor, Formal Description of Programming Concepts-III, North-Holland (1986) 193–217.

17. Felleisen, M. and Friedman, D. P. A syntactic theory of sequential state. Theoretical Computer Science, 69, 3 (1989) 243–287. Preliminary version in: Conference Record of the 14th ACM Symposium on Principles of Programming Languages, 1987.

18. Felleisen, M. and Hieb, R. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 102 (1992) 235–271. Technical Report 89-100, Rice University.

19. Felleisen, M., Friedman, D. P., Kohlbecker, E., and Duba, B. A syntactic theory of sequential control. Theoretical Computer Science, 52, 3 (1987) 205–237. Preliminary version: Reasoning with Continuations, in Proceedings of the 1st IEEE Symposium on Logic in Computer Science, 1986.

20. Felleisen, M., Wand, M., Friedman, D.P., and Duba, B.F. Abstract continuations: A mathematical semantics for handling full functional jumps. In Proceedings of the ACM Conference on Lisp and Functional Programming (1988) 52–62.

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

22. Flanagan, C., Sabry, A., Duba, B. F., and Felleisen, M. The essence of compiling with continuations. In Proceedings of the ACM Sigplan Conference on Programming Language Design and Implementation (1993). To appear.

23. Friedman, D. P., Haynes, C.T., and Kohlbecker, E. Programming with continuations. In Pepper, P., editor, Program Transformations and Programming Environments, Springer-Verlag (1985) 263–274.

24. Friedman, D. P., Wand, M., and Haynes, C.T. Essentials of Programming Languages. The MIT Press (1992).

25. Galbiati, L. and Talcott, C. L. A simplifier for untyped lambda expressions. In Proceedings Conditional Term Rewriting Systems, Lecture Notes in Computer Science, 516 (1990) 342–353.

26. Griffin, T.G. A formulae-as-types notion of control. In Conference Record of the 17th ACM Symposium on Principles of Programming Languages (1990) 47–58.

27. Haynes, C.T., Friedman, D. P., and Wand, M. Obtaining coroutines from continuations. Journal of Computer Languages (Pergamon Press), 11, 3/4 (1986) 143–153.

28. Hieb, R., Dybvig, K., and Bruggeman, C. Representing control in the presence of first-class continuations. In Proceedings of the ACM Sigplan Conference on Programming Language Design and Implementation (1990) 66–77.

29. Kelsey, R. and Hudak, P. Realistic compilation by program transformation. In Conference Record of the 16th ACM Symposium on Principles of Programming Languages (1989) 281–292.

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

31. Landin, P.J. The mechanical evaluation of expressions. Computer Journal, 6, 4 (1964) 308–320.

32. Leroy, X. The Zinc Experiment: An Economical Implementation of the ML Language. Technical Report 117, INRIA (1990).

33. Mason, I. and Talcott, C. L. Equivalence in functional languages with effects. Journal of Functional Programming, 1, 3 (July 1991) 287–327.

34. Mazurkiewicz, A.W. Proving algorithms by tail functions. Information and Control, 18 (1971) 220–226.

35. Meyer, A. R. and Wand, M. Continuation semantics in typed lambdacalculi. In Proceedings Workshop Logics of Programs, Lecture Notes in Computer Science, 193 (1985) 219–224.

36. Moggi, E. Computational lambda-calculus and monads. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science (1989) 14–23. Also appeared as: LFCS Report ECS-LFCS-88-86, University of Edinburgh, 1988.

37. Morris, L. The next 700 formal language descriptions. Lisp and Functional Programming (1993). To appear.

38. Nielson, F. A denotational framework for data flow analysis. Acta Informatica, 18 (1982) 265–287.

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

40. Rees, J. and Clinger, W. Revised^{3} report on the algorithmic language Scheme. Sigplan Notices, 21, 12 (1986) 37–79.

41. Reynolds, J. C. Definitional interpreters for higher-order programming languages. In Proceedings of the ACM Annual Conference (1972) 717– 740.

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

43. Shivers, O. Control-Flow Analysis of Higher-Order Languages or Taming Lambda. PhD thesis, Carnegie-Mellon University (1991).

44. Sitaram, D. and Felleisen, M. Reasoning with continuations II: Full abstraction for models of control. In Proceedings of the ACM Conference on Lisp and Functional Programming (1990) 161–175.

45. Steel, T.B., editor. Formal Language Description Languages for Computer Programming. North-Holland (1966).

46. Steele, G. L. Rabbit: A Compiler for Scheme. MIT AI Memo 474, Massachusetts Institute of Technology (1978).

47. Strachey, C. and Wadsworth, C.P. Continuations: A Mathematical Semantics for Handling Full Jumps. Technical Monograph PRG-11, Oxford University Computing Laboratory, Programming Research Group (1974).

48. Talcott, C. L. A theory for program and data specification. Theoretical Computer Science, 104 (1992) 129–159. Preliminary version in Proceedings of the International Symposium on Design and Implementation of Symbolic Computation Systems, (Lecture Notes in Computer Science, 429, 1990).

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