BRICS

Basic Research in Computer Science

A Simple Proof of a Folklore Theorem about Delimited Control

Dariusz Biernacki Olivier Danvy BRICS Report Series RS-05-25 ISSN 0909-0878 August 2005 BRICS RS-05-25 Biernacki & Danvy: A Simple Proof of a Folklore Theorem about Delimited Control Copyright \begin{matrix}c \\ ◯ \end{matrix} 2005, Dariusz Biernacki & 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/05/25/

A Simple Proof of a Folklore Theorem about Delimited Control ^{∗}

Dariusz Biernacki and Olivier Danvy BRICS^{†} Department of Computer Science University of Aarhus^{‡}

August 2, 2005

Abstract

We formalize and prove the folklore theorem that the static delimited-control operators shift and reset can be simulated in terms of the dynamic delimitedcontrol operators control and prompt. The proof is based on small-step operational semantics.

Keywords Delimited continuations, abstract machines.

∗To appear in the Journal of Functional Programming as a Theoretical Pearl.

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

‡ IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark.

Email: {dabi,danvy}@brics.dk

Contents

1 Introduction 1

2 The formalization 1 2.1 A definitional abstract machine for shift and reset . . . . . . . . . . 1 2.2 A definitional abstract machine for control and prompt . . . . . . . . . 3 2.3 Static vs. dynamic delimited continuations . . . . . . . . . . . . . . . . 3

3 The folklore theorem and its formal proof 6 3.1 An auxiliary abstract machine for control and prompt . . . . . . . . . 6 3.2 A family of relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.3 The formal proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

4 Conclusion 10

List of Figures

1 A definitional abstract machine for shift and reset . . . . . . . . . . 2 2 A definitional abstract machine for control and prompt . . . . . . . . . 4

1 Introduction

In the recent upsurge of interest in delimited continuations [1, 5, 9, 12, 15] it appears to be taken for granted that dynamic delimited continuations can simulate static delimited continuations by delimiting the context of their resumption. And indeed this property has been mentioned early in the literature about delimited continuations [4, Section 5]. We are, however, not aware of any proof of this folklore theorem, and our goal here is to provide such a proof. To this end, we present two abstract machines—one for static delimited continuations as provided by the control operators shift and reset [4] and inducing a partial evaluation function eval_{sr}, and one for dynamic delimited continuations as provided by the control operators control and prompt [8] and inducing a partial evaluation function eval_{cp}—and one compositional mapping [[·]] from programs using shift and reset to programs using control and prompt. We then prove that the following diagram commutes:

[figure: _{Exp_{sr}}; ^{eval^{sr}}; [[·]]; _{Val_{sr}}; ≃_{v}; _{Exp_{cp}}; _{eval_{cp}}; _{Val_{cp}}]

where the value equivalence ≃_{v}, for ground values, is defined as equality.

2 The formalization

Figures 1 and 2 display two abstract machines, one for the λ-calculus extended with shift and reset, and one for the λ-calculus extended with control and prompt. These two machines only differ in the application of captured contexts (which represent delimited continuations in the course of executing source programs).

For simplicity, in the source syntax, we distinguish between λ-bound variables (x) and shift- or control-bound variables (k). We use the same meta-variables (e, n, i, x, k, v, ρ, C_{1} and C_{2}) ranging over the components of the two abstract machines whenever it does not lead to ambiguity. Programs are closed terms.

2.1 A definitional abstract machine for shift and reset

In our earlier work [2], we derived a definitional abstract machine for shift and reset by defunctionalizing the continuation and meta-continuation of Danvy and Filinski’s definitional evaluator [4]. This definitional abstract machine is displayed in Figure 1; it is a straightforward extension of Felleisen et al.’s CEK machine [7] with a meta-context. The source language is the untyped λ-calculus extended with integers, the successor function, shift (noted S), and reset (noted ⟨⟨⟨·⟩⟩⟩). The machine is an extension of the CEK machine because when given a program that does not use shift and reset, it operates in lock step with the CEK machine. When delimiting • Terms and identifiers: e ::= ⌜n⌝ | i | λx.e | e_{0} e_{1} | succ e | ⟨⟨⟨e⟩⟩⟩ | Sk.e i ::= x | k

• Values (integers, closures, and captured contexts): v ::= n | [x, e, ρ] | C_{1} • Environments: ρ ::= ρ_{mt} | ρ{i ↦ v}

