BRICS RS-96-19 Hatcliff & Danvy: Thunks and the λ-Calculus

BRICS

Basic Research in Computer Science

Thunks and the λ-Calculus

John Hatcliff Olivier Danvy

BRICS Report Series RS-96-19 ISSN 0909-0878 June 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, 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 publications in the BRICS Report Series. 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 WWW and anonymous FTP:

http://www.brics.dk/
ftp ftp.brics.dk (cd pub/BRICS)

Thunks and the λ-calculus ^{∗}

John Hatcliff ^{†} DIKU Copenhagen University ^{‡}

        (hatcliff@diku.dk)

Olivier Danvy BRICS ^{§} Aarhus University ^{¶}

                                    (danvy@brics.dk)

May 1996

Abstract

Thirty-five years ago, thunks were used to simulate call-by-name under call-by-value in Algol 60. Twenty years ago, Plotkin presented continuation-based simulations of call-by-name under call-by-value and vice versa in the λ-calculus. We connect all three of these classical simulations by factorizing the continuation-based call-by-name simulation C_{n} with a thunk-based call-by-name simulation T followed by the continuation-based call-by-value simulation C_{v} extended to thunks.

Λ  Λ_{thunks}

Λ_{CPS}

C_{n}

[figure] T [figure]

C_{v}

[figure]

We show that T actually satisfies all of Plotkin’s correctness criteria for C_{n} (i.e., his Indifference, Simulation, and Translation theorems). Furthermore, most of the correctness theorems for C_{n} can now be seen as simple corollaries of the corresponding theorems for C_{v} and T .

∗To appear in the Journal of Functional Programming.

†Supported by the Danish Research Academy and by the DART project (Design, Analysis and Reasoning about Tools) of the Danish Research Councils.

‡Computer Science Department, Universitetsparken 1, 2100 Copenhagen Ø, Denmark.

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

¶Computer Science Department, Ny Munkegade, B. 540, 8000 Aarhus C, Denmark.

1 Introduction

In his seminal paper, “Call-by-name, call-by-value and the λ-calculus” [27], Plotkin presents simulations of call-by-name by call-by-value (and viceversa). Both of Plotkin’s simulations rely on continuations. Since Algol 60, however, programming wisdom has it that thunks can be used to obtain a simpler simulation of call-by-name by call-by-value. We show that composing a thunk-based call-by-name simulation T with Plotkin’s continuationbased call-by-value simulation C_{v} actually yields Plotkin’s continuationbased call-by-name simulation C_{n} (Sections 2 and 3). Revisiting Plotkin’s correctness theorems (Section 4), we provide a correction to his Translation property for C_{n}, and show that the thunk-based simulation T satisfies all of Plotkin’s properties for C_{n}. The factorization of C_{n} by C_{v} and T makes it possible to derive correctness properties for C_{n} from the corresponding results for C_{v} and T . This factorization has also found several other applications already (Section 5). The extended version of this paper [15] gives a more detailed development as well as all proofs.

2 Continuation-based and Thunk-based Simulations

We consider Λ, the untyped λ-calculus parameterized by a set of basic constants b [27, p. 127].

\begin{aligned}e & ∈ & Λ \\ e & ::= & b | x | λx.e | e_{0} e_{1} \end{aligned}

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 ∈ Λ

Figure 1 displays Plotkin’s call-by-name CPS transformation C_{n} (which simulates call-by-name under call-by-value). (Side note: the term “CPS” stands for “Continuation-Passing Style”. It was coined in Steele’s MS thesis [35].) Figure 2 displays Plotkin’s call-by-value CPS transformation C_{v} (which simulates call-by-value under call-by-name). Figure 3 displays the standard thunk-based simulation of call-by-name using call-by-value evaluation of the language Λ_{τ}. Λ_{τ} extends Λ as follows.

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

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

Figure 1: Call-by-name CPS transformation

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 2: Call-by-value CPS transformation

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 3: Call-by-name thunk transformation

The operator delay suspends the evaluation 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 ∈ Λ_{τ}

The operator force triggers the evaluation of such a suspended expression. This is formalized by the following notion of reduction. Definition 1 (τ-reduction)

force (delay e) ⟶_{τ} e

