BRICS RS-97-7 Hatcliff & Danvy: Thunks and the λ-Calculus BRICS

Basic Research in Computer Science

Thunks and the λ-Calculus

(Extended Version)

John Hatcliff Olivier Danvy BRICS Report Series RS-97-7 ISSN 0909-0878 March 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, 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/97/7/

Thunks and the λ-calculus (extended version)

John Hatcliff  Olivier Danvy
BRICS^{∗}
Oklahoma State University ^{†}  University of Aarhus ^{‡}

March 1997

Abstract

Plotkin, in his seminal article Call-by-name, call-by-value and the λ-calculus, formalized evaluation strategies and simulations using operational semantics and continuations. In particular, he showed how call-by-name evaluation could be simulated under call-by-value evaluation and vice versa. Since Algol 60, however, call-by-name is both implemented and simulated with thunks rather than with continuations. We recast this folk theorem in Plotkin’s setting, and show that thunks, even though they are simpler than continuations, are sufficient for establishing all the correctness properties of Plotkin’s call-by-name simulation.

Furthermore, we establish a new relationship between Plotkin’s two continuation-based simulations C_{n} and C_{v}, by deriving C_{n} as the composition of our thunk-based simulation T and of C_{v}^{+} — an extension of C_{v} handling thunks. Almost all of the correctness properties of C_{n} follow from the properties of T and C_{v}^{+}. This simplifies reasoning about call-by-name continuation-passing style.

We also give several applications involving factoring continuationbased transformations using thunks.

∗ Basic Research in Computer Science, Centre of the Danish National Research Foundation.

† Computer Science Department 219 Mathematical Sciences, Stillwater, OK 74078-1053, USA.

E-mail: hatcliff@a.cs.okstate.edu ‡ Department of Computer Science Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark.

E-mail: danvy@brics.dk

Contents

1 Introduction and Background 5 1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2 An example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.3 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4 Syntax and semantics of λ-terms . . . . . . . . . . . . . . . . 8

1.4.1 The language Λ . . . . . . . . . . . . . . . . . . . . . . 8 1.4.2 Values . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.4.3 Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.4.4 Operational semantics . . . . . . . . . . . . . . . . . . 10 1.4.5 Operational equivalence . . . . . . . . . . . . . . . . . 11

1.5 Continuation-based simulations . . . . . . . . . . . . . . . . . 12 1.5.1 Call-by-name continuation-passing style . . . . . . . . 12 1.5.2 Call-by-value continuation-passing style . . . . . . . . 15

2 Thunks 17 2.1 Thunk introduction . . . . . . . . . . . . . . . . . . . . . . . . 17 2.2 Reduction of thunked terms . . . . . . . . . . . . . . . . . . . 17

2.2.1 τ-reduction . . . . . . . . . . . . . . . . . . . . . . . . 17 2.2.2 A language closed under reductions . . . . . . . . . . . 18

2.3 A thunk-based simulation . . . . . . . . . . . . . . . . . . . . 18 2.3.1 Indifference . . . . . . . . . . . . . . . . . . . . . . . . 19 2.3.2 Simulation . . . . . . . . . . . . . . . . . . . . . . . . 19 2.3.3 Translation . . . . . . . . . . . . . . . . . . . . . . . . 20

2.4 Thunks implemented in Λ . . . . . . . . . . . . . . . . . . . . 23

3 Connecting the Thunk-based and the Continuation-based Simulations 24 3.1 CPS transformation of thunk constructs . . . . . . . . . . . . 25 3.2 The connection between the thunk-based and continuation-

based simulations . . . . . . . . . . . . . . . . . . . . . . . . . 27 3.3 Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

3.3.1 Deriving correctness properties of C_{n} . . . . . . . . . . 30 3.3.2 Deriving a CPS transformation directed by strictness

information . . . . . . . . . . . . . . . . . . . . . . . . 31 3.3.3 Deriving a call-by-need CPS transformation . . . . . . 31

3.4 Assessment . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 4 Thunks in a Typed Setting 33

4.1 Thunk introduction for a typed language . . . . . . . . . . . . 33 4.2 CPS transformations for a typed language . . . . . . . . . . . 34 4.3 Connecting the thunk-based and the continuation-based sim-

ulations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 4.4 Assessment . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

5 Related Work 37

6 Conclusion 37

A Proofs 38

A.1 Correctness of C_{n} . . . . . . . . . . . . . . . . . . . . . . . . . 38 A.1.1 Indifference . . . . . . . . . . . . . . . . . . . . . . . . 38 A.1.2 Simulation . . . . . . . . . . . . . . . . . . . . . . . . 39 A.1.3 Translation . . . . . . . . . . . . . . . . . . . . . . . . 39

A.2 Correctness of T . . . . . . . . . . . . . . . . . . . . . . . . . 40 A.2.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . 40 A.2.2 The language T ⟨[Λ]⟩^{∗} . . . . . . . . . . . . . . . . . . . 41 A.2.3 Simulation . . . . . . . . . . . . . . . . . . . . . . . . 42 A.2.4 Translation . . . . . . . . . . . . . . . . . . . . . . . . 45

A.3 Correctness of T_{L} . . . . . . . . . . . . . . . . . . . . . . . . . 47 A.3.1 The language T_{L}⟨[Λ]⟩^{∗} . . . . . . . . . . . . . . . . . . 47 A.3.2 Indifference and Simulation . . . . . . . . . . . . . . . 47 A.3.3 Translation . . . . . . . . . . . . . . . . . . . . . . . . 48

A.4 Correctness of C_{v}^{+} . . . . . . . . . . . . . . . . . . . . . . . . . 49 A.4.1 Indifference and Simulation . . . . . . . . . . . . . . . 49

List of Figures

1 Abstract syntax of the language Λ . . . . . . . . . . . . . . . 9 2 Single-step evaluation rules . . . . . . . . . . . . . . . . . . . 10 3 Plotkin’s call-by-name CPS transformation . . . . . . . . . . 13 4 Plotkin’s call-by-value CPS transformation . . . . . . . . . . 16 5 Thunk introduction . . . . . . . . . . . . . . . . . . . . . . . . 17 6 Evaluation of thunked terms . . . . . . . . . . . . . . . . . . . 19 7 Thunk elimination . . . . . . . . . . . . . . . . . . . . . . . . 20 8 Thunk introduction implemented in Λ . . . . . . . . . . . . . 24 9 Call-by-value CPS transformation (extended to thunks) … 26 10 Optimizing call-by-name CPS transformation . . . . . . . . . 28 11 Optimizing call-by-value CPS transformation . . . . . . . . . 29 12 Typing rules for Λ . . . . . . . . . . . . . . . . . . . . . . . . 33 13 Typing rules for Λ_{τ} . . . . . . . . . . . . . . . . . . . . . . . . 34 14 Transformation on types for T . . . . . . . . . . . . . . . . . 34 15 Transformation on types for C_{n} . . . . . . . . . . . . . . . . . 35 16 Transformation on types for C_{v} . . . . . . . . . . . . . . . . . 35 17 Mapping Λ thunks to abstract Λ_{τ} thunks . . . . . . . . . . . 48

1 Introduction and Background

1.1 Motivation

Plotkin, in his seminal article Call-by-name, call-by-value and the λ-calculus [23], formalizes both call-by-name and call-by-value procedure calling mechanisms for λ-calculi. Call-by-name evaluation is described with a standardization theorem for the λβ-calculus. Call-by-value evaluation is described with a standardization theorem for a new calculus (the λβ_{v}-calculus). Plotkin then shows that call-by-name can be simulated by call-by-value and vice versa. The simulations also give interpretations of each calculus in terms of the other.

Both of Plotkin’s simulations rely on continuations — a technique used earlier to model the meaning of jumps in the denotational-semantics approach to programming languages [33] and to express relationships between memory-management techniques [12], among other things [27]. Since Algol 60, however, programming wisdom has it that thunks^{1} can be used to obtain a simpler simulation of call-by-name by call-by-value.^{2}

Our aim is to clarify the properties of thunks with respect to Plotkin’s classic study of evaluation strategies and continuation-passing styles [23]. We begin by defining a thunk-introducing transformation T and prove that thunks are sufficient for establishing all the technical properties Plotkin considered for his continuation-based call-by-name simulation C_{n}.^{3}

Given this, one may question what rôle continuations actually play in C_{n} since they are unnecessary for achieving a simulation. We show that the continuation-passing structure of C_{n} can actually be obtained by extending Plotkin’s call-by-value continuation-based simulation C_{v} to process the abstract representation of thunks and composing this extended transformation C_{v}^{+} with T , i.e.,^{4}

1The term “thunk” was coined to describe the compiled representation of delayed expressions in implementations of Algol 60 [17]. The terminology has been carried over and applied to various methods of delaying the evaluation of expressions [25].

2Plotkin acknowledges that thunks provide some simulation properties but states that “...these ‘protecting by a λ’ techniques do not seem to be extendable to a complete simulation and it is fortunate that the technique of continuations is available.” [23, p. 147]. By “protecting by a λ”, Plotkin refers to a representation of thunks as λ-abstractions with a dummy parameter. When we discussed our investigation of thunks with him, Plotkin told us that he had also found recently the “protecting by a λ” technique to be sufficient for a complete simulation [24].

3Plotkin actually gives a slightly different simulation P_{n} [23, p. 153]. We note in Section 1.5.1 that Plotkin’s Translation theorem for P_{n} does not hold. A slight modification to P_{n} gives the translation C_{n} which does satisfy the Translation theorem. Therefore, in the present work, we will take C_{n} along with Plotkin’s original call-by-value continuation-based simulation C_{v} as the canonical continuation-based simulations.

λβ_{v} ⊢ C_{n}⟨[e]⟩ = (C_{v}^{+} ∘ T )⟨[e]⟩.

This establishes a previously unrecognized connection between C_{n} and C_{v} and gives insight into the structural similarities between call-by-name and call-by-value continuation-passing style.

We show that almost all of the technical properties that Plotkin established for C_{n} follow from the properties of C_{v}^{+} and T . So as a byproduct, when reasoning about C_{n} and C_{v}, it is often sufficient to reason about C_{v}^{+} and the simpler simulation T . We give several applications involving deriving optimized continuation-based simulations for call-by-name and call-by-need languages.

1.2 An example

Consider the program (λx_{1}.(λx_{2}.x_{1}) Ω) b where Ω represents some term whose evaluation diverges under any evaluation strategy and where b represents some basic constant. Call-by-name evaluation dictates that arguments be passed unevaluated to functions. Thus, call-by-name evaluation of the example program proceeds as follows:

(λx_{1}.(λx_{2}.x_{1}) Ω) b ⟼_{n} (λx_{2}.b) Ω  (1)
⟼_{n} b

Call-by-value evaluation dictates that arguments be simplified to values (i.e., constants or abstractions) before being passed to functions. Thus, call-by-value evaluation of the example program proceeds as follows:

(λx_{1}.(λx_{2}.x_{1}) Ω) b ⟼_{v} (λx_{2}.b) Ω
⟼_{v} (λx_{2}.b) Ω′
⟼_{v} (λx_{2}.b) Ω′′
⟼_{v} ...

Since the term Ω never reduces to a value, λx_{2}.b cannot be applied — and the evaluation does not terminate.

4In fact, C_{n} and C_{v}^{+} ∘ T only differ by “administrative reductions” [23, p. 149] (i.e., reductions introduced by the transformations that implement continuation-passing). Thus, for optimizing transformations C_{n.opt} and C_{v.opt}^{+} that produce CPS terms without administrative reductions [8], the output of C_{n.opt} is identical to the output of C_{v.opt}^{+} ∘ T .

The difference between call-by-name and call-by-value evaluation lies in how arguments are treated. To simulate call-by-name with call-by-value evaluation, one needs a mechanism for turning arbitrary arguments into values. This can be accomplished using a suspension constructor delay. delay e turns the expression e into a value and thus suspends its evaluation. The suspension destructor force triggers the evaluation of an expression suspended by delay. Accordingly, suspensions have the following evaluation property.

force (delay e) ⟼_{v} e

Introducing delay and force in the example program via a thunking transformation T provides a simulation of call-by-name under call-by-value evaluation.

(λx_{1}.(λx_{2}.force x_{1}) (delay Ω)) (delay b)
⟼_{v} (λx_{2}.force (delay b)) (delay Ω) (2)
⟼_{v}  force (delay b)
⟼_{v}  b

Applying Plotkin’s call-by-name continuation-passing transformation C_{n} to the example program also gives a simulation of call-by-name under call-by-value evaluation [23].

\begin{matrix}(λk.\begin{matrix}(λk.k (λx_{1}.λk.(λk.k (λx_{2}.λk.x_{1} k)) (λy_{1}.y_{1} C_{n}⟨[Ω]⟩ k))) \\ (λy_{2}.y_{2} (λk.k b) k)) \end{matrix} \\ (λy_{3}.y_{3}) \end{matrix}  (3)

The resulting program is said to be in continuation-passing style (CPS). A tedious but straightforward rewriting shows that the call-by-value evaluation of the CPS program above yields b — the result of the original program when evaluated under call-by-name. Even after optimizing the CPS program by performing “administrative reductions” (i.e., reductions of abstractions that implement continuation-passing and do not appear in the original program such as the λk.... and λy_{i}.... of line (3)) [23, p. 149],

(λx_{1}.λk.(λx_{2}.λk.x_{1} k) C_{n}⟨[Ω]⟩ k) (λk.k b) (λy_{3}.y_{3})  (4)

the evaluation is still more involved than for the thunked program.^{5} 1.3 Overview

5The original term at line (1) requires 2 evaluation steps. The thunked version at line (2) requires 3 steps. The unoptimized CPS version at line (3) requires 11 steps.

The remainder of this section gives necessary background material covering the syntax and semantics of λ-terms and Plotkin’s continuation-passing simulations. Section 2 presents the thunk-based simulation T and associated correctness results. Section 3 presents the factoring of C_{n} via thunks and gives several applications. Section 4 recasts the results of the previous sections in a typed setting. Section 5 gives a discussion of related work. Section 6 concludes.

1.4 Syntax and semantics of λ-terms

This section briefly reviews the syntax, equational theories, and operational semantics associated with λ-terms. The notation used is essentially Barendregt’s [3]. The presentation of calculi in Section 1.4.3 follows Sabry and Felleisen [31] and the presentation of operational semantics in Section 1.4.4 is adapted from Plotkin [23].

1.4.1 The language Λ

Figure 1 presents the syntax of the language Λ. The language is a pure untyped functional language including constants, identifiers, λ-abstractions (functions), and applications. To simplify substitution, we follow Barendregt’s variable convention^{6} and work with the quotient of Λ under αequivalence [3]. We write e_{1} ≡ e_{2} when e_{1} and e_{2} are α-equivalent.

The notation FV(e) denotes the set of free variables in e and e_{1}[x := e_{2}] denotes the result of the capture-free substitution of all free occurences of x in e_{1} by e_{2}. A context C is a term with a “hole” [·]. The operation of filling the context C with a term e yields the term C [e], possibly capturing some free variables of e in the process. Contexts[l] denotes the set of contexts from some language l. Closed terms — terms with no free variables — are called programs. Programs[l] denotes the set of programs from some language l.

The optimized CPS version at line (4) requires 6 steps. As Sabry and Felleisen note [31, p. 302], this last program can be optimized further by unfolding source reductions, eliminating administrative reductions exposed by the unfolding, and then expanding back the source reductions. However, an optimized version of C_{n} capturing these additional steps would be significantly more complicated than T (making it much harder to reason about its correctness). Moreover, the resulting CPS program would still require more evaluation steps in general than the corresponding program in the image of T .

