BRICS RS-99-51 O. Danvy: Formalizing Implementation Strategies for First-Class Continuations BRICS

Basic Research in Computer Science

Formalizing Implementation Strategies for First-Class Continuations

Olivier Danvy BRICS Report Series RS-99-51 ISSN 0909-0878 December 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Olivier Danvy.

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/99/51/

Formalizing Implementation Strategies for First-Class Continuations ^{⋆}

Olivier Danvy

BRICS ^{⋆⋆} Department of Computer Science, University of Aarhus Building 540, Ny Munkegade, DK-8000 Aarhus C, Denmark

                    E-mail: danvy@brics.dk
            Home page: http://www.brics.dk/~danvy

Abstract. We present the first formalization of implementation strategies for first-class continuations. The formalization hinges on abstract machines for continuation-passing style (CPS) programs with a special treatment for the current continuation, accounting for the essence of first-class continuations. These abstract machines are proven equivalent to a standard, substitution-based abstract machine. The proof techniques work uniformly for various representations of continuations. As a byproduct, we also present a formal proof of the two folklore theorems that one continuation identifier is enough for second-class continuations and that second-class continuations are stackable. A large body of work exists on implementing continuations, but it is predominantly empirical and implementation-oriented. In contrast, our formalization abstracts the essence of first-class continuations and provides a uniform setting for specifying and formalizing their representation.

1 Introduction

Be it for coroutines, threads, mobile code, interactive computer games, or computer sessions, one often needs to suspend and to resume a computation. Suspending a computation amounts to saving away its state, and resuming a suspended computation amounts to restoring the saved state. Such saved copies may be ephemeral and restored at most once (e.g., coroutines, threads, and computer sessions that were ‘saved to disk’), or they may need to be restored repeatedly (e.g., in a computer game). This functionality is reminiscent of continuations, which represent the rest of a computation [22].

In this article, we consider how to implement first-class continuations. A wealth of empirical techniques exist to take a snapshot of control during the execution of a program (call/cc) and to restore this snapshot (throw): SML/NJ, for example, allocates continuations entirely in the heap, reducing call/cc and throw to a matter of swapping pointers [1]; T and Scheme 48 allocate continuations on a stack, copying this stack in the heap and back to account for

⋆ Extended version available as the technical report BRICS RS-99-51.

⋆⋆