We also consider the conventional notions of reduction β, β_{v}, η, and η_{v} [3, 27, 32]. Definition 2 (β,β_{v}, η, η_{v}-reduction)

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

For a notion of reduction r, ⟶_{r} also denotes construct compatible onestep reduction, ⟶ ⟶_{r} denotes the reflexive, transitive closure of ⟶_{r}, and =_{r} denotes the smallest equivalence relation generated by ⟶_{r} [3]. We will also write λr ⊢ e_{1} = e_{2} when e_{1} =_{r} e_{2} (similarly for the other relations).

Figure 4 extends C_{v} (see Figure 2) to obtain C_{v}^{+} which CPS-transforms thunks. C_{v}^{+} faithfully implements τ-reduction in terms of β_{v} (and thus β) reduction. We write β_{i} below to signify that the property holds indifferently for β_{v} and β.

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

Proof:

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

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

3 Connecting the Continuation-based and Thunk-based Simulations

C_{n} can be factored into two conceptually distinct steps: (1) the suspension of argument evaluation (captured in T ); and (2) the sequentialization of function application to give the usual tail-calls of CPS terms (captured in C_{v}^{+}).

Theorem 1 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′]⟩ = C_{v}^{+}⟨[λx.T ⟨[e′]⟩]⟩
= λk.k (λx.(C_{v}^{+} ∘ T )⟨[e′]⟩)
=_{β_{i}} λk.k (λx.C_{n}⟨[e′]⟩) ...by the ind. hyp.
= C_{n}⟨[λx.e′]⟩

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}]⟩

This theorem implies that the diagram in the abstract commutes up to β_{i}- equivalence, i.e., indifferently up to β_{v}- and β-equivalence. Note that C_{v}^{+} ∘ T and C_{n} only differ by administrative reductions. In fact, if we consider optimizing versions of C_{n} and C_{v} that remove administrative redexes, then the diagram commutes up to identity (i.e., up to α-equivalence).

Figures 5 and 6 present two such optimizing transformations C_{n.opt} and C_{v.opt}. The output of C_{n.opt} is β_{v}η_{v} equivalent to the output of C_{n}, and similarly for C_{v.opt} and C_{v}, as shown by Danvy and Filinski [7, pp. 387 and 367]. Both are applied to the identity continuation. In Figures 5 and 6, they are presented in a two-level language à la Nielson and Nielson [22]. Operationally, the overlined λ’s and @’s correspond to functional abstractions and applications in the program implementing the translation, while the underlined λ’s and @’s represent abstract-syntax constructors. It is simple to transcribe C_{n.opt} and C_{v.opt} 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 2 For all e ∈ Λ, (C_{v.opt}^{+} ∘ T )⟨[e]⟩\overline{@}(\overline{λ}a.a) ≡ C_{n.opt}⟨[e]⟩\overline{@}(\overline{λ}a.a).

Proof: A simple structural induction similar to the one required in the proof of Theorem 1. 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_{0}.y_{0}\underline{@}(\underline{λ}y_{1}.k\overline{@}y_{1}))
= \overline{λ}k.(\overline{λ}y_{0}.y_{0}\underline{@}(\underline{λ}y_{1}.k\overline{@}y_{1}))\overline{@}x
= \overline{λ}k.x\underline{@}(\underline{λ}y_{1}.k\overline{@}y_{1})
= C_{n.opt}⟨[x]⟩

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 4: Call-by-value CPS transformation (extended to thunks)

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 5: Optimizing call-by-name CPS transformation

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 6: Optimizing call-by-value CPS transformation 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 7: Single-step evaluation rules

4 Revisiting Plotkin’s Correctness Properties

Figure 7 presents single-step evaluation rules specifying the call-by-name and call-by-value operational semantics of Λ programs (closed terms). 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

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

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

For a language l, Programs[l] denotes the closed terms in l. For metalanguage expressions E_{1}, E_{2}, we write E_{1} ≃ E_{2} when E_{1} and E_{2} are both undefined, or else both are defined and denote α-equivalent terms. We will also write E_{1} ≃_{r} E_{2} when E_{1} and E_{2} are both undefined, or else are both defined and denote r-convertible terms for the convertibility relation generated by some notion of reduction r.

