BRICS RS-01-49 Danvy & Nielsen: A First-Order One-Pass CPS Transformation BRICS

Basic Research in Computer Science

A First-Order One-Pass CPS Transformation

Olivier Danvy Lasse R. Nielsen BRICS Report Series RS-01-49 ISSN 0909-0878 December 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Olivier Danvy & Lasse R. Nielsen.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/01/49/

A First-Order One-Pass CPS Transformation ^{∗}

Olivier Danvy and Lasse R. Nielsen

BRICS ^{†}

Department of Computer Science University of Aarhus ^{‡}

December 2001

Abstract

We present a new transformation of call-by-value lambda-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Because it operates in one pass, it directly yields compact CPS programs that are comparable to what one would write by hand. Because it is compositional, it allows proofs by structural induction. Because it is first-order, reasoning about it does not require the use of a logical relation.

This new CPS transformation connects two separate lines of research. It has already been used to state a new and simpler correctness proof of a direct-style transformation, and to develop a new and simpler CPS transformation of control-flow information.

∗Extended version of an article to appear in the proceedings of FOSSACS’02, Grenoble, France, April 2002.

† Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

‡ Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark.

E-mail: {danvy,lrn}@brics.dk

Contents

1 Introduction 3

2 From higher-order to first-order 4 2.1 A higher-order specification . . . . . . . . . . . . . . . . . . . . . 4 2.2 Circumventing the higher-order functions . . . . . . . . . . . . . 5

3 From non-compositional to compositional 7 3.1 A non-compositional specification . . . . . . . . . . . . . . . . . . 7 3.2 Eliminating the non-compositionality . . . . . . . . . . . . . . . . 8

4 From two passes to one pass 8 4.1 A two-pass specification . . . . . . . . . . . . . . . . . . . . . . . 8 4.2 A colon translation for proving simulation . . . . . . . . . . . . . 8 4.3 Merging CPS transformation and colon translation . . . . . . . . 9

5 Correctness of the first-order one-pass CPS transformation 10 5.1 Reduction rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 5.2 Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

6 Reasoning about CPS-transformed programs 13 6.1 A higher-order one-pass CPS transformation . . . . . . . . . . . 13 6.2 A first-order two-pass CPS transformation . . . . . . . . . . . . . 13 6.3 A first-order one-pass CPS transformation . . . . . . . . . . . . . 14 6.4 Non-compositional CPS transformations . . . . . . . . . . . . . . 14

7 Conclusion and issues 14 7.1 The big picture . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 7.2 Scaling up . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 7.3 A shortcoming . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 7.4 Summary and conclusion . . . . . . . . . . . . . . . . . . . . . . 17

A An example of continuation-passing program 17

List of Figures

1 Higher-order one-pass CPS transformation . . . . . . . . . . . . . 4 2 First-order one-pass CPS transformation . . . . . . . . . . . . . . 6

1 Introduction

The transformation into continuation-passing style (CPS) is an encoding of arbitrary λ-terms into an evaluation-order-independent subset of the λ-calculus [30, 36]. As already reviewed by Reynolds [35], continuations and the CPS transformation share a long history. The CPS transformation was first formalized by Plotkin [30], and first used in practice by Steele, in the first compiler for the Scheme programming language [39]. Unfortunately, its direct implementation as a rewriting system yields extraneous redexes known as administrative redexes. These redexes interfere both with proving the correctness of a CPS transformation [30] and with using it in a compiler [22, 39]. At the turn of the 1990’s, two flavors of “one-pass” CPS transformations that contract administrative redexes at transformation time were developed. One flavor is compositional and higher-order, using a functional accumulator [1, 10, 41]. The other is noncompositional and first-order, using evaluation contexts [37]. They have both been proven correct and are used in compilers as well as to reason about CPS programs.

Because the existing one-pass CPS transformations are either higher-order or non-compositional, their correctness proofs are complicated, and so is reasoning about CPS-transformed programs. In this article, we present a one-pass CPS transformation that is both compositional and first-order and thus is simple to prove correct and to reason about. It is also more efficient in practice.

Overview: The rest of this article is structured as follows. We present three derivations of our first-order, one-pass, and compositional CPS transformation. We derive it from the higher-order one-pass CPS transformation (Section 2), from Sabry and Wadler’s non-compositional CPS transformation (Section 3), and from Steele’s two-pass CPS transformation (Section 4). We also prove its correctness with a simulation theorem à la Plotkin (Section 5).

higher-order one-pass compositional

CPS transformation

Section 2 [figure]

[figure]

first-order one-pass non-compositional CPS transformation

Section 3

[figure] first-order two-pass compositional CPS transformation

Section 4 [figure]

[figure]

first-order one-pass compositional CPS transformation

Section 5

[figure] correctness We then compare the process of reasoning about CPS-transformed programs, depending on which kind of CPS transformation is used (Section 6). Finally, we conclude (Section 7).

Prerequisites: The syntax of the λ-calculus is as follows. We follow the tradition of distinguishing between trivial and serious terms. (This distinction originates in Reynolds’s work [36] and has been used by Moggi to distinguish between values and computations [25].)

e ::= t | s  e ∈ Expr (terms)
t ::= x | λx.e t, K ∈ Val (trivial terms, i.e., values)
s ::= e_{0} e_{1}  s ∈ Comp (serious terms, i.e., computations)
x, k ∈ Ide  (identifiers)

We distinguish terms up to α-equivalence, i.e., renaming of bound variables.

2 From higher-order to first-order

2.1 A higher-order specification

Figure 1 displays a higher-order, one-pass, compositional CPS transformation.