6In terms occurring in definitions and proofs etc., all bound variables are chosen to be different from free variables [3, p. 26].

e ∈ Λ
e ::= b | x | λx.e | e_{0} e_{1}

Figure 1: Abstract syntax of the language Λ

1.4.2 Values

Certain terms of Λ are designated as values. Values roughly correspond to terms that may be results of the operational semantics presented below. The sets Values_{n}[Λ] and Values_{v}[Λ] below represent the set of values from the language Λ under call-by-name and call-by-value evaluation respectively.

v ∈ Values_{n}[Λ]
v ::= b | λx.e

v ∈ Values_{v}[Λ] v ::= b | x | λx.e  ...where e ∈ Λ

Note that identifiers are included in Values_{v}[Λ] since only values will be substituted for identifiers under call-by-value evaluation. We use v as a meta-variable for values and where no ambiguity results we will ignore the distinction between call-by-name and call-by-value values.

1.4.3 Calculi

λ-calculi are formal theories of equations between λ-terms. We consider calculi generated by one or more of the following principal axiom schemata (also called notions of reduction) along with the logical axioms and inference rules presented below.

Notions of reduction

(λx.e_{1}) e_{2} ⟶_{β} e_{1}[x := e_{2}]  (β)
(λx.e) v ⟶_{β_{v}} e[x := v]  v ∈ Values_{v}[Λ]  (β_{v})
λx.e x ⟶_{η} e  x ∉ FV(e)  (η)
λx.v x ⟶_{η_{v}} v  v ∈ Values_{v}[Λ] ∧ x ∉ FV(v) (η_{v})

Logical axioms and inference rules

e_{1} ⟶ e_{2} ⇒ C [e_{1}] = C [e_{2}] ∀ contexts C (Compatibility)
e = e  (Reflexivity)
e_{1} = e_{2}, e_{2} = e_{3} ⇒ e_{1} = e_{3}  (Transitivity)
e_{1} = e_{2} ⇒ e_{2} = e_{1}  (Symmetry)

Call-by-name:

(λx.e_{0}) e_{1} ⟼_{n} e_{0}[x := e_{1}] \frac{e_{0} ⟼_{n} e′_{0}}{e_{0} e_{1} ⟼_{n} e′_{0} e_{1}}

Call-by-value:

(λx.e) v ⟼_{v} e[x := v] \frac{e_{0} ⟼_{v} e′_{0}}{e_{0} e_{1} ⟼_{v} e′_{0} e_{1}}

\frac{e_{1} ⟼_{v} e′_{1}}{(λx.e_{0}) e_{1} ⟼_{v} (λx.e_{0}) e′_{1}}

Figure 2: Single-step evaluation rules

The underlying notions of reduction completely identify a theory. For example, β generates the theory λβ and β_{v} generates the theory λβ_{v}. In general, we write λA to refer to the theory generated by a set of axioms A. When a theory λA proves an equation e_{1} = e_{2}, we write λA ⊢ e_{1} = e_{2}. If the proof does not involve the inference rule (Symmetry), we write λA ⊢ e_{1} ⟶ ⟶ e_{2}, and if the proof only involves the rule (Compatibility) we write λA ⊢ e_{1} ⟶ e_{2}. Reductions in calculational style proofs are denoted by subscripting reduction symbols (e.g., ⟶_{β}, ⟶ ⟶_{η_{v}}). If a property holds for both λβ and λβ_{v}, we say the property holds for λβ_{i}.

1.4.4 Operational semantics

Figure 2 presents single-step evaluation rules which define the call-by-name and call-by-value operational semantics of Λ programs.^{7} The (partial) evaluation functions eval_{n} and eval_{v} are defined in terms of the reflexive, transitive closure (denoted ⟼^{∗}) of the single-step evaluation rules.

eval_{n}(e) = v iff e ⟼_{n}^{∗} v
eval_{v}(e) = v iff e ⟼_{v}^{∗} v

7The rules of Figure 2 are a simplified version of Plotkin’s [23, pp. 146 and 136]. To simplify the presentation, we do not consider evaluation rules defined over open terms or functional constants (i.e., δ-rules).

We write e ⟼_{i} e′ when both e ⟼_{n} e′ and e ⟼_{v} e′ (similarly for eval_{i}). Given meta-language expressions E_{1} and E_{2} where one or both may be undefined, we write E_{1} ≃ E_{2} when E_{1} and E_{2} are both undefined, or else both are defined and denote α-equivalent terms. Similarly, for any notion of reduction r, we write E_{1} ≃_{r} E_{2} when E_{1} and E_{2} are both undefined, or else are both defined and denote r-equivalent terms.

An evaluation eval(e) may be undefined for two reasons:

1. e heads an infinite evaluation sequence, i.e., e ⟼ e_{1} ⟼ e_{2} ⟼ ...,

2. e heads an evaluation sequence which ends in a stuck term — a nonvalue which cannot be further evaluated (e.g., the application of a basic constant to some argument).

The following definition gives programs that are stuck under call-by-name and call-by-value evaluation.

\begin{aligned}s & ∈ & Stuck_{n}[Λ] \\ s & ::= & b e | s e \end{aligned}  \begin{aligned}s & ∈ & Stuck_{v}[Λ] \\ s & ::= & b e | s e | (λx.e) s \end{aligned} ...where e ∈ Λ

A simple induction over the structure of e ∈ Programs[Λ] shows that either e ∈ Values_{n}[Λ], or e ∈ Stuck_{n}[Λ], or e ⟼_{n} e′. A similar property holds for call-by-value.

1.4.5 Operational equivalence

Plotkin’s definitions of call-by-name and call-by-value operational equivalence are as follows [23, pp. 147 and 144].

Definition 1 (CBN operational equivalence) For all e_{1}, e_{2} ∈ Λ, e_{1} ≈_{n} e_{2} iff for any context C ∈ Contexts[Λ] such that C [e_{1}] and C [e_{2}] are programs, eval_{n}(C [e_{1}]) and eval_{n}(C [e_{2}]) are either both undefined, or else both defined and one is a given basic constant b iff the other is.

Definition 2 (CBV operational equivalence) For all e_{1}, e_{2} ∈ Λ, e_{1} ≈_{v} e_{2} iff for any context C ∈ Contexts[Λ] such that C [e_{1}] and C [e_{2}] are programs, eval_{v}(C [e_{1}]) and eval_{v}(C [e_{2}]) are either both undefined, or else both defined and one is a given basic constant b iff the other is.

The calculi of Section 1.4.3 can be used to reason about operational behavior. To establish the operational equivalence two terms, it is sufficient to show that the terms are convertible in an appropriate calculus.

Theorem 1 (Soundness of calculi for Λ) For all e_{1}, e_{2} ∈ Λ,

λβ ⊢ e_{1} = e_{2} ⇒ e_{1} ≈_{n} e_{2}
λβ_{v} ⊢ e_{1} = e_{2} ⇒ e_{1} ≈_{v} e_{2}

Proof: See [23, pp. 147 and 144]

Note that η is unsound for both call-by-name and call-by-value since it does not preserve termination properties.^{8} Termination properties can be preserved by requiring the contractum of an η-redex to be a value. For example, η_{v} preserves call-by-value termination properties. However, even these restricted forms are unsound in an untyped setting due to “improper” uses of basic constants. For example,

λx.b x ⟶_{η_{v}} b

but λx.b x ≉_{v} b (take C = [·]). Thus, extending the setting considered by Plotkin (i.e., untyped terms with basic constants) to include an elegant theory of η-like reduction seems problematic.^{9} However, in specific settings where constraints on the structure of terms disallow such problematic cases, limited forms of η reduction can be applied soundly.^{10}

1.5 Continuation-based simulations

This section presents Plotkin’s continuation-based simulations of call-by-name in call-by-value and vice versa [23]. As characterized by Meyer and Wand [18], “CPS terms are tail-recursive: no argument is an application. Therefore there is at most one redex which is not inside the scope of an abstraction, and thus call-by-value evaluation coincides with outermost or call-by-name evaluation.”

1.5.1 Call-by-name continuation-passing style

Figure 3 gives Plotkin’s call-by-name CPS transformation P_{n} where the k’s and the y’s are fresh variables (i.e., variables not appearing free in the argument of P_{n}). The transformation is defined using two translation functions:

8For example, λx.Ω x ⟶_{η} Ω but eval_{i}(λx.Ω x) is defined whereas eval_{i}(Ω) is undefined.

9Sabry and Felleisen similarly discuss problems with η and η_{v} reduction [30, p. 5] [31, p. 322].

10This is the case with the languages of terms in the image of CPS transformations presented in the following section.

P_{n}⟨[·]⟩ : Λ→Λ
P_{n}⟨[v]⟩ = λk.k P_{n}⟨v⟩
P_{n}⟨[x]⟩ = x
P_{n}⟨[e_{0} e_{1}]⟩ = λk.P_{n}⟨[e_{0}]⟩ (λy_{0}.y_{0} P_{n}⟨[e_{1}]⟩ k)
P_{n}⟨·⟩ : Values_{n}[Λ]→Λ
P_{n}⟨b⟩ = b
P_{n}⟨λx.e⟩ = λx.P_{n}⟨[e]⟩

Figure 3: Plotkin’s call-by-name CPS transformation

P_{n}⟨[·]⟩ is the general translation function for terms of Λ; P_{n}⟨·⟩ is the translation function for call-by-name values. The following theorem given by Plotkin [23, p. 153] captures correctness properties of the transformation.

Theorem 2 (Plotkin 1975) For all e ∈ Programs[Λ] and e_{1}, e_{2} ∈ Λ,

1. Indifference: eval_{v}(P_{n}⟨[e]⟩ I ) ≃ eval_{n}(P_{n}⟨[e]⟩ I )

2. Simulation: P_{n}⟨eval_{n}(e)⟩ ≃ eval_{v}(P_{n}⟨[e]⟩ I )

3. Translation:

λβ ⊢ e_{1} = e_{2} iff λβ_{v} ⊢ P_{n}⟨[e_{1}]⟩ = P_{n}⟨[e_{2}]⟩
iff λβ ⊢ P_{n}⟨[e_{1}]⟩ = P_{n}⟨[e_{2}]⟩
iff λβ_{v} ⊢ P_{n}⟨[e_{1}]⟩ I = P_{n}⟨[e_{2}]⟩ I
iff λβ ⊢ P_{n}⟨[e_{1}]⟩ I = P_{n}⟨[e_{2}]⟩ I

The Indifference property states that, given the identity function I = λy.y as the initial continuation, the result of evaluating a CPS term using call-by-value evaluation is the same as the result of using call-by-name evaluation. In other words, terms in the image of the transformation are evaluation-order independent. This follows because all function arguments are values in the image of the transformation (and this condition is preserved under β_{i} reductions).

The Simulation property states that, given the identity function as an initial continuation, evaluating a CPS term using call-by-value evaluation simulates the evaluation of the original term using call-by-name evaluation.

The Translation property purports that β-equivalence classes are preserved and reflected by P_{n}. However, the property does not hold because^{11}

λβ ⊢ e_{1} = e_{2} ⇏ λβ_{i} ⊢ P_{n}⟨[e_{1}]⟩ = P_{n}⟨[e_{2}]⟩.

In some cases, η_{v} is needed to establish the equivalence of the CPS-images of two β-convertible terms. For example, λx.(λz.z) x ⟶_{β} λx.x but

P_{n}⟨[λx.(λz.z) x]⟩ = λk.k (λx.λk.(λk.k (λz.z)) (λy.y x k))
⟶_{β_{v}} λk.k (λx.λk.(λy.y x k) (λz.z))
⟶_{β_{v}} λk.k (λx.λk.(λz.z) x k)
⟶_{β_{v}} λk.k (λx.λk.x k)
⟶_{η_{v}} λk.k (λx.x)  ...η_{v} is needed for this step
= P_{n}⟨[λx.x]⟩.

In practice, η_{v} reductions such as those required in the example above are unproblematic if they are embedded in proper CPS contexts. When λk.k (λx.λk.x k) is embedded in a CPS context, x will always bind to a term of the form λk.e during evaluation. However, if the term is not embedded in a CPS context (e.g., [·] (λy.y b)), the η_{v} reduction is unsound.

The simplest solution for recovering the Translation property is to change the translation of identifiers from P_{n}⟨[x]⟩ = x to λk.x k. Let C_{n} be the modified translation which is identical to P_{n} except that

C_{n}⟨[x]⟩ = λk.x k

For the example above, the new translation gives

λβ_{i} ⊢ C_{n}⟨[λx.(λz.z) x]⟩ = C_{n}⟨[λx.x]⟩.

The following theorem gives the correctness properties for C_{n}.

Theorem 3 For all e ∈ Programs[Λ] and e_{1}, e_{2} ∈ Λ,

1. Indifference: eval_{v}(C_{n}⟨[e]⟩ I ) ≃ eval_{n}(C_{n}⟨[e]⟩ I )

2. Simulation: C_{n}⟨eval_{n}(e)⟩ ≃_{β_{i}} eval_{v}(C_{n}⟨[e]⟩ I )

11The proof given in [23, p. 158] breaks down where it is stated “It is straightforward to show that λβ ⊢ e_{1} = e_{2} implies λβ_{v} ⊢ P_{n}⟨[e_{1}]⟩ = P_{n}⟨[e_{2}]⟩ ...”.

3. Translation:

λβ ⊢ e_{1} = e_{2} iff λβ_{v} ⊢ C_{n}⟨[e_{1}]⟩ = C_{n}⟨[e_{2}]⟩
iff λβ ⊢ C_{n}⟨[e_{1}]⟩ = C_{n}⟨[e_{2}]⟩
iff λβ_{v} ⊢ C_{n}⟨[e_{1}]⟩ I = C_{n}⟨[e_{2}]⟩ I
iff λβ ⊢ C_{n}⟨[e_{1}]⟩ I = C_{n}⟨[e_{2}]⟩ I

The Indifference and Translation properties for C_{n} are identical to those of P_{n}. However, the Simulation property for C_{n} holds up to β_{i}- equivalence^{12} while Simulation for P_{n} holds up to α-equivalence.^{13}

We show in Section 3.3.1 that proofs of Indifference, Simulation, and most of the Translation can be derived from the correctness properties of C_{v}^{+} and T (as discussed in Section 1). All that remains of Translation is the ⇐ direction of the first bi-implication; this follows in a straightforward manner from Plotkin’s original proof for P_{n} (see Appendix A.1.3).

1.5.2 Call-by-value continuation-passing style

Figure 4 gives Plotkin’s call-by-value CPS transformation. The following theorem captures correctness properties of the translation.

Theorem 4 (Plotkin 1975) For all e ∈ Programs[Λ] and e_{1}, e_{2} ∈ Λ,

1. Indifference: eval_{n}(C_{v}⟨[e]⟩ I ) ≃ eval_{v}(C_{v}⟨[e]⟩ I )

2. Simulation: C_{v}⟨eval_{v}(e)⟩ ≃ eval_{n}(C_{v}⟨[e]⟩ I )

3. Translation:

If λβ_{v} ⊢ e_{1} = e_{2} then λβ_{v} ⊢ C_{v}⟨[e_{1}]⟩ = C_{v}⟨[e_{2}]⟩

Also λβ_{v} ⊢ C_{v}⟨[e_{1}]⟩ = C_{v}⟨[e_{2}]⟩ iff λβ ⊢ C_{v}⟨[e_{1}]⟩ = C_{v}⟨[e_{2}]⟩