Plotkin expressed the correctness of his simulations C_{n} and C_{v} via three properties: Indifference, Simulation, and Translation. Indifference states that call-by-name and call-by-value evaluation coincide on terms in the image of the CPS transformation. Simulation states that the desired evaluation strategy is properly simulated. Translation states how the transformation relates program calculi for each evaluation strategy (e.g., λβ, λβ_{v}). Let us restate these properties for Plotkin’s original presentation of C_{n} (hereby noted P_{n}) [27, p. 153], that only differs from Figure 1 at the line for identifiers.

P_{n}⟨[x]⟩ = x

Theorem 3 (Plotkin 1975) For all e ∈ Programs[Λ],

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 )

where I denotes the identity function and is used as the initial continuation.

Plotkin also claimed the following Translation property.

Claim 1 (Plotkin 1975) For all e_{1}, e_{2} ∈ Λ,

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 Translation property purports to show that β-equivalence classes are preserved and reflected by P_{n}. The property, however, does not hold because

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

The proof breaks down at the statement “It is straightforward to show that λβ ⊢ e_{1} = e_{2} implies λβ_{v} ⊢ P_{n}⟨[e_{1}]⟩ = P_{n}⟨[e_{2}]⟩ ...” [27, p. 158]. 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))  (1)
⟶_{β_{v}} λk.k (λx.λk.(λy.y x k) (λz.z))  (2)

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

Since the two distinct terms at lines (4) and (5) are β_{i}-normal, confluence of β_{i} implies λβ_{i} ⊬ P_{n}⟨[e_{1}]⟩ = P_{n}⟨[e_{2}]⟩.

In practice, though, η_{v} reductions such as those required in the example above are unproblematic if they are embedded in proper CPS contexts (e.g., contexts in the language of terms in the image of P_{n} closed under β_{i} reductions). 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. In this case, the η_{v} reduction can be expressed by a β_{v} reduction. If the term, however, is not embedded in a CPS context (e.g., [·] (λy.y b)), the η_{v} reduction is unsound, i.e., it fails to preserve operational equivalence as defined by Plotkin [27, pp. 144,147]. Such reductions are unsound due to “improper” uses of basic constants. For example, λx.b x ⟶_{η_{v}} b but λx.b x ≉_{v} b (take C = [·]) where ≈_{v} is the call-by-value operational equivalence relation defined by Plotkin [15, p. 9]. Note, finally, that a simple typing discipline eliminates improper uses of basic constants, and consequently give soundness for η_{v}.

The simplest solution for recovering the Translation property is to change the translation of identifiers from P_{n}⟨[x]⟩ = x to λk.x k — obtaining the translation C_{n} given in Figure 1.^{1}

For the example above, the modified translation gives

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

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

Theorem 4 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 )

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

1In the context of Parigot’s λμ-calculus [25], de Groote independently noted the problem with Plotkin’s Translation theorem and proposed a similar correction [10].

The Indifference and Translation properties remain the same. The Simulation property, however, holds up to β_{i}-equivalence while Plotkin’s Simulation for P_{n} holds up to α-equivalence. For 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.

In fact, proofs of Indifference, Simulation, and most of the Translation can be derived from the correctness properties of C_{v}^{+} and T (see Section 5). All that remains of Translation is to show that λβ ⊢ C_{n}⟨[e_{1}]⟩ I = C_{n}⟨[e_{2}]⟩ I implies λβ ⊢ e_{1} = e_{2} and this follows in a straightforward manner from Plotkin’s original proof for P_{n} [15, p. 31]. The following theorem gives the Indifference, Simulation, and Translation properties for C_{v}.

Theorem 5 (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}]⟩

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 4), the theory λβ_{v} is incomplete in the sense that it cannot prove the equivalence of some terms whose CPS images are provably equivalent using λβ or λβ_{v} [32]. The properties of C_{v} as stated in Theorem 5 can be extended to the transformation C_{v}^{+} defined on the language T — the set of terms in the image of T closed under β_{i}τ reduction. It is straightforward to show that the following grammar generates exactly the set of terms T [15, pp. 32,33].

t ::= b | force x | force (delay t) | λx.t | t_{0} (delay t_{1})