E : Expr → Ide → Comp
E[[t]] = \overline{λ}k.k \underline{@} T [[t]]
E[[s]] = \overline{λ}k.S[[s]] \overline{@} k
S : Comp → Ide → Comp
S[[e_{0} e_{1}]] = \overline{λ}k.E′[[e_{0}]] \overline{@} (\overline{λ}x_{0}.E′[[e_{1}]] \overline{@} (\overline{λ}x_{1}.x_{0} \underline{@} x_{1} \underline{@} k))
T : Val → Val
T [[x]] = x
T [[λx.e]] = \underline{λ}x.\underline{λ}k.E[[e]] \overline{@} k
E′ : Expr → (Val → Comp) → Comp
E′[[t]] = \overline{λ}κ.κ \overline{@} T [[t]]
E′[[s]] = \overline{λ}κ.S′[[s]] \overline{@} κ
S′ : Comp → (Val → Comp) → Comp
S′[[e_{0} e_{1}]] = \overline{λ}κ.E′[[e_{0}]] \overline{@} (\overline{λ}x_{0}.E′[[e_{1}]] \overline{@} (\overline{λ}x_{1}.x_{0} \underline{@} x_{1} \underline{@} (\underline{λ}x_{2}.κ \overline{@} x_{2})))

Figure 1: Higher-order one-pass CPS transformation E is applied to terms in tail position [3] and E′ to terms appearing in non-tail position; they are otherwise similar. S is applied to serious terms in tail position and S′ to terms appearing in non-tail position; they are otherwise similar. T is applied to trivial terms.

In Figure 1, transformation-time abstractions (\overline{λ}) and applications (infix \overline{@}) are overlined. Underlined abstractions (\underline{λ}) and applications (infix \underline{@}) are hygienic syntax constructors, i.e., they generate fresh variables.

An expression e is CPS-transformed into the result of \underline{λ}k.E[[e]] \overline{@} k.

2.2 Circumventing the higher-order functions

Let us analyze the function spaces in Figure 1. All the calls to E, S, E′, and S′ are fully applied and thus these functions could as well be uncurried. The resulting CPS transformation is only higher order because of the function space Val → Comp used in E′ and S′. Let us try to circumvent this function space.

A simple control-flow analysis of the uncurried CPS transformation tells us that while both E and E′ invoke T , T only invokes E, E only invokes S, and S only invokes E′ while E′ and S′ invoke each other. The following diagram illustrates these relationships.

\xymatrix{E \ar[r] \ar[dr] & S \ar[r] & E′ \ar[dl] \ar[r] & S′ \ar[l] \\  & T \ar[ul]}

Therefore, if we could prevent S from calling E′, both E′ and S′ would become dead code, and only E, S, and T would remain. We would then obtain a firstorder one-pass CPS transformation.

Let us unfold the definition of S and reason by inversion. The four following cases occur. (We only detail the β-reductions in the first case.)

S[[t_{0} t_{1}]] \overline{@} k =_{def} E′[[t_{0}]] \overline{@} (\overline{λ}x_{0}.E′[[t_{1}]] \overline{@} (\overline{λ}x_{1}.x_{0} \underline{@} x_{1} \underline{@} k))
=_{def} (\overline{λ}x_{0}.E′[[t_{1}]] \overline{@} (\overline{λ}x_{1}.x_{0} \underline{@} x_{1} \underline{@} k)) \overline{@} T [[t_{0}]]
→_{β} E′[[t_{1}]] \overline{@} (\overline{λ}x_{1}.T [[t_{0}]] \underline{@} x_{1} \underline{@} k)
=_{def} (\overline{λ}x_{1}.T [[t_{0}]] \underline{@} x_{1} \underline{@} k) \overline{@} T [[t_{1}]]
→_{β} T [[t_{0}]] \underline{@} T [[t_{1}]] \underline{@} k
S[[t_{0} s_{1}]] \overline{@} k =_{β} S′[[s_{1}]] \overline{@} (\overline{λ}x_{1}.T [[t_{0}]] \underline{@} x_{1} \underline{@} k)
S[[s_{0} t_{1}]] \overline{@} k =_{β} S′[[s_{0}]] \overline{@} (\overline{λ}x_{0}.x_{0} \underline{@} T [[t_{1}]] \underline{@} k)
S[[s_{0} s_{1}]] \overline{@} k =_{β} S′[[s_{0}]] \overline{@} (\overline{λ}x_{0}.S′[[s_{1}]] \overline{@} (\overline{λ}x_{1}.x_{0} \underline{@} x_{1} \underline{@} k))

This analysis makes explicit all of the functions κ that S passes to S′. By definition of S′, we also know where these functions are applied: in the twolevel eta-redex \underline{λ}x_{2}.κ \overline{@} x_{2}. We can take advantage of this knowledge by invoking S rather than S′, extend its domain to Comp → Expr → Comp, and pass it the result of eta-expanding κ. The result reads as follows.

S[[t_{0} t_{1}]] \overline{@} k ≡ T [[t_{0}]] \underline{@} T [[t_{1}]] \underline{@} k
S[[t_{0} s_{1}]] \overline{@} k ≡ S[[s_{1}]] \overline{@} (\underline{λ}x_{1}.T [[t_{0}]] \underline{@} x_{1} \underline{@} k)
S[[s_{0} t_{1}]] \overline{@} k ≡ S[[s_{0}]] \overline{@} (\underline{λ}x_{0}.x_{0} \underline{@} T [[t_{1}]] \underline{@} k)
S[[s_{0} s_{1}]] \overline{@} k ≡ S[[s_{0}]] \overline{@} (\underline{λ}x_{0}.S[[s_{1}]] \overline{@} (\underline{λ}x_{1}.x_{0} \underline{@} x_{1} \underline{@} k))

In this derived transformation, E′ and S′ are no longer used. Since they are the only higher-order components of the uncurried CPS transformation, the derived transformation, while still one-pass and compositional, is first-order. Its control-flow graph can be depicted as follows.

[figure: E; S; T]