12For example, C_{n}⟨eval_{n}((λz.λy.z) b)⟩ = λy.λk.k b whereas eval_{v}(C_{n}⟨[(λz.λy.z) b]⟩ I ) = λy.λk.(λk.k b) k.

13This is because P_{n} commutes with substitution up to α-equivalence, i.e., C_{n}⟨[e_{0}[x := e_{1}]]⟩ ≡ C_{n}⟨[e_{0}]⟩[x := C_{n}⟨[e_{1}]⟩] whereas C_{n} commutes with substitution only up to β_{i}- equivalence, i.e., C_{n}⟨[e_{0}[x := e_{1}]]⟩ =_{β_{i}} C_{n}⟨[e_{0}]⟩[x := C_{n}⟨[e_{1}]⟩]. This renders the usual colon translation technique [23, p. 154] insufficient for proving Simulation for C_{n}. Evaluation steps involving substitution lead to terms which lie outside the image of the colon translation associated with C_{n}. A similar situation occurs with the thunk-based simulation T introduced in Section 2 (see Section 2.3.2, Footnote 17).

C_{v}⟨[·]⟩ : Λ→Λ
C_{v}⟨[v]⟩ = λk.k C_{v}⟨v⟩
C_{v}⟨[e_{0} e_{1}]⟩ = λk.C_{v}⟨[e_{0}]⟩ (λy_{0}.C_{v}⟨[e_{1}]⟩ (λy_{1}.y_{0} y_{1} k))

C_{v}⟨·⟩ : Values_{v}[Λ]→Λ
C_{v}⟨b⟩ = b
C_{v}⟨x⟩ = x
C_{v}⟨λx.e⟩ = λx.C_{v}⟨[e]⟩

Figure 4: Plotkin’s call-by-value CPS transformation

The intuition behind the Indifference and Simulation properties is the same as for C_{n}. The Translation property states that β_{v}-convertible terms are also convertible in the image of C_{v}. In contrast to the theory λβ appearing in the Translation property for C_{n} (Theorem 3), the theory λβ_{v} is incomplete in the sense that it cannot establish the convertibility of some pairs of terms in the image of the CPS transformation [31].^{14}

Finally, note that neither C_{n} nor C_{v} (nor P_{n}) are fully abstract (i.e., they do not preserve operational equivalence) [23, pp. 154 and 148]. Specifically, e_{1} ≈_{n} e_{2} does not imply C_{n}⟨[e_{1}]⟩ ≈_{v} C_{n}⟨[e_{2}]⟩ (and similarly for C_{v}).^{15}

14Plotkin gives the following example of the incompleteness [23, p. 153]. Let e_{1} ≡ ((λx.x x) (λx.x x)) y and e_{2} ≡ (λx.x y) ((λx.x x) (λx.x x)). Then λβ_{v} ⊢ C_{v}⟨[e_{1}]⟩ = C_{v}⟨[e_{2}]⟩ and λβ ⊢ C_{v}⟨[e_{1}]⟩ = C_{v}⟨[e_{2}]⟩ but λβ_{v} ⊬ e_{1} = e_{2}. Sabry and Felleisen [31] give an equational theory λA (where A is a set of axioms including β_{v}η_{v}) and show it complete in the sense that λA ⊢ e_{1} = e_{2} iff λβη ⊢ F⟨[e_{1}]⟩ = F⟨[e_{2}]⟩. F is Fischer’s call-by-value CPS transformation [12] where continuations are the first arguments to functions (instead of the second arguments as in Plotkin’s C_{v}). Note that their results cannot be immediately carried over to this setting since the reduction properties of terms generated by the transformation F are sufficiently different from the reduction properties of terms generated by Plotkin’s transformation C_{v} (see [31, p. 314]).

15For examples of why full abstraction fails, see [23, pp. 154 and 149] and [30, p. 30]. For a detailed presentation of fully abstract translations in a typed setting, see the work of Riecke [28, 29].

T : Λ→Λ_{τ}
T ⟨[b]⟩ = b
T ⟨[x]⟩ = force x
T ⟨[λx.e]⟩ = λx.T ⟨[e]⟩
T ⟨[e_{0} e_{1}]⟩ = T ⟨[e_{0}]⟩ (delay T ⟨[e_{1}]⟩)

Figure 5: Thunk introduction

2 Thunks

2.1 Thunk introduction

To establish the simulation properties of thunks, we extend the language Λ to the language Λ_{τ} that includes suspension operators.

e ∈ Λ_{τ}
e ::= ... | delay e | force e

The operator delay suspends the computation of an expression — thereby coercing an expression to a value. Therefore, delay e is added to the value sets in Λ_{τ}.

v ∈ Values_{n}[Λ_{τ}]
v ::= ... | delay e

v ∈ Values_{v}[Λ_{τ}] v ::= ... | delay e ...where e ∈ Λ_{τ}

Figure 5 presents the definition of the thunk-based simulation T .

2.2 Reduction of thunked terms

2.2.1 τ-reduction

The operator force triggers the evaluation of a suspension created by delay. This is formalized by the following notion of reduction.

Definition 3 (τ-reduction) force (delay e) ⟶_{τ} e

The notion of reduction τ generates the theory λτ as outlined in Section 1.4.3. Combining reductions β and τ generates the theory λβτ. Similarly, β_{v} and τ give λβ_{v}τ.

It is easy to show that τ is Church-Rosser. The Church-Rosser property for βτ and β_{v}τ follows by the Hindley-Rosen Lemma [3, pp. 53 – 65] since β [3, p. 62] and β_{v} [23, p. 135] are also Church-Rosser, and it can be shown that ⟶ ⟶_{τ} commutes with ⟶ ⟶_{β} and ⟶ ⟶_{β_{v}}.

The evaluation rules for Λ_{τ} are obtained by adding the following rules to both the call-by-name and call-by-value evaluation rules of Figure 2.

\frac{e ⟼ e′}{force e ⟼ force e′} force (delay e) ⟼ e

2.2.2 A language closed under reductions

To determine the correctness properties of thunks, we consider the set of terms T ⊂ Λ_{τ} which are reachable from the image of T via β and τ reductions.

T =^{def} {t ∈ Λ_{τ} | ∃e ∈ Λ . λβτ ⊢ T ⟨[e]⟩ ⟶ ⟶ t}

The set of terms T can be described with the following grammar.

t ∈ T ⟨[Λ]⟩^{∗}
t ::= b | force x | force (delay t) | λx.t | t_{0} (delay t_{1})

Appendix A.2.2 shows that the language T ⟨[Λ]⟩^{∗} = T. Note that every β-redex in T ⟨[Λ]⟩^{∗} is also a β_{v}-redex (since all function arguments are suspensions).

2.3 A thunk-based simulation

We want to show that thunks are sufficient for establishing a call-by-name simulation satisfying all of the correctness properties of the continuationpassing simulation C_{n}. Specifically, we prove the following theorem which recasts the correctness theorem for C_{n} (Theorem 3) in terms of T .^{16}

Theorem 5 For all e ∈ Programs[Λ] and e_{1}, e_{2} ∈ Λ,

1. Indifference: eval_{v}(T ⟨[e]⟩) ≃ eval_{n}(T ⟨[e]⟩)

2. Simulation: T ⟨[eval_{n}(e)]⟩ ≃_{τ} eval_{v}(T ⟨[e]⟩)

16The last two assertions of the Translation component of Theorem 3 do not appear here since the identity function as the initial continuation only plays a role in CPS evaluation.

e_{0} ∼^{τ} T ⟨[e_{0}]⟩  ^{e_{1} ∼^{τ} t_{1}^{j}}  ^{e_{2} ∼^{τ} t_{2}^{j}}  .....^{⟼_{β_{v}}  ⟼_{β_{v}}  ⟼_{β_{v}}}^{⟼_{τ}^{∗}  ⟼_{τ}^{∗}}^{t_{1}^{1}  t_{2}^{1}}^{T ⟨[e_{0}]⟩  t_{1}^{i_{1}}  t_{2}^{i_{2}}} e_{0}  e_{1}  e_{2}  ..... ⟼_{n}  ⟼_{n}  ⟼_{n}

Figure 6: Evaluation of thunked terms

3. Translation: λβ ⊢ e_{1} = e_{2} iff λβ_{v}τ ⊢ T ⟨[e_{1}]⟩ = T ⟨[e_{2}]⟩ iff λβτ ⊢ T ⟨[e_{1}]⟩ = T ⟨[e_{2}]⟩

2.3.1 Indifference

The Indifference property for T is immediate since all function arguments are values (specifically suspensions) in the language T ⟨[Λ]⟩^{∗}.

2.3.2 Simulation

In general, the steps involved in T ⟨[eval_{n}(e)]⟩ and eval_{v}(T ⟨[e]⟩) can be pictured as in Figure 6 (in the figure, ⟼_{τ} and ⟼_{β_{v}} denote ⟼_{v} steps which correspond to τ and β_{v} reduction, respectively).^{17} Initially, T ⟨[e_{0}]⟩ ⟼_{β_{v}} t_{1}^{1} where t_{1}^{1} is related to e_{1} by the following inductively defined relation ∼^{τ}.

\begin{matrix}∼^{τ}.1 & b ∼^{τ} b \\ ∼^{τ}.2 & x ∼^{τ} force x \\ ∼^{τ}.3 & \frac{e ∼^{τ} t}{λx.e ∼^{τ} λx.t} \end{matrix} ∼^{τ}.4 \begin{matrix}e_{0} & ∼^{τ} & t_{0} & e_{1} & ∼^{τ} & t_{1} \\ e_{0} e_{1} & ∼^{τ} & t_{0} (delay t_{1}) \end{matrix}

∼^{τ}.5 \frac{e ∼^{τ} t}{e ∼^{τ} force (delay t)}

17 Note that Simulation for T holds up to τ-equivalence because T commutes with substitution up to τ-equivalence. Taking e = (λx.λy.x) b illustrates that T ⟨[eval_{n}(e)]⟩ may be in τ-normal form where eval_{v}(T ⟨[e]⟩) may contain τ-redexes inside the body of a resulting abstraction.

T^{−1} : T ⟨[Λ]⟩^{∗} →Λ
T^{−1}⟨[b]⟩ = b
T^{−1}⟨[force x]⟩ = x
T^{−1}⟨[force (delay t)]⟩ = T^{−1}⟨[t]⟩
T^{−1}⟨[λx.t]⟩ = λx.T^{−1}⟨[t]⟩
T^{−1}⟨[t_{0} (delay t_{1})]⟩ = T^{−1}⟨[e_{0}]⟩ T^{−1}⟨[e_{1}]⟩

Figure 7: Thunk elimination

Simple inductions show that e ∼^{τ} T ⟨[e]⟩, and that e ∼^{τ} t implies T ⟨[e]⟩ is τ-equivalent to t.

Now for the remaining steps in Figure 6, the following property states that each ⟼_{n} step on a Λ term implies corresponding ⟼_{v} steps on appropriately related thunked terms.

Property 1 For all e_{0}, e_{1} ∈ Programs[Λ] and t_{0} ∈ Programs[T ⟨[Λ]⟩^{∗}] such

that e_{0} ∼^{τ} t_{0},

e_{0} ⟼_{n} e_{1} ⇒ ∃t_{1} ∈ T ⟨[Λ]⟩^{∗} . t_{0} ⟼_{v}^{+} t_{1} ∧ e_{1} ∼^{τ} t_{1}

It is also the case that every terminating evaluation sequence over Λ terms corresponds to a terminating evaluation sequence over thunked terms (and vice-versa). These properties are sufficient for establishing the Simulation property for T (see Appendix A.2.3).

2.3.3 Translation

To prove the Translation for T , we establish an equational correspondence between the language Λ under theory λβ and language T ⟨[Λ]⟩^{∗} under theory λβ_{i}τ (i.e., λβ_{v}τ as well as λβτ). Basically, equational correspondence holds when a one-to-one correspondence exists between equivalence classes of the two theories.

The thunk introduction T of Figure 5 establishes a mapping from Λ to T ⟨[Λ]⟩^{∗}. For the reverse direction, the thunk elimination T^{−1} of Figure 7 establishes a mapping from T ⟨[Λ]⟩^{∗} back to Λ.

The relationship between equational theories for source terms and thunked terms is as follows.

Theorem 6 (Equational Correspondence) For all e, e_{1}, e_{2} ∈ Λ and t, t_{1}, t_{2} ∈ T ⟨[Λ]⟩^{∗},

1. λβ ⊢ e = (T^{−1} ∘ T )⟨[e]⟩

2. λβ_{i}τ ⊢ t = (T ∘ T^{−1})⟨[t]⟩

3. λβ ⊢ e_{1} = e_{2} iff λβ_{i}τ ⊢ T ⟨[e_{1}]⟩ = T ⟨[e_{2}]⟩
4. λβ_{i}τ ⊢ t_{1} = t_{2} iff λβ ⊢ T^{−1}⟨[t_{1}]⟩ = T^{−1}⟨[t_{2}]⟩

Note that component 3 of Theorem 6 corresponds to the thunk Translation property (component 3 of Theorem 5).

The proof of Theorem 6 follows the outline of a proof with similar structure given by Sabry and Felleisen [31]. First, we characterize the interaction of T and T^{−1} (components 1 and 2 of Theorem 6). Then, we examine the relation between reductions in the theories λβ and λβ_{i}τ (components 3 and 4 of Theorem 6).

The following property states that T^{−1} ∘ T is the identity function over Λ.

Property 2 For all e ∈ Λ, e = (T^{−1} ∘ T )⟨[e]⟩.

This follows from the fact that T^{−1} simply removes all suspension operators. However, removing suspension operators has the effect of collapsing τ-redexes. This leads to a slightly weaker condition for the opposite direction.

Property 3 For all t ∈ T ⟨[Λ]⟩^{∗}, λτ ⊢ t = (T ∘ T^{−1})⟨[t]⟩.

In other words, T ∘ T^{−1} is not the identity function, but maintains τequivalence. For example,

(T ∘ T^{−1})⟨[(λx.force (delay b)) (delay b)]⟩ = T ⟨[(λx.b) b]⟩
= (λx.b) (delay b).

Components 1 and 2 of Theorem 6 follow immediately from Properties 2 and 3.

For components 3 and 4 of Theorem 6, it is sufficient to establish the following two properties. The first property shows that any reduction in Λ corresponds to one or more reductions in T ⟨[Λ]⟩^{∗}.

Property 4 For all e_{1}, e_{2} ∈ Λ,

λβ ⊢ e_{1} ⟶ e_{2} ⇒ λβ_{i}τ ⊢ T ⟨[e_{1}]⟩ ⟶ ⟶ T ⟨[e_{2}]⟩.

For example, the β-reduction

λβ ⊢ e_{1} ≡ (λx.x b) (λy.y) ⟶ (λy.y) b ≡ e_{2}

corresponds to the β_{i}-reduction

λβ_{i}τ ⊢ T ⟨[e_{1}]⟩ ≡ (λx.(force x) (delay b)) (delay (λy.force y)) ⟶ (force (delay (λy.force y))) (delay b)

However, an additional τ-reduction (and in general multiple τ-reductions) is needed to reach T ⟨[e_{2}]⟩, i.e.,

λβ_{i}τ ⊢ (force (delay (λy.force y))) (delay b) ⟶ (λy.force y) (delay b) ≡ T ⟨[e_{2}]⟩ .

For the other direction, the following property states that any reduction in T ⟨[Λ]⟩^{∗} corresponds to zero or one reductions in Λ.