Theorem 6 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} [27, pp. 148–152]. Translation follows from the Translation component of Theorem 5 and Property 1 [15, p. 39].

Thunks are sufficient for establishing a call-by-name simulation satisfying all of the correctness properties of the continuation-passing simulation C_{n}. Specifically, we prove the following theorem which recasts the correctness theorem for C_{n} (Theorem 4) in terms of T . The last two assertions of the Translation component of Theorem 4 do not appear here since the identity function as the initial continuation only plays a rôle in CPS evaluation.

Theorem 7 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]⟩)

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

Proof: The proof of Indifference is trivial: one can intuitively see from the grammar for T (which includes the set of terms in the image of T closed under evaluation steps) that call-by-name and call-by-value evaluation will coincide since all function arguments are values.

The proof of Simulation is somewhat involved. It begins by inductively defining a relation ∼^{τ} ⊆ Λ × Λ_{τ} such that e ∼^{τ} t holds exactly when λτ ⊢ T ⟨[e]⟩ = t. The crucial step is then to show that for all e ∈ Programs[Λ] and t ∈ Programs[Λ_{τ}] such that e ∼^{τ} t, e ⟼_{n} e′ implies that there exists a t′ such that t ⟼_{v}^{+} t′ and e′ ∼^{τ} t′ [15, Sect. 2.3.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 Λ

Translation is established by first defining a translation T^{−1} : Λ_{τ} →Λ that simply removes delay and force constructs. One then shows that T and T^{−1} establish an equational correspondence [32] (or more precisely a reflection [33]) between theories λβ and λβ_{v}τ (and λβ and λβτ). Translation follows as a corollary of this stronger result [15, Sect. 2.3.3].

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 Section 3. Elsewhere [14], 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].

Figure 8 presents the transformation T_{L} that implements thunks directly in Λ using what Plotkin described as the “protecting by a λ” technique [27, p. 147]. An expression is delayed by wrapping it in an abstraction with a dummy parameter. A thunk is forced by applying it to a dummy argument.

The following theorem recasts the correctness theorem for C_{n} (Theorem 4) in terms of T_{L}.

Theorem 8 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: \begin{aligned}λβ ⊢ e_{1} = e_{2} & iff & λβ_{v} ⊢ T_{L}⟨[e_{1}]⟩ = T_{L}⟨[e_{2}]⟩ \\ & iff & λβ ⊢ T_{L}⟨[e_{1}]⟩ = T_{L}⟨[e_{2}]⟩ \end{aligned}

Proof: Follows the same pattern as the proof of Theorem 7 [15, Sect. 2.4].

5 Applications

5.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 1. Here we show only the results where evaluation is undefined or results in a basic constant b. See [15, p. 31] for a derivation of C_{n} Simulation for arbitrary results.

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 1 and the soundness of β_{v}
⇔ eval_{n}((C_{v}^{+} ∘ T )⟨[e]⟩ (λy.y)) = b ...Theorem 6 (Indifference)
⇔ eval_{n}(C_{n}⟨[e]⟩ (λy.y)) = b  ...Theorem 1 and the soundness of β

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

eval_{n}(e) = b

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

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

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

5.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 [4, 21, 24]. In an earlier work [9], we gave a transformation T_{s} that optimizes thunk introduction based on strictness information. 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 staged approach can be contrasted with Burn and Le Métayer’s monolithic strategy [5].

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}^{+}.

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

5.3 Deriving a call-by-need CPS transformation

Okasaki, Lee, and Tarditi [24] 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 with memo-thunks [4]. 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 it with the memo-thunk introduction.

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.

5.4 Alternative CPS transformations

Thunks can be used to factor a variety of call-by-name CPS transformations. In addition to those discussed here, one can factor a variant of Reynolds’s CPS transformation directed by strictness information [14, 30], as well as a call-by-name analogue of Fischer’s call-by-value CPS transformation [11, 32].

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} (see Figure 8) instead of T , C_{v} ∘ T_{L} still gives a valid CPS simulation of callby-name by call-by-value. However, β_{i} equivalence with C_{n} is not obtained (i.e., λβ_{i} ⊬ C_{n}⟨[e]⟩ = (C_{v} ∘ T_{L})⟨[e]⟩), as shown by the following derivations.

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