The resulting CPS transformation is displayed in Figure 2. Since it is first-order, there are no overlined abstractions and applications, and therefore we omit all underlines as well as the infix @. An expression e is CPS-transformed into the result of λk.E[[e]] k.

E : Expr × Ide → Comp
E[[t]] k = k T [[t]]
E[[s]] k = S[[s]] k
S : Comp × Expr → Comp
S[[t_{0} t_{1}]] K = T [[t_{0}]] T [[t_{1}]] K
S[[t_{0} s_{1}]] K = S[[s_{1}]] (λx_{1}.T [[t_{0}]] x_{1} K)
S[[s_{0} t_{1}]] K = S[[s_{0}]] (λx_{0}.x_{0} T [[t_{1}]] K)
S[[s_{0} s_{1}]] K = S[[s_{0}]] (λx_{0}.S[[s_{1}]] (λx_{1}.x_{0} x_{1} K))
T : Val → Val
T [[x]] = x
T [[λx.e]] = λx.λk.E[[e]] k

Figure 2: First-order one-pass CPS transformation

This first-order CPS transformation is compositional (in the sense of denotational semantics) because on the right-hand side, all recursive calls are on proper sub-parts of the left-hand-side term [42, page 60]. One could say, however, that it is not purely defined by recursive descent, since S is defined by cases on immediate sub-expressions, using a sort of structural look-ahead. (A change of grammar would solve that problem, though.) The main cost incurred by the inversion step above is that it requires 2^{n} clauses for a source term with n sub-terms that need to be considered (e.g., a tuple).

3 From non-compositional to compositional

3.1 A non-compositional specification

The first edition of Essentials of Programming Languages [18] dedicated a chapter to the CPS transformation, with the goal to be as intuitive and pedagogical as possible and to produce CPS terms similar to what one would write by hand. This CPS transformation inspired Sabry and Felleisen to design a radically different CPS transformation based on evaluation contexts that produces a remarkably compact output due to an extra reduction rule, β_{lift} [11, 37]. Sabry and Wadler then simplified this CPS transformation [38, Figure 18], e.g., omitting β_{lift}. This simplified CPS transformation now forms the basis of the chapter on the CPS transformation in the second edition of Essentials of Programming Languages [19].

Using the same notation as in Figure 2, Sabry and Wadler’s CPS transformation reads as follows. An expression e is CPS-transformed into λk.E[[e]], where:

E[[e]] = S[[e]] k
S[[t]] K = K T [[t]]
S[[t_{0} t_{1}]] K = T [[t_{0}]] T [[t_{1}]] K
S[[t_{0} s_{1}]] K = S[[s_{1}]] (λx_{1}.S[[t_{0} x_{1}]] K)
S[[s_{0} e_{1}]] K = S[[s_{0}]] (λx_{0}.S[[x_{0} e_{1}]] K)
T [[x]] = x
T [[λx.e]] = λx.λk.E[[e]]

For each serious expression s with a serious immediate sub-expression s′, S recursively traverses s′ with a new continuation. In this new continuation, s′ is replaced by a fresh variable (i.e., a trivial immediate sub-expression) in s. The result, now with one less serious immediate sub-expression, is transformed recursively. The idea was the same in Sabry and Felleisen’s context-based CPS transformation [37, Definition 5], which we study elsewhere [12, 14, 27].

These CPS transformations hinge on a unique free variable k and also they are not compositional. For example, on the right-hand side of the definition of S just above, some recursive calls are on terms that are not proper sub-parts of the left-hand-side term. The input program changes dynamically during the transformation, and proving termination therefore requires a size argument. In contrast, a compositional transformation entails a simpler termination proof by structural induction.

3.2 Eliminating the non-compositionality

Sabry and Wadler’s CPS transformation can be made compositional through the following unfolding steps.

Unfolding S in S[[t_{0} x_{1}]] K: The result is T [[t_{0}]] T [[x_{1}]] K, which is equivalent to T [[t_{0}]] x_{1} K.

Unfolding S in S[[x_{0} e_{1}]] K: Two cases occur (thus splitting this clause for S into two).

• If e_{1} is a value (call it t_{1}), the result is T [[x_{0}]] T [[t_{1}]] K, which is

equivalent to x_{0} T [[t_{1}]] K.

• If e_{1} is a computation (call it s_{1}), the result is S[[s_{1}]] (λx_{1}.S[[x_{0} x_{1}]] K). Unfolding the inner occurrence of S yields S[[s_{1}]] (λx_{1}.T [[x_{0}]] T [[x_{1}]] K),

which is equivalent to S[[s_{1}]] (λx_{1}.x_{0} x_{1} K).

The resulting unfolded transformation is compositional. It also coincides with the definition of S in Figure 2 and thus connects the two separate lines of research.

4 From two passes to one pass

4.1 A two-pass specification

Plotkin’s CPS transformation [30] can be phrased as follows.

\begin{aligned}C[[t]] & = & λk.k Φ(t) \\ C[[e_{0} e_{1}]] & = & λk.C[[e_{0}]] (λx_{0}.C[[e_{1}]] (λx_{1}.x_{0} x_{1} k)) \\ Φ(x) & = & x \\ Φ(λx.e) & = & λx.C[[e]] \end{aligned}

Directly implementing it yields CPS terms containing a mass of administrative redexes that need to be contracted in a second pass [39].

4.2 A colon translation for proving simulation

Plotkin’s simulation theorem shows a correspondence between reductions in the source program and in the transformed program. To this end, he introduced the so-called “colon translation” to bypass the initial administrative reductions of a CPS-transformed term.

The colon translation makes it possible to focus on the reduction of the abstractions inherited from the source program. The simulation theorem is shown by relating each reduction step, as depicted by the following diagram.

e

reduction [figure]

CPS transformation