Property 5 For all t_{1}, t_{2} ∈ T ⟨[Λ]⟩^{∗},

λβ_{i}τ ⊢ t_{1} ⟶ t_{2} ⇒ λβ ⊢ T^{−1}⟨[t_{1}]⟩ ⟶ ⟶ T^{−1}⟨[t_{2}]⟩.

Specifically, a τ-reduction in T ⟨[Λ]⟩^{∗} implies no reductions in Λ. This is because T^{−1} collapses τ-redexes. For example,

λβ_{i}τ ⊢ t_{1} ≡ force (delay b) ⟶ b ≡ t_{2},

but T^{−1}⟨[t_{1}]⟩ = b = T^{−1}⟨[t_{2}]⟩, so no reductions occur.

A β_{i}-reduction in T ⟨[Λ]⟩^{∗} implies one β-reduction in Λ. For example, the β_{i}-reduction

λβ_{i}τ ⊢ t_{1} ≡ (λx.(force x) (delay b)) (delay (λy.force y)) ⟶ (force (delay λy.force y)) (delay b) ≡ t_{2}

corresponds to the β-reduction

λβ ⊢ T^{−1}⟨[t_{1}]⟩ ≡ (λx.x b) (λy.y) ⟶ (λy.y) b ≡ T^{−1}⟨[t_{2}]⟩.

Given these properties, components 3 and 4 of Theorem 6 can be proved in a straightforward manner by appealing to Church-Rosser and compatibility properties of β and β_{i}τ reduction (see Appendix A.2.4).

2.4 Thunks implemented in Λ

Representing thunks via abstract suspension operators delay and force simplifies the technical presentation and enables the connection between C_{n} and C_{v} presented in the next section. Elsewhere [15], we show that the delay/force representation of thunks and associated properties (i.e., reduction properties and translation into CPS) are not arbitrary, but are determined by the relationship between strictness and continuation monads [19].

However, thunks can be implemented directly in Λ using what Plotkin described as the “protecting by a λ” technique [23, p. 147]. Specifically, an expression is delayed by wrapping it in an abstraction with a dummy parameter. A suspension is forced by applying it to a dummy argument. The following transformation encodes Λ_{τ} terms using this technique (we only show the transformation on suspension operators).

L : Λ_{τ} →Λ
...
L⟨[delay e]⟩ = λz.L⟨[e]⟩  ...where z ∉ FV(e)
L⟨[force e]⟩ = e b

This implementation of delay and force preserves the two basic properties of suspensions:

1. L⟨[delay e]⟩ = λz.L⟨[e]⟩ is a value; and

2. τ-reduction is faithfully implemented in both the call-by-name and call-by-value calculi, i.e.,

L⟨[force (delay e)]⟩ = (λz.L⟨[e]⟩) b ⟶_{β_{i}} L⟨[e]⟩.

Now, by composing L with T we obtain the thunk-introducing transformation T_{L} of Figure 8 that implements thunks directly in Λ. The following theorem recasts the correctness theorem for C_{n} (Theorem 3) in terms of T_{L}.

Theorem 7 For all e ∈ Programs[Λ] and e_{1}, e_{2} ∈ Λ,

1. Indifference: eval_{v}(T_{L}⟨[e]⟩) ≃ eval_{n}(T_{L}⟨[e]⟩)

2. Simulation: T_{L}⟨[eval_{n}(e)]⟩ ≃_{β_{i}} eval_{v}(T_{L}⟨[e]⟩)

3. Translation: λβ ⊢ e_{1} = e_{2} iff λβ_{v} ⊢ T_{L}⟨[e_{1}]⟩ = T_{L}⟨[e_{2}]⟩ iff λβ ⊢ T_{L}⟨[e_{1}]⟩ = T_{L}⟨[e_{2}]⟩

T_{L} : Λ→Λ
T_{L}⟨[b]⟩ = b
T_{L}⟨[x]⟩ = x b  ...for some arbitrary basic constant b
T_{L}⟨[λx.e]⟩ = λx.T_{L}⟨[e]⟩
T_{L}⟨[e_{0} e_{1}]⟩ = T_{L}⟨[e_{0}]⟩ (λz.T_{L}⟨[e_{1}]⟩)  ...where z ∉ FV(e_{1})

Figure 8: Thunk introduction implemented in Λ

Proof: The proofs for T_{L} may be carried out directly using the same techniques as for T . It is simpler, however, to take advantage of the fact that T_{L} = L ∘ T and reason indirectly. Specifically, one can show that for all t ∈ Programs[T ⟨[Λ]⟩^{∗}], L⟨[eval_{v}(t)]⟩ ≃ eval_{i}(L⟨[t]⟩). Additionally, L and its inverse L^{−1} establish an equational correspondence between T ⟨[Λ]⟩^{∗} and T_{L}⟨[Λ]⟩^{∗} (terms in the image of T_{L} closed under β_{i} reduction). Now composing these results for L with Theorem 5 for T establishes each component of the current theorem (see Appendix A.3).

3 Connecting the Thunk-based and the Continuation-based Simulations

We now extend Plotkin’s C_{v} to a call-by-value CPS transformation C_{v}^{+} that handles suspension operators delay and force. Clearly C_{v}^{+} should preserve call-by-value meaning, but in the case of thunked terms, call-by-value evaluation gives call-by-name meaning. Therefore, one would expect the result of C_{v}^{+} ∘ T to be continuation-passing terms that encode call-by-name meaning. In fact, we show that for all e ∈ Λ, (C_{v}^{+} ∘ T )⟨[e]⟩ is identical to C_{n}⟨[e]⟩ modulo administrative reductions. As a byproduct, C_{n} can be factored as C_{v}^{+} ∘ T as captured by the following diagram.

[figure: Λ; C_{n}; T; T ⟨[Λ]⟩^{∗}; C_{v}^{+}; CPS terms]

We give several applications of this factorization.

3.1 CPS transformation of thunk constructs

We begin by extending C_{v} to transform delay and force — thereby obtaining the transformation C_{v}^{+}. The definitions follow directly from the two basic properties of thunks: delay e is a value; and force (delay e) ⟶_{τ} e.

First, since delay e ∈ Values_{v}[Λ_{τ}], C_{v}^{+}⟨[delay e]⟩ = λk.k (C_{v}^{+}⟨delay e⟩). Notice that in the definition of C_{v} (see Figure 4) all expressions C_{v}⟨[e]⟩ require a continuation for evaluation. Therefore, an expression is delayed by simply not passing it a continuation, i.e., C_{v}^{+}⟨delay e⟩ = C_{v}^{+}⟨[e]⟩. As required, C_{v}^{+}⟨[e]⟩ is a value. This effectively implements delay by “protecting by a λ”. However, the “protecting λ” is not associated with a dummy parameter but with the continuation parameter in C_{v}^{+}⟨delay e⟩ = C_{v}^{+}⟨[e]⟩.

Since the suspension of an expression is achieved by depriving it of a continuation, a suspension is naturally forced by supplying it with a continuation.^{18} This leads to the following definition.

C_{v}^{+}⟨[force e]⟩ = λk.C_{v}^{+}⟨[e]⟩ (λv.v k)

The following property shows that C_{v}^{+} faithfully implements τ-reduction.

Property 6 For all e ∈ Λ_{τ}, λβ_{i} ⊢ C_{v}^{+}⟨[force (delay e)]⟩ = C_{v}^{+}⟨[e]⟩

Proof:

C_{v}^{+}⟨[force (delay e)]⟩  =  λk.(λk.k (C_{v}^{+}⟨[e]⟩)) (λv.v k)
⟶_{β_{i}} λk.(λv.v k) C_{v}^{+}⟨[e]⟩
⟶_{β_{i}} λk.C_{v}^{+}⟨[e]⟩ k
⟶_{β_{i}} C_{v}^{+}⟨[e]⟩

18These encodings of thunks with continuations are well-known to functional programmers. For example, they can be found in Dupont’s PhD thesis [11].

C_{v}^{+}⟨[·]⟩ : Λ_{τ} →Λ
...
C_{v}^{+}⟨[force e]⟩ = λk.C_{v}^{+}⟨[e]⟩ (λy.y k)

C_{v}^{+}⟨·⟩ : Values_{v}[Λ_{τ}]→Λ
...
C_{v}^{+}⟨delay e⟩ = C_{v}^{+}⟨[e]⟩

Figure 9: Call-by-value CPS transformation (extended to thunks)

The last step holds since a straightforward case analysis shows that C_{v}^{+}⟨[e]⟩ always has the form λk.e′ for some e′ ∈ Λ.

The clauses of Figure 9 extend the definition of C_{v} in Figure 4. The properties of C_{v} as stated in Theorem 4 can be extended to the transformation C_{v}^{+}.^{19}

Theorem 8 For all t ∈ Programs[T ⟨[Λ]⟩^{∗}] and t_{1}, t_{2} ∈ T ⟨[Λ]⟩^{∗},

1. Indifference: eval_{n}(C_{v}^{+}⟨[t]⟩ I ) ≃ eval_{v}(C_{v}^{+}⟨[t]⟩ I )

2. Simulation: C_{v}^{+}⟨eval_{v}(t)⟩ ≃ eval_{n}(C_{v}^{+}⟨[t]⟩ I )

3. Translation:

If λβ_{v}τ ⊢ t_{1} = t_{2} then λβ_{v} ⊢ C_{v}^{+}⟨[t_{1}]⟩ = C_{v}^{+}⟨[t_{2}]⟩

Also λβ_{v} ⊢ C_{v}^{+}⟨[t_{1}]⟩ = C_{v}^{+}⟨[t_{2}]⟩ iff λβ ⊢ C_{v}^{+}⟨[t_{1}]⟩ = C_{v}^{+}⟨[t_{2}]⟩ Proof: For Indifference and Simulation it is only necessary to extend Plotkin’s colon-translation proof technique and definition of stuck terms to account for delay and force. The proofs then proceed along the same lines as Plotkin’s original proofs for C_{v} [23, pp. 148–152] (see Appendix A.4). Translation follows from the Translation component of Theorem 4 and Property 6.

19One might expect Theorem 8 to hold for the more general Λ_{τ} instead of simply T ⟨[Λ]⟩^{∗}. However, Simulation fails for Λ_{τ} because some stuck Λ_{τ} programs do not stick when translated to CPS. For example, eval_{v}(force (λx.x)) sticks but eval_{n}(C_{v}^{+}⟨[force (λx.x)]⟩ (λy.y)) = λk.k (λy.y). This mismatch on sticking is due to “improper” uses of delay and force. The proof of Theorem 8 goes through since the syntax of T ⟨[Λ]⟩^{∗} only allows “proper” uses of delay and force. Furthermore, an analogue of Theorem 8 does hold for a typed version of Λ_{τ} (see [10, 15]) since well-typedness eliminates the possibility of stuck terms.

3.2 The connection between the thunk-based and continuationbased simulations

We now show the connection between the continuation-based simulations C_{n} and C_{v}^{+} and the thunk-based simulation T . C_{n} can be factored into two conceptually distinct steps:

• the suspension of argument evaluation (captured in T );

• the sequentialization of function application to give the usual tail-calls of CPS terms (captured in C_{v}^{+}).

Theorem 9 For all e ∈ Λ,

λβ_{i} ⊢ (C_{v}^{+} ∘ T )⟨[e]⟩ = C_{n}⟨[e]⟩

Proof: by induction over the structure of e:

case e ≡ b:

(C_{v}^{+} ∘ T )⟨[b]⟩ = C_{v}^{+}⟨[b]⟩
= λk.k b
= C_{n}⟨[b]⟩

case e ≡ x:

(C_{v}^{+} ∘ T )⟨[x]⟩ = C_{v}^{+}⟨[force x]⟩
= λk.(λk.k x) (λy.y k)
⟶_{β_{i}} λk.(λy.y k) x
⟶_{β_{i}} λk.x k
= C_{n}⟨[x]⟩

case e ≡ λx.e′:

(C_{v}^{+} ∘ T )⟨[λx.e′]⟩ = λk.k (λx.(C_{v}^{+} ∘ T )⟨[e′]⟩)
=_{β_{i}} λk.k (λx.C_{n}⟨[e′]⟩) ...by the ind. hyp.
= C_{n}⟨[λx.e′]⟩

C_{n.opt}⟨[·]⟩ : Λ→(Λ→Λ)→Λ
C_{n.opt}⟨[v]⟩ = \overline{λ}k.k\overline{@}C_{n.opt}⟨v⟩
C_{n.opt}⟨[x]⟩ = \overline{λ}k.x\underline{@}(\underline{λ}y.k\overline{@}y)
C_{n.opt}⟨[e_{0} e_{1}]⟩ = \overline{λ}k.C_{n.opt}⟨[e_{0}]⟩\overline{@}(\overline{λ}y_{0}.y_{0}\begin{matrix}\underline{@} & (\underline{λ}k.C_{n.opt}⟨[e_{1}]⟩\overline{@}(\overline{λ}y_{1}.k\underline{@}y_{1})) \\ \underline{@} & (\underline{λ}y_{2}.k\overline{@}y_{2})) \end{matrix}

C_{n.opt}⟨·⟩ : Values_{n}[Λ]→Λ
C_{n.opt}⟨b⟩ = b
C_{n.opt}⟨λx.e⟩ = \underline{λ}x.\underline{λ}k.C_{n.opt}⟨[e]⟩\overline{@}(\overline{λ}y.k\underline{@}y)

Figure 10: Optimizing call-by-name CPS transformation

case e ≡ e_{0} e_{1}:

(C_{v}^{+} ∘ T )⟨[e_{0} e_{1}]⟩ = C_{v}^{+}⟨[T ⟨[e_{0}]⟩ (delay T ⟨[e_{1}]⟩)]⟩
=λk.(C_{v}^{+} ∘ T )⟨[e_{0}]⟩ (λy_{0}.(λk.k (C_{v}^{+} ∘ T )⟨[e_{1}]⟩) (λy_{1}.y_{0} y_{1} k))
⟶_{β_{i}} λk.(C_{v}^{+} ∘ T )⟨[e_{0}]⟩ (λy_{0}.(λy_{1}.y_{0} y_{1} k) (C_{v}^{+} ∘ T )⟨[e_{1}]⟩)
⟶_{β_{i}} λk.(C_{v}^{+} ∘ T )⟨[e_{0}]⟩ (λy_{0}.y_{0} (C_{v}^{+} ∘ T )⟨[e_{1}]⟩ k)
=_{β_{i}} λk.C_{n}⟨[e_{0}]⟩ (λy_{0}.y_{0} C_{n}⟨[e_{1}]⟩ k) ...by the ind. hyp.
= C_{n}⟨[e_{0} e_{1}]⟩

Note that C_{v}^{+} ∘ T and C_{n} only differ by administrative reductions. In fact, if we consider versions of C_{n} and C_{v} which optimize by removing administrative reductions, then the correspondence holds up to identity (i.e., up to α-equivalence).

Figures 10 and 11 present the optimizing transformations C_{n.opt} and C_{v.opt} given by Danvy and Filinski [8, pp. 387 and 367].^{20} The transformations are presented in a two-level language à la Nielson and Nielson [21]. Operationally, the overlined λ’s and @’s correspond to functional abstractions and

20The output of C_{n.opt} is β_{v}η_{v} equivalent to the output of C_{n} (similarly for C_{v.opt} and C_{v}). A proof of Indifference and Simulation for C_{v.opt} is given in [8]. This proof extends to C_{v.opt}^{+} in a straightforward manner.

