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-10 ISSN 0909-0878 March 2005 BRICS RS-05-10 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/10/

A Simple Proof of a Folklore Theorem about Delimited Control

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

March 18, 2005

Abstract

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

Keywords Delimited continuations, abstract machines.

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

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

The recent upsurge of interest in delimited continuations [1,5,8,12] seems to take it 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 [7] 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.

In the source syntax, we distinguish between λ-bound variables (x) and shiftor 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 [6] with a meta-context. The source language is the untyped λ-calculus extended with integers, the successor function, shift (noted S), and reset (noted ⟨⟨⟨·⟩⟩⟩).

• 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 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}} .

N.B.: ρ is a partial function mapping identifiers to values, ρ_{mt} is the empty environment, i.e., a function with an empty domain; and ρ{i ↦ v} is defined as follows:

(ρ\{i ↦ v\})(i′) = \{ \begin{matrix}v & if i′ = i \\ (ρ \ \{i\})(i′) & otherwise \end{matrix}

where ρ \ {i} denotes the restriction of ρ to its domain excluding i.

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 [7]. 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 #).

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.

• 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

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, 11] whereas programs using control and prompt give rise to a more complex notion of continuation-passing style that threads a dynamic state [3, 5, 12]. This difference in the semantics of shift and control also induces distinct computational behaviors. For example,

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;^{1} this function is written in the syntax of Scheme [9]:

(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 in 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 in 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))))

1This example is due to Biernacka, Biernacki, and Danvy (March 2005).

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 β-optimization, every application of k to a simple expression e 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 observationally equivalent 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 [10], we annotate the components of the machine for shift and reset with a tilde.

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) ñ ≃_{v} n iff ñ = n

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

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

(d) C̃_{1} ≃_{v} C_{1} iff C̃_{1} ≃_{c} C_{1}

(3) Environments:

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

(b) ρ̃{i ↦ ṽ} ≃_{env} ρ{i ↦ v} iff ṽ ≃_{v} v and ρ̃\ {i} ≃_{env} ρ \ {i}.

(4) Contexts:

(a) ẼND ≃_{c} END

(b) ÃRG ((ẽ, ρ̃), C̃_{1}) ≃_{c} ARG ((e, ρ), C_{1}) iff ẽ ≃_{e} e, ρ̃ ≃_{env} ρ, and C̃_{1} ≃_{c} C_{1}

(c) F̃UN (ṽ, C̃_{1}) ≃_{c} FUN (v, C_{1}) iff ṽ ≃_{v} v and C̃_{1} ≃_{c} C_{1}

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

(5) Meta-contexts:

(a) ñil ≃_{mc} nil

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

(6) Configurations:

(a) ⟨ẽ, ρ̃, C̃_{1}, C̃_{2}⟩ẽval ≃ ⟨e, ρ, C_{1}, C_{2}⟩_{eval} iff ẽ ≃_{e} e, ρ̃ ≃_{env} ρ, C̃_{1} ≃_{c} C_{1}, and C̃_{2} ≃_{mc} C_{2}

(b) ⟨C̃_{1}, ṽ, C̃_{2}⟩{ \atop cont_{1}} ≃ ⟨C_{1}, v, C_{2}⟩_{cont_{1}} iff

C̃_{1} ≃_{c} C_{1}, ṽ ≃_{v} v, and C̃_{2} ≃_{mc} C_{2}

(c) ⟨C̃_{2}, ṽ⟩{ \atop cont_{2}} ≃ ⟨C_{2}, v⟩_{cont_{2}} iff

C̃_{2} ≃_{mc} C_{2} and ṽ ≃_{v} v

3.3 The formal proof

As a stepping stone, we show that running the abstract machine for shift and reset on a program e and running the auxiliary abstract machine for control and prompt on a program [[e]] yield results that are equivalent in the sense of the above relations.

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

Moreover, we show that the abstract machines 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, ρ̃, C̃_{1}, C̃_{2}⟩ẽval and δ = ⟨λx.#(k x), ρ, C_{1}, C_{2}⟩_{eval}.

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