• Contexts: C_{1} ::= END | ARG ((e, ρ), C_{1}) | FUN (v, C_{1}) | SUCC (C_{1})

• Meta-contexts: C_{2} ::= nil | C_{1} :: C_{2}

• Initial transition, transition rules, and final transition:

e

⇒_{sr}

⟨e, ρ_{mt}, END, nil⟩_{eval}
⟨⌜n⌝, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{sr} ⟨C_{1}, n, C_{2}⟩_{cont_{1}}
⟨i, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{sr} ⟨C_{1}, ρ(i), C_{2}⟩_{cont_{1}}
⟨λx.e, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{sr} ⟨C_{1}, [x, e, ρ], C_{2}⟩_{cont_{1}}
⟨e_{0} e_{1}, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{sr} ⟨e_{0}, ρ, ARG ((e_{1}, ρ), C_{1}), C_{2}⟩_{eval}

⟨succ e, ρ, C_{1}, C_{2}⟩^{eval} ⇒_{sr} ⟨e, ρ, SUCC (C_{1}), C_{2}⟩_{eval}

⟨⟨⟨⟨e⟩⟩⟩, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{sr} ⟨e, ρ, END, C_{1} :: C_{2}⟩_{eval}

⟨Sk.e, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{sr} ⟨e, ρ{k ↦ C_{1}}, END, C_{2}⟩_{eval}

⟨END, v, C_{2}⟩_{cont_{1}} ⇒_{sr} ⟨C_{2}, v⟩_{cont_{2}}
⟨ARG ((e, ρ), C_{1}), v, C_{2}⟩_{cont_{1}} ⇒_{sr} ⟨e, ρ, FUN (v, C_{1}), C_{2}⟩_{eval}

⟨FUN ([x, e, ρ], C_{1}), v, C_{2}⟩^{cont_{1}} ⇒_{sr} ⟨e, ρ{x ↦ v}, C_{1}, C_{2}⟩_{eval}

⟨FUN (C′_{1}, C_{1}), v, C_{2}⟩_{cont_{1}} ⇒_{sr} ⟨C′_{1}, v, C_{1} :: C_{2}⟩_{cont_{1}}

⟨SUCC (C_{1}), n, C_{2}⟩^{cont_{1}} ⇒_{sr} ⟨C_{1}, n + 1, C_{2}⟩_{cont_{1}}

⟨C_{1} :: C_{2}, v⟩_{cont_{2}} ⇒_{sr} ⟨C_{1}, v, C_{2}⟩_{cont_{1}}
⟨nil, v⟩_{cont_{2}} ⇒_{sr} v

Figure 1: A definitional abstract machine for shift and reset

control with reset, the machine pushes the current context on the current metacontext, and proceeds with an empty context. When abstracting control with shift, the machine captures the current context and proceeds with an empty context. When applying a captured context, the machine pushes the current context on the current meta-context, and proceeds with the captured context. Definition 1. The partial evaluation function eval_{sr} mapping programs to values is defined as follows: eval_{sr} (e) = v if and only if ⟨e, ρ_{mt}, END, nil⟩_{eval} ⇒_{sr}^{+} ⟨nil, v⟩_{cont_{2}} .

We could define the function eval_{sr} in terms of the initial and final transition, but they play only an administrative role, i.e., to load an input term to the machine and to unload the computed value from the machine.

2.2 A definitional abstract machine for control and prompt