C_{v.opt}⟨[·]⟩ : Λ→(Λ→Λ)→Λ
C_{v.opt}⟨[v]⟩ = \overline{λ}k.k\overline{@}C_{v.opt}⟨v⟩
C_{v.opt}⟨[e_{0} e_{1}]⟩ = \overline{λ}k.C_{v.opt}⟨[e_{0}]⟩\overline{@}(\overline{λ}y_{0}.C_{v.opt}⟨[e_{1}]⟩\overline{@}(\overline{λ}y_{1}.y_{0}\underline{@}y_{1}\underline{@}(\underline{λ}y_{2}.k\overline{@}y_{2})))
C_{v.opt}⟨·⟩ : Values_{v}[Λ]→Λ
C_{v.opt}⟨b⟩ = b
C_{v.opt}⟨x⟩ = x
C_{v.opt}⟨λx.e⟩ = \underline{λ}x.\underline{λ}k.C_{v.opt}⟨[e]⟩\overline{@}(\overline{λ}y.k\underline{@}y)

Figure 11: Optimizing call-by-value CPS transformation

applications in the program implementing the translation, while the underlined λ’s and @’s represent abstract-syntax constructors. The figures can be transliterated into functional programs.

The optimizing transformation C_{v.opt}^{+} is obtained from C_{v.opt} by adding the following definitions.

C_{v.opt}^{+}⟨[force e]⟩ = \overline{λ}k.C_{v.opt}^{+}⟨[e]⟩\overline{@}(\overline{λ}y_{0}.y_{0}\underline{@}(\underline{λ}y_{1}.k\overline{@}y_{1}))
C_{v.opt}^{+}⟨delay e⟩ = \underline{λ}k.C_{v.opt}^{+}⟨[e]⟩\overline{@}(\overline{λ}y.k\underline{@}y)

Taking an operational view of these two-level specifications, the following theorem states that, for all e ∈ Λ, the result of applying C_{v.opt}^{+} to T ⟨[e]⟩ (with an initial continuation \overline{λ}a.a) is α-equivalent to the result of applying C_{n.opt} to e (with an initial continuation \overline{λ}a.a).

Theorem 10 For all e ∈ Λ,

(C_{v.opt}^{+} ∘ T )⟨[e]⟩ = C_{n.opt}⟨[e]⟩

Proof: A simple structural induction similar to the one required in the proof of Theorem 9. We show only the case for identifiers (the others are similar). The overlined constructs are computed at translation time, and thus simplifying overlined constructs using β-conversion yields equivalent specifications. case e ≡ x:

(C_{v.opt}^{+} ∘ T )⟨[x]⟩ = \overline{λ}k.(\overline{λ}k.k\overline{@}x)\overline{@}(\overline{λ}y.y\underline{@}(\underline{λ}y.k\overline{@}y))
= \overline{λ}k.(\overline{λ}y.y\underline{@}(\underline{λ}y.k\overline{@}y))\overline{@}x
= \overline{λ}k.x\underline{@}(\underline{λ}y.k\overline{@}y)
= C_{n.opt}⟨[x]⟩

3.3 Applications

3.3.1 Deriving correctness properties of C_{n}

When working with CPS, one often needs to establish technical properties for both a call-by-name and a call-by-value CPS transformation. This requires two sets of proofs that both involve CPS. By appealing to the factoring property, however, often only one set of proofs over call-by-value CPS terms is necessary. The second set of proofs deals with thunked terms which have a simpler structure. For instance, Indifference and Simulation for C_{n} follow from Indifference and Simulation for C_{v}^{+} and T and Theorem 9.^{21}

For Indifference, let e, b ∈ Λ where b is a basic constant. Then

eval_{v}(C_{n}⟨[e]⟩ (λy.y)) = b

⇔ eval_{v}((C_{v}^{+} ∘ T )⟨[e]⟩ (λy.y)) = b ...Theorem 9 and soundness of β_{v}
⇔ eval_{n}((C_{v}^{+} ∘ T )⟨[e]⟩ (λy.y)) = b ...Theorem 8 (Indifference)
⇔ eval_{n}(C_{n}⟨[e]⟩ (λy.y)) = b  ...Theorem 9 and soundness of β

For Simulation, let e, b ∈ Λ where b is a basic constant. Then

eval_{n}(e) = b

⇔ eval_{v}(T ⟨[e]⟩) = b  ...Theorem 5 (Simulation)
⇔ eval_{n}((C_{v}^{+} ∘ T )⟨[e]⟩ (λy.y)) = b ...Theorem 8 (Simulation)
⇔ eval_{v}((C_{v}^{+} ∘ T )⟨[e]⟩ (λy.y)) = b ...Theorem 8 (Indifference)
⇔ eval_{v}(C_{n}⟨[e]⟩ (λy.y)) = b  ...Theorem 9 and soundness of β_{v}

For Translation, it is not possible to establish Theorem 3 (Translation for C_{n}) in the manner above since Theorem 8 (Translation for C_{v}^{+}) is weaker in comparison. However, the following weaker version can be derived (the full version is proved in Appendix A.1.3). Let e_{1}, e_{2} ∈ Λ. Then

21Here we show only the results where evaluation is undefined or results in a basic constant b. Appendix A.1.2 gives the derivation of C_{n} Simulation for arbitrary results.

λβ ⊢ e_{1} = e_{2}
⇔ λβ_{v}τ ⊢ T ⟨[e_{1}]⟩ = T ⟨[e_{2}]⟩  ...Theorem 5 (Translation)
⇒ λβ_{i} ⊢ (C_{v}^{+} ∘ T )⟨[e_{1}]⟩ = (C_{v}^{+} ∘ T )⟨[e_{2}]⟩ ...Theorem 8 (Translation)
⇔ λβ_{i} ⊢ C_{n}⟨[e_{1}]⟩ = C_{n}⟨[e_{2}]⟩  ...Theorem 9
⇒ λβ_{i} ⊢ C_{n}⟨[e_{1}]⟩ I = C_{n}⟨[e_{2}]⟩ I  ...compatibility of =_{β_{i}}

3.3.2 Deriving a CPS transformation directed by strictness information

Strictness information indicates arguments that may be safely evaluated eagerly (i.e., without being delayed) — in effect, reducing the number of thunks needed in a program and the overhead associated with creating and evaluating suspensions [5, 10, 22]. In recent work [10], we gave a transformation T_{s} that optimizes thunk introduction based on strictness information.^{22} We then used the factorization of C_{n} by C_{v}^{+} and T to derive an optimized CPS transformation C_{s} for strictness-analyzed call-by-name terms. This situation is summarized by the following diagram.

Λ

C_{s}

[figure]

[figure]

T_{s}

+ strictness info

[figure]

(thunked & unthunked)

C_{v}^{+}

[figure]

CPS terms

The resulting transformation C_{s} yields both call-by-name-like and callby-value-like continuation-passing terms. Due to the factorization, the proof of correctness for the optimized transformation follows as a corollary of the correctness of the strictness analysis, and the correctness of T and C_{v}^{+}.

3.3.3 Deriving a call-by-need CPS transformation

Okasaki, Lee, and Tarditi [22] have also applied the factorization to obtain a “call-by-need CPS transformation” C_{need}. The lazy evaluation strategy characterizing call-by-need is captured by memoizing the thunks [5]. C_{need} is obtained by extending C_{v}^{+} to transform memo-thunks to CPS terms with store operations (which are used to implement the memoization) and composing with the memo-thunk introduction as follows.

22Amtoft [1] and Stecker and Wand [32] have proven the correctness of transformations which optimize the introduction of thunks based on strictness information.

Λ

C_{need}

[figure]

[figure]

T

[figure]

memo-thunks

C_{v}^{+}

[figure]

CPS terms

+ store operations

Okasaki et al. optimize C_{need} by using strictness information along the lines discussed above. They also use sharing information to detect where memo-thunks can be replaced by ordinary thunks. In both cases, optimizations are achieved by working with simpler thunked terms as opposed to working directly with CPS terms.

3.4 Assessment

Thunks can be used to factor a variety of call-by-name CPS transformations. In addition to those discussed here, we have factored a variant of Reynolds’s CPS transformation directed by strictness information [15, 26], as well as a call-by-name analogue of Fischer’s call-by-value CPS transformation [12, 31].

Obtaining the desired call-by-name CPS transformation via C_{v}^{+} and T depends on the representation of thunks. For example, if one works with T_{L} instead of T , C_{v} ∘ T_{L} still gives a valid CPS simulation of call-by-name by call-by-value. However, the following derivations show that β_{i} equivalence with C_{n} is not obtained (i.e., λβ_{i} ⊬ C_{n}⟨[e]⟩ = (C_{v} ∘ T_{L})⟨[e]⟩).

(C_{v} ∘ T_{L})⟨[x]⟩ = C_{v}⟨[x b]⟩
= λk.(x b) k
(C_{v} ∘ T_{L})⟨[e_{0} e_{1}]⟩ = C_{v}⟨[T_{L}⟨[e_{0}]⟩ (λz.T_{L}⟨[e_{1}]⟩)]⟩
= λk.(C_{v} ∘ T_{L})⟨[e_{0}]⟩ (λy.(y (λz.(C_{v} ∘ T_{L})⟨[e_{1}]⟩)) k)

The representation of thunks given by T_{L} is too concrete in the sense that the delaying and forcing of computation is achieved using specific instances

Γ ⊢ b : ι Γ ⊢ x : Γ(x)

\frac{Γ, x:σ_{1} ⊢ e : σ_{2}}{Γ ⊢ λx.e : σ_{1} →σ_{2}}  \frac{Γ ⊢ e_{0} : σ_{1} →σ_{2} Γ ⊢ e_{1} : σ_{1}}{Γ ⊢ e_{0} e_{1} : σ_{2}}

\begin{aligned}σ & ∈ & Types[Λ_{τ}] \\ σ & ::= & ι | σ_{1} →σ_{2} \end{aligned}  \begin{aligned}Γ & ∈ & Asm[Λ_{τ}] \\ Γ & ::= & · | Γ, x:σ \end{aligned}

Figure 12: Typing rules for Λ

of the more general abstraction and application constructs. When composed with T_{L}, C_{v} treats the specific instances of thunks in their full generality, and the resulting CPS terms contain a level of inessential encoding of delay and force.

4 Thunks in a Typed Setting

Plotkin’s continuation-passing transformations were originally stated in terms of untyped λ-calculi. These transformations have been shown to preserve well-typedness of terms [13, 14, 18, 20]. In this section, we introduce typing rules for the suspension operators of Λ_{τ} and show that the thunk transformation T also preserves well-typedness of terms. In addition, we show how the relationship between C_{v}^{+} ∘ T and C_{n} is reflected in transformations on types.

4.1 Thunk introduction for a typed language

Figure 12 presents type assignment rules for the language Λ [4]. Γ is a set {x_{1} : σ_{1}, ..., x_{n} : σ_{n}} of type assumptions for identifiers. We assume that the identifiers of Γ are pairwise distinct. Γ, x:σ abbreviates Γ ∪ {x : σ}.

Figure 13 presents type assignment rules for the language Λ_{τ}. A type constructor ˜· is added to type suspension constructs delay and force. σ̃ types a suspension (i.e., a thunk) that will yield a value of type σ when forced.^{23}

23Note that we use the same meta-variables (Γ for type assumptions, σ for types, and e for terms) for both Λ and Λ_{τ}. Ambiguity is avoided by subscripting the typing judgement symbol ⊢_{τ} for the language Λ_{τ}.

Γ ⊢_{τ} b : ι Γ ⊢_{τ} x : Γ(x)

\frac{Γ, x:σ_{1} ⊢_{τ} e : σ_{2}}{Γ ⊢_{τ} λx.e : σ_{1} →σ_{2}}  \frac{Γ ⊢_{τ} e_{0} : σ_{1} →σ_{2} Γ ⊢_{τ} e_{1} : σ_{1}}{Γ ⊢_{τ} e_{0} e_{1} : σ_{2}}

\frac{Γ ⊢_{τ} e : σ}{Γ ⊢_{τ} delay e : σ̃}  \frac{Γ ⊢_{τ} e : σ̃}{Γ ⊢_{τ} force e : σ}

\begin{aligned}σ & ∈ & Types[Λ_{τ}] \\ σ & ::= & ι | σ_{1} →σ_{2} | σ̃ \end{aligned}  \begin{aligned}Γ & ∈ & Asm[Λ_{τ}] \\ Γ & ::= & · | Γ, x:σ \end{aligned}

Figure 13: Typing rules for Λ_{τ}

T ⟨[·]⟩ : Types[Λ]→Types[Λ_{τ}]
T ⟨[ι]⟩ = ι
T ⟨[σ_{1} →σ_{2}]⟩ = { \atop T ⟨[σ_{1}]⟩}→T ⟨[σ_{2}]⟩

T ⟨[·]⟩ : Asm[Λ]→Asm[Λ_{τ}]
T ⟨[Γ, x:σ]⟩ = T ⟨[Γ]⟩, x:{ \atop T ⟨[σ]⟩}

Figure 14: Transformation on types for T

Figure 14 presents the type transformation for T . The definition of T on function types and on type assumptions reflects the fact that all function arguments are thunks in the image of T .

The following property states that T preserves well-typedness of terms.

Property 7 If Γ ⊢ e : σ then T ⟨[Γ]⟩ ⊢_{τ} T ⟨[e]⟩ : T ⟨[σ]⟩.

Proof: by induction over the derivation of Γ ⊢ e : σ.

4.2 CPS transformations for a typed language

Figures 15 and 16 present the type transformations for C_{n} and C_{v} (where Ans is a distinguished type of final answers [18]). The definition of C_{n} on

C_{n}⟨[·]⟩ : Types[Λ]→Types[Λ]
C_{n}⟨[σ]⟩ = (C_{n}⟨σ⟩→Ans)→Ans
C_{n}⟨ι⟩ = ι
C_{n}⟨σ_{1} →σ_{2}⟩ = C_{n}⟨[σ_{1}]⟩→C_{n}⟨[σ_{2}]⟩

C_{n}⟨[·]⟩ : Asm[Λ]→Asm[Λ]
C_{n}⟨[Γ, x:σ]⟩ = C_{n}⟨[Γ]⟩, x:C_{n}⟨[σ]⟩

Figure 15: Transformation on types for C_{n}

C_{v}⟨[·]⟩ : Types[Λ]→Types[Λ]
C_{v}⟨[σ]⟩ = (C_{v}⟨σ⟩→Ans)→Ans
C_{v}⟨ι⟩ = ι
C_{v}⟨σ_{1} →σ_{2}⟩ = C_{v}⟨σ_{1}⟩→C_{v}⟨[σ_{2}]⟩

C_{v}⟨[·]⟩ : Asm[Λ]→Asm[Λ]
C_{v}⟨[Γ, x:σ]⟩ = C_{v}⟨[Γ]⟩, x:C_{v}⟨σ⟩

Figure 16: Transformation on types for C_{v}

function types and on type assumptions reflects the fact that source functions are translated to functions whose arguments are expressions needing a continuation. The definition of C_{v} on function types and on type assumptions reflects the fact that source functions are translated to functions whose arguments are values.

The following property states that C_{n} and C_{v} preserve well-typedness of terms.

Property 8 • If Γ ⊢ e : σ then C_{n}⟨[Γ]⟩ ⊢ C_{n}⟨[e]⟩ : C_{n}⟨[σ]⟩.

• If Γ ⊢ e : σ then C_{v}⟨[Γ]⟩ ⊢ C_{v}⟨[e]⟩ : C_{v}⟨[σ]⟩.

Proof: by induction over the derivation of Γ ⊢ e : σ (see [13, 14, 18, 20] for further details).