[figure] e′

CPS transformation

[figure]

C[[e]]K

administrative reductions

[figure]

C[[e′]]K

administrative reductions

[figure]

e: K reduction

[figure]

e′: K

The colon translation is itself a CPS transformation. It transforms a source expression and a continuation into a CPS term; this CPS term is the one that appears after contracting the initial administrative redexes of the CPS-transformed expression applied to the continuation. In other words, if we write the colon translation of the expression e and the continuation K as e : K, then the following holds: C[[e]] K →^{∗} e : K.

The colon translation can be derived from the CPS transformation by predicting the result of the initial administrative reductions from the structure of the source term. For example, a serious term of the form t_{0} e_{1} is CPStransformed into λk.(λk.k Φ(v)) (λx_{0}.C[[e_{1}]] (λx_{1}.x_{0} x_{1} k)). Applying this CPS term to a continuation enables the following administrative reductions.

(λk.(λk.k Φ(t_{0})) (λx_{0}.C[[e_{1}]] (λx_{1}.x_{0} x_{1} k))) K
→_{β} (λk.k Φ(t_{0})) (λx_{0}.C[[e_{1}]] (λx_{1}.x_{0} x_{1} K))
→_{β} (λx_{0}.C[[e_{1}]] (λx_{1}.x_{0} x_{1} K)) Φ(t_{0})
→_{β} C[[e_{1}]] λx_{1}.Φ(t_{0}) x_{1} K

The result is a smaller term that can be CPS-transformed recursively. This insight leads one to Plotkin’s colon translation, as defined below.

\begin{aligned}t: K & = & K Φ(t) \\ t_{0} t_{1} : K & = & Φ(t_{0}) Φ(t_{1}) K \\ t_{0} s_{1} : K & = & s_{1} : (λx_{1}.Φ(t_{0}) x_{1} K) \\ s_{0} e_{1} : K & = & s_{0} : (λx_{0}.C[[e_{1}]] (λx_{1}.x_{0} x_{1} K)) \end{aligned}

4.3 Merging CPS transformation and colon translation

For Plotkin’s purpose—reasoning about the output of the CPS transformation— contracting the initial administrative reductions in each step is sufficient. Our goal, however, is to remove all administrative redexes in one pass. Since the colon translation contracts some administrative redexes, and thus more than the CPS transformation, further administrative redexes can be contracted by using the colon translation in place of all occurrences of C.

The CPS transformation is used once in the colon translation and once in the definition of Φ. For consistency, we distinguish two cases in the colon translation, depending on whether the expression is a value or not, and we use the colon translation if it is not a value. In the definition of Φ, we introduce the continuation identifier and then we use the colon translation. The resulting extended colon translation reads as follows.

\begin{aligned}t: K & = & K Φ(t) \\ t_{0} t_{1} : K & = & Φ(t_{0}) Φ(t_{1}) K \\ t_{0} s_{1} : K & = & s_{1} : (λx_{1}.Φ(t_{0}) x_{1} K) \\ s_{0} t_{1} : K & = & s_{0} : (λx_{0}.x_{0} Φ(t_{1}) K) \\ s_{0} s_{1} : K & = & s_{0} : (λx_{0}.(s_{1} : (λx_{1}.x_{0} x_{1} K))) \\ Φ(x) & = & x \\ Φ(λx.e) & = & λx.λk.(e: k) \end{aligned}

With a change of notation, this extended colon translation coincides with the first-order one-pass CPS transformation from Figure 2. In other words, not only does the extended colon translation remove more administrative redexes than the original one, but it actually removes as many as the two-pass transformation.

5 Correctness of the first-order one-pass CPS transformation

We prove the correctness of the transformation of Figure 2 in the traditional way established by Plotkin [30]. To this end, we first define a reduction relation on programs and then we prove a simulation theorem.

5.1 Reduction rules

We give the reduction relation using evaluation contexts in the style of Felleisen [17]. The evaluation contexts are given by the following grammar.

E ::= [ ] | E e | t E

A context is an expression with a hole. We plug the hole of a context E with an expression e (noted E[e]) as follows.

\begin{aligned}[ ][e] & = & e \\ (E e′)[e] & = & (E[e]) e′ \\ (t E)[e] & = & t (E[e]) \end{aligned}

This definition of evaluation contexts satisfies a unique decomposition property, namely that any expression that is not a value can be decomposed into a context and an application of values, i.e.,

∀s.∃E, t_{0}, t_{1}.s = E[t_{0} t_{1}]

and this decomposition is unique.

We then define a reduction relation on expressions with the following rule:

E[(λx.e) t] → E[e[t/x]]

where e[t/x] is the usual capture-avoiding substitution of t for free occurrences of x in e. We call an expression on the form (λx.e) t a redex.

We say that e is reducible if there exists an e′ such that e → e′. So, for example, values are not reducible. We write →^{+}, →^{∗}, and →^{n} for the transitive closure, the reflexive and transitive closure, and the n-times composition of the relation →.

Some computations are not reducible. They are said to “stick”. The set of stuck terms is exactly those on the form E[x t], i.e., the application of a variable to a value in an evaluation context. Since the decomposition is unique, such an expression cannot be reducible.

5.2 Simulation

Plotkin used four lemmas and a colon translation to prove the correctness of his CPS transformation. Since our CPS transformation already performs the administrative reductions at transformation time, we do not need to introduce any colon translation and thus Plotkin’s initial-reduction lemma holds trivially. Therefore, we work directly with the CPS transformation in the following three lemmas.

Lemma 1 (Substitution) If e is an expression, t a value, x a variable, and K another value then

(E[[e]] K)[T [[t]]/x] = E[[e[t/x]]] (K[T [[t]]/x])

If e is an expression, k is a variable, and K an expression then

(E[[e]] k)[K/k] = E[[e]] K