Case: δ̃ = ⟨F̃UN (C̃_{1}′, C̃_{1}), ṽ, C̃_{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 δ̃′ = ⟨C̃_{1}′, ṽ, C̃_{1} :: C̃_{2}⟩{ \atop cont_{1}}. From the definition of the auxiliary abstract machine for control and prompt, δ ⇒_{cp} δ′, where δ′ = ⟨C′_{1}, v, C_{1} :: C_{2}⟩_{cont_{1}} , and C′_{1} = ρ(k). By assumption, C̃_{1}′ ≃_{v} C′_{1}, C̃_{1} ≃_{c} C_{1} and C̃_{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 e, and for any values ṽ and v, eval_{sr} (e) = ṽ if and only if eval_{aux} ([[e]]) = v and ṽ ≃_{v} v.

Proof. The initial configurations ⟨e, ρ̃_{mt}, ẼND, ñil⟩ẽval and ⟨[[e]], ρ_{mt}, END, nil⟩_{eval} are in the relation ≃ and thus by Lemma 3 both abstract machines reach their final configurations ⟨ñil, ṽ⟩{ \atop cont_{2}} and ⟨nil, v⟩_{cont_{2}} after the same number of transitions and with ṽ ≃_{v} v, or both diverge.

Theorem 1. For any program e, and for any values ṽ and v, eval_{sr} (e) = ṽ if and only if eval_{cp} ([[e]]) = v and ṽ ≃_{v} v.

Proof. Follows directly from Proposition 1 and Proposition 2.

Corollary 1 (Folklore). For any program e, and for any integer n, eval_{sr} (e) = n if and only if eval_{cp} ([[e]]) = 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 proofs.

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. Shan has recently presented a converse simulation [12]. This converse simulation is considerably more involved than the present one, and it has 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. This work is 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. Technical Report BRICS RS-04-29, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 2004. A preliminary version was presented at the the Fourth ACM SIGPLAN Workshop on Continuations (CW 2004).

[3] Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A dynamic continuation-passing style for dynamic delimited continuations. Technical Report BRICS RS-05-5, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, February 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. Available at http://www.cs.indiana.edu/~sabry/

research.html, February 2005.

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

[7] 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.

[8] 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.

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

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

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

[12] 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, Snowbird, Utah, September 2004.

Recent BRICS Report Series Publications

RS-05-10 Dariusz Biernacki and Olivier Danvy. A Simple Proof of a Folklore Theorem about Delimited Control. March 2005. ii+11 pp.

RS-05-9 Gudmund Skovbjerg Frandsen and Peter Bro Miltersen. Reviewing Bounds on the Circuit Size of the Hardest Functions. March 2005. 6 pp. To appear in Information Processing Letters.

RS-05-8 Peter D. Mosses. Exploiting Labels in Structural Operational Semantics. February 2005. 15 pp. Appears in Fundamenta Informaticae, 60:17–31, 2004.

RS-05-7 Peter D. Mosses. Modular Structural Operational Semantics. February 2005. 46 pp. Appears in Journal of Logic and Algebraic Programming, 60–61:195–228, 2004.

RS-05-6 Karl Krukow and Andrew Twigg. Distributed Approximation of Fixed-Points in Trust Structures. February 2005. 41 pp.

RS-05-5 A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations. Dariusz Biernacki and Olivier Danvy and Kevin Millikin. February 2005.

RS-05-4 Andrzej Filinski and Henning Korsholm Rohde. Denotational Aspects of Untyped Normalization by Evaluation. February 2005.

RS-05-3 Olivier Danvy and Mayer Goldberg. There and Back Again. January 2005. iii+16 pp. Extended version of an article to appear in Fundamenta Informatica. This version supersedes BRICS RS-02-12.

RS-05-2 Dariusz Biernacki and Olivier Danvy. On the Dynamic Extent of Delimited Continuations. January 2005. ii+30 pp.

RS-05-1 Mayer Goldberg. On the Recursive Enumerability of Fixed-Point Combinators. January 2005. 7 pp. Superseedes BRICS report RS-04-25.

RS-04-41 Olivier Danvy. Sur un Exemple de Patrick Greussay. December 2004. 14 pp.

RS-04-40 Mads Sig Ager, Olivier Danvy, and Henning Korsholm Rohde. Fast Partial Evaluation of Pattern Matching in Strings. December 2004. 22 pp. To appear in TOPLAS. Supersedes BRICS report RS-03-20.