4.3 Connecting the thunk-based and the continuation-based simulations

The following definition extends C_{v} to the types of Λ_{τ}.

C_{v}^{+}⟨σ̃⟩ = C_{v}^{+}⟨[σ]⟩

This reflects the fact that suspensions are translated to terms expecting a continuation (see Figure 9). It is simple to show that the well-typedness property for C_{v} (Property 8) extends to C_{v}^{+}.

The factoring of C_{n} by T and C_{v}^{+} (Theorem 9) is reflected in the transformations on types as follows.

Property 9

1. C_{v}^{+}⟨[T ⟨[σ]⟩]⟩ = C_{n}⟨[σ]⟩  types
2. C_{v}^{+}⟨T ⟨[σ]⟩⟩ = C_{n}⟨σ⟩  value types
3. C_{v}^{+}⟨[T ⟨[Γ]⟩]⟩ = C_{n}⟨[Γ]⟩  type assumptions

Proof: The proof of components 1 and 2 proceeds by induction over the structure of σ. The case of function types for values is as follows.

C_{v}⟨T ⟨[σ_{1} →σ_{2}]⟩⟩ = C_{v}^{+}⟨{ \atop T ⟨[σ_{1}]⟩}→T ⟨[σ_{2}]⟩⟩
= C_{v}^{+}⟨{ \atop T ⟨[σ_{1}]⟩}⟩→C_{v}^{+}⟨[T ⟨[σ_{2}]⟩]⟩
= C_{v}^{+}⟨[T ⟨[σ_{1}]⟩]⟩→C_{v}^{+}⟨[T ⟨[σ_{2}]⟩]⟩
= C_{n}⟨[σ_{1}]⟩→C_{n}⟨[σ_{2}]⟩  ...by ind. hyp.
= C_{n}⟨σ_{1} →σ_{2}⟩

4.4 Assessment

C_{n} and C_{v} are alike in that they both introduce continuation-passing terms. This is reflected by the similarity in the definitions C_{n}⟨[σ]⟩ = (C_{n}⟨σ⟩→Ans)→Ans and C_{v}⟨[σ]⟩ = (C_{v}⟨σ⟩→Ans)→Ans. C_{n} and C_{v} differ in how arguments are treated. This is reflected by the difference in the definitions C_{n}⟨σ_{1} →σ_{2}⟩ = C_{n}⟨[σ_{1}]⟩→C_{n}⟨[σ_{2}]⟩ and C_{v}⟨σ_{1} →σ_{2}⟩ = C_{v}⟨σ_{1}⟩→C_{v}⟨[σ_{2}]⟩. The only effect of T is to change how arguments are treated. This is reflected by the fact that the only effect of T on types is the introduction of suspension types for arguments, i.e., T ⟨[σ_{1} →σ_{2}]⟩ = { \atop T ⟨[σ_{1}]⟩}→T ⟨[σ_{2}]⟩. Thus, the action by T is exactly what is needed to move from C_{v}^{+} to C_{n}.

5 Related Work

Ingerman [17], in his work on the implementation of Algol 60, gave a general technique for generating machine code implementing procedure parameter passing. The term thunk was coined to refer to the compiled representation of a delayed expression as it gets pushed on the control stack [25]. Since then, the term thunk has been applied to other higher-level representations of delayed expressions and we have followed this practice.

Bloss, Hudak, and Young [5] study thunks as the basis of implementation of lazy evaluation. Optimizations associated with lazy evaluation (e.g., overwriting a forced expression with its resulting value) are encapsulated in the thunk. They give several representations with differing effects on space and time overhead.

Riecke [28] has used thunks to obtain fully-abstract translations between versions of PCF with differing evaluation strategies. In effect, he establishes a fully-abstract version of the Simulation property of Theorem 7.^{24} The thunk translation required for full abstraction is much more complicated than our transformation T and consequently it cannot be used to factor C_{n}. In addition, since Riecke’s translation is based on typed-indexed retractions, it does not seem possible to use it (and the corresponding results) in an untyped setting as we require here.

Asperti and Curien give an interesting formulation of thunks in a categorical setting [2, 7]. Two combinators freeze and unfreeze, which are analogous to our delay and force but have slightly different equational properties, are used to implement lazy evaluation in the Categorical Abstract Machine. In addition, freeze and unfreeze can be elegantly characterized using a comonad.

6 Conclusion

The technique of thunks has been widely applied in both theory and practice. Our aim has been to clarify the properties of thunks with respect to Plotkin’s classic study of evaluation strategies and continuation-passing styles [23].

We have shown that all of the correctness properties of the continuationbased simulation C_{n} can be obtained via a simpler thunk-based transformation T . As a consequence, simulating call-by-name operational behavior and equational reasoning in a call-by-value setting are simpler than with C_{n}.

24The Indifference property is also immediate for Riecke since all function arguments are values in the image of his translation (and this property is maintained under reductions).

Furthermore, we have shown that the thunk transformation T establishes a previously unrecognized connection between the simulations C_{n} and C_{v} — C_{n} can be obtained by composing C_{v}^{+} with T . The benefit is that almost all the technical properties of C_{n} follow from the formal properties of C_{v}^{+} and T . T can also be used to factor a call-by-name version of Fischer’s call-by-value CPS transformation F as used by Sabry and Felleisen [31], and also to factor a variant of Reynolds’s CPS transformation directed by strictness information [15]. These factorings prove useful in several applications dealing with the implementation of call-by-name and lazy languages [10, 22].

For simplicity, we have presented both the simulation and the factorization results for thunks using simple Λ terms. However, the results scale up to more realistic languages with e.g., primitive operators, products and co-products, and recursive functions [15]. In a preliminary version of Section 3.2 [9], we presented the factorization of C_{n} via C_{v}^{+} and T , for the untyped λ-calculus with n-ary functions (à la Scheme [6]).

This work is part of a broader investigation of the structure of continuation-passing styles. Elsewhere [15, 16] we have shown how structural relationships between many different continuation-passing styles can be exploited to simplify transformations, correctness proofs, and reasoning about CPS programs. This investigation aims to clarify intuition and to aid in understanding the often complicated structure of CPS programs.

Acknowledgements

Andrzej Filinski, Julia Lawall, Sergey Kotov and David Schmidt gave helpful comments on earlier drafts of this paper. Thanks are also due to Dave Sands for several useful discussions. Finally, we are grateful to the reviewers.

The diagrams of Section 3 were drawn with Kristoffer Rose’s XY-pic package.

A Proofs

A.1 Correctness of C_{n}

A.1.1 Indifference

One may appeal to the factoring of C_{n} to prove Indifference for C_{n} up to β-equivalence. The proof is similar to the proof of Simulation in the following section. To prove Indifference up to α-equivalence (as stated in Theorem 3), consider the following grammar.^{25}

\begin{aligned}u & ∈ & Λ_{cps} \\ u & ::= & w | u w \end{aligned}  \begin{aligned}w & ∈ & Values[Λ_{cps}] \\ w & ::= & b | x | λx.u \end{aligned}

An induction on the structure of e ∈ Λ shows that C_{n}⟨[e]⟩ ∈ Values[Λ_{cps}]. It then follows that C_{n}⟨[e]⟩ (λx.x) ∈ Λ_{cps}. Now Indifference for C_{n} follows from the fact that for all u ∈ Programs[Λ_{cps}], u ⟼_{n} u′ iff u ⟼_{v} u′ (and moreover u′ ∈ Programs[Λ_{cps}]).

A.1.2 Simulation

Simulation for C_{n} can be derived by appealing to the factoring of C_{n}. Let e ∈ Λ. Then

C_{n}⟨eval_{n}(e)⟩ ≃_{β_{i}} C_{v}^{+}⟨T ⟨[eval_{n}(e)]⟩⟩

...factoring of C_{n} (Theorem 9)

≃_{β_{i}} C_{v}^{+}⟨eval_{v}(T ⟨[e]⟩)⟩

...T Simulation (Theorem 5) and C_{v}^{+} Translation (Theorem 8)

≃ eval_{n}((C_{v}^{+} ∘ T )⟨[e]⟩ (λx.x))

...C_{v}^{+} Simulation (Theorem 8)

≃ eval_{v}((C_{v}^{+} ∘ T )⟨[e]⟩ (λx.x))

...C_{v}^{+} Indifference (Theorem 8)

≃_{β_{i}} eval_{v}(C_{n}⟨[e]⟩ (λx.x))

...factoring of C_{n} (Theorem 9) and soundness of β_{v} (Theorem 1)

A.1.3 Translation

Section 3.3.1 shows that the following portion of Translation for C_{n} can be derived from the correctness properties of C_{v}^{+} and T . Let e_{1}, e_{2} ∈ Λ.

If λβ ⊢ e_{1} = e_{2} then λβ_{v} ⊢ C_{n}⟨[e_{1}]⟩ = C_{n}⟨[e_{2}]⟩
Also λβ_{v} ⊢ C_{n}⟨[e_{1}]⟩ = C_{n}⟨[e_{2}]⟩ iff λβ ⊢ C_{n}⟨[e_{1}]⟩ = C_{n}⟨[e_{2}]⟩
iff λβ_{v} ⊢ C_{n}⟨[e_{1}]⟩ I = C_{n}⟨[e_{2}]⟩ I iff λβ ⊢ C_{n}⟨[e_{1}]⟩ I = C_{n}⟨[e_{2}]⟩ I

It only remains to show the converse of the first implication. For this, it is sufficient to show λβ ⊢ C_{n}⟨[e_{1}]⟩ I = C_{n}⟨[e_{2}]⟩ I implies λβ ⊢ e_{1} = e_{2} which follows immediately from Plotkin’s original proof for P_{n}. The relevant section of the proof begins at the second paragraph under “Proof of Theorem 6” [23, p. 158]. One only needs to show that for all e ∈ Λ, e ∼^{∘} C_{n}⟨[e]⟩ I (where ∼^{∘} is defined by Plotkin) and this follows by a straightforward induction over the structure of e.

25Suggested by Kristian Nielsen and Morten Heine Sørensen.

A.2 Correctness of T

A.2.1 Preliminaries

The definition of stuck terms is extended from Λ (see Section 1.4.4) to Λ_{τ} as follows.

s ∈ Stuck_{n}[Λ_{τ}]
s ::= ... | (delay e_{0}) e_{1} | force b | force λx.e | force s
...where e, e_{0}, e_{1} ∈ Λ_{τ}
s ∈ Stuck_{v}[Λ_{τ}]
s ::= ... | (delay e_{0}) e_{1} | force b | force λx.e | force s
...where e, e_{0}, e_{1} ∈ Λ_{τ}

A simple induction over the structure of e ∈ Programs[Λ_{τ}] shows that either e ∈ Values_{n}[Λ_{τ}], or e ∈ Stuck_{n}[Λ_{τ}], or e ⟼_{n} e′ (similarly for call-by-value).

The following properties shows how T and T^{−1} interact with substitution.

Property 10 For all e_{1}, e_{2} ∈ Λ,

T ⟨[e_{1}]⟩[x := delay T ⟨[e_{2}]⟩] ⟶ ⟶_{τ} T ⟨[e_{1}[x := e_{2}]]⟩.

Proof: by induction over the structure of e_{1}. The interesting case is...

case e_{1} ≡ x :

T ⟨[x]⟩[x := delay T ⟨[e_{2}]⟩] = (force x)[x := delay T ⟨[e_{2}]⟩]
≡  force (delay T ⟨[e_{2}]⟩)
⟶_{τ} T ⟨[e_{2}]⟩
≡  T ⟨[x[x := e_{2}]]⟩

The rest of the cases follow trivially or by the induction hypothesis and compatibility of reductions.

Property 11 For all t_{1}, t_{2} ∈ T ⟨[Λ]⟩^{∗},

T^{−1}⟨[t_{1}]⟩[x := T^{−1}⟨[t_{2}]⟩] ≡ T^{−1}⟨[t_{1}[x := delay t_{2}]]⟩.

Proof: a simple induction over the structure of t_{1}.

A.2.2 The language T ⟨[Λ]⟩^{∗}

This section shows that the language T ⟨[Λ]⟩^{∗} (see Section 2.2.2) corresponds to the set of terms T reachable from the image of T via βτ reduction.

T =^{def} {t ∈ Λ_{τ} | ∃e ∈ Λ . λβτ ⊢ T ⟨[e]⟩ ⟶ ⟶ t}

First, we show that T ⟨[Λ]⟩^{∗} is closed under relevant substitutions (Property 12) and under βτ reduction (Property 13).

Property 12 For all t_{1}, t_{2} ∈ T ⟨[Λ]⟩^{∗}, t_{1}[x := delay t_{2}] ∈ T ⟨[Λ]⟩^{∗}.

Proof: by induction over the structure of t_{1}. The interesting case is...

case t_{1} ≡ force x: (force x)[x := delay t_{2}] = force (delay t_{2}) ∈ T ⟨[Λ]⟩^{∗}

The other cases are either trivial or follow from the induction hypothesis.

Property 13 For all t ∈ T ⟨[Λ]⟩^{∗}, λβτ ⊢ t ⟶ t′ implies t′ ∈ T ⟨[Λ]⟩^{∗}.

Proof: by induction over the structure of t. It is sufficient to show the following.

case t ≡ force (delay t′) ⟶_{τ} t′ ∈ T ⟨[Λ]⟩^{∗} case t ≡ (λx.t_{0}) (delay t_{1}) ⟶_{β} t_{0}[x := delay t_{1}] ∈ T ⟨[Λ]⟩^{∗}

...since T ⟨[Λ]⟩^{∗} is closed under substitution (Property 12)

To show that T ⟨[Λ]⟩^{∗} = T, it is shown that T ⊆ T ⟨[Λ]⟩^{∗} and T ⟨[Λ]⟩^{∗} ⊆ T.

Property 14 T ⊆ T ⟨[Λ]⟩^{∗}.

Proof: Let t ∈ T. From the definition of T there exists an e ∈ Λ such that λβτ ⊢ T ⟨[e]⟩ ⟶ ⟶ t in n steps. Now we show t ∈ T ⟨[Λ]⟩^{∗} by induction on n. case n = 0 : a simple induction over the structure of e shows T ⟨[e]⟩ ∈ T ⟨[Λ]⟩^{∗}. case n = i + 1 : then λβτ ⊢ T ⟨[e]⟩ ⟶ ⟶ t ⟶ u. By ind. hyp. t ∈ T ⟨[Λ]⟩^{∗} and therefore u ∈ T ⟨[Λ]⟩^{∗} since T ⟨[Λ]⟩^{∗} is closed under reduc- tions (Property 13).

Property 15 T ⟨[Λ]⟩^{∗} ⊆ T.

Proof: It is required to show that t ∈ T ⟨[Λ]⟩^{∗} implies t ∈ T, i.e., there exists an e ∈ Λ such that λβτ ⊢ T ⟨[e]⟩ ⟶ ⟶ t. The proof is by induction over the structure of t. The interesting case is...

case t ≡ force (delay t_{0}):

Since t_{0} ∈ T ⟨[Λ]⟩^{∗}, by the induction hypothesis there exists an e_{0} ∈ Λ such that λβτ ⊢ T ⟨[e_{0}]⟩ ⟶ ⟶ t_{0}. So take e ≡ (λx.x) e_{0}.

The stuck terms of T ⟨[Λ]⟩^{∗} are defined as follows.

s ∈ Stuck_{n}[T ⟨[Λ]⟩^{∗}]
s ::= b (delay t) | s (delay t)