Proof: The first equation is proven by induction on the structure of e, following the definition of substitution.

The second equation follows directly from the definition of E[[e]] K. qed

Lemma 2 (Single-step simulation) The reductions of the transformed program match the reductions of the source program in the sense that

e → e′ ⟹ E[[e]] K →^{+} E[[e′]] K

Proof: If e → e′ then there exists a context E, a redex t_{0} t_{1}, and an expression e′′ such that e = E[t_{0} t_{1}] and e′ = E[e′′]. The proof, which we omit, is by induction on the context E. qed

Lemma 2 accounts for all reducible expressions. The following lemma handles the expressions that stick.

Lemma 3 (Preservation of stuck terms) If e sticks (i.e., if it is a computation that is not reducible) and K is a value, then S[[e]] K sticks.

Proof: Since all stuck expressions are of the form E[x t], the proof is by induction on E. qed

Theorem 1 (Simulation) If e is an expression and v is a CPS value then

(∃t.e →^{∗} t ∧ T [[t]] = v) ⟺ E[[e]] λx.x →^{∗} v

Proof:

1. (∃t.e →^{∗} t ∧ T [[t]] = v) ⟹ E[[e]] λx.x →^{∗} v

Let e, v, and t be given with v = T [[t]]. From repeated use of Lemma 2, it follows that E[[e]] λx.x →^{∗} E[[t]] λx.x, and E[[t]] λx.x = (λx.x) T [[t]] → T [[t]] = v.

2. E[[e]] λx.x →^{∗} v ⟹ (∃t.e →^{∗} t ∧ T [[t]] = v)

Let e and v be given. Then this implication is proved by contraposition, i.e., assume that ∃t.e →^{∗} t ∧ T [[t]] = v fails to hold. Either there is no t such that e →^{∗} t, or there is one, but T [[t]] ≠ v.

The expression e does not reduce to a value t in two cases: when e diverges, i.e., has an infinite derivation, and when it reduces to a stuck term. In either case E[[e]] λx.x has the same behavior.

• e diverges ⟹ E[[e]] λx.x diverges If an expression e diverges, there exists no finite number n such that e →^{n} e′ and e′ is not reducible (i.e., either a value or a stuck expression). That is, for all numbers n there exists an expression e_{n} such

that e →^{n} e_{n}.

Now, let n be a natural number. We consider the sequence e → e_{1} → ⋯ → e_{n}, which exists since e diverges. Then, from Lemma 2 we know that there is another reduction sequence E[[e]] λx.x →^{+} E[[e_{1}]] λx.x →^{+} ⋯ →^{+} E[[e_{n}]] λx.x of length at least n. Therefore E[[e]] λx.x has reduction sequences of arbitrary length and thus it diverges as well.

• e →^{∗} e′ and e′ sticks ⟹ E[[e]] λx.x →^{∗} e′′ and e′′ sticks From repeated use of Lemma 2 we know that E[[e]] λx.x →^{∗} E[[e′]] λx.x, and from Lemma 3 we know that E[[e′]] λx.x sticks.

• Let t be given such that e →^{∗} t∧T [[t]] ≠ v. Then it cannot be the case that E[[e]] λx.x →^{∗} v. This follows from the implication in the other direction, since then E[[e]] λx.x →^{∗} T [[t]] ≠ v.

Together these cases account for all possible reductions of an expression, which suffices to prove the simulation theorem. qed

6 Reasoning about CPS-transformed programs

How to go about proving properties of CPS-transformed programs depends on which kind of CPS transformation was used. In this section, we review each of them in turn. As our running example, we prove that the CPS transformation preserves types. (The CPS transformation of types exists [24, 40] and has a logical content [20, 26].) We consider the simply typed λ-calculus, with a typing judgment of the form Γ ⊢ e: τ.

6.1 A higher-order one-pass CPS transformation

Danvy and Filinski used a typing argument to prove that their one-pass CPS transformation is well-defined [10, Theorem 1]. To prove the corresponding simulation theorem, they used a notion of schematic continuations. Since then, for the same purpose, we have developed a higher-order analogue of Plotkin’s colon translation [13, 27].

Proving structural properties of CPS programs is not completely trivial. Matching the higher-order nature of the one-pass CPS transformation, a logical relation is needed, e.g., to prove ordering properties of CPS terms [9, 15, 16]. (The analogy between these ordering properties and substitution properties of linear λ-calculi has prompted Polakow and Pfenning to develop an ordered logical framework [31, 32, 33].) A logical relation amounts to structural induction at higher types. Therefore, it is crucial that the higher-order one-pass CPS transformation be compositional.

The CPS transformation preserves types: To prove the well-typedness of a CPS-transformed term, we proceed by structural induction on the typing derivation of the source term (or by structural induction on the source expression), together with a logical relation on the functional accumulator.

6.2 A first-order two-pass CPS transformation

Sabry and Felleisen also considered a two-pass CPS transformation. They used developments [2, Section 11.2] to prove that it is total [37, Proposition 2].

To prove structural properties of simplified CPS programs, one can (1) characterize the property prior to simplification, and (2) prove that simplifications preserve the property. Danvy took these steps to prove occurrence conditions of continuation identifiers [8], and so did Damian and Danvy to characterize the effect of the CPS transformation on control flow and binding times [4, 6]. It is Polakow’s thesis that an ordered logical framework provides a good support for stating and proving such properties [31, 34].

The CPS transformation preserves types: To prove the well-typedness of a CPS-transformed term, we first proceed by structural induction on the typing derivation of the source term. (It is thus crucial that the CPS transformation be compositional.) For the second pass, we need to show that the administrative contractions preserve the typeability and the type of the result. But this follows from the subject reduction property of the simply typed λ-calculus.

6.3 A first-order one-pass CPS transformation