In our earlier work [2], we also showed how to modify the abstract machine for shift and reset to obtain a definitional abstract machine for control and prompt [6, 8]. This abstract machine is displayed in Figure 2. The source language is the λ-calculus extended with integers, the successor function, control (noted F) and prompt (noted #). The machine is an extension of the CEK machine because when given a program that does not use control and prompt, it operates in lock step with the CEK machine. When delimiting control with prompt, the machine pushes the current context on the current meta-context, and proceeds with an empty context. When abstracting control with control, the machine captures the current context and proceeds with an empty context. When applying a captured context, the machine concatenates the captured context to the current context and proceeds with the resulting context.

Definition 2. The partial evaluation function eval_{cp} mapping programs to values is defined as follows: eval_{cp} (e) = v if and only if ⟨e, ρ_{mt}, END, nil⟩_{eval} ⇒_{cp}^{+} ⟨nil, v⟩_{cont_{2}} .

2.3 Static vs. dynamic delimited continuations

In Figure 1, shift and reset are said to be static because the application of a delimited continuation (represented as a captured context) does not depend on the current context. It is implemented by pushing the current context on the stack of contexts and installing the captured context as the new current context, as shown by the following transition:

⟨FUN (C′_{1}, C_{1}), v, C_{2}⟩_{cont_{1}} ⇒_{sr} ⟨C′_{1}, v, C_{1} :: C_{2}⟩_{cont_{1}}

A subsequent shift operation will therefore capture the remainder of the reinstated context, statically.

In Figure 2, control and prompt are said to be dynamic because the application of a delimited continuation (also represented as a captured context) depends on the current context. It is implemented by concatenating the captured context to the current context, as shown by the following transition:

⟨FUN (C′_{1}, C_{1}), v, C_{2}⟩_{cont_{1}} ⇒_{cp} ⟨C′_{1} ⋆ C_{1}, v, C_{2}⟩_{cont_{1}}

A subsequent control operation will therefore capture the remainder of the reinstated context together with the then-current context, dynamically.

The two abstract machines differ only in this single transition. Because of this single transition, programs using shift and reset are compatible with the traditional notion of continuation-passing style [2, 4, 14] whereas programs using control and prompt give rise to a more complex notion of continuation-passing style that threads a dynamic state [3, 5, 15]. This difference in the semantics of shift and control also induces distinct computational behaviors, as illustrated in the following example.

• Terms and identifiers: e ::= ⌜n⌝ | i | λx.e | e_{0} e_{1} | succ e | #e | Fk.e i ::= x | k

• Values (integers, closures, and captured contexts): v ::= n | [x, e, ρ] | C_{1} • Environments: ρ ::= ρ_{mt} | ρ{i ↦ v}

• Contexts: C_{1} ::= END | ARG ((e, ρ), C_{1}) | FUN (v, C_{1}) | SUCC (C_{1})

• Concatenation of contexts:

END ⋆ C′_{1} =^{def} C′_{1}
(ARG ((e, ρ), C_{1})) ⋆ C′_{1} =^{def} ARG ((e, ρ), C_{1} ⋆ C′_{1})
(FUN (v, C_{1})) ⋆ C′_{1} =^{def} FUN (v, C_{1} ⋆ C′_{1})
(SUCC (C_{1})) ⋆ C′_{1} =^{def} SUCC (C_{1} ⋆ C′_{1})

• Meta-contexts: C_{2} ::= nil | C_{1} :: C_{2}

• Initial transition, transition rules, and final transition:

e

⇒_{cp}

⟨e, ρ_{mt}, END, nil⟩_{eval}
⟨⌜n⌝, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{cp} ⟨C_{1}, n, C_{2}⟩_{cont_{1}}
⟨i, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{cp} ⟨C_{1}, ρ(i), C_{2}⟩_{cont_{1}}
⟨λx.e, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{cp} ⟨C_{1}, [x, e, ρ], C_{2}⟩_{cont_{1}}
⟨e_{0} e_{1}, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{cp} ⟨e_{0}, ρ, ARG ((e_{1}, ρ), C_{1}), C_{2}⟩_{eval}

⟨succ e, ρ, C_{1}, C_{2}⟩^{eval} ⇒_{cp} ⟨e, ρ, SUCC (C_{1}), C_{2}⟩_{eval}

⟨#e, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{cp} ⟨e, ρ, END, C_{1} :: C_{2}⟩_{eval}

⟨Fk.e, ρ, C_{1}, C_{2}⟩_{eval} ⇒_{cp} ⟨e, ρ{k ↦ C_{1}}, END, C_{2}⟩_{eval}

⟨END, v, C_{2}⟩_{cont_{1}} ⇒_{cp} ⟨C_{2}, v⟩_{cont_{2}}
⟨ARG ((e, ρ), C_{1}), v, C_{2}⟩_{cont_{1}} ⇒_{cp} ⟨e, ρ, FUN (v, C_{1}), C_{2}⟩_{eval}

⟨FUN ([x, e, ρ], C_{1}), v, C_{2}⟩^{cont_{1}} ⇒_{cp} ⟨e, ρ{x ↦ v}, C_{1}, C_{2}⟩_{eval}

⟨FUN (C′_{1}, C_{1}), v, C_{2}⟩_{cont_{1}} ⇒_{cp} ⟨C′_{1} ⋆ C_{1}, v, C_{2}⟩_{cont_{1}}

⟨SUCC (C_{1}), n, C_{2}⟩^{cont_{1}} ⇒_{cp} ⟨C_{1}, n + 1, C_{2}⟩_{cont_{1}}

⟨C_{1} :: C_{2}, v⟩_{cont_{2}} ⇒_{cp} ⟨C_{1}, v, C_{2}⟩_{cont_{1}}
⟨nil, v⟩_{cont_{2}} ⇒_{cp} v

Figure 2: A definitional abstract machine for control and prompt

Copying vs. reversing a list: Using call-with-current-delimited-continuation
(instead of shift or control) and delimit-continuation (instead of reset or prompt),

let us consider the following function that traverses a given list and returns another list [2, Sec. 4.5]; this function is written in the syntax of Scheme [11]:

     (define traverse
       (lambda (xs)
         (letrec ([visit
                   (lambda (xs)
                     (if (null? xs)
                         '()
                         (visit (call-with-current-delimited-continuation
                                  (lambda (k)
                                    (cons (car xs) (k (cdr xs))))))))])
           (delimit-continuation
             (lambda ()
               (visit xs))))))

• The function \underline{co}p\underline{ies} its input list if shift and reset are used instead of call-with-

     current-delimited-continuation and delimit-continuation. The reason why is

that reinstating a shift-abstracted context keeps it distinct from the current context. Here, shift successively abstracts a delimited context that solely consists of the call to visit. Intuitively, this delimited context reads as follows:

          (lambda (v)
            (delimit-continuation
              (lambda ()
                (visit v))))

• The function \underline{reverses} its input list if control and prompt are used instead

     of call-with-current-delimited-continuation and delimit-continuation. The

reason why is that reinstating a control-abstracted context grafts it to the current context. Here, control successively abstracts a context that consists of the call to visit followed by the construction of a reversed prefix of the input list. Intuitively, when the input list is (1 2 3), the successive contexts read as follows:

          (lambda (v) (visit v))
          (lambda (v) (cons 1 (visit v))
          (lambda (v) (cons 2 (cons 1 (visit v))))

Programming folklore. To obtain the effect of shift and reset using control and prompt, one should replace every occurrence of a shift-bound variable k by its ηexpanded and delimited version λx.#(k x). (As a β_{v}-optimization, every application of k to a trivial expression e (typically a value) can be replaced by #(k e).)

And indeed, replacing

     (cons (car xs) (k (cdr xs)))

by

     (cons (car xs) (delimit-continuation
                      (lambda ()
                        (k (cdr xs)))))

in the definition of traverse above makes it copy its input list, no matter whether

shift and reset or control and prompt are used.

We formalize the replacement above with the following compositional translation from the language with shift and reset to the language with control and prompt.

Definition 3. The translation [[·]] is defined as follows:

[[⌜n⌝]] = ⌜n⌝
[[x]] = x
[[k]] = λx.#(k x), where x is fresh
[[λx.e]] = λx.[[e]]
[[e_{0} e_{1}]] = [[e_{0}]] [[e_{1}]]
[[⟨⟨⟨e⟩⟩⟩]] = #[[e]]
[[Sk.e]] = Fk.[[e]]

In the next section, we prove that for any program e, eval_{sr} (e) and eval_{cp} ([[e]]) are equivalent (in the sense of Definition 5 below) and, in particular, equal for ground values.

3 The folklore theorem and its formal proof

We first define an auxiliary abstract machine for control and prompt that implements the application of an η-expanded and delimited continuation in one step. By construction, this auxiliary abstract machine is equivalent to the definitional one of Figure 2. We then show that the auxiliary machine operates in lock step with the definitional abstract machine of Figure 1. To this end, we define a family of relations between the abstract machine for shift and reset and the auxiliary abstract machine. The folklore theorem follows.

3.1 An auxiliary abstract machine for control and prompt

Definition 4. The auxiliary abstract machine for control and prompt is defined as follows:

(1) All the components, including configurations δ, of the auxiliary abstract machine are identical to the components of the definitional abstract machine of Figure 2.

(2) The transitions of the auxiliary abstract machine, denoted δ ⇒_{aux} δ′, are defined as follows:

• if δ = ⟨FUN ([x, #(k x), ρ], C_{1}), v, C_{2}⟩_{cont_{1}} then δ′ = ⟨C′_{1}, v, C_{1} :: C_{2}⟩_{cont_{1}} , where C′_{1} = ρ(k);

• otherwise, δ′ is the configuration such that δ ⇒_{cp} δ′, if it exists.

(3) The partial evaluation function eval_{aux} is defined in the usual way: eval_{aux} (e) = v if and only if ⟨e, ρ_{mt}, END, nil⟩_{eval} ⇒_{aux}^{+} ⟨nil, v⟩_{cont_{2}} .

The following lemma shows that the definitional abstract machine for control and prompt simulates the single step of the auxiliary abstract machine in several steps.

Lemma 1. For all v, C_{1}, C′_{1} and C_{2},

⟨FUN ([x, #(k x), ρ], C_{1}), v, C_{2}⟩_{cont_{1}} ⇒_{cp}^{+} ⟨C′_{1}, v, C_{1} :: C_{2}⟩_{cont_{1}} , where C′_{1} = ρ(k).

Proof. From the definition of the abstract machine for control and prompt in Figure 2:

⟨FUN ([x, #(k x), ρ], C_{1}), v, C_{2}⟩_{cont_{1}} ⇒_{cp}
⟨#(k x), ρ{x ↦ v}, C_{1}, C_{2}⟩_{eval} ⇒_{cp}
⟨k x, ρ{x ↦ v}, END, C_{1} :: C_{2}⟩_{eval} ⇒_{cp}
⟨k, ρ{x ↦ v}, ARG ((x, ρ{x ↦ v}), END), C_{1} :: C_{2}⟩_{eval} ⇒_{cp}
⟨ARG ((x, ρ{x ↦ v}), END), C′_{1}, C_{1} :: C_{2}⟩_{cont_{1}} ⇒_{cp}
⟨x, ρ{x ↦ v}, FUN (C′_{1}, END), C_{1} :: C_{2}⟩_{eval} ⇒_{cp}
⟨FUN (C′_{1}, END), v, C_{1} :: C_{2}⟩_{cont_{1}} ⇒_{cp}
⟨C′_{1}, v, C_{1} :: C_{2}⟩_{cont_{1}}

Proposition 1. For any program e and for any value v, eval_{cp} (e) = v if and only if eval_{aux} (e) = v.

Proof. Follows directly from Definition 4 and Lemma 1.

3.2 A family of relations

We now define a family of relations between the abstract machine for shift and reset and the auxiliary abstract machine for control and prompt. To distinguish between the two machines, as a diacritical convention [13], we annotate the components of the machine for shift and reset with a hat.

Definition 5. The relations between the components of the abstract machine for shift and reset and the auxiliary abstract machine for control and prompt are defined as follows:

(1) Terms: ê ≃_{e} e iff [[ê]] = e

(2) Values:

(a) n̂ ≃_{v} n iff n̂ = n

(b) [x̂, ê, ρ̂] ≃_{v} [x, e, ρ] iff x̂ = x, ê ≃_{e} e and ρ̂ ≃_{env} ρ

(c) Ĉ_{1} ≃_{v} [x, #(k x), ρ] iff Ĉ_{1} ≃_{c} ρ(k)

(3) Environments:

(a) ρ̂_{mt} ≃_{env} ρ_{mt}

(b) ρ̂{x ↦ v̂} ≃_{env} ρ{x ↦ v} iff v̂ ≃_{v} v and ρ̂\ {x} ≃_{env} ρ \ {x}, where ρ\{i} denotes the restriction of ρ to its domain excluding i

(c) ρ̂{k ↦ Ĉ_{1}} ≃_{env} ρ{k ↦ C_{1}} iff Ĉ_{1} ≃_{c} C_{1} and ρ̂\ {k} ≃_{env} ρ \ {k} (4) Contexts:

(a) ÊND ≃_{c} END

(b) ÂRG ((ê, ρ̂), Ĉ_{1}) ≃_{c} ARG ((e, ρ), C_{1}) iff ê ≃_{e} e, ρ̂ ≃_{env} ρ, and Ĉ_{1} ≃_{c} C_{1}

(c) F̂UN (v̂, Ĉ_{1}) ≃_{c} FUN (v, C_{1}) iff v̂ ≃_{v} v and Ĉ_{1} ≃_{c} C_{1}

(d) { \atop SUCC} (Ĉ_{1}) ≃_{c} SUCC (C_{1}) iff Ĉ_{1} ≃_{c} C_{1}

(5) Meta-contexts:

(a) n̂il ≃_{mc} nil

(b) Ĉ_{1} :: Ĉ_{2} ≃_{mc} C_{1} :: C_{2} iff Ĉ_{1} ≃_{c} C_{1} and Ĉ_{2} ≃_{mc} C_{2}

(6) Configurations:

(a) ⟨ê, ρ̂, Ĉ_{1}, Ĉ_{2}⟩êval ≃ ⟨e, ρ, C_{1}, C_{2}⟩_{eval} iff

ê ≃_{e} e, ρ̂ ≃_{env} ρ, Ĉ_{1} ≃_{c} C_{1}, and Ĉ_{2} ≃_{mc} C_{2}

(b) ⟨Ĉ_{1}, v̂, Ĉ_{2}⟩{ \atop cont_{1}} ≃ ⟨C_{1}, v, C_{2}⟩_{cont_{1}} iff

Ĉ_{1} ≃_{c} C_{1}, v̂ ≃_{v} v, and Ĉ_{2} ≃_{mc} C_{2}

(c) ⟨Ĉ_{2}, v̂⟩{ \atop cont_{2}} ≃ ⟨C_{2}, v⟩_{cont_{2}} iff

Ĉ_{2} ≃_{mc} C_{2} and v̂ ≃_{v} v

The relations are intended to capture the equivalence of the abstract machine for shift and reset and the auxiliary abstract machine for control and prompt when run on a term ê and on its translation [[ê]], respectively. Most of the cases are homomorphic on the structure of a component. The critical cases are: (1)—a formalization of the programming folklore formulated in Section 2.3, and (2)(c)—a formalization of the fact that a control-abstracted continuation is applied by concatenating its representation to the current context whereas when a shift-abstracted continuation is applied, its representation is kept separate from the current context.

3.3 The formal proof

We first show that indeed, running the abstract machine for shift and reset on a program ê and running the auxiliary abstract machine for control and prompt on a program [[ê]] yield results that are equivalent in the sense of the above relations. Then by Proposition 1, we obtain the equivalence result of the abstract machine for shift and reset and the definitional abstract machine for control and prompt, as summarized in the following diagram:

[figure: _{Exp_{sr}}; ^{eval^{sr}}; [[·]]; _{Val_{sr}}; ≃_{v}; _{Exp_{cp}}; _{eval_{cp}}; eval_{aux}; _{Val_{cp}}]

More precisely, we show that the abstract machine for shift and reset and the auxiliary abstract machine for control and prompt operate in lock-step with respect to the relations. To this end we need to prove the following lemmas.

Lemma 2. For all configurations δ̂, δ, δ̂′ and δ′, if δ̂ ≃ δ then

δ̂ ⇒_{sr} δ̂′ if and only if δ ⇒_{aux} δ′ and δ̂′ ≃ δ′.

Proof. By case inspection of δ̂ ≃ δ. All cases follow directly from the definition of the relation ≃ and the definitions of the abstract machines. We present two crucial cases:

Case: δ̂ = ⟨k, ρ̂, Ĉ_{1}, Ĉ_{2}⟩êval and δ = ⟨λx.#(k x), ρ, C_{1}, C_{2}⟩_{eval}.

From the definition of the abstract machine for shift and reset, δ̂ ⇒_{sr} δ̂′, where δ̂′ = ⟨Ĉ_{1}, ρ̂(k), Ĉ_{2}⟩{ \atop cont_{1}}. From the definition of the auxiliary abstract machine for control and prompt, δ ⇒_{aux} δ′, where δ′ = ⟨C_{1}, [x, #(k x), ρ], C_{2}⟩_{cont_{1}} . By assumption, ρ̂(k) ≃_{c} ρ(k), Ĉ_{1} ≃_{c} C_{1} and Ĉ_{2} ≃_{mc} C_{2}. Hence, δ̂′ ≃ δ′.

Case: δ̂ = ⟨F̂UN (Ĉ_{1}′, Ĉ_{1}), v̂, Ĉ_{2}⟩êval and δ = ⟨FUN ([x, #(k x), ρ], C_{1}), v, C_{2}⟩_{eval}. From the definition of the abstract machine for shift and reset, δ̂ ⇒_{sr} δ̂′, where δ̂′ = ⟨Ĉ_{1}′, v̂, Ĉ_{1} :: Ĉ_{2}⟩{ \atop cont_{1}}. From the definition of the auxiliary abstract machine for control and prompt, δ ⇒_{aux} δ′, where δ′ = ⟨C′_{1}, v, C_{1} :: C_{2}⟩_{cont_{1}} , and C′_{1} = ρ(k). By assumption, Ĉ_{1}′ ≃_{c} C′_{1}, v̂ ≃_{v} v, Ĉ_{1} ≃_{c} C_{1} and Ĉ_{2} ≃_{mc} C_{2}. Hence, δ̂′ ≃ δ′.

Lemma 3. For all configurations δ̂, δ, δ̂′ and δ′, and for any n ≥ 1, if δ̂ ≃ δ then

δ̂ ⇒_{sr}^{n} δ̂′ if and only if δ ⇒_{aux}^{n} δ′ and δ̂′ ≃ δ′.

Proof. By induction on n, using Lemma 2.

We are now in position to prove the formal statement of the equivalence between the two abstract machines:

Proposition 2. For any program ê, either both eval_{sr} (ê) and eval_{aux} ([[ê]]) are undefined or there exist values v̂ and v, such that eval_{sr} (ê) = v̂, eval_{aux} ([[ê]]) = v, and v̂ ≃_{v} v.

Proof. Since the initial configurations ⟨ê, ρ̂_{mt}, ÊND, n̂il⟩êval and ⟨[[ê]], ρ_{mt}, END, nil⟩_{eval} are in the relation ≃, then by Lemma 3 both abstract machines reach their final configurations ⟨n̂il, v̂⟩{ \atop cont_{2}} and ⟨nil, v⟩_{cont_{2}} after the same number of transitions and with v̂ ≃_{v} v, or both diverge.

Theorem 1. For any program ê, either both eval_{sr} (ê) and eval_{cp} ([[ê]]) are undefined or there exist values v̂ and v, such that eval_{sr} (ê) = v̂, eval_{cp} ([[ê]]) = v, and v̂ ≃_{v} v.

Proof. Follows directly from Proposition 1 and Proposition 2.

Corollary 1 (Folklore). For any program ê, and for any integer n, eval_{sr} (ê) = n if and only if eval_{cp} ([[ê]]) = n.

Extending the source language with more syntactic constructs (other ground values and primitive operations, conditional expressions, recursive definitions, etc.) is straightforward. It is equally simple to extend the proof.

Our simple proof is based on the original (operational) specification of static and dynamic delimited continuations. An alternative proof could be based, e.g., on equational reasoning [6, 10].

4 Conclusion

We have formalized and proved that the dynamic delimited-control operators control and prompt can simulate the static delimited-control operators shift and reset by delimiting the context of the resumption of captured continuations. Several converse simulations have been presented recently [3, 12, 15]. These converse simulations are considerably more involved than the present one, and have not been formalized and proved yet.

Acknowledgments: We are grateful to Mads Sig Ager, Małgorzata Biernacka, Julia Lawall, Kevin Millikin, and Kristian Støvring for their comments. Special thanks to the anonymous reviewers for an insightful e-mail exchange. This work is partially supported by the ESPRIT Working Group APPSEM II (http://www.appsem. org) and by the Danish Natural Science Research Council, Grant no. 21-03-0545.

References

[1] Zena M. Ariola, Hugo Herbelin, and Amr Sabry. A type-theoretic foundation of continuations and prompts. In Kathleen Fisher, editor, Proceedings of the 2004 ACM SIGPLAN International Conference on Functional Programming, pages 40–53, Snowbird, Utah, September 2004. ACM Press.

[2] Małgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Research Report BRICS RS-05-24, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, August 2005. To appear in Logical Methods in Computer Science. A preliminary version was presented at the Fourth ACM SIGPLAN Workshop on Continuations (CW 2004).

[3] Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A dynamic continuationpassing style for dynamic delimited continuations. Research Report BRICS RS-05-16, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, May 2005.

[4] Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151–160, Nice, France, June 1990. ACM Press.

[5] R. Kent Dybvig, Simon Peyton-Jones, and Amr Sabry. A monadic framework for subcontinuations. Technical Report 615, Computer Science Department, Indiana University, Bloomington, Indiana, June 2005.

[6] Matthias Felleisen. The theory and practice of first-class prompts. In Jeanne Ferrante and Peter Mager, editors, Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 180–190, San Diego, California, January 1988. ACM Press.

[7] Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD machine, and the λ-calculus. In Martin Wirsing, editor, Formal Description of Programming Concepts III, pages 193–217. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986.

[8] Matthias Felleisen, Mitchell Wand, Daniel P. Friedman, and Bruce F. Duba. Abstract continuations: A mathematical semantics for handling full functional jumps. In Robert (Corky) Cartwright, editor, Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pages 52–62, Snowbird, Utah, July 1988. ACM Press.

[9] Martin Gasbichler and Michael Sperber. Final shift for call/cc: direct implementation of shift and reset. In Simon Peyton Jones, editor, Proceedings of the 2002 ACM SIGPLAN International Conference on Functional Programming, SIGPLAN Notices, Vol. 37, No. 9, pages 271–282, Pittsburgh, Pennsylvania, September 2002. ACM Press.

[10] Yukiyoshi Kameyama and Masahito Hasegawa. A sound and complete axiomatization of delimited continuations. In Olin Shivers, editor, Proceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming, pages 177–188, Uppsala, Sweden, August 2003. ACM Press.

[11] Richard Kelsey, William Clinger, and Jonathan Rees, editors. Revised^{5} report on the algorithmic language Scheme. Higher-Order and Symbolic Computation, 11(1):7–105, 1998.

[12] Oleg Kiselyov. How to remove a dynamic prompt: Static and dynamic delimited continuation operators are equally expressible. Technical Report 611, Computer Science Department, Indiana University, Bloomington, Indiana, March 2005.

[13] Robert E. Milne and Christopher Strachey. A Theory of Programming Language Semantics. Chapman and Hall, London, and John Wiley, New York, 1976.

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

[15] Chung-chieh Shan. Shift to control. In Olin Shivers and Oscar Waddell, editors, Proceedings of the 2004 ACM SIGPLAN Workshop on Scheme and Functional Programming, Technical report TR600, Computer Science Department, Indiana University, Snowbird, Utah, September 2004.

Recent BRICS Report Series Publications

RS-05-25 Dariusz Biernacki and Olivier Danvy. A Simple Proof of a Folklore Theorem about Delimited Control. August 2005. ii+11 pp. To appear in Journal of Functional Programming. This version supersedes BRICS RS-05-10.

RS-05-24 Ma�gorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An Operational Foundation for Delimited Continuations in the CPS Hierarchy. August 2005. iv+43 pp. To appear in the journal Logical Methods in Computer Science. This version supersedes BRICS RS-05-11.

RS-05-23 Karl Krukow, Mogens Nielsen, and Vladimiro Sassone. A Framework for Concrete Reputation-Systems. July 2005. 48 pp. This is an extended version of a paper to be presented at ACM CCS’05.

RS-05-22 Ma�gorzata Biernacka and Olivier Danvy. A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines. July 2005. iv+39 pp.

RS-05-21 Philipp Gerhardy and Ulrich Kohlenbach. General Logical Metatheorems for Functional Analysis. July 2005. 65 pp.

RS-05-20 Ivan B. Damgård, Serge Fehr, Louis Salvail, and Christian Schaffner. Cryptography in the Bounded Quantum Storage Model. July 2005.

RS-05-19 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Bas qLuttik. Finite Equational Bases in Process Algebra: Results and Open Questions. June 2005. 28 pp. To appear in the LNCS series in Jan Willem Klop’s 60th birthday volume.

RS-05-18 Peter Bogetoft, Ivan B. Damgård, Thomas Jakobsen, Kurt Nielsen, Jakob Pagter, and Tomas Toft. Secure Computing, Economy, and Trust: A Generic Solution for Secure Auctions with Real-World Applications. June 2005. 37 pp.

RS-05-17 Ivan B. Damgård, Thomas B. Pedersen, and Louis Salvail. A Quantum Cipher with Near Optimal Key-Recycling. May 2005.

RS-05-16 Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations. May 2005. ii+24 pp.

RS-05-15 Ma�gorzata Biernacka and Olivier Danvy. A Concrete Framework for Environment Machines. May 2005. ii+25 pp.