s ∈ Stuck_{v}[T ⟨[Λ]⟩^{∗}]
s ::= b (delay t) | s (delay t)

...where t ∈ T ⟨[Λ]⟩^{∗}.

A simple induction over the structure of t ∈ Programs[T ⟨[Λ]⟩^{∗}] shows that either t ∈ Values_{n}[Λ_{τ}], or t ∈ Stuck_{n}[T ⟨[Λ]⟩^{∗}], or t ⟼_{n} t′ (similarly for call-by-value). Note that improper uses of delay and force (e.g., (delay e) b, force λx.e) which were present in the stuck terms of Λ_{τ} (see Appendix A.2.1) do not occur in T ⟨[Λ]⟩^{∗}. Intuitively, since T ⟨[Λ]⟩^{∗} simulates call-by-name evaluation, the stuck terms of T ⟨[Λ]⟩^{∗} parallel Stuck_{n}[Λ] (see Section 1.4.4).

A.2.3 Simulation

The proof for T Simulation proceeds as outlined in Section 2.3.2. The following property shows that all T ⟨[Λ]⟩^{∗} terms related by ∼^{τ} to a certain Λ term are τ equivalent.

Property 16 For all e ∈ Λ and for all t ∈ T ⟨[Λ]⟩^{∗} such that e ∼^{τ} t, λτ ⊢ T ⟨[e]⟩ = t.

Proof: by induction over the derivation of e ∼^{τ} t.

The following property shows how the relation ∼^{τ} interacts with substitution.

Property 17 For all e_{0}, e_{1} ∈ Λ and t_{0}, t_{1} ∈ T ⟨[Λ]⟩^{∗},

e_{0} ∼^{τ} t_{0} ∧ e_{1} ∼^{τ} t_{1} ⇒ e_{0}[x := e_{1}] ∼^{τ} t_{0}[x := delay t_{1}]

The following property expresses that evaluation of thunked terms may involve moving past initial τ reductions.

Property 18 For all e ∈ Programs[Λ] and t ∈ Programs[T ⟨[Λ]⟩^{∗}] such that

e ∼^{τ} t,

e ≡ b ∼^{τ} t ⇒ t ⟼_{v}^{∗} b
e ≡ λx.e_{0} ∼^{τ} t ⇒ t ⟼_{v}^{∗} λx.t_{0}  where e_{0} ∼^{τ} t_{0}
e ≡ e_{0} e_{1} ∼^{τ} t ⇒ t ⟼_{v}^{∗} t_{0} (delay t_{1}) where e_{0} ∼^{τ} t_{0} and e_{1} ∼^{τ} t_{1}

Proof: by induction over the derivation of e ∼^{τ} t. We show only the cases necessary for the second component (the others are similar).

case ∼^{τ}.3 : λx.e_{0} ∼^{τ} λx.t_{0} because e_{0} ∼^{τ} t_{0}: immediate case ∼^{τ}.5 : λx.e_{0} ∼^{τ} force (delay t′) because λx.e_{0} ∼^{τ} t′:

force (delay t′) ⟼_{v} t′
⟼_{v}^{∗} λx.t_{0}  where e_{0} ∼^{τ} t_{0}  ...by ind. hyp.

The following property (corresponding to Property 1 of Section 2.3.2) states that each ⟼_{n} step on a Λ program implies corresponding ⟼_{v} steps on a thunked program.

Property 19 (T — one step simulation) For all e_{0}, e_{1} ∈ Programs[Λ] and t_{0} ∈ Programs[T ⟨[Λ]⟩^{∗}] such that e_{0} ∼^{τ} t_{0},

e_{0} ⟼_{n} e_{1} ⇒ ∃t_{1} ∈ T ⟨[Λ]⟩^{∗} . t_{0} ⟼_{v}^{+} t_{1} ∧ e_{1} ∼^{τ} t_{1}

Proof: by induction over the derivation of e_{0} ⟼_{n} e_{1}. The proof uses Property 18 extensively.

case (λx.e_{a}) e_{b} ⟼_{n} e_{a}[x := e_{b}]:

t_{0} ⟼_{v}^{∗} t′_{a} (delay t_{b})  where λx.e_{a} ∼^{τ} t′_{a} and e_{b} ∼^{τ} t_{b}
⟼_{v}^{∗} (λx.t_{a}) (delay t_{b}) where e_{a} ∼^{τ} t_{a}
⟼_{v} t_{a}[x := delay t_{b}]

and e_{a}[x := e_{b}] ∼^{τ} t_{a}[x := delay t_{b}] by Property 17. case e_{a} e_{b} ⟼_{n} e′_{a} e_{b} because e_{a} ⟼_{n} e′_{a}:

t_{0} ⟼_{v}^{∗} t_{a} (delay t_{b}) where e_{a} ∼^{τ} t_{a} and e_{b} ∼^{τ} t_{b}
⟼_{v}^{+} t′_{a} (delay t_{b}) where e′_{a} ∼^{τ} t′_{a}  ...by ind. hyp.

and e′_{a} e_{b} ∼^{τ} t′_{a} (delay t_{b}) by rule ∼^{τ}.5.

The following property states that if a Λ program is stuck under eval_{n}, then all T ⟨[Λ]⟩^{∗} programs related to it by ∼^{τ} will reach a stuck program under eval_{v}.

Property 20 (T — coincidence of stuck terms) For all programs s ∈ Stuck_{n}[Λ] and t ∈ Programs[T ⟨[Λ]⟩^{∗}],

s ∼^{τ} t ⇒ ∃t′ ∈ T ⟨[Λ]⟩^{∗} . t ⟼_{v}^{∗} t′ ∧ t′ ∈ Stuck_{n}[T ⟨[Λ]⟩^{∗}] = Stuck_{v}[T ⟨[Λ]⟩^{∗}]

Proof: First, note that

Stuck_{n}[T ⟨[Λ]⟩^{∗}] = Stuck_{v}[T ⟨[Λ]⟩^{∗}]

(see Appendix A.2.1). The proof then proceeds by induction over the structure of s ∈ Stuck_{n}[Λ] (see Section 1.4.4) appealing to Property 18 at each step.

case s ≡ b e_{1}:

t ⟼_{v}^{∗} t_{b} (delay t_{1})  where b ∼^{τ} t_{b} and e_{1} ∼^{τ} t_{1}
⟼_{v}^{∗} b (delay t_{1})
∈ Stuck_{n}[T ⟨[Λ]⟩^{∗}]

case s ≡ s_{0} e_{1}:

t ⟼_{v}^{∗} t_{0} (delay t_{1})  where s_{0} ∼^{τ} t_{0} and e_{1} ∼^{τ} t_{1}
⟼_{v}^{∗} t_{s} (delay t_{1}) where t_{s} ∈ Stuck_{n}[T ⟨[Λ]⟩^{∗}] ...by ind. hyp.
∈ Stuck_{n}[T ⟨[Λ]⟩^{∗}]

Lemma 1 (T — simulation) For all e ∈ Programs[Λ],

T ⟨[eval_{n}(e)]⟩ ≃_{τ} eval_{v}(T ⟨[e]⟩)

Proof: case eval_{n}(e) is defined, i.e., e ⟼_{n}^{∗} v: Since e ∼^{τ} T ⟨[e]⟩, an induction over the number of steps in e ⟼_{n}^{∗} v (applying Property 19) gives T ⟨[e]⟩ ⟼_{v}^{∗} t where v ∼^{τ} t. Now by Property 18, one can see that for all closed values v ∈ Values_{n}[Λ], t ⟼_{v}^{∗} w where w ∈ Values_{v}[Λ_{τ}] and v ∼^{τ} w. Finally, λτ ⊢ T ⟨[v]⟩ = w by Property 16. case eval_{n}(e) is undefined: we have two cases: case e heads an infinite sequence e = e_{1} ⟼_{n} e_{2} ⟼_{n} ...: Since e ∼^{τ} T ⟨[e]⟩, applying Property 19 repeatedly gives an infinite sequence T ⟨[e]⟩ = t_{1} ⟼_{v}^{+} t_{2} ⟼_{v}^{+} ... and so eval_{v}(T ⟨[e]⟩) is undefined as well. case e ⟼_{n}^{∗} s ∈ Stuck_{n}[Λ]: Since e ∼^{τ} T ⟨[e]⟩, applying Property 19 repeatedly gives T ⟨[e]⟩ ⟼_{v}^{∗} t where s ∼^{τ} t. By Property 20, t ⟼_{v}^{∗} t_{s} ∈ Stuck_{v}[T ⟨[Λ]⟩^{∗}] and so eval_{v}(T ⟨[e]⟩) is undefined as well.

A.2.4 Translation

This section establishes the equational correspondence (Theorem 6) between the language Λ under theory λβ and language T ⟨[Λ]⟩^{∗} under theory λβ_{i}τ. This is sufficient for establishing the Translation property for T (Theorem 5).

Components 1 and 2 of Theorem 6 follow from Properties 2 and 3 of Section 2.3.3. Both of these properties follow from simple structural inductions and the proofs are omitted.

The following property (corresponding to Property 4 of Section 2.3.3) states that each reduction on source terms corresponds to one or more reductions on thunked terms.

Property 21 For all e_{1}, e_{2} ∈ Λ,

λβ ⊢ e_{1} ⟶ e_{2} ⇒ λβ_{i}τ ⊢ T ⟨[e_{1}]⟩ ⟶ ⟶ T ⟨[e_{2}]⟩

Proof: It is sufficient to show the following:

case λβ ⊢ (λx.e_{1}) e_{2} ⟶ e_{1}[x := e_{2}]:

T ⟨[(λx.e_{1}) e_{2}]⟩ = (λx.T ⟨[e_{1}]⟩) (delay T ⟨[e_{2}]⟩)
⟶_{β_{i}} T ⟨[e_{1}]⟩[x := delay T ⟨[e_{2}]⟩]
⟶ ⟶_{τ} T ⟨[e_{1}[x := e_{2}]]⟩ ...by Property 10

The following property (corresponding to Property 5 of Section 2.3.3) shows that each reduction on thunked terms corresponds to zero or one reduction on source terms.

Property 22 For all t_{1}, t_{2} ∈ T ⟨[Λ]⟩^{∗},

λβ_{i}τ ⊢ t_{1} ⟶ t_{2} ⇒ λβ ⊢ T^{−1}⟨[t_{1}]⟩ ⟶ ⟶ T^{−1}⟨[t_{2}]⟩

Proof: It is sufficient to show the following:

case λβ_{i}τ ⊢ force (delay t) ⟶ t:

T^{−1}⟨[force (delay t)]⟩ = T^{−1}⟨[delay t]⟩
= T^{−1}⟨[t]⟩ ...by definition of T^{−1}

case λβ_{i}τ ⊢ (λx.t_{1}) (delay t_{2}) ⟶ ⟶ t_{1}[x := delay t_{2}]:

T^{−1}⟨[(λx.t_{1}) (delay t_{2})]⟩ = (λx.T^{−1}⟨[t_{1}]⟩) T^{−1}⟨[t_{2}]⟩
⟶_{β}  T^{−1}⟨[t_{1}]⟩[x := T^{−1}⟨[t_{2}]⟩]
≡  T^{−1}⟨[t_{1}[x := delay t_{2}]]⟩

...by Property 11.

Components 3 and 4 of the equational correspondence (Theorem 6) are now proved as follows:

(1) λβ ⊢ e_{1} ⟶ ⟶ e_{2} ⇒ λβ_{i}τ ⊢ T ⟨[e_{1}]⟩ ⟶ ⟶ T ⟨[e_{2}]⟩

...by ind. on # of reductions and Prop. 21.

(2) λβ ⊢ e_{1} = e_{2} ⇒ λβ_{i}τ ⊢ T ⟨[e_{1}]⟩ = T ⟨[e_{2}]⟩

...by Church-Rosser and (1).

(3) λβ_{i}τ ⊢ t_{1} ⟶ ⟶ t_{2} ⇒ λβ ⊢ T^{−1}⟨[t_{1}]⟩ ⟶ ⟶ T^{−1}⟨[t_{2}]⟩

...by ind. on # of reductions and Prop. 22.

(4) λβ_{i}τ ⊢ t_{1} = t_{2} ⇒ λβ ⊢ T^{−1}⟨[t_{1}]⟩ = T^{−1}⟨[t_{2}]⟩

...by Church-Rosser and (3).

(5) λβ_{i}τ ⊢ T ⟨[e_{1}]⟩ = T ⟨[t_{2}]⟩ ⇒ λβ ⊢ (T^{−1} ∘ T )⟨[e_{1}]⟩ = (T^{−1} ∘ T )⟨[e_{2}]⟩

...by (4).

(6)  ⇒ λβ ⊢ e_{1} = e_{2}

...by Prop. 2.

(7) λβ ⊢ T^{−1}⟨[t_{1}]⟩ = T^{−1}⟨[t_{2}]⟩ ⇒ λβ_{i}τ ⊢ (T ∘ T^{−1})⟨[t_{1}]⟩ = (T ∘ T^{−1})⟨[t_{2}]⟩

...by (2).

(8)  ⇒ λβ_{i}τ ⊢ t_{1} = t_{2}

...by Prop. 3.

A.3 Correctness of T_{L}

A.3.1 The language T_{L}⟨[Λ]⟩^{∗}

The language of terms T_{L}⟨[Λ]⟩^{∗} in the image of T_{L} closed under β_{i} reduction is as follows (z ∉ FV(t) in the third clause and z ∉ FV(t_{1}) in the fifth clause).

t ∈ Terms[T_{L}⟨[Λ]⟩^{∗}]
t ::= b | x b | (λz.t) b | λx.t | t_{0} (λz.t_{1})

The proofs of correctness for the grammar are similar to the proofs of correctness for T ⟨[Λ]⟩^{∗} given in Section A.2.2.

A.3.2 Indifference and Simulation

To prove Indifference and Simulation for T_{L}, we take advantage of the fact that T_{L} = L ∘ T . The following three properties (which are straightforward to prove) are sufficient for establishing Indifference and Simulation properties for L (see Lemma 2 below).

Property 23 (L — commutation with substitution) For all e ∈ Λ_{τ}, L⟨[e_{0}[x := e_{1}]]⟩ ≡ L⟨[e_{0}]⟩[x := L⟨[e_{1}]⟩]

Property 24 (L — one step indifference and simulation) For all e_{0}, e_{1} ∈ Programs[Λ_{τ}],

e_{0} ⟼_{v} e_{1} ⇒ L⟨[e_{0}]⟩ ⟼_{i} L⟨[e_{1}]⟩

Property 25 (L — coincidence of stuck terms) For all s ∈ Stuck_{v}[T ⟨[Λ]⟩^{∗}], L⟨[s]⟩ ∈ Stuck_{n}[Λ] ⊂ Stuck_{v}[Λ].

L^{−1} : Terms[T_{L}⟨[Λ]⟩^{∗}]→Terms[T ⟨[Λ]⟩^{∗}]
L^{−1}⟨[b]⟩ = b
L^{−1}⟨[x b]⟩ = force x
L^{−1}⟨[(λz.t) b]⟩ = force (delay L^{−1}⟨[t]⟩)
L^{−1}⟨[λx.t]⟩ = λx.L^{−1}⟨[t]⟩
L^{−1}⟨[t_{0} (λz.t_{1})]⟩ = L^{−1}⟨[t_{0}]⟩ (delay L^{−1}⟨[t_{1}]⟩)

Figure 17: Mapping Λ thunks to abstract Λ_{τ} thunks

Lemma 2 (L — Indifference and Simulation) For all t ∈ Programs[T_{L}⟨[Λ]⟩^{∗}],