The proof in Section 5 follows the spirit of Plotkin’s original proof [30] but is more direct since it does not require a colon translation.

A first-order CPS transformation makes it possible to prove structural properties of a CPS-transformed program by structural induction on the source program. We find these proofs noticeably simpler than the ones mentioned in Section 6.1. For two other examples, Damian and Danvy have used the present first-order CPS transformation to develop a CPS transformation of control-flow information [5] that is simpler than existing ones [4, 6, 29], and Nielsen has used it to present a new and simpler correctness proof of a direct-style transformation [27, 28].

Again, for structural induction to go through, it is crucial that the CPS transformation be compositional.

The CPS transformation preserves types: To prove the well-typedness of a CPS-transformed term, we proceed by structural induction on the typing derivation of the source term.

6.4 Non-compositional CPS transformations

Sabry and Felleisen’s proofs are by induction on the size of the source program [37, Appendix A, page 337]. Proving type preservation would require a substitution lemma.

7 Conclusion and issues

7.1 The big picture

Elsewhere [11, 12, 14], we have developed further connections between higherorder and context-based one-pass CPS transformations. The overall situation is summarized in the following diagram.

Plotkin, 1975

Danvy & Filinski, 1992

[figure]

{Plotkin, \atop 1975}

[figure] EoPL1, 1991

Sabry & Felleisen, 1993

[figure] context-based CPS transformation

Sabry & Wadler, 1997

[figure] Danvy & Nielsen, 2001

[figure]

[figure]

colon translation Danvy & Nielsen,

2001

[figure]

Section 4 [figure]

[figure]

compositional higher-order one-pass CPS transformation

[figure]

Danvy & Nielsen,

2001

[figure]

Section 2

[figure]

simplified context-based CPS transformation [figure]

Section 3 [figure]

[figure]

Friedman, Wand, & Haynes, 2001

[figure] compositional first-order one-pass CPS transformation

EoPL2, 2001

This diagram is clearly in two parts: the left part stems from Plotkin’s work and the right part from the first edition of Essentials of Programming Languages. The left-most part represents the CPS transformation with the colon translation. The vertical line in the middle represents the path of compositional CPS transformations. The vertical line on the right represents the path of noncompositional CPS transformations. The right arrow from the colon translation is our higher-order colon translation [13]. The upper arrows between the left part and the right part of the diagram correspond to our work on β-redexes [11], defunctionalization [12], and refocusing in syntactic theories [14].

The present work links the left part and the right part of the diagram further.

7.2 Scaling up

Our derivation of a first-order, one-pass CPS transformation generalizes to other evaluation orders, e.g., call-by-name. (Indeed each evaluation order gives rise to a different CPS transformation [21].) The CPS transformation also scales up to the usual syntactic constructs of a programming language such as primitive operations, tuples, conditional expressions, and sequencing.

A practical problem, however, arises for block structure, i.e., let- and letrecexpressions. For example, a let-expression is CPS-transformed as follows (extending Figure 1).

S[[let x = e_{1} in e_{2}]] = \overline{λ}k.E[[e_{1}]] \overline{@} (\underline{λ}x.E[[e_{2}]] \overline{@} k)
S′[[let x = e_{1} in e_{2}]] = \overline{λ}κ.E′[[e_{1}]] \overline{@} (\underline{λ}x.E′[[e_{2}]] \overline{@} κ)

In contrast to Section 2.2, the call site of the functional accumulator (i.e., where it is applied) cannot be determined in one pass with finite look-ahead. This information is context sensitive because κ can be applied in arbitrarily deeply nested blocks. Therefore no first-order one-pass CPS transformation can flatten nested blocks in general if it is also to be compositional.

To flatten nested blocks, one can revert to a non-compositional CPS transformation, to a two-pass CPS transformation, or to a higher-order CPS transformation. (Elsewhere [11], we have shown that such a higher-order, compositional, and one-pass CPS transformation is dependently typed. Its type depends on the nesting depth.)

In the course of this work, and in the light of Section 3.2, we have conjectured that the problem of block structure should also apply to a first-order one-pass CPS transformation such as Sabry and Wadler’s. This is the topic of the next section.

7.3 A shortcoming

Sabry and Wadler’s transformation [38] also handles let expressions (extending the CPS transformation of Section 3.1):

S[[let x = e_{1} in e_{2}]] K = S[[e_{1}]] (λx.S[[e_{2}]] K)

If we view this equation as the result of circumventing a functional accumulator, we can see that it assumes this accumulator never to be applied. But it is easy to construct a source term where the accumulator would need to be applied—e.g., the following one.

S[[t_{0} (let x = t_{1} in t_{2})]] K = S[[let x = t_{1} in t_{2}]] (λx_{1}.T [[t_{0}]] x_{1} K)
= S[[t_{1}]] (λx.S[[t_{2}]] (λx_{1}.T [[t_{0}]] x_{1} K))
= S[[t_{1}]] (λx.(λx_{1}.T [[t_{0}]] x_{1} K) T [[t_{2}]])
= (λx.(λx_{1}.T [[t_{0}]] x_{1} K) T [[t_{2}]]) T [[t_{1}]]

The resulting term is semantically correct, but syntactically it contains an extraneous administrative redex.

In contrast, a higher-order one-pass CPS transformation yields the following more compact term, corresponding to what one might write by hand (with the provision that one usually writes a let expression rather than a β-redex).

S[[t_{0} (let x = t_{1} in t_{2})]] k ≡ (λx.T [[t_{0}]] T [[t_{2}]] k) T [[t_{1}]]

The CPS transformation of the second edition of Essentials of Programming Languages inherits this shortcoming for non-tail let expressions containing computations in their header (i.e., for non-simple let expressions that are not in tail position, to use the terminology of the book).

7.4 Summary and conclusion