5.5 The factorization holds for types

Plotkin’s continuation-passing transformations were originally stated in terms of untyped λ-calculi. These transformations have been shown to preserve well-typedness of terms [12, 13, 18, 20]. The thunk transformation T also preserves well-typedness of terms, and the relationship between C_{v}^{+} ∘ T and C_{n} is reflected in transformations on types [15, Sect. 4].

6 Related Work

Ingerman [16], 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 [29]. 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 [4] study thunks as the basis of an 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 [31] 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 for thunks. The 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). 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 formulate thunks in a categorical setting [2, 6]. Two combinators freeze and unfreeze, which are analogous to 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 co-monad.

In his original paper [27, p. 147], Plotkin 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.” [27, p. 147]. By “protecting by a λ”, Plotkin refers to a representation of thunks as λ-abstractions with a dummy parameter, as in Figure 8. In a set of unpublished notes, however, he later showed that the “protecting by a λ” technique is sufficient for a complete simulation [28].

An earlier version of Section 3 appeared in the proceedings of WSA’92 [8]. Most of these proofs have been checked in Elf [26] by Niss and the first author [23]. Elsewhere [14], we also consider an optimizing version of T that does not introduce thunks for identifiers occurring as function arguments:

T_{opt}⟨[e x]⟩ = T_{opt}⟨[e]⟩ x

T_{opt} generates a language T_{opt} which is more refined than T (referred to in Theorem 6).

Finally, Lawall and Danvy investigate staging the call-by-value CPS transformation into conceptually different passes elsewhere [17].

7 Conclusion

We have connected the traditional thunk-based simulation T of call-by-name under call-by-value and Plotkin’s continuation-based simulations C_{n} and C_{v} of call-by-name and call-by-value. Almost all of the technical properties Plotkin established for C_{n} follow from the properties of T and C_{v}^{+} (the extension of C_{v} to thunks). When reasoning about C_{n} and C_{v}, it is thus often sufficient to reason about C_{v}^{+} and the simpler simulation T . We have also given several applications involving deriving optimized continuation-based simulations for call-by-name and call-by-need languages and performing CPS transformation after static program analysis.

Acknowledgements

Andrzej Filinski, Sergey Kotov, Julia Lawall, Henning Niss, and David Schmidt gave helpful comments on earlier drafts of this paper. Thanks are also due to Dave Sands for several useful discussions. Special thanks to Gordon Plotkin for enlightening conversations at the LDPL’95 workshop and for subsequently mailing us his unpublished course notes. Finally, we are grateful to the reviewers for their lucid comments and their exhortation to be more concise, and to our editors, for their encouragement and direction.

The commuting diagram was drawn with Kristoffer Rose’s XY-pic package.

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, number 724 in 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] Adrienne Bloss, Paul Hudak, and Jonathan Young. Code optimization for lazy evaluation. LISP and Symbolic Computation, 1:147–164, 1988.

[5] Geoffrey Burn and Daniel Le Métayer. Proving the correctness of compiler optimisations based on a global program analysis. Journal of Functional Programming, 6(1), 1996.

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

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

[8] Olivier Danvy and John Hatcliff. Thunks (continued). In Proceedings of the Second International Workshop on Static Analysis WSA’92, volume 81-82 of Bigre Journal, pages 3–11, Bordeaux, France, September 1992. IRISA, Rennes, France.

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

[10] Philippe de Groote. A CPS-translation of the λμ-calculus. In Sophie Tison, editor, 19th Colloquium on Trees in Algebra and Programming (CAAP’94), number 787 in Lecture Notes in Computer Science, pages 47–58, Edinburgh, Scotland, April 1994.

[11] Michael J. Fischer. Lambda-calculus schemata. In Talcott [36], pages 259–288. An earlier version appeared in an ACM Conference on Proving Assertions about Programs, SIGPLAN Notices, Vol. 7, No. 1, January 1972.

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

[13] Bob Harper and Mark Lillibridge. Polymorphic type assignment and CPS conversion. In Talcott [36].

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