L⟨[eval_{v}(t)]⟩ ≃ eval_{i}(L⟨[t]⟩)

Proof: The proof follows from Properties 23, 24, and 25 and has the same structure as the proof for T Simulation (Lemma 1, Appendix A.2.3).

Now, Simulation for T_{L} is proved as follows (the proof of Indifference is similar).

T_{L}⟨[eval_{n}(e)]⟩ ≃ (L ∘ T )⟨[eval_{n}(e)]⟩
≃_{β_{i}} L⟨[eval_{v}(T ⟨[e]⟩)]⟩

...T Simulation (Theorem 5) and Theorem 11

≃ eval_{v}((L ∘ T )⟨[e]⟩)

...L Simulation (Lemma 2)

≃ eval_{v}(T_{L}⟨[e]⟩)

A.3.3 Translation

For Translation for T_{L}, we again take advantage of the fact that T_{L} = L ∘ T and show that L and its inverse L^{−1} (given in Figure 17) establish an equational correspondence between T ⟨[Λ]⟩^{∗} and T_{L}⟨[Λ]⟩^{∗}.

Theorem 11 (Equational Correspondence for T_{L}) For all e, e_{1}, e_{2} ∈ Terms[T ⟨[Λ]⟩^{∗}] and t, t_{1}, t_{2} ∈ Terms[T_{L}⟨[Λ]⟩^{∗}], 1. λβ_{i}τ ⊢ e = (L^{−1} ∘ L)⟨[e]⟩

2. λβ_{i} ⊢ t = (L ∘ L^{−1})⟨[t]⟩

3. λβ_{i}τ ⊢ e_{1} = e_{2} iff λβ_{i} ⊢ L⟨[e_{1}]⟩ = L⟨[e_{2}]⟩
4. λβ_{i} ⊢ t_{1} = t_{2} iff λβ_{i}τ ⊢ L^{−1}⟨[t_{1}]⟩ = L^{−1}⟨[t_{2}]⟩

The proofs for the equational correspondence mirror those of the equational correspondence for T (Theorem 6 — see Sections 2.3.3 and A.2.4) and are easy to establish. Now, given the equational correspondences established by T (Theorem 6) and L (Theorem 11), Translation for T_{L} is proved as follows.

λβ ⊢ e_{1} = e_{2}
⇔ λβ_{i}τ ⊢ T ⟨[e_{1}]⟩ = T ⟨[e_{2}]⟩  ...Theorem 6 (Component 3)
⇔ λβ_{i} ⊢ (L ∘ T )⟨[e_{1}]⟩ = (L ∘ T )⟨[e_{2}]⟩  ...Theorem 11 (Component 3)
⇔ λβ_{i} ⊢ T_{L}⟨[e_{1}]⟩ = T_{L}⟨[e_{2}]⟩  ...definition of T_{L}

A.4 Correctness of C_{v}^{+}

A.4.1 Indifference and Simulation

Following Plotkin’s proofs for C_{v} [23, pp. 149–152], Indifference and Simulation for C_{v}^{+} on T ⟨[Λ]⟩^{∗} are proved simultaneously. The proofs only involve minor extensions to Plotkin’s original proofs and we summarize only the differences.^{26}

First, we show that C_{v}^{+} commutes with substitution.

Property 26 (C_{v}^{+} — commutation with substitution) For all e ∈ Λ_{τ} and v ∈ Values_{v}[Λ_{τ}],

C_{v}^{+}⟨[e[x := v]]⟩ ≡ C_{v}^{+}⟨[e]⟩[x := C_{v}^{+}⟨v⟩]

Proof: by induction of the structure of e. To extend Plotkin’s proof, we need only consider the cases where e ≡ delay e′ and e ≡ force e′. These follow immediately from the inductive hypothesis.

Next, we extend Plotkin’s colon translation for C_{v} [23, p. 150] to C_{v}^{+}, i.e., to handle delay (which is included in the cases for values v) and force.

26Note that Properties 26, 27, and 28 are stronger than necessary since they are stated for Λ_{τ} ⊃ T ⟨[Λ]⟩^{∗}.

Definition 4 (C_{v}^{+} — colon translation) For all closed v, v_{0}, v_{1} ∈ Values_{v}[Λ_{τ}], closed non-values e, e_{0}, e_{1} ∈ Λ_{τ}, closed e′_{1} ∈ Λ_{τ}, and for all closed κ ∈ Values_{n}[Λ],

v : κ = κ C_{v}^{+}⟨v⟩
e_{0} e′_{1} : κ = e_{0} : (λy_{0}.C_{v}^{+}⟨[e′_{1}]⟩ (λy_{1}.y_{0} y_{1} κ))
v_{0} e_{1} : κ = e_{1} : (λy_{1}.C_{v}^{+}⟨v_{0}⟩ y_{1} κ)
v_{0} v_{1} : κ = C_{v}^{+}⟨v_{0}⟩ C_{v}^{+}⟨v_{1}⟩ κ
force e : κ = e : (λy.y κ)
force v : κ = C_{v}^{+}⟨v⟩ κ

Property 27 (C_{v}^{+} — correctness of colon translation) For all e ∈ Λ_{τ} and closed κ ∈ Values_{n}[Λ],

C_{v}^{+}⟨[e]⟩ κ ⟼_{i}^{+} e : κ

Proof: We only show the cases for delay and force. The remaining cases are identical to Plotkin’s proof for C_{v} [23, p. 150].

case e ≡ delay e_{0}:

C_{v}^{+}⟨[delay e_{0}]⟩ κ = (λk.k C_{v}^{+}⟨delay e_{0}⟩) κ
⟼_{i} κ C_{v}^{+}⟨delay e_{0}⟩
= delay e_{0} : κ

case e ≡ force e_{0}:

C_{v}^{+}⟨[force e_{0}]⟩ κ = (λk.C_{v}^{+}⟨[e_{0}]⟩ (λy.y k)) κ
⟼_{i} C_{v}^{+}⟨[e_{0}]⟩ (λy.y κ)
⟼_{i}^{+} e_{0} : (λy.y κ)

...by ind. hyp. and call this term z

If e_{0} ∉ Values_{v}[Λ], then

z = force e_{0} : κ

If e_{0} ∈ Values_{v}[Λ], then

z = (λy.y κ) C_{v}^{+}⟨e_{0}⟩
⟼_{i} C_{v}^{+}⟨e_{0}⟩ κ
= force e_{0} : κ

The following property states that one ⟼_{v} step in Λ_{τ} implies one or more ⟼_{i} steps on CPS programs.

Property 28 (C_{v}^{+} — one step simulation) For all e_{0}, e_{1} ∈ Programs[Λ_{τ}] and closed κ ∈ Values_{n}[Λ],

e_{0} ⟼_{v} e_{1} ⇒ e_{0} : κ ⟼_{i}^{+} e_{1} : κ

Proof: by induction over the derivation of e_{0} ⟼_{v} e_{1}. We only show the cases for delay and force. The remaining cases are identical to Plotkin’s proofs for C_{v} [23, p. 151].

case force (delay e) ⟼_{v} e:

force (delay e) : κ = C_{v}^{+}⟨delay e⟩ κ
= C_{v}^{+}⟨[e]⟩ κ
⟼_{i}^{+} e : κ ...by Property 27

case force e ⟼_{v} force e′ because e ⟼_{v} e′:

force e : κ = e : (λy.y κ)
⟼_{i}^{+} e′ : (λy.y κ) ...by ind. hyp. and call this term z

If e′ ∉ Values_{v}[Λ_{τ}], then

z = force e′ : κ

If e′ ∈ Values_{v}[Λ_{τ}], then

z = (λy.y κ) C_{v}^{+}⟨e′⟩
⟼_{i} C_{v}^{+}⟨e′⟩ κ
= force e′ : κ

The following property states that if a T ⟨[Λ]⟩^{∗} program is stuck under eval_{v}, then its CPS image will reach a stuck program under eval_{i}.^{27}

Property 29 (C_{v}^{+} — coincidence of stuck terms) For all s ∈ Stuck_{v}[T ⟨[Λ]⟩^{∗}] and all closed κ ∈ Values_{n}[Λ], s : κ ∈ Stuck_{n}[Λ] ⊂ Stuck_{v}[Λ].

Proof: First note that Stuck_{n}[Λ] ⊂ Stuck_{v}[Λ]. The proof then proceeds by induction over the definition of s ∈ Stuck_{v}[T ⟨[Λ]⟩^{∗}] (see Appendix A.2.2).

case s ≡ b (delay t):

b (delay t) : κ = b C_{v}^{+}⟨[t]⟩ κ and since b C_{v}^{+}⟨[t]⟩ ∈ Stuck_{n}[Λ] then b C_{v}^{+}⟨[t]⟩ κ ∈ Stuck_{n}[Λ]. case s ≡ s_{0} (delay t):

27Note that this doesn’t hold for Λ_{τ} (see footnote 19).

s_{0} (delay t) : κ = s_{0} : (λy_{0}.C_{v}^{+}⟨[delay t_{1}]⟩ (λy_{1}.y_{0} t_{1} κ)) ∈ Stuck_{n}[Λ] by ind. hyp.

Given Properties 27, 28 and 29, the proof of Indifference and Simulation for C_{v}^{+} on T ⟨[Λ]⟩^{∗} (Theorem 8) follow exactly Plotkin’s proof for C_{v} [23, p. 152]. The proof is similar in structure to the proof of Simulation for T (see Appendix A.2.3).

References

[1] Torben Amtoft. Minimal thunkification. In Patrick Cousot, Moreno Falaschi, Gilberto Filè, and Antoine Rauzy, editors, Proceedings of the Third International Workshop on Static Analysis WSA’93, volume 724 of Lecture Notes in Computer Science, pages 218–229, Padova, Italy, September 1993.

[2] Andrea Asperti. A categorical understanding of environment machines. Journal of Functional Programming, 2(1):23–59, January 1992.

[3] Henk Barendregt. The Lambda Calculus — Its Syntax and Semantics. North-Holland, 1984.

[4] Henk Barendregt. Lambda calculi with types. In Samson Abramsky, Dov M. Gabby, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Vol. 2, chapter 2, pages 118–309. Oxford University Press, Oxford, 1992.

[5] Adrienne Bloss, Paul Hudak, and Jonathan Young. Code optimization for lazy evaluation. LISP and Symbolic Computation, 1:147–164, 1988.

[6] William Clinger and Jonathan Rees (editors). Revised^{4} report on the algorithmic language Scheme. LISP Pointers, IV(3):1–55, July-September 1991.

[7] Pierre-Louis Curien. Categorical Combinators, Sequential Algorithms and Functional Programming, volume 1 of Research Notes in Theoretical Computer Science. Pitman, 1986.

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

[9] Olivier Danvy and John Hatcliff. Thunks (continued). In Proceedings of the Workshop on Static Analysis WSA’92, volume 81-82 of Bigre Journal, pages 3–11, Bordeaux, France, September 1992. IRISA, Rennes, France. Extended version available as Technical Report CIS-92-28, Kansas State University.

[10] Olivier Danvy and John Hatcliff. CPS transformation after strictness analysis. ACM Letters on Programming Languages and Systems, 1(3):195–212, 1993.

[11] Francis Dupont. Langage fonctionnels et parallélisme. Une réalisation pour le système CAML. PhD thesis, École Polytechnique, Palaiseau, France, July 1990.

[12] Michael J. Fischer. Lambda-calculus schemata. In Talcott [34]. An earlier version appeared in the Proceedings of the ACM Conference on Proving Assertions about Programs, SIGPLAN Notices, Vol. 7, No. 1, January 1972.

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

[14] Bob Harper and Mark Lillibridge. Polymorphic type assignment and CPS conversion. In Talcott [34].

[15] John Hatcliff. The Structure of Continuation-Passing Styles. PhD thesis, Department of Computing and Information Sciences, Kansas State University, Manhattan, Kansas, USA, July 1994.

[16] John Hatcliff and Olivier Danvy. A generic account of continuationpassing styles. In Hans Boehm, editor, Proceedings of the Twenty-first Annual ACM Symposium on Principles of Programming Languages, Portland, Oregon, January 1994. ACM Press.

[17] P. Z. Ingerman. Thunks, a way of compiling procedure statements with some comments on procedure declarations. Communications of the ACM, 4(1):55–58, 1961.

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

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

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

[21] Flemming Nielson and Hanne Riis Nielson. Two-Level Functional Languages, volume 34 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

[22] Chris Okasaki, Peter Lee, and David Tarditi. Call-by-need and continuation-passing style. In Talcott [34].

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

[24] Gordon D. Plotkin. Personal communication, New Orleans, Louisiana, March 1993.

[25] Eric Raymond (editor). The New Hacker’s Dictionary. The MIT Press, 1992.

[26] John C. Reynolds. On the relation between direct and continuation semantics. In Jacques Loeckx, editor, 2nd Colloquium on Automata, Languages and Programming, number 14 in Lecture Notes in Computer Science, pages 141–156, Saarbrücken, West Germany, July 1974.

[27] John C. Reynolds. The discoveries of continuations. In Talcott [34], pages 233–247.

[28] Jon G. Riecke. Fully abstract translations between functional languages. In Robert (Corky) Cartwright, editor, Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 245–254, Orlando, Florida, January 1991. ACM Press.

[29] Jon G. Riecke. The Logic and Expressibility of Simply-typed Callby-value and Lazy Languages. PhD thesis, MIT, Cambridge, Massachusetts, August 1991.

[30] Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Technical Report 92-180, Department of Computer Science, Rice University, Houston, Texas, 1992.

[31] Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. In Talcott [34], pages 289–360.

[32] Paul Steckler and Mitch Wand. Selective thunkification. In Proceedings of the First International Static Analysis Symposium, pages 162–178, Namur, Belgium, September 1994.

[33] Christopher Strachey and Christopher P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Technical Monograph PRG-11, Oxford University Computing Laboratory, Programming Research Group, Oxford, England, 1974.

[34] Carolyn L. Talcott, editor. Special issue on continuations, LISP and Symbolic Computation, Vol. 6, Nos. 3/4. Kluwer Academic Publishers, 1993.

Recent BRICS Report Series Publications

RS-97-7 John Hatcliff and Olivier Danvy. Thunks and the λ-Calculus (Extended Version). March 1997. 55 pp. Extended version of article to appear in the Journal of Functional Programming.

RS-97-6 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. March 1997. 53 pp. Extended version of an article to appear in the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’97), Amsterdam, The Netherlands, June 1997.

RS-97-5 Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. March 1997. 18 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-97-4 Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for Labelled Markov Processes. March 1997. 48 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-97-3 Carsten Butz and Ieke Moerdijk. A Definability Theorem for First Order Logic. March 1997. 10 pp.

RS-97-2 David A. Schmidt. Abstract Interpretation in the Operational Semantics Hierarchy. March 1997. 33 pp.

RS-97-1 Olivier Danvy and Mayer Goldberg. Partial Evaluation of the Euclidian Algorithm (Extended Version). January 1997. 16 pp. To appear in the journal Lisp and Symbolic Computation.

RS-96-62 P. S. Thiagarajan and Igor Walukiewicz. An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. December 1996. i+13 pp. To appear in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings.

RS-96-61 Sergei Soloviev. Proof of a Conjecture of S. Mac Lane. December 1996. 53 pp. Extended abstract appears in Pitt, Rydeheard and Johnstone, editors, Category Theory and Computer Science: 6th International Conference, CTCS ’95 Proceedings, LNCS 953, 1995, pages 59–80.