We have presented a one-pass CPS transformation that is both first-order and compositional. This CPS transformation makes it possible to reason about CPS-transformed programs by structural induction over source programs. Its correctness proof (i.e., the proof of its simulation theorem) is correspondingly very simple. The second author’s PhD thesis [27, 28] also contains a new and simpler correctness proof of the converse transformation, i.e., the direct-style transformation [7]. Finally, this new CPS transformation has enabled Damian and Danvy to define a one-pass CPS transformation of control-flow information [4, 5].

Acknowledgments: Thanks are due to Dan Friedman for a substantial email discussion with the first author about compositionality in the summer of 2000, and to Amr Sabry for a similar discussion at the Third ACM SIGPLAN Workshop on Continuations, in January 2001. This article results from an attempt at unifying our points of view, and has benefited from comments by Daniel Damian, Andrzej Filinski, Mayer Goldberg, Julia Lawall, David Toman, and the anonymous referees. Special thanks to Julia Lawall for a substantial round of proof-reading.

A An example of continuation-passing program

The following ML functions compute the map functional. One is in direct style, and the other one in CPS.

 (*  map : ('a -> 'b) * 'a list -> 'b list *)
 fun map (f, nil)
     = nil
   | map (f, x :: xs)
     = (f x) :: (map (f, xs))
 (*  map_c : ('a * ('b -> 'c) -> 'c) * 'a list * ('b list -> 'c) -> 'c *)
 fun map_c (f_c, nil, k)
     = k nil
   | map_c (f_c, x :: xs, k)
     = f_c (x, fn v => map_c (f_c, xs, fn vs => k (v :: vs)))

The direct-style function map takes a direct-style function and a list as arguments, and yields another list as result.

The continuation-passing function map c takes a continuation-passing function, a list, and a continuation as arguments. It yields a result of type 'c, which is also the type of the final result of any CPS program that uses map c. Matching the result type 'b list of map, the continuation of map c has type 'b list -> 'c. Matching the argument type 'a -> 'b of map, the first argument of map c is a continuation-passing function of type 'a * ('b -> 'c) -> 'c.

In the base case, map returns nil whereas map c sends nil to the continuation. For a non-empty list, map constructs a list with the result of its first argument on the head of the list and with the result of a recursive call on the rest of the list. In contrast, map c calls its first argument on the head of the list with a new continuation that, when sent a result, recursively calls map c on the rest of the list with a new continuation that, when sent a list of results, constructs a list and sends it to the continuation. In map c, all calls are tail calls.

References

[1] Andrew W. Appel. Compiling with Continuations. Cambridge University Press, New York, 1992.

[2] Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundation of Mathematics. North-Holland, 1984. Revised edition.

[3] William D. Clinger. Proper tail recursion and space efficiency. In Keith D. Cooper, editor, Proceedings of the ACM SIGPLAN’98 Conference on Programming Languages Design and Implementation, pages 174– 185, Montréal, Canada, June 1998. ACM Press.

[4] Daniel Damian. On Static and Dynamic Control-Flow Information in Program Analysis and Transformation. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-5.

[5] Daniel Damian and Olivier Danvy. A simple CPS transformation of controlflow information. Technical Report BRICS RS-01-55, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 2001.

[6] Daniel Damian and Olivier Danvy. Syntactic accidents in program analysis: On the impact of the CPS transformation. Journal of Functional Programming, 2002. To appear. Extended version available as the technical report BRICS-RS-01-54.

[7] Olivier Danvy. Back to direct style. Science of Computer Programming, 22(3):183–195, 1994.

[8] Olivier Danvy. Formalizing implementation strategies for first-class continuations. In Gert Smolka, editor, Proceedings of the Ninth European Symposium on Programming, number 1782 in Lecture Notes in Computer Science, pages 88–103, Berlin, Germany, March 2000. Springer-Verlag.

[9] Olivier Danvy, Belmina Dzafic, and Frank Pfenning. On proving syntactic properties of CPS programs. In Third International Workshop on Higher-Order Operational Techniques in Semantics, volume 26 of Electronic Notes in Theoretical Computer Science, pages 19–31, Paris, France, September 1999. Also available as the technical report BRICS RS-99-23.

[10] Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361–391, 1992.

[11] Olivier Danvy and Lasse R. Nielsen. CPS transformation of beta-redexes. In Amr Sabry, editor, Proceedings of the Third ACM SIGPLAN Workshop on Continuations, Technical report 545, Computer Science Department, Indiana University, pages 35–39, London, England, January 2001. Also available as the technical report BRICS RS-00-35.

[12] Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. In Harald Søndergaard, editor, Proceedings of the Third International Conference on Principles and Practice of Declarative Programming, pages 162–174, Firenze, Italy, September 2001. ACM Press. Extended version available as the technical report BRICS RS-01-23.

[13] Olivier Danvy and Lasse R. Nielsen. A higher-order colon translation. In Kuchen and Ueda [23], pages 78–91. Extended version available as the technical report BRICS RS-00-33.

[14] Olivier Danvy and Lasse R. Nielsen. Syntactic theories in practice. In Mark van den Brand and Rakesh M. Verma, editors, Informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), volume 59.4 of Electronic Notes in Theoretical Computer Science, Firenze, Italy, September 2001. Extended version available as the technical report BRICS RS-01-31.

[15] Olivier Danvy and Frank Pfenning. The occurrence of continuation parameters in CPS terms. Technical report CMU-CS-95-121, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, February 1995.

[16] Belmina Dzafic. Formalizing program transformations. Master’s thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 1998.

[17] Matthias Felleisen. The Calculi of λ-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Department of Computer Science, Indiana University, Bloomington, Indiana, August 1987.

[18] Daniel P. Friedman, Mitchell Wand, and Christopher T. Haynes. Essentials of Programming Languages. The MIT Press and McGraw-Hill, 1991.