[15] John Hatcliff and Olivier Danvy. Thunks and the λ-calculus. Technical Report 95/3, DIKU, Computer Science Department, University of Copenhagen, Copenhagen, Denmark, February 1995.

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

[17] Julia L. Lawall and Olivier Danvy. Separating stages in the continuation-passing style transformation. In Susan L. Graham, editor, Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 124–136, Charleston, South Carolina, January 1993. ACM Press.

[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, Ithaca, New York, 1990.

[21] Alan Mycroft. Abstract Interpretation and Optimising Transformations for Applicative Programs. PhD thesis, University of Edinburgh, Edinburgh, Scotland, 1981.

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

[23] Henning Niss and John Hatcliff. Encoding operational semantics in logical frameworks: A critical review of LF/Elf. In Bengt Nördstrom, editor, Proceedings of the 1995 Workshop on Programming Language Theory, Göteborg, Sweden, November 1995.

[24] Chris Okasaki, Peter Lee, and David Tarditi. Call-by-need and continuation-passing style. In Carolyn L. Talcott, editor, Special issue on continuations (Part II), LISP and Symbolic Computation, Vol. 7, No. 1, pages 57–81. Kluwer Academic Publishers, January 1994.

[25] Michel Parigot. λμ-calculus: an algorithmic interpretation of classical natural deduction. In Andrei Voronkov, editor, Proceedings of the International Conference on Logic Programming and Automated Reasoning, number 624 in Lecture Notes in Artificial Intelligence, pages 190–201, St. Petersburg, Russia, July 1992.

[26] Frank Pfenning. Logic programming in the LF logical framework. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149–181. Cambridge University Press, 1991.

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

[28] Gordon D. Plotkin. Course notes on operational semantics. Unpublished manuscript, 1978.

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

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

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

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

[33] Amr Sabry and Philip Wadler. Compiling with reflections. In R. Kent Dybvig, editor, Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, Philadelphia, Pennsylvania, May 1996. ACM Press.

[34] Paul Steckler and Mitchell Wand. Selective thunkification. In Baudouin Le Charlier, editor, Static Analysis, number 864 in Lecture Notes in Computer Science, pages 162–178, Namur, Belgium, September 1994.

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

[36] Carolyn L. Talcott, editor. Special issue on continuations (Part I), LISP and Symbolic Computation, Vol. 6, Nos. 3/4. Kluwer Academic Publishers, December 1993.

Recent Publications in the BRICS Report Series

RS-96-19 John Hatcliff and Olivier Danvy. Thunks and the λ-Calculus. June 1996. 22 pp. To appear in Journal of Functional Programming.

RS-96-18 Thomas Troels Hildebrandt and Vladimiro Sassone. Comparing Transition Systems with Independence and Asynchronous Transition Systems. June 1996. 14 pp. To appear in Montanari and Sassone, editors, Concurrency Theory: 7th International Conference, CONCUR ’96 Proceedings, LNCS 1119, 1996.

RS-96-17 Olivier Danvy, Karoline Malmkj�r, and Jens Palsberg. Eta-Expansion Does The Trick (Revised Version). May 1996. 29 pp. To appear in ACM Transactions on Programming Languages and Systems (TOPLAS).

RS-96-16 Lisbeth Fajstrup and Martin Rau�en. Detecting Deadlocks in Concurrent Systems. May 1996. 10 pp.

RS-96-15 Olivier Danvy. Pragmatic Aspects of Type-Directed Partial Evaluation. May 1996. 27 pp.

RS-96-14 Olivier Danvy and Karoline Malmkj�r. On the Idempotence of the CPS Transformation. May 1996. 15 pp.

RS-96-13 Olivier Danvy and Ren� e Vestergaard. Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation. May 1996. 28 pp. To appear in 8th International Symposium on Programming Languages, Implementations, Logics, and Programs, PLILP ’96 Proceedings, LNCS, 1996.

RS-96-12 Lars Arge, Darren E. Vengroff, and Jeffrey S. Vitter. External-Memory Algorithms for Processing Line Segments in Geographic Information Systems. May 1996. 34 pp. A shorter version of this paper appears in Spirakis, editor, Algorithms - ESA ’95: Third Annual European Symposium Proceedings, LNCS 979, 1995, pages 295�310.