Basic Research in Computer Science (http://www.brics.dk), Centre of the Danish National Research Foundation.

call/cc and throw [16, 17];^{1} and PC Scheme, Chez Scheme, and Larceny allocate continuations on a segmented stack [2, 4, 15]. Clinger, Hartheimer, and Ost’s recent article [4] provides a comprehensive overview of implementation strategies for first-class continuations and of their issues: ideally, first-class continuations should exert zero overhead for programs that do not use them.

Our goal and non-goal: We formalize implementation strategies for first-class continuations. We do not formalize first-class continuations per se (cf., e.g., Felleisen’s PhD thesis [12] or Duba, Harper, and MacQueen’s formal account of call/cc in ML [10]).

Our work: We consider abstract machines for continuation-passing style (CPS) programs, focusing on the implementation of continuations. As a stepping stone, we formalize the folklore theorem that one register is enough to implement second-class continuations. We then formalize the three implementation techniques for first-class continuations mentioned above: heap, stack, and segmented stack. The formalization and its proof techniques (structural induction on terms and on derivation trees) are uniform: besides clarifying what it means to implement continuations, be they second-class or first-class, our work provides a platform to state and prove the correctness of each implementation. Also, this platform is not restricted to CPS programs: through Flanagan et al.’s results [13], it is applicable to direct-style programs if one represents control with a stack of evaluation contexts instead of a stack of functions.

1.1 Related work

The four works most closely related to ours are Clinger, Hartheimer, and Ost’s overview of implementation strategies for first-class continuations [4]; Flanagan, Sabry, Duba, and Felleisen’s account of compiling with continuations and more specifically, their two first abstract machines [13]; Danvy and Lawall’s syntactic characterization of second-class and first-class continuations in CPS programs [8]; and Danvy, Dzafic, and Pfenning’s work on the occurrence of continuation parameters in CPS programs [6, 9, 11].

1.2 Overview

Section 2 presents our source language: the λ-calculus in direct style and in CPS, the CPS transformation, and an abstract machine for CPS programs that will be our reference point here. This standard machine treats continuation identifiers on par with all the other identifiers. The rest of this article focuses on continuation identifiers and how to represent their bindings – i.e., on the essence of how to implement continuations.

1 This strategy is usually attributed to Drew McDermott in the late 70’s [19], but apparently it was already considered in the early ’70s at Queen Mary and Westfield College to implement PAL (John C. Reynolds, personal communication, Aarhus, Denmark, fall 1999).

Section 3 addresses second-class continuations. In a CPS program with secondclass continuations, continuation identifiers are not only linear (in the sense of Linear Logic), but they also denote a stackable resource, and indeed it is folklore that second-class continuations can be implemented LIFO on a “control stack”. We formalize this folklore by characterizing second-class continuations syntactically in a CPS program and by presenting an abstract machine where the bindings of continuation identifiers are represented with a stack. We show this stack machine to be equivalent to the standard one.

Section 4 addresses first-class continuations. In a CPS program with firstclass continuations, continuation identifiers do not denote a stackable resource in general. First-class continuations, however, are relatively rare, and thus over the years, “zero-overhead” implementations have been sought [4]: implementations that do support first-class continuations but only tax programs that use them. We consider the traditional strategy of stack-allocating all continuations by default, as if they were all second-class, and of copying this stack in case of first-class continuations. We formalize this empirical strategy with a new abstract machine, which we show to be equivalent to the standard one.

Section 5 outlines how to formalize alternative implementation strategies, such as segmenting the stack and recycling unshared continuations.

2 CPS programs

We consider closed programs: direct-style (DS) λ-terms with literals. The BNF of DS programs is displayed in Figure 1. Assuming a call-by-value evaluation strategy, the BNF of CPS programs is displayed in Figure 2. CPS programs are prototypically obtained by CPS-transforming DS programs, as defined in Figure 3 [7, 20, 21].

Figure 4 displays our starting point: a standard abstract machine implementing β-reduction for CPS programs. This machine is a simplified version of another machine studied jointly with Belmina Dzafic and Frank Pfenning [6, 9, 11]. We use two judgments, indexed by the syntactic categories of CPS terms. The judgment

⊢_{std}^{CProg} p ↪ a

is satisfied whenever a CPS program p evaluates to an answer a. The auxiliary judgment

⊢_{std}^{CExp} e ↪ a

is satisfied whenever a CPS expression e evaluates to an answer a. The machine starts and stops with the initial continuation k_{init}, which is a distinguished fresh continuation identifier. Answers can be either the trivial expressions ℓ or λx.λk.e, or the error token.

For expository simplicity, our standard machine uses substitutions to implement variable bindings. Alternatively and equivalently, it could use an environment and represent functional values as closures [18]. And indeed Flanagan et al. present a similar standard abstract machine which uses an environment [13, Figure 4].

p ∈ DProg — DS programs p ::= e e ∈ DExp — DS expressions e ::= e_{0} e_{1} | t t ∈ DTriv — DS trivial expressions t ::= ℓ | x | λx.e ℓ ∈ Lit — literals x ∈ Ide — identifiers

Fig. 1. BNF of DS programs

p ∈ CProg — CPS programs p ::= λk.e e ∈ CExp — CPS (serious) expressions e ::= t_{0} t_{1} c | c t t ∈ CTriv — CPS trivial expressions t ::= ℓ | x | v | λx.λk.e c ∈ Cont — continuations c ::= λv.e | k ℓ ∈ Lit — literals x ∈ Ide — source identifiers k ∈ IdeC — fresh continuation identifiers v ∈ IdeV — fresh parameters of continuations a ∈ Answer — CPS answers a ::= ℓ | λx.λk.e | error

Fig. 2. BNF of CPS programs

[[e]]_{cps}^{DProg} = λk.[[e]]_{cps}^{DExp}k  – where k is fresh
[[e_{0} e_{1}]]_{cps}^{DExp}c = [[e_{0}]]_{cps}^{DExp}λv_{0}.[[e_{1}]]_{cps}^{DExp}λv_{1}.v_{0} v_{1} c – where v_{0} and v_{1} are fresh
[[t]]_{cps}^{DExp}c = c [[t]]_{cps}^{DTriv}
[[ℓ]]_{cps}^{DTriv} = ℓ
[[x]]_{cps}^{DTriv} = x
[[λx.e]]_{cps}^{DTriv} = λx.λk.[[e]]_{cps}^{DExp}k  – where k is fresh

Fig. 3. The left-to-right, call-by-value CPS transformation

\frac{⊢std^{CExp} e[k_{init}/k] ↪ a}{⊢std^{CProg} λk.e ↪ a}

⊢std^{CExp} ℓ t c ↪ error

\frac{⊢std^{CExp} e[t/x, c/k] ↪ a}{⊢std^{CExp} (λx.λk.e) t c ↪ a}

\frac{⊢std^{CExp} e[t/v] ↪ a}{⊢std^{CExp} (λv.e) t ↪ a}

⊢std^{CExp} k_{init} t ↪ t

Fig. 4. Standard machine for CPS programs

3 A stack machine for CPS programs with second-class continuations

As a stepping stone, this section formalizes the folklore theorem that in the absence of first-class continuations, one continuation identifier is enough, i.e., in Figure 2, IdeC can be defined as a singleton set. To this end, we prove that in the output of the CPS transformation, only one continuation identifier is indeed enough. We also prove that this property is closed under arbitrary β-reduction. We then rephrase the BNF of CPS programs with IdeC as a singleton set (Section 3.1). In the new BNF, only CPS programs with second-class continuations can be expressed. We present a stack machine for these CPS programs and we prove it equivalent to the standard machine of Figure 4 (Section 3.2). Flanagan et al. present a similar abstract machine [13, Figure 5], but without relating it formally to their standard abstract machine.

3.1 One continuation identifier is enough Each expression in a DS program occurs in one evaluation context. Correspondingly, each expression in a CPS program has one continuation. We formalize this observation in terms of continuation identifiers with the judgment defined in Figure 5, where FC(t) yields the set of continuation identifiers occurring free in t.

\frac{k ∉ FC(t_{0})  k ∉ FC(t_{1})  k ⊧2cc^{Cont} c}{k ⊧2cc^{CExp} t_{0} t_{1} c}  \frac{k ⊧2cc^{Cont} c  k ∉ FC(t)}{k ⊧2cc^{CExp} c t}

\frac{k ⊧2cc^{CExp} e}{k ⊧2cc^{Cont} λv.e}  \overline{k ⊧2cc^{Cont} k}

Fig. 5. Characterization of a second-class continuation abstraction λk.e

Definition 1 (Second-class position, second-class continuations). In a continuation abstraction λk.e, we say that k occurs in second-class position and denotes a second-class continuation whenever the judgment k ⊧_{2cc}^{CExp} e is satisfied.

Below, we prove that actually, in the output of the CPS transformation, all continuation identifiers denote second-class continuations. In Figure 6, we thus generalize our judgment to a whole CPS program.

Definition 2 (2Cont-validity). We say that a CPS program p is 2Cont-valid whenever the judgment ⊧_{2cc*}^{CProg} p is satisfied. Informally, ⊧_{2cc*}^{CProg} p holds if and only if all continuation abstractions λk.e occurring in p satisfy k ⊧_{2cc}^{CExp} e.

Lemma 1 (The CPS transformation yields 2Cont-valid programs). For any p ∈ DProg, ⊧_{2cc*}^{CProg} [[p]]_{cps}^{DProg}.

Proof. A straightforward induction over DS programs. □

\frac{k ⊧2cc*^{CExp} e}{⊧2cc*^{CProg} λk.e}

\frac{⊧2cc*^{CTriv} t_{0}  ⊧2cc*^{CTriv} t_{1}  k ⊧2cc*^{Cont} c}{k ⊧2cc*^{CExp} t_{0} t_{1} c}  \frac{k ⊧2cc*^{Cont} c  ⊧2cc*^{CTriv} t}{k ⊧2cc*^{CExp} c t}

\overline{⊧2cc*^{CTriv} ℓ}  \overline{⊧2cc*^{CTriv} x}  \overline{⊧2cc*^{CTriv} v}  \frac{k ⊧2cc*^{CExp} e}{⊧2cc*^{CTriv} λx.λk.e}

\frac{k ⊧2cc*^{CExp} e}{k ⊧2cc*^{Cont} λv.e}  \overline{k ⊧2cc*^{Cont} k}

Fig. 6. Characterization of a CPS program with second-class continuations

Furthermore, 2Cont-validity is closed under β-reduction, which means that it is preserved by regular evaluation as well as by the arbitrary simplifications of a CPS compiler [21]. The corresponding formal statement and its proof are straightforward and omitted here: we rely on them in the proof of Theorem 1.

Therefore each use of each continuation identifier k is uniquely determined, capturing the fact that in the BNF of 2Cont-valid CPS programs, one continuation identifier is enough. To emphasize this fact, let us specialize the BNF of Figure 2 by defining IdeC as the singleton set {⋆}, yielding the BNF of 2CPS programs displayed in Figure 7.

p ∈ 2CProg — 2CPS programs p ::= λ⋆.e

e ∈ 2CExp — 2CPS (serious) expressions e ::= t_{0} t_{1} c | c t t ∈ 2CTriv — 2CPS trivial expressions t ::= ℓ | x | v | λx.λ⋆.e c ∈ 2Cont — continuations c ::= λv.e | ⋆ ℓ ∈ Lit — literals x ∈ Ide — source identifiers ⋆ ∈ Token — single continuation identifier v ∈ IdeV — fresh parameters of continuations a ∈ 2Answer — 2CPS answers a ::= ℓ | λx.λ⋆.e | error

Fig. 7. BNF of 2CPS programs

Let [[·]]_{strip}^{CProg} denote the straightforward homomorphic mapping from a 2Contvalid CPS program to a 2CPS program and [[·]]_{name}^{2CProg} denote its inverse, such that ∀p ∈ CProg, [[[[p]]_{strip}^{CProg}]]_{name}^{2CProg} ≡_{α} p whenever the judgment ⊧_{2cc*}^{CProg} p is satisfied, and ∀p′ ∈ 2CProg, [[[[p]]_{name}^{2CProg}]]_{strip}^{CProg} = p′. These two translations are generalized in Section 4 and thus we omit their definition here.

3.2 A stack machine for 2CPS programs Figure 8 displays a stack-based abstract machine for 2CPS programs. We obtained it from the standard machine of Section 2, page 4, by implementing the bindings of continuation identifiers with a global “control stack” φ.

φ ∈ 2CStack — control stacks φ ::= • | φ, λv.e

The machine starts and stops with an empty control stack •. When a function is applied, its continuation is pushed on φ. When a continuation is needed, it is popped from φ. If φ is empty, the intermediate result sent to the continuation is the final answer. We distinguish tail calls (i.e., function calls where the continuation is ⋆) by not pushing anything on φ, thereby achieving proper tail recursion.

\frac{• ⊢2cc^{2CExp} e ↪ a}{⊢2cc^{2CProg} λ⋆.e ↪ a}

φ ⊢2cc^{2CExp} ℓ t c ↪ error

\frac{φ ⊢2cc^{2CExp} e[t/x] ↪ a}{φ ⊢2cc^{2CExp} (λx.λ⋆.e) t ⋆ ↪ a}  \frac{φ, λv.e′ ⊢2cc^{2CExp} e[t/x] ↪ a}{φ ⊢2cc^{2CExp} (λx.λ⋆.e) t λv.e′ ↪ a}

\frac{φ ⊢2cc^{2CExp} e[t/v] ↪ a}{φ ⊢2cc^{2CExp} (λv.e) t ↪ a}  \overline{• ⊢2cc^{2CExp} ⋆ t ↪ t}  \frac{φ ⊢2cc^{2CExp} e[t/v] ↪ a}{φ, λv.e ⊢2cc^{2CExp} ⋆ t ↪ a}

Fig. 8. Stack machine for 2CPS programs

N.B. The machine does not substitute continuations for continuation identifiers, and therefore one might be surprised by the rule handling the redex (λv.e) t. Such redexes, however, can occur in the source program.

Formally, the judgment

⊢_{2cc}^{2CProg} p ↪ a

is satisfied whenever a CPS program p ∈ 2CProg evaluates to an answer a ∈ 2Answer. The auxiliary judgment

φ ⊢_{2cc}^{2CExp} e ↪ a

is satisfied whenever an expression e ∈ 2CExp evaluates to an answer a, given a control stack φ ∈ 2CStack.

We prove the equivalence between the stack machine and the standard machine by showing that the computations for each abstract machine (represented by derivations) are in bijective correspondence. To this end, we define a “controlstack substitution” over the state of the stack machine (i.e., expression under evaluation and current control stack) to obtain the state of the standard machine (i.e., expression under evaluation). We define control-stack substitution inductively over 2CPS expressions and continuations.

Definition 3 (Control-stack substitution for 2CPS programs). Given a stack φ of 2Cont continuations, the stack substitution of any e ∈ 2CExp (resp. c ∈ 2Cont), noted e{φ}_{2} (resp. c{φ}_{2}), yields a CExp expression (resp. a Cont continuation) and is defined as follows.

(t_{0} t_{1} c){φ}_{2} = [[t_{0}]]_{name}^{2CTriv} [[t_{1}]]_{name}^{2CTriv} (c{φ}_{2})
(c t){φ}_{2} = (c{φ}_{2}) [[t]]_{name}^{2CTriv}

(λv.e){φ}_{2} = λv.(e{φ}_{2})_{⋆{•}_{2} = k_{init}}_{⋆{φ, λv.e}_{2} = λv.(e{φ}_{2})}

Stack substitution is our key tool for mapping a state of the stack machine into a state of the standard machine. It yields CExp expressions and Cont continuations that have one free continuation identifier: k_{init}.

Lemma 2 (2Cont-validity of stack-substituted expressions and continuations).

1. For any e ∈ 2CExp and for any stack of 2Cont continuations φ, the judgment k_{init} ⊧_{2cc*}^{CExp} e{φ}_{2} is satisfied.

2. For any c ∈ 2Cont and for any stack of 2Cont continuations φ, the judgment k_{init} ⊧_{2cc*}^{Cont} c{φ}_{2} is satisfied.

Proof. By mutual induction on the structure of e and c. □

Lemma 3 (Control-stack substitution for 2CPS programs).

1. For any e′ ∈ CExp satisfying k ⊧_{2cc*}^{CExp} e′ for some k and for any stack of 2Cont continuations φ, [[e′]]_{strip}^{CExp}{φ}_{2} = e′[⋆{φ}_{2}/k].

2. For any e ∈ 2CExp, for any t′ ∈ CTriv satisfying ⊧_{2cc*}^{CTriv} t′, for any identifier i in Ide or in IdeV, and for any stack of 2Cont continuations φ, e[[[t′]]_{strip}^{CTriv}/i]{φ}_{2} = e{φ}_{2}[t′/i].

Theorem 1 (Simulation). The stack machine of Figure 8 and the standard machine are equivalent:

1. For any 2Cont-valid CPS program p, ⊢_{std}^{CProg} p ↪ a if and only if ⊢_{2cc}^{2CProg} [[p]]_{strip}^{CProg} ↪ [[a]]_{strip}^{Answer}.

2. For any CPS expression e satisfying k ⊧_{2cc*}^{CExp} e for some k and for any stack of 2Cont continuations φ, ⊢_{std}^{CExp} [[e]]_{strip}^{CExp}{φ}_{2} ↪ a if and only if φ ⊢_{2cc}^{2CExp} [[e]]_{strip}^{CExp} ↪ [[a]]_{strip}^{Answer}.

Proof. The theorem follows in each direction by an induction over the structure of the derivations, using Lemma 3. Let us show the case of tail calls in one direction.

Case E = \frac{E_{1} φ ⊢_{2cc}^{2CExp} e[t/x] ↪ [[a]]_{strip}^{Answer}}{φ ⊢_{2cc}^{2CExp} (λx.λ⋆.e) t ⋆ ↪ [[a]]_{strip}^{Answer}} ,

where E_{1} names the derivation ending in φ ⊢_{2cc}^{2CExp} e[t/x] ↪ [[a]]_{strip}^{Answer}.

By applying the induction hypothesis to E_{1}, we obtain a derivation

{E′_{1} \atop ⊢_{std}^{CExp} e[t/x]\{φ\}_{2} ↪ a}

Since e[t/x] is a 2CPS expression, there exists a CPS expression e′ satisfying k ⊧_{2cc*}^{CExp} e′ for some k and there exists a CPS trivial expression t′ satisfying ⊧_{2cc*}^{CTriv} t′ such that e = [[e′]]_{strip}^{CExp} and t = [[t′]]_{strip}^{CTriv}.

By Lemma 3,

[[e′]]_{strip}^{CExp}[[[t′]]_{strip}^{CExp}/x]{φ}_{2} = [[e′]]_{strip}^{CExp}{φ}_{2}[t′/x]
= e′[⋆{φ}_{2}/k][t′/x]
= e′[t′/x, ⋆{φ}_{2}/k]  – because t′ has no free k and φ has no free x.

By inference,

\frac{⊢_{std}^{CExp} e′[t′/x, ⋆\{φ\}_{2}/k] ↪ a}{⊢_{std}^{CExp} (λx.λk.e′) t′ (⋆\{φ\}_{2}) ↪ a}

Now by definition of stack substitution,

(λx.λk.e′) t′ (⋆{φ}_{2}) = [[(λx.λk.e) t k′]]_{strip}^{CExp}{φ}_{2},  – for some k′.

In other words, there exists a derivation

\frac{E′_{1} ⊢_{std}^{CExp} [[e[t/x]]]_{strip}^{CExp}\{φ\}_{2} ↪ a}{⊢_{std}^{CExp} [[(λx.λk.e) t k′]]_{strip}^{CExp}\{φ\}_{2} ↪ a}

which is what we wanted to show. □

3.3 Summary and conclusion As a stepping stone towards Section 4, we have formalized and proven two folklore theorems: (1) for CPS programs with second-class continuations, one identifier is enough; and (2) the bindings of continuation identifiers can be implemented with a stack for CPS programs with second-class continuations. To this end, we have considered a simplified abstract machine and taken the same conceptual steps as in our earlier joint work with Dzafic and Pfenning [6, 9, 11]. This earlier work is formalized in Elf, whereas the present work is not (yet). The rest of this article reports an independent foray. In the next section, we adapt the stack machine to CPS programs with first-class continuations, thereby formalizing an empirical implementation strategy for first-class continuations.

4 A stack machine for CPS programs with first-class continuations

First-class continuations occur because of call/cc. The call-by-value CPS transformation of call/cc reads as follows.

[[call/cc e]]_{cps}^{DExp}c = [[e]]_{cps}^{DExp}λf.f (λx.λk.c x) c – where f, x, and k are fresh.

On the right-hand-side of this definitional equation, c occurs twice: once as a regular, second-class continuation, and once more, in λx.λk.c x. In that term, k is declared but not used – c is used instead and denotes a first-class continuation.

Such CPS programs do not satisfy the judgments of Figures 5 and 6. And indeed, Danvy and Lawall observed that in a CPS program, first-class continuations can be detected through continuation identifiers occurring “out of turn”, so to speak [8].

Because it makes no assumptions on the binding discipline of continuation identifiers, the standard machine of Section 2, page 4, properly handles CPS programs with first-class continuations. First-class continuations, however, disqualify the stack machine of Section 3, page 7.

The goal of this section is to develop a stack machine for CPS programs with first-class continuations. To this end, we formalize what it means for a continuation identifier to occur in first-class position. We also prove that arbitrary β-reduction never promotes a continuation identifier occurring in second-class position into one occurring in first-class position. We then rephrase the BNF of CPS programs to single out continuation identifiers occurring in first-class position and their declaration. And similarly to Section 3, we tag with “⋆” all the declarations of continuation identifiers occurring in second-class position or not occurring at all, and all second-class positions of continuation identifiers (Section 4.1). We then present a stack machine for these 1CPS programs that copies the stack when first-class continuation abstractions are invoked. We prove it equivalent to the standard machine of Figure 4 (Section 4.2).

4.1 One continuation identifier is not enough

Following Danvy and Lawall [8], we now say that a continuation identifier occurs in first-class position whenever it occurs elsewhere than in second-class position, which is syntactically easy to detect. We formalize first-class occurrences with the judgment displayed in Figure 9.

\frac{k ∈ FC(t_{0})}{k ⊧1cc^{CExp} t_{0} t_{1} c}  \frac{k ∈ FC(t_{1})}{k ⊧1cc^{CExp} t_{0} t_{1} c}  \frac{k ⊧1cc^{Cont} c}{k ⊧1cc^{CExp} t_{0} t_{1} c}

\frac{k ⊧1cc^{Cont} c}{k ⊧1cc^{CExp} c t}  \frac{k ∈ FC(t)}{k ⊧1cc^{CExp} c t}

\frac{k ⊧1cc^{CExp} e}{k ⊧1cc^{Cont} λv.e}

Fig. 9. Characterization of a first-class continuation abstraction λk.e

Definition 4 (First-class position, first-class continuations). In a continuation abstraction λk.e, we say that k occurs in first-class position and denotes a first-class continuation whenever the judgment k ⊧_{1cc}^{CExp} e is satisfied.

N.B. For any continuation abstraction λk.e, at most one of k ⊧_{1cc}^{CExp} e and k ⊧_{2cc}^{CExp} e is satisfied.

In Section 3, we stated that 2Cont-validity is closed under β-reduction. Similarly here, β-reduction may demote a first-class continuation identifier into a second-class one, but it can never promote a second-class continuation identifier into a first-class one. The corresponding formal statement and its proof are straightforward and omitted here: we rely on them in the proof of Theorem 2.

For example, in

λk.(λx.λk′.k x) ℓ k

k occurs in first-class position. However, β-reducing this term yields

λk.k ℓ

where k occurs in second-class position.

In Section 3, we capitalized on the fact that each second-class position was uniquely determined. Here, we still capitalize on this fact by only singling out continuation identifiers in first-class position.^{2}

Introduction: For all continuation abstractions λk.e satisfying k ⊧_{1cc}^{CExp} e, we tag the declaration of k with λ^{1} and we keep the name k. Otherwise, we replace it with ⋆.

Elimination: When a continuation identifier occurs, if it is the latest one declared, we replace it with ⋆; otherwise, we keep its name.

The resulting BNF for 1CPS programs is displayed in Figure 10. The back and forth translation functions are displayed in Figures 11 and 12. They generalize their counterpart in Section 3.

Lemma 4 (Inverseness of stripping and naming). ∀p ∈ CProg, [[[[p]]_{strip}^{CProg}]]_{name}^{1CProg} ≡_{α} p and ∀p′ ∈ 1CProg, [[[[p′]]_{name}^{1CProg}]]_{strip}^{CProg} = p′.

4.2 A stack machine for CPS programs with first-class continuations We handle first-class continuations by extending the formalization of Section 3 with a new syntactic form:

c ∈ 1Cont — continuations c ::= λv.e | ⋆ | k | swap φ

The new form swap φ makes it possible to represent a copy of the control stack φ. It requires us to extend control-stack substitution as follows.

Definition 5 (Control-stack substitution for 1CPS programs). Given a stack φ of 1Cont continuations, The stack substitution of any e ∈ 1CExp (resp. c ∈ 1Cont), noted e{φ}_{1} (resp. c{φ}_{1}), yields a CExp expression (resp. a Cont continuation) and is defined as follows.

(t_{0} t_{1} c){φ}_{1} = ([[t_{0}]]_{name}^{1CTriv} [[t_{1}]]_{name}^{1CTriv}) (c{φ}_{1})
(c t){φ}_{1} = (c{φ}_{1}) [[t]]_{name}^{1CTriv}

(λv.e){φ}_{1} = λv.(e{φ}_{1})
⋆{•}_{1} = k_{init}
⋆{φ, λv.e}_{1} = λv.(e{φ}_{1})
k{φ}_{1} = k
(swap φ′){φ}_{1} = ⋆{φ′}_{1}

2 Andrzej Filinski suggested this concise notation (personal communication, Aarhus, Denmark, summer 1999). p ∈ 1CProg — 1CPS programs p ::= λ⋆.e | λ^{1}k.e e ∈ 1CExp — 1CPS (serious) expressions e ::= t_{0} t_{1} c | c t t ∈ 1CTriv — 1CPS trivial expressions t ::= ℓ | x | v | λx.λ⋆.e | λx.λ^{1}k.e c ∈ 1Cont — continuations c ::= λv.e | ⋆ | k ℓ ∈ Lit — literals x ∈ Ide — source identifiers k ∈ IdeC — fresh continuation identifiers ⋆ ∈ Token — single continuation identifier v ∈ IdeV — fresh parameters of continuations a ∈ 1Answer — 1CPS answers a ::= ℓ | λx.λ⋆.e | λx.λ^{1}k.e | error

Fig. 10. BNF of 1CPS programs

[[λk.e]]_{strip}^{CProg} = \begin{cases}λ^{1}k.[[e]]_{strip}^{CExp}k & if k ⊧1cc^{CExp} e \\ λ⋆.[[e]]_{strip}^{CExp}k & otherwise \end{cases}

[[t_{0} t_{1} c]]_{strip}^{CExp}k = [[t_{0}]]_{strip}^{CTriv} [[t_{1}]]_{strip}^{CTriv} ([[c]]_{strip}^{Cont}k)
[[c t]]_{strip}^{CExp}k = ([[c]]_{strip}^{Cont}k) [[t]]_{strip}^{CTriv}

[[ℓ]]_{strip}^{CTriv} = ℓ
[[x]]_{strip}^{CTriv} = x
[[v]]_{strip}^{CTriv} = v
[[λx.λk.e]]_{strip}^{CTriv} = \begin{cases}λx.λ^{1}k.[[e]]_{strip}^{CExp}k & if k ⊧1cc^{CExp} e \\ λx.λ⋆.[[e]]_{strip}^{CExp}k & otherwise \end{cases}
[[λv.e]]_{strip}^{Cont}k = λv.[[e]]_{strip}^{CExp}k
[[k′]]_{strip}^{Cont}k = \begin{cases}⋆ & if k = k′ \\ k′ & otherwise \end{cases}

Fig. 11. Translation from CPS to 1CPS – stripping continuation identifiers

[[λ⋆.e]]_{name}^{1CProg} = λk.[[e]]_{name}^{1CExp}k  – where k is fresh
[[λ^{1}k.e]]_{name}^{1CProg} = λk.[[e]]_{name}^{1CExp}k
[[t_{0} t_{1} c]]_{name}^{1CExp}k = [[t_{0}]]_{name}^{1CTriv} [[t_{1}]]_{name}^{1CTriv} ([[c]]_{name}^{1Cont}k)
[[c t]]_{name}^{1CExp}k = ([[c]]_{name}^{1Cont}k) [[t]]_{name}^{1CTriv}

[[ℓ]]_{name}^{1CTriv} = ℓ
[[x]]_{name}^{1CTriv} = x
[[v]]_{name}^{1CTriv} = v
[[λx.λ⋆.e]]_{name}^{1CTriv} = λx.λk.[[e]]_{name}^{1CExp}k  – where k is fresh
[[λ^{1}x.λk.e]]_{name}^{1CTriv} = λx.λk.[[e]]_{name}^{1CExp}k
[[λv.e]]_{name}^{1Cont}k = λv.[[e]]_{name}^{1CExp}k
[[⋆]]_{name}^{1Cont}k = k
[[k′]]_{name}^{1Cont}k = k′
[[ℓ]]_{name}^{1Answer} = ℓ
[[λx.λ⋆.e]]_{name}^{1Answer} = λx.λk.[[e]]_{name}^{1CExp}k  – where k is fresh
[[λ^{1}x.λk.e]]_{name}^{1Answer} = λx.λk.[[e]]_{name}^{1CExp}k
[[error]]_{name}^{1Answer} = error

Fig. 12. Translation from 1CPS to CPS – naming continuation identifiers

\frac{• ⊢1cc^{1CExp} e ↪ a}{⊢1cc^{1CProg} λ⋆.e ↪ a}  \frac{• ⊢1cc^{1CExp} e[swap •/k] ↪ a}{⊢1cc^{1CProg} λ^{1}k.e ↪ a}

φ ⊢1cc^{1CExp} ℓ t c ↪ error
\frac{φ ⊢1cc^{1CExp} e[t/x] ↪ a}{φ ⊢1cc^{1CExp} (λx.λ⋆.e) t ⋆ ↪ a}  \frac{φ, λv.e′ ⊢1cc^{1CExp} e[t/x] ↪ a}{φ ⊢1cc^{1CExp} (λx.λ⋆.e) t λv.e′ ↪ a}

\frac{φ ⊢1cc^{1CExp} e[t/x, swap φ/k] ↪ a}{φ ⊢1cc^{1CExp} (λx.λ^{1}k.e) t ⋆ ↪ a}  \frac{φ, λv.e′ ⊢1cc^{1CExp} e[t/x, swap (φ, λv.e′)/k] ↪ a}{φ ⊢1cc^{1CExp} (λx.λ^{1}k.e) t λv.e′ ↪ a}

\frac{φ′ ⊢1cc^{1CExp} e[t/x] ↪ a}{φ ⊢1cc^{1CExp} (λx.λ⋆.e) t (swap φ′) ↪ a}  \frac{φ′ ⊢1cc^{1CExp} e[t/x, swap φ′/k] ↪ a}{φ ⊢1cc^{1CExp} (λx.λ^{1}k.e) t (swap φ′) ↪ a}

\frac{φ ⊢1cc^{1CExp} e[t/v] ↪ a}{φ ⊢1cc^{1CExp} (λv.e) t ↪ a}  \overline{• ⊢1cc^{1CExp} ⋆ t ↪ t}  \frac{φ ⊢1cc^{1CExp} e[t/v] ↪ a}{φ, λv.e ⊢1cc^{1CExp} ⋆ t ↪ a}

φ ⊢1cc^{1CExp} swap • t ↪ t

\frac{φ′ ⊢1cc^{1CExp} e[t/v] ↪ a}{φ ⊢1cc^{1CExp} swap (φ′, λv.e) t ↪ a}

Fig. 13. Stack machine for 1CPS programs

Figure 13 displays a stack-based abstract machine for 1CPS programs. This machine is a version of the stack machine of Section 3 where the substitution for continuation identifiers occurring in second-class position or not occurring at all is implemented with a global control stack (as in Figure 8), and where the substitution for continuation identifiers occurring in first-class position is implemented by copying the stack into a swap form (which is new).

Calls: When a function declaring a second-class continuation is applied, its continuation is pushed on φ. When a function declaring a first-class continuation is applied, its continuation is also pushed on φ and the resulting new stack is copied into a swap form.

Returns: When a continuation is needed, it is popped from φ. If φ is empty, the intermediate result sent to the continuation is the final answer. When a swap form is encountered, its copy of φ is restored.

More formally, the judgment

⊢_{1cc}^{1CProg} p ↪ a

is satisfied whenever a CPS program p ∈ 1CProg evaluates to an answer a ∈ 1Answer. The auxiliary judgment

φ ⊢_{1cc}^{1CExp} e ↪ a

is satisfied whenever an expression e ∈ 1CExp evaluates to an answer a, given a control stack φ ∈ 1CStack. The machine starts and stops with an empty control stack.

We prove the equivalence between the stack machine and the standard machine as in Section 3.2.

Theorem 2 (Simulation). The stack machine of Figure 13 and the standard machine are equivalent:

1. ⊢_{std}^{CProg} p ↪ a if and only if ⊢_{1cc}^{1CProg} [[p]]_{strip}^{CProg} ↪ [[a]]_{strip}^{Answer}.

2. ⊢_{std}^{CExp} [[e]]_{strip}^{CExp}k{φ}_{1} ↪ a if and only if φ ⊢_{1cc}^{1CExp} [[e]]_{strip}^{CExp}k ↪ [[a]]_{strip}^{Answer}, for some k.

Proof. Similar to the proof of Theorem 1. □

4.3 Summary and conclusion

We have formalized and proven correct a stack machine for CPS programs with first-class continuations. This machine is idealized in that, e.g., it has no provision for stack overflow. Nevertheless, it embodies the most classical implementation strategy for first-class continuations: the stack is copied at call/cc time, i.e., in the CPS world, when a first-class continuation identifier is declared; and conversely, the stack is restored at throw time, i.e., in the CPS world, when a first-class continuation identifier is invoked. This design keeps second-class continuations costless – in fact it is a zero-overhead strategy in the sense of Clinger, Hartheimer, and Ost [4, Section 3.1]: only programs using first-class continuations pay for them.

Furthermore, and as in Section 3, our representation of φ embodies its LIFO nature without committing to an actual representation. This representation can be retentive (in which case φ is implemented as a pointer into the heap) or destructive (in which case φ is implemented as, e.g., a rewriteable array) [3]. In both cases, swap φ is implemented as copying φ. Copying the pointer yields captured continuations to be shared and copying the array yields multiple representations of captured continuations.

5 A segmented stack machine for first-class continuations

Coroutines and threads are easily simulated using call/cc, but these simulations are allergic to representing control as a rewriteable array. Indeed for every switch this array is copied in the heap, yielding multiple copies to coexist without sharing, even though these copies are mostly identical.

Against this backdrop, implementations such as PC Scheme [2] segment the stack, using the top segment as a stack cache: if this cache overflows, it is flushed to the heap and the computation starts afresh with an empty cache; and if it underflows, the last flushed cache is restored. Flushed caches are linked LIFO in the heap.^{3} A segmented stack accomodates call/cc and throw very simply: at call/cc time, the cache is flushed to the heap and a pointer to it is retained; and

3 If the size of the stack cache is one, the segmented implementation coincides with a heap implementation.

at throw time, the flushed cache that is pointed to is restored. As for the bulk of the continuations, it is not copied but shared between captured continuations.

It is simple to expand the stack machine of Section 4 into a segmented stack machine. One simply needs to define the judgment

Φ; φ ⊢_{1cc′}^{CExp} e ↪ a

where φ, e, and a are in Section 4 and Φ denotes a LIFO list of φ’s. (One also needs an overflow predicate for φ.)

Thus equipped, it is also simple to expand the stack substitution of Section 4, and to state and prove a simulation theorem similar to Theorem 2, thereby formalizing what Clinger, Hartheimer, and Ost name the “chunked-stack strategy” [4]. Another moderate effort makes it possible to formalize the author’s incremental garbage collection of unshared continuations by one-bit reference counting [5]. One is also in position to formalize “one-shot continuations” [14].

Acknowledgments: I am grateful to Belmina Dzafic and Frank Pfenning for our joint work, which forms the foundation of the present foray. Throughout, and as always, Andrzej Filinski has been a precious source of sensible comments and suggestions. This article has also benefited from the interest and comments of Lars R. Clausen, Daniel Damian, Bernd Grobauer, Niels O. Jensen, Julia L. Lawall, Lasse R. Nielsen, Morten Rhiger, and Zhe Yang. I am also grateful for the opportunity to have presented this work at Marktoberdorf, at the University of Tokyo, and at KAIST in the summer and in the fall of 1999. Finally, thanks are due to the anonymous referees for stressing the issue of retention vs. deletion.

References

1. Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In Third International Symposium on Programming Language Implementation and Logic Programming, number 528 in Lecture Notes in Computer Science, pages 1– 13, Passau, Germany, August 1991.

2. David B. Bartley and John C. Jensen. The implementation of PC Scheme. In Proceedings of the 1986 ACM Conference on Lisp and Functional Programming, pages 86–93, Cambridge, Massachusetts, August 1986.

3. Daniel M. Berry. Block structure: Retention or deletion? (extended abstract). In Conference Record of the Third Annual ACM Symposium on Theory of Computing, pages 86–100, Shaker Heights, Ohio, May 1971.

4. William Clinger, Anne H. Hartheimer, and Eric M. Ost. Implementation strategies for first-class continuations. Higher-Order and Symbolic Computation, 12(1):7–45, 1999.

5. Olivier Danvy. Memory allocation and higher-order functions. In Proceedings of the ACM SIGPLAN’87 Symposium on Interpreters and Interpretive Techniques, SIGPLAN Notices, Vol. 22, No 7, pages 241–252, Saint-Paul, Minnesota, June 1987.

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

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

8. Olivier Danvy and Julia L. Lawall. Back to direct style II: First-class continuations. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. V, No. 1, pages 299–310, San Francisco, California, June 1992.

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

10. Bruce F. Duba, Robert Harper, and David B. MacQueen. Typing first-class continuations in ML. In Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 163–173, Orlando, Florida, January 1991.

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

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

13. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN’93 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 28, No 6, pages 237–247, Albuquerque, New Mexico, June 1993.

14. Christopher T. Haynes and Daniel P. Friedman. Embedding continuations in procedural objects. ACM Transactions on Programming Languages and Systems, 9(4):582–598, 1987.

15. Robert Hieb, R. Kent Dybvig, and Carl Bruggeman. Representing control in the presence of first-class continuations. In Proceedings of the ACM SIGPLAN’90 Conference on Programming Languages Design and Implementation, SIGPLAN Notices, Vol. 25, No 6, pages 66–77, White Plains, New York, June 1990.

16. Richard A. Kelsey and Jonathan A. Rees. A tractable Scheme implementation. Lisp and Symbolic Computation, 7(4):315–336, 1994.

17. David Kranz, Richard Kesley, Jonathan Rees, Paul Hudak, Jonathan Philbin, and Norman Adams. Orbit: An optimizing compiler for Scheme. In Proceedings of the 1986 Symposium on Compiler Construction, SIGPLAN Notices, Vol. 21, No 7, pages 219–233, Palo Alto, California, June 1986.

18. Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, 6:308–320, 1964.

19. Drew McDermott. An efficient environment allocation scheme in an interpreter for a lexically-scoped Lisp. In Conference Record of the 1980 LISP Conference, pages 154–162, Stanford, California, August 1980.

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

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

22. Christopher Strachey and Christopher P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Higher-Order and Symbolic Computation, 13(1/2), 2000. Reprint of the technical monograph PRG-11, Oxford University Computing Laboratory (1974).

Recent BRICS Report Series Publications

RS-99-51 Olivier Danvy. Formalizing Implementation Strategies for First-Class Continuations. December 1999. 16 pp. Appears in Smolka, editor, Programming Languages and Systems: Ninth European Symposium on Programming, ESOP ’00 Proceedings, LNCS 1782, 2000pp. 88–103.

RS-99-50 Gerth Stølting Brodal and Srinivasan Venkatesh. Improved Bounds for Dictionary Look-up with One Error. December 1999. 5 pp. Appears in Information Processing Letters 75(1– 2):57–59, 2000.

RS-99-49 Alexander A. Ageev and Maxim I. Sviridenko. An Approximation Algorithm for Hypergraph Max k-Cut with Given Sizes of Parts. December 1999. 12 pp. Appears in Paterson, editor, Eighteenth Annual European Symposiumon on Algorithms, ESA ’00 Proceedings, LNCS 1879, 2000, pages 32–49.

RS-99-48 Rasmus Pagh. Faster Deterministic Dictionaries. December 1999. 14 pp. Appears in Shmoys, editor, The Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’00 Proceedings, 2000, pages 487–493. Journal version in Journal of Algorithms, 41(1):69–85, 2001, with the title Deterministic Dictionaries.

RS-99-47 Peter Bro Miltersen and Vinodchandran N. Variyam. Derandomizing Arthur-Merlin Games using Hitting Sets. December 1999. 21 pp. Appears in Beame, editor, 40th Annual Symposium on Foundations of Computer Science, FOCS ’99 Proceedings, 1999, pages 71–80.

RS-99-46 Peter Bro Miltersen, Vinodchandran N. Variyam, and Osamu Watanabe. Super-Polynomial Versus Half-Exponential Circuit Size in the Exponential Hierarchy. December 1999. 14 pp. Appears in Asano, Imai, Lee, Nakano and Tokuyama, editors, Computing and Combinatorics: 5th Annual International Conference, COCOON ’99 Proceedings, LNCS 1627, 1999, pages 210–220.

RS-99-45 Torben Amtoft. Partial Evaluation for Constraint-Based Program Analyses. December 1999. 13 pp.