[19] Daniel P. Friedman, Mitchell Wand, and Christopher T. Haynes. Essentials of Programming Languages, second edition. The MIT Press, 2001.

[20] Timothy G. Griffin. A formulae-as-types notion of control. In Paul Hudak, editor, Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 47–58, San Francisco, California, January 1990. ACM Press.

[21] John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 458–471, Portland, Oregon, January 1994. ACM Press.

[22] David Kranz, Richard Kesley, Jonathan Rees, Paul Hudak, Jonathan Philbin, and Norman Adams. Orbit: An optimizing compiler for Scheme. In Proceedings of the ACM SIGPLAN’86 Symposium on Compiler Construction, pages 219–233, Palo Alto, California, June 1986. ACM Press.

[23] Herbert Kuchen and Kazunori Ueda, editors. Functional and Logic Programming, 5th International Symposium, FLOPS 2001, number 2024 in Lecture Notes in Computer Science, Tokyo, Japan, March 2001. Springer-Verlag.

[24] Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi (summary). In Rohit Parikh, editor, Logics of Programs – Proceedings, number 193 in Lecture Notes in Computer Science, pages 219–224, Brooklyn, June 1985. Springer-Verlag.

[25] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.

[26] Chetan R. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1990.

[27] Lasse R. Nielsen. A study of defunctionalization and continuation-passing style. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-7.

[28] Lasse R. Nielsen. A simple correctness proof of the direct-style transformation. Technical Report BRICS RS-02-02, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, January 2002.

[29] Jens Palsberg and Mitchell Wand. CPS transformation of flow information. Unpublished manuscript, available at http://www.cs.purdue.edu/

~palsberg/publications.html, June 2001.

[30] Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

[31] Jeff Polakow. Ordered Linear Logic and Applications. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, August 2001. Technical Report CMU-CS-01-152.

[32] Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In Jean-Yves Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications, number 1581 in Lecture Notes in Computer Science, pages 295–309, L’Aquila, Italy, April 1999. Springer-Verlag.

[33] Jeff Polakow and Frank Pfenning. Properties of terms in continuation passing style in an ordered logical framework. In Joëlle Despeyroux, editor, Workshop on Logical Frameworks and Meta-Languages (LFM 2000), Santa

Barbara, California, June 2000. http://www-sop.inria.fr/certilab/
LFM00/Proceedings/.

[34] Jeff Polakow and Kwangkeun Yi. Proving syntactic properties of exceptions in an ordered logical framework. In Kuchen and Ueda [23], pages 61–77.

[35] John C. Reynolds. The discoveries of continuations. Lisp and Symbolic Computation, 6(3/4):233–247, 1993.

[36] John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363–397, 1998. Reprinted from the proceedings of the 25th ACM National Conference (1972).

[37] Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3/4):289–360, 1993.

[38] Amr Sabry and Philip Wadler. A reflection on call-by-value. ACM Transactions on Programming Languages and Systems, 19(6):916–941, 1997.

[39] Guy L. Steele Jr. Rabbit: A compiler for Scheme. Technical Report AI-TR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978.

[40] Mitchell Wand. Embedding type structure in semantics. In Mary S. Van Deusen and Zvi Galil, editors, Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 1–6, New Orleans, Louisiana, January 1985. ACM Press.

[41] Mitchell Wand. Correctness of procedure representations in higher-order assembly language. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Mathematical Foundations of Programming Semantics, number 598 in Lecture Notes in Computer Science, pages 294–311, Pittsburgh, Pennsylvania, March 1991. Springer-Verlag. 7th International Conference.

[42] Glynn Winskel. The Formal Semantics of Programming Languages. Foundation of Computing Series. The MIT Press, 1993.

Recent BRICS Report Series Publications

RS-01-49 Olivier Danvy and Lasse R. Nielsen. A First-Order One-Pass CPS Transformation. December 2001. 21 pp. Extended version of a paper to appear in the proceedings of FOSSACS ’02.

RS-01-48 Mogens Nielsen and Frank D. Valencia. Temporal Concurrent Constraint Programming: Applications and Behavior. December 2001. 36 pp.

RS-01-47 Jesper Buus Nielsen. Non-Committing Encryption is Too Easy in the Random Oracle Model. December 2001. 20 pp.

RS-01-46 Lars Kristiansen. The Implicit Computational Complexity of Imperative Programming Languages. November 2001. 46 pp.

RS-01-45 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. An Extended Quadratic Frobenius Primality Test with Average Case Error Estimates. November 2001. 43 pp.

RS-01-44 M. Oliver Möller, Harald Rueß, and Maria Sorea. Predicate Abstraction for Dense Real-Time Systems. November 2001. 27 pp.

RS-01-43 Ivan B. Damgård and Jesper Buus Nielsen. From Known-Plaintext Security to Chosen-Plaintext Security. November 2001. 18 pp.

RS-01-42 Zoltán Ésik and Werner Kuich. Rationally Additive Semirings. November 2001. 11 pp.

RS-01-41 Ivan B. Damgård and Jesper Buus Nielsen. Perfect Hiding and Perfect Binding Universally Composable Commitment Schemes with Constant Expansion Factor. October 2001. 43 pp.

RS-01-40 Daniel Damian and Olivier Danvy. CPS Transformation of Flow Information, Part II: Administrative Reductions. October 2001. 9 pp.

RS-01-39 Olivier Danvy and Mayer Goldberg. There and Back Again. October 2001. 14 pp.

RS-01-38 Zoltán Ésik. Free De Morgan Bisemigroups and Bisemilattices. October 2001. 13 pp.

RS-01-37 Ronald Cramer and Victor Shoup. Universal Hash Proofs and a Paradigm for Adaptive Chosen Ciphertext Secure Public-Key Encryption. October 2001. 34 pp.