BRICS RS-00-33 Danvy & Nielsen: A Higher-Order Colon Translation BRICS

Basic Research in Computer Science

A Higher-Order Colon Translation

Olivier Danvy Lasse R. Nielsen BRICS Report Series RS-00-33 ISSN 0909-0878 December 2000 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2000, Olivier Danvy & Lasse R. Nielsen.

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/00/33/

A Higher-Order Colon Translation ^{∗}

Olivier Danvy and Lasse R. Nielsen

BRICS ^{†}

Department of Computer Science University of Aarhus ^{‡}

December 2000

Abstract

A lambda-encoding such as the CPS transformation gives rise to administrative redexes. In his seminal article “Call-by-name, call-by-value and the lambda-calculus”, 25 years ago, Plotkin tackled administrative reductions using a so-called colon translation. In “Representing control, a study of the CPS transformation”, 15 years later, Danvy and Filinski integrated administrative reductions in the CPS transformation, making it operate in one pass. This one-pass transformation is higher-order, and can be used for other lambda-encodings, but we do not see its associated proof technique used in practice—instead, Plotkin’s colon translation appears to be favored. Therefore, in an attempt to link the higher-order transformation and Plotkin’s proof technique, we recast Plotkin’s proof of Indifference and Simulation in a higher-order setting. To this end, we extend the colon translation from first order to higher order.

Keywords: Call by name, call by value, λ-calculus, continuation-passing style (CPS), CPS transformation, administrative reductions, colon translation, onepass CPS transformation, Indifference, Simulation.

∗To appear in the proceedings of FLOPS 2001.

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

‡ Ny Munkegade, Building 540, DK-8000 Aarhus C, Denmark.

E-mail: {danvy,lrn}@brics.dk

Contents

1 Introduction 3 2 Call-by-name and call-by-value λ-calculi 4

2.1 Call by value . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Call by name . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 Evaluation-order independent reduction . . . . . . . . . . . . . . 5 2.4 Stuck terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 The meta language of the one-pass CPS transformation 5 4 The one-pass CPS transformation 8 5 The goal 10 6 Plotkin’s four lemmas 11 7 Plotkin’s double proof 14 8 Conclusion 15

List of Figures

1 The left-to-right, call-by-value CPS transformation in one pass . 8

1 Introduction

In “Call-by-name, call-by-value and the λ-calculus” [9], Plotkin provided the first formalization of the transformation into continuation-passing style (CPS) [10, 11]. Plotkin’s CPS transformation is first-order. As most λ-encodings, it is plagued with so-called administrative redexes, i.e., redexes that are only artefacts of the λ-encoding. Their reduction steps are interspersed with the reduction steps corresponding to actual reduction steps in the original direct-style program. In the early 90s, a higher-order version of the CPS transformation was developed that eliminates all administrative redexes at transformation time, in one pass [1, 3, 12]. This higher-order version has been formalized in several ways: using a notion of ‘schematic’ continuations [3], using higher-order rewriting [4], and using logical relations [2]. None of these various ways of formalizing a one-pass CPS transformation, however, match Plotkin’s original proof technique.

Does it mean that Plotkin’s proof technique is inherently first-order? In this article, we answer this question negatively. We adapt his proof technique to the higher-order setting of one-pass CPS transformations.

To tackle administrative reductions, in his formalization, Plotkin introduced a so-called colon translation that eliminates administrative redexes until a redex is reached that corresponds to an actual redex in the original program. Our goal here is to present a higher-order colon translation that yields the same effect for a one-pass CPS transformation, thus adapting Plotkin’s original proof technique to a higher-order operational setting.

Prerequisites: We assume a basic familiarity with Plotkin’s work, as can be gathered from his original article [9] or from Hatcliff and Danvy’s revisitation [7]. The one-pass CPS transformation is presented in Danvy and Filinski’s article [3] (Section 3 of that article reviews administrative redexes and the colon translation). A pictorial presentation of actual and administrative reductions can be found in Section 3 of Danvy, Dzafic, and Pfenning’s 1999 article [2]. Nevertheless, we have tried to make the present article stand alone.

Overview: Section 2 reviews call by name and call by value in the untyped λ-calculus. Sections 3 and 4 present the one-pass CPS transformation and its meta-language. Section 5 states our goal (proving Plotkin’s Indifference and Simulation theorems) and our means (a higher-order colon translation). Section 6 recasts Plotkin’s four lemmas and Section 7 restates his proof. Section 8 concludes.

2 Call-by-name and call-by-value λ-calculi

We define the untyped λ-calculus by giving its syntax and two semantics, one for call by value (CBV) and the other for call by name (CBN).

Definition 1 (Syntax of the λ-calculus with uninterpreted constants)

e ::= x | λx.e | e @ e | c

We only distinguish expressions up to renaming of bound variables. So for example, λx.x and λy.y are considered equal.

2.1 Call by value

The CBV semantics of closed expressions is given using evaluation contexts in the style of Felleisen [5].

The evaluation contexts are as follows.

C_{v}[ ] ::= [ ] | C_{v}[ ] @ e | v_{v} @ C_{v}[ ]

where v_{v} is a value.

Values form a subset of expressions and are defined as follows.

v_{v} ::= λx.e | c

The reduction rule is defined as follows.

C_{v}[(λx.e) @ v_{v}] ⟼_{v} C_{v}[e[v_{v}/x]]

where e[v/x] is the standard capture-avoiding substitution.

Eval_{v} is the following partial function:

\{ \begin{matrix}Eval_{v}(e) = v_{v} & iff e ⟼_{v}^{i} v_{v} for some value v_{v} and integer i \\ Eval_{v}(e) is undefined & otherwise \end{matrix}

where ⟼_{v}^{i} denotes i iterations of ⟼_{v}.

2.2 Call by name

We give the CBN semantics for closed expressions as in Section 2.1. The evaluation contexts are:

C_{n}[ ] ::= [ ] | C_{n}[ ] @ e

The values are:

v_{n} ::= λx.e | c

The reduction rule is:

C_{n}[(λx.e) @ e′] ⟼_{n} C_{n}[e[e′/x]]

Eval_{n} is the following partial function:

\{ \begin{matrix}Eval_{n}(e) = v_{n} & iff e ⟼_{n}^{i} v_{n} for some value v_{n} and integer i \\ Eval_{n}(e) is undefined & otherwise \end{matrix}

2.3 Evaluation-order independent reduction

In the remainder of this article, the arrow ⟼ (without annotation) corresponds to a reduction that is legal in both call by value and call by name. In other words, the ⟼ relation is the intersection of the ⟼_{v} and ⟼_{n} relations.

2.4 Stuck terms

In both the call-by-value and the call-by-name semantics, we can write closed expressions that are not values, but for which there are no legal reductions. Plotkin said that such expressions “stick”.

The stuck closed expressions w.r.t. the CBV semantics are:

Sticks_{v} ::= c @ v_{v} | Sticks_{v} @ e | v_{v} @ Sticks_{v}

or simply C_{v}[c @ v_{v}].

The stuck expressions are disjoint from the values. All closed expressions are either values, stuck, or there is a possible reduction.

The stuck closed expressions w.r.t. the CBN semantics are:

Sticks_{n} ::= Sticks_{n} @ e | c @ e

or simply C_{n}[c @ e].

Again the stuck expressions are disjoint from the values, and all closed expressions are either values, stuck, or allow a reduction.

3 The meta language of the one-pass CPS transformation

The one-pass CPS transformation maps direct-style λ-expressions into λ-expr-essions that can be reduced at transformation time, yielding λ-expressions in CPS. Therefore, the implementation language for the transformation contains two kinds of applications, two kinds of λ-abstractions, and two kinds of variables:

E ::= c | x | λx.E | E @ E | X | \overline{λ}X.E | E \overline{@} E

Following tradition we refer to overlined constructs as static and non-overlined ones as dynamic. The identifiers ranged over by X and x are called static and dynamic variables, respectively. Substituting an expression for a static variable is a static substitution, and substituting an expression for a dynamic variable is a dynamic substitution. As in Section 2, we only distinguish expressions up to renaming of bound variables, both for static and dynamic variables.

We define the following typing system for the meta language:

τ ::= Syntax | τ → τ

\overline{Γ ⊢ c : Syntax}  \overline{Γ ⊢ x : Syntax}  \frac{Γ ⊢ E : Syntax}{Γ ⊢ λx.E : Syntax}

\frac{Γ ⊢ E_{0} : Syntax  Γ ⊢ E_{1} : Syntax}{Γ ⊢ E_{0} @ E_{1} : Syntax}  \frac{Γ(X) = τ}{Γ ⊢ X : τ}

\frac{Γ, X : τ_{1} ⊢ E : τ_{2}}{Γ ⊢ \overline{λ}X.E : τ_{1} → τ_{2}}  \frac{Γ ⊢ E_{0} : τ_{1} → τ_{2}  Γ ⊢ E_{1} : τ_{1}}{Γ ⊢ E_{0} \overline{@} E_{1} : τ_{2}}

Any expression typeable in this typing system is simply typed and hence its reduction terminates and any evaluation strategy leads to the same normal form. We choose to use call by value, arbitrarily.

The meta-language values are:

v_{V} ::= c | x | λx.v_{V} | v_{V} @ v_{V} | \overline{λ}X.E

N.B. If a meta-language value v_{V} has type Syntax, it is an expression in the λ-calculus as defined in Section 2. In particular, v_{V} is free of static variables.

The evaluation contexts are:

C_{V}[ ] ::= [ ] | λx.C_{V}[ ] | C_{V}[ ] @ E | v_{V} @ C_{V}[ ] | C_{V}[ ] \overline{@} E | v_{V} \overline{@} C_{V}[ ]

The reduction rule only allows us to reduce static β-redexes:

C_{V}[(\overline{λ}X.E) \overline{@} v_{V}] ⟼_{V} C_{V}[E[v_{V}/X]]

Proposition 1 (Context nesting) Since nested contexts are themselves contexts, the reduction rule satisfies the following property.

E ⟼_{V} E′ ⟺ C_{V}[E] ⟼_{V} C_{V}[E′]

Proof: Omitted. □ We define the static evaluation function, Eval_{V}, by

Eval_{V}(E) = v_{V} ⟺ E ⟼_{V}^{∗} v_{V}

where ⟼_{V}^{∗} denotes zero or more iterations of ⟼_{V}. By definition reductions on well-typed expressions are strongly normalizing, so Eval_{V} is total on these.

We treat the meta language as a higher-order language in the sense that we equate expressions up to β-equivalence (written ≡_{V}). We only use simply typed and thus strongly normalizing expressions, so we can equate any expression to the value it reduces to.

The dynamic substitution of a closed value, as used for λ-expressions in Section 2, can be extended directly to meta-language terms. The interaction between static and dynamic substitutions satisfies the following property.

Proposition 2 (Substitution) If E is a meta-language expression, v_{V} is a meta-language value, and e is a closed λ-expression, then

E[v_{V}/X][e/x] = E[e/x][v_{V}[e/x]/X].

Proof: By structural induction on E.

Cases E = c, x, and Y (Y ≠ X): In these cases X is not free in E, and hence X is not free in E[e/x]. It follows that

E[v_{V}/X][e/x] = E[e/x] = E[e/x][v_{V}[e/x]/X].

Cases E = E_{1} @ E_{2} and E_{1} \overline{@} E_{2}: These cases both follow directly from the induction hypothesis and the definition of substitution.

Case E = X: X[v_{V}/X][e/x] = v_{V}[e/x] = X[e/x][v_{V}[e/x]/X]

Case E = λy.E_{1} and \overline{λ}Y.E_{1}: Since we equate expressions up to alpha-renaming of bound variables, we can assume that y is not free in v_{V} and y ≠ x as well as Y ≠ X. These cases are thus similar to the E_{1} @ E_{2} case.

□

Corollary 1 (Dynamic substitution respects static β-equivalence) If E and E′ are meta-language expressions, v is a value, and x is a dynamic variable, then

E ⟼_{V}^{∗} E′ ⟹ E[v/x] ⟼_{V}^{∗} E′[v/x].

I.e., if E ≡_{V} E′ then E[v/x] ≡_{V} E′[v/x].

Proof: It suffices to show that if E ⟼_{V} E′ then E[v/x] ⟼_{V} E′[v/x]. Since E ⟼_{V} E only if there exists a context C_{V}[ ] such that E = C_{V}[(\overline{λ}X.E_{1}) \overline{@} V] ⟼_{V} C_{V}[E_{1}[V/X]] = E′, the proof is by induction on the structure of the context.

Case C_{V}[ ] = [ ]: In this case E = (\overline{λ}X.E_{1}) \overline{@} V and E′ = E_{1}[V/X].

((\overline{λ}X.E_{1}) \overline{@} V)[v/x] = (\overline{λ}X.E_{1}[v/x]) \overline{@} V [v/x]
⟼_{V} E_{1}[v/x][V [v/x]/X]
= E_{1}[V/X][v/x] by Proposition 2

Case C_{V}[ ] = C_{1}[ ] \overline{@} E_{2}:

E[v/x] = C_{1}[(\overline{λ}X.E_{1}) \overline{@} V][v/x]
= (C_{1}[(\overline{λ}X.E_{1}) \overline{@} V] \overline{@} E_{2})[v/x]
= C_{1}[(\overline{λ}X.E_{1}) \overline{@} V][v/x] \overline{@} E_{2}[v/x]
⟼_{V} C_{1}[E_{1}[V/X]][v/x] \overline{@} E_{2}[v/x]  by I.H. and Prop. 1
= (C_{1}[E_{1}[V/X]] \overline{@} E_{2})[v/x]
= C_{V}[E_{1}[V/X]][v/x]
= E′[v/x]

Cases C_{V}[ ] = C_{1}[ ] @ E_{2}, V \overline{@} C_{1}[ ], V @ C_{1}[ ], and λy.C_{1}[ ]: Similar to the previous case.

□

This corollary shows that we can use an arbitrary representative for the equivalence classes up to ≡_{V} when performing dynamic reductions. Therefore, in the remainder of this article, we will use = instead of ≡_{V}.

4 The one-pass CPS transformation

We consider the one-pass version of Plotkin’s (left-to-right) call-by-value CPS transformation [3]. (Many others exist, depending, e.g., on the evaluation order of the source language [6].)

[[·]] : Syntax → (Syntax → Syntax) → Syntax
[[c]] = \overline{λ}K.K \overline{@} c
[[x]] = \overline{λ}K.K \overline{@} x
[[λx.e]] = \overline{λ}K.K \overline{@} λx.λk.[[e]]′ \overline{@} k
[[e_{1} @ e_{2}]] = \overline{λ}K.[[e_{1}]] \overline{@} \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.K \overline{@} v
[[·]]′ : Syntax → Syntax → Syntax
[[c]]′ = \overline{λ}K.K @ c
[[x]]′ = \overline{λ}K.K @ x
[[λx.e]]′ = \overline{λ}K.K @ λx.λk.[[e]]′ \overline{@} k
[[e_{1} @ e_{2}]]′ = \overline{λ}K.[[e_{1}]] \overline{@} \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ K

The transformation uses some fixed variables that are assumed to be “fresh”, i.e., that do not occur in the program to be transformed. These variables are denoted by ‘k’ and ‘v’, which are dynamic variables. We also fix the static variables K, V_{1}, and V_{2}. The static variables cannot clash with variables in the original program, but they must be distinct. All these fresh variables are written in Roman font.

Figure 1: The left-to-right, call-by-value CPS transformation in one pass

The one-pass CPS transformation is defined inductively with the two functions [[·]] and [[·]]′ displayed in Figure 1. Whereas Plotkin’s CPS transformation uses only one function, the one-pass transformation uses two, depending on whether the continuation is known statically ([[·]]) or not ([[·]]′). These two functions map λ-expressions as defined in Section 2 to expressions in the meta language defined in Section 3. Their type are easily inferred using the rules of Section 3.

We define the function Ψ to map direct-style values to CPS values:

\begin{aligned}Ψ(c) & = & c \\ Ψ(λx.e) & = & λx.λk.[[e]]′ \overline{@} k \end{aligned}

N.B. [[v_{v}]] = \overline{λ}K.K \overline{@} Ψ(v_{v}) and [[v_{v}]]′ = \overline{λ}K.K @ Ψ(v_{v}).

The two-level η-redex λv.κ \overline{@} v coerces a meta-language expression of type Syntax → Syntax into a meta-language expression of type Syntax, and therefore, the two CPS-transformation functions are related as follows.

Proposition 3 If e is a λ-expression and κ is a meta-language expression of type Syntax → Syntax then

[[e]]′ \overline{@} λv.κ \overline{@} v ⟼^{∗} [[e]] \overline{@} κ

remembering that we equate expressions up to static β-equivalence and that the identifier v is fresh, so it is not free in κ.

Proof: By structural induction on e.

Case e = x:

[[x]]′ \overline{@} λv.κ \overline{@} v = (λv.κ \overline{@} v) @ x
⟼ κ \overline{@} v[x/v]
= κ \overline{@} x  by Corollary 1
= [[x]] \overline{@} κ

Case e = λx.e_{1}:

[[λx.e_{1}]]′ \overline{@} λv.κ \overline{@} v = (λv.κ \overline{@} v) @ Ψ(λx.e_{1})
⟼ κ \overline{@} v[Ψ(λx.e_{1})/v]
= κ \overline{@} Ψ(λx.e_{1})
= [[λx.e_{1}]] \overline{@} κ

Case e = e_{1} @ e_{2}:

[[e_{1} @ e_{2}]]′ \overline{@} λv.κ \overline{@} v = [[e_{1}]] \overline{@} \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.κ \overline{@} v
= [[e_{1} @ e_{2}]] \overline{@} κ
□

5 The goal

Plotkin proved three properties of the CPS transformation: Indifference, Simulation, and Translation. We prove the first two for the one-pass CPS transformation.

Theorem 1 (Indifference) Eval_{v}([[e]] \overline{@} \overline{λ}V.V) = Eval_{n}([[e]] \overline{@} \overline{λ}V.V).

The Indifference theorem formalizes a key property of CPS, namely that CPS programs are evaluation-order independent.

Theorem 2 (Simulation) Eval_{v}([[e]] \overline{@} \overline{λ}V.V) = Ψ(Eval_{v}(e)).

where Ψ was defined in Section 4, just before Proposition 3.

The Simulation theorem formalizes the correctness of the call-by-value CPS transformation. For one point, the theorem shows that termination is preserved, but more essentially, it says that evaluating a CPS-transformed program yields the CPS counterpart of the result of evaluating the original program.

To prove Indifference and Simulation, Plotkin used four lemmas. We prove the same four lemmas for the one-pass CPS transformation. Plotkin’s proof then applies as is (see Section 7).

To handle administrative redexes, Plotkin introduced a colon translation. This translation is an infix operation mapping an expression and a continuation to the CPS counterpart of that expression applied to the continuation, but bypassing the initial administrative redexes introduced by the CPS transformation. To account for meta-level reductions at CPS-transformation time, we define a higher-order version of Plotkin’s colon translation.

Definition 2 (Higher-order colon translation)

c : κ = κ \overline{@} Ψ(c)
λx.e : κ = κ \overline{@} Ψ(λx.e)
v_{1} @ v_{2} : κ = Ψ(v_{1}) @ Ψ(v_{2}) @ λv.κ \overline{@} v
v_{1} @ e_{2} : κ = e_{2} : \overline{λ}V_{2}.Ψ(v_{1}) @ V_{2} @ λv.κ \overline{@} v  e_{2} not a value
e_{1} @ e_{2} : κ = e_{1} : \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.κ \overline{@} v  e_{1} not a value

Unlike Plotkin’s colon translation, which is first order and interspersed with the actual reductions, this colon translation is higher order (as indicated by the overlines) and its static, administrative reductions occur before the actual, dynamic reductions.

6 Plotkin’s four lemmas

Lemma 1 (Substitution lemma) For all λ-expressions e and all closed values v and variables x,

\begin{aligned}[[e]][Ψ(v)/x] & = & [[e[v/x]]] \\ [[e]]′[Ψ(v)/x] & = & [[e[v/x]]]′ \end{aligned}

Proof: By structural induction on e.

Case e = x:

[[x]][Ψ(v)/x] = (\overline{λ}K.K \overline{@} x)[Ψ(v)/x]
= \overline{λ}K.K \overline{@} Ψ(v)
= [[v]]
= [[x[v/x]]]

Case e = y:

[[y]][Ψ(v)/x] = (\overline{λ}K.K \overline{@} y)[Ψ(v)/x]
= \overline{λ}K.K \overline{@} y
= [[y[v/x]]]

Case e = λy.e_{1}, where y ≠ x

[[λy.e_{1}]][Ψ(v)/x] = (\overline{λ}K.K \overline{@} λy.λk.[[e_{1}]]′ \overline{@} k)[Ψ(v)/x]
= \overline{λ}K.K \overline{@} ((λy.λk.[[e_{1}]]′ \overline{@} k)[Ψ(v)/x])
= \overline{λ}K.K \overline{@} (λy.λk.[[e_{1}]]′[Ψ(v)/x] \overline{@} k)
= \overline{λ}K.K \overline{@} (λy.λk.[[e_{1}[v/x]]]′ \overline{@} k)  by I.H.
= [[λy.e_{1}[v/x]]]

Case e = e_{1} @ e_{2}:

[[e_{1} @ e_{2}]][Ψ(v)/x]
= \overline{λ}K.([[e_{1}]] \overline{@} \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.K \overline{@} v)[Ψ(v)/x]
= \overline{λ}K.([[e_{1}]][Ψ(v)/x]) \overline{@} \overline{λ}V_{1}.([[e_{2}]][Ψ(v)/x]) \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.K \overline{@} v
= \overline{λ}K.[[e_{1}[v/x]]] \overline{@} \overline{λ}V_{1}.[[e_{2}[v/x]]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.κ \overline{@} v by I.H.
= [[e_{1}[v/x] @ e_{2}[v/x]]]
= [[(e_{1} @ e_{2})[v/x]]]

The cases for [[·]]′ are similar. □

Lemma 2 (Administrative reductions) If e is a closed λ-expression and κ is a closed meta-language expression of type Syntax → Syntax then [[e]] \overline{@} κ ⟼_{V}^{+} e : κ (i.e., they are equal modulo ≡_{V}).

Proof: By structural induction on e.

Case e = c:

[[c]] \overline{@} κ = (\overline{λ}K.K \overline{@} c) \overline{@} κ
⟼_{V} κ \overline{@} c
= c : κ

Case e = λx.e_{1}:

[[λx.e_{1}]] \overline{@} κ = (\overline{λ}K.K \overline{@} Ψ(λx.e_{1})) \overline{@} κ
⟼_{V} κ \overline{@} Ψ(λx.e_{1})
= λx.e_{1} : κ

Case e = v_{1} @ v_{2}:

[[v_{1} @ v_{2}]] \overline{@} κ
= (\overline{λ}K.[[v_{1}]] \overline{@} \overline{λ}V_{1}.[[v_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.K \overline{@} v) \overline{@} κ
= (\overline{λ}K.(\overline{λ}K.K \overline{@} Ψ(v_{1}))\overline{@} \overline{λ}V_{1}.(\overline{λ}K.K \overline{@} Ψ(v_{2})) \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.K \overline{@} v)\overline{@}κ
⟼_{V}^{5} Ψ(v_{1}) @ Ψ(v_{2}) @ λv.κ \overline{@} v
= v_{1} @ v_{2} : κ

Case e = v_{1} @ e_{2}:

[[v_{1} @ e_{2}]] \overline{@} κ
= (\overline{λ}K.[[v_{1}]] \overline{@} \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.K \overline{@} v) \overline{@} κ
= (\overline{λ}K.(\overline{λ}K.K \overline{@} Ψ(v_{1})) \overline{@} \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.K \overline{@} v) \overline{@} κ
⟼_{V}^{3} [[e_{2}]] \overline{@} \overline{λ}V_{2}.Ψ(v_{1}) @ V_{2} @ λv.κ \overline{@} v
⟼_{V}^{∗} e_{2} : \overline{λ}V_{2}.Ψ(v_{1}) @ V_{2} @ λv.κ \overline{@} v  by I.H.
= v_{1} @ e_{2} : κ

Case e = e_{1} @ e_{2}:

[[e_{1} @ e_{2}]] \overline{@} κ
= (\overline{λ}K.[[e_{1}]] \overline{@} \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.K \overline{@} v) \overline{@} κ
⟼_{V} [[e_{1}]] \overline{@} \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.κ \overline{@} v
⟼_{V}^{∗} e_{1} : \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.κ \overline{@} v by I.H.
= e_{1} @ e_{2} : κ

This enumeration accounts for all expressions e. □

Lemma 3 (Single-step simulation) If e is a closed λ-expression, κ is a closed meta-language expression of type Syntax → Syntax, and e ⟼_{v} e′ then e : κ ⟼^{+} e′ : κ.

Proof: By structural induction on the evaluation context in the derivation of e ⟼_{v} e′.

Case C[ ] = [ ], i.e., (λx.e) @ v ⟼_{v} e[v/x]:

(λx.e) @ v : κ

= Ψ(λx.e) @ Ψ(v) @ λv.κ \overline{@} v
= (λx.λk.[[e]]′ \overline{@} k) @ Ψ(v) @ λv.κ \overline{@} v
⟼ ((λk.[[e]]′ \overline{@} k)[Ψ(v)/x]) @ λv.κ \overline{@} v
= (λk.[[e]]′[Ψ(v)/x] \overline{@} k) @ λv.κ \overline{@} v by Corollary 1
= (λk.[[e[v/x]]]′ \overline{@} k) @ λv.κ \overline{@} v  by Lemma 1
⟼ [[e[v/x]]]′ \overline{@} (λv.κ \overline{@} v)
⟼^{∗} [[e[v/x]]] \overline{@} κ  by Proposition 3
= e[v/x] : κ  by Lemma 2

Case C[ ] = C_{1}[ ] @ e_{2}, i.e., C_{1}[e_{1}] @ e_{2} ⟼_{v} C_{1}[e′_{1}] @ e_{2} derived from e_{1} ⟼_{v} e′_{1}:

C_{1}[e_{1}] @ e_{2} : κ

= C_{1}[e_{1}] : \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.κ \overline{@} v
⟼^{+} C_{1}[e′_{1}] : \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.κ \overline{@} v by I.H.
= e′  to give it a name

• If C_{1}[e′_{1}] is not a value, then C_{1}[e′_{1}] @ e_{2} : κ = e′

• If C_{1}[e′_{1}] is a value then

e′ = [[e_{2}]] \overline{@} \overline{λ}V_{2}.(Ψ(C_{1}[e′_{1}]) @ V_{2}) @ λv.κ \overline{@} v
= e_{2} : \overline{λ}V_{2}.Ψ(C_{1}[e′_{1}]) @ V_{2} @ (λv.κ \overline{@} v)  by Lemma 2
= e′′

– If e_{2} is not a value, then C_{1}[e′_{1}] @ e_{2} : κ = e′′.

– If e_{2} is a value, then

\begin{aligned}e′′ & = & Ψ(C_{1}[e′_{1}]) @ Ψ(e_{2}) @ λv.κ \overline{@} v \\ & = & C_{1}[e′_{1}] @ e_{2} : κ \end{aligned}

Case C[ ] = v_{1} @ C_{1}[ ], i.e., v_{1} @ C_{1}[e_{2}] ⟼_{v} v_{1} @ C_{1}[e′_{2}] derived from e_{2} ⟼_{v} e′_{2}:

v_{1} @ C_{1}[e_{2}] : κ = C_{1}[e_{2}] : \overline{λ}V_{2}.Ψ(v_{1}) @ V_{2} @ λv.κ \overline{@} v
⟼^{+} C_{1}[e′_{2}] : \overline{λ}V_{2}.Ψ(v_{1}) @ V_{2} @ λv.κ \overline{@} v by I.H.
= e′

• If C_{1}[e′_{2}] is a not value then v_{1} @ C_{1}[e′_{2}] : κ = e′.

• If C_{1}[e′_{2}] is a value then

\begin{aligned}e′ & = & Ψ(v_{1}) @ Ψ(C_{1}[e′_{2}]) @ λv.κ \overline{@} v \\ & = & v_{1} @ e′_{2} : κ \end{aligned}

□

Lemma 4 (Coincidence of stuck expressions) If e ∈ Sticks_{v} and κ is a closed meta-language expression with type Syntax → Syntax, then e : κ ∈ Sticks_{n} ∩ Sticks_{v}.

Proof: By induction on the structure of the stuck expression e.

Case e = c @ v:

\begin{aligned}(c @ v) : κ & = & Ψ(c) @ Ψ(v) @ λv.κ \overline{@} v \\ & = & c @ Ψ(v) @ λv.κ \overline{@} v \end{aligned}

which is stuck since c @ Ψ(v) is stuck both in call-by-name and call-by-value.

Case e = v_{1} @ e_{2} where e_{2} ∈ Sticks_{v}:

(v_{1} @ e_{2}) : κ = e_{2} : \overline{λ}V_{2}.Ψ(v_{1}) @ V_{2} @ λv.κ \overline{@} v

which is stuck by induction hypothesis, e_{2} being closed and structurally smaller that e.

Case e = e_{1} @ e_{2} where e_{1} ∈ Sticks_{v}:

(e_{1} @ e_{2}) : κ = e_{1} : \overline{λ}V_{1}.[[e_{2}]] \overline{@} \overline{λ}V_{2}.V_{1} @ V_{2} @ λv.κ \overline{@} v

which is stuck by induction hypothesis, e_{1} being closed and structurally smaller that e.

□

7 Plotkin’s double proof

Plotkin proved both Indifference and Simulation using four lemmas similar to the ones in the previous section. Let us restate his proof. Proof: Let us show that for any e, Eval_{v}([[e]] \overline{@} \overline{λ}V.V) and Eval_{n}([[e]] \overline{@} \overline{λ}V.V) either are both defined and yield the same result, which is Ψ(Eval_{v}(e)), or they are both undefined.

1. If Eval_{v}(e) = v_{v} (i.e., if e ⟼_{v}^{i} v_{v} for some i, by the definition of Eval_{v}(·) in Section 2.1) then

[[e]] \overline{@} \overline{λ}V.V = e : \overline{λ}V.V  by Lemma 2
⟼^{∗} v_{v} : \overline{λ}V.V  by repeated use of Lemma 3
= (\overline{λ}V.V) \overline{@} Ψ(v_{v}) since v_{v} is a value
= Ψ(v_{v})
= Ψ(Eval_{v}(e))

Therefore Eval_{v}([[e]] \overline{@} \overline{λ}V.V) = Ψ(Eval_{v}(e)). Furthermore, Lemma 3 only uses reductions in ⟼, and this relation is the intersection of the ⟼_{v} and ⟼_{n} relations. Therefore Eval_{v}([[e]] \overline{@} \overline{λ}V.V) = Eval_{n}([[e]] \overline{@} \overline{λ}V.V).

2. If Eval_{v}(e) is undefined then it is either because e reduces to a stuck term, or because e has an infinite reduction sequence.

(a) In the first case there exists an e′ ∈ Sticks_{v} such that e ⟼_{v}^{∗} e′. In that case

[[e]] \overline{@} \overline{λ}V.V = e : \overline{λ}V.V  by Lemma 2
⟼^{∗} e′ : \overline{λ}V.V  by repeated use of Lemma 3
∈ Sticks_{n} ∩ Sticks_{v} by Lemma 4

In words, whether one uses call by name or call by value, [[e]] \overline{@} \overline{λ}V.V reduces to a stuck term.

(b) In the second case there exists a sequence of expressions

e ⟼_{v} e_{1} ⟼_{v} e_{2} ⟼_{v} ⋯ ⟼_{v} e_{n} ⟼_{v} ⋯

In that case

[[e]] \overline{@} \overline{λ}V.V = e : \overline{λ}V.V by Lemma 2
⟼^{+} e_{1} : \overline{λ}V.V by Lemma 3
⟼^{+} e_{2} : \overline{λ}V.V by Lemma 3
⟼^{+} …
⟼^{+} e_{n} : \overline{λ}V.V by Lemma 3
⟼^{+} …

In words, [[e]] \overline{@} \overline{λ}V.V has an infinite reduction sequence too, both in call by name and in call by value.

Together these two cases prove the Simulation and Indifference theorems. □

8 Conclusion

We have adapted Plotkin’s four lemmas to the one-pass CPS transformation, which required us to introduce a higher-order colon translation. Given these four lemmas, Plotkin’s Indifference and Simulation theorems and their proof apply directly to validate the one-pass CPS transformation.

Other λ-encodings exist that give rise to administrative reductions—for example, in denotational semantics, the denotation of a program is obtained by a syntax-directed translation into the λ-calculus. The resulting λ-term contains many administrative redexes that need to be dealt with to reason about programs. A good semantics-directed compiler is expected to eliminate these administrative redexes at compile time. For example, an identifier is typically mapped into an application of the environment, and scope resolution is expected from a compiler, so that variables are looked up in constant time at run time. Factoring out administrative redexes at compile time (a.k.a. staging [8]) is accepted good practice. When the compiler is written in a higher-order functional language (say, ML), administrative reductions can be represented as ML reductions. What we have shown here is a way to prove the correctness of this higher-order representation in the particular case of the CPS transformation.

Acknowledgments: This work is supported by the ESPRIT Working Group

APPSEM (http://www.md.chalmers.se/Cs/Research/Semantics/APPSEM/).

Part of it was carried out while the second author was visiting John Hannan at Penn State, in the fall of 2000. We are grateful to the anonymous reviewers and to Julia Lawall for perceptive comments.

References

[1] Andrew W. Appel. Compiling with Continuations. Cambridge University Press, New York, 1992.

[2] Olivier Danvy, Belmina Dzafic, and Frank Pfenning. On proving syntactic properties of CPS programs. In Third International Workshop on Higher-Order Operational Techniques in Semantics, volume 26 of Electronic Notes in Theoretical Computer Science, pages 19–31, Paris, France, September 1999. Also available as the technical report BRICS RS-99-23.

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

[4] Olivier Danvy and Kristoffer Høgsbro Rose. Higher-order rewriting and partial evaluation. In Tobias Nipkow, editor, Rewriting Techniques and Applications, Lecture Notes in Computer Science, Kyoto, Japan, March 1998. Springer-Verlag. Extended version available as the technical report BRICS-RS-97-46.

[5] Matthias Felleisen. The Calculi of λ-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Department of Computer Science, Indiana University, Bloomington, Indiana, August 1987.

[6] John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 458–471, Portland, Oregon, January 1994. ACM Press.

[7] John Hatcliff and Olivier Danvy. Thunks and the λ-calculus. Journal of Functional Programming, 7(2):303–319, 1997. Extended version available as the technical report BRICS RS-97-7.

[8] Ulrik Jørring and William L. Scherlis. Compilers and staging transformations. In Mark Scott Johnson and Ravi Sethi, editors, Proceedings of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, pages 86–96, St. Petersburg, Florida, January 1986. ACM Press.

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

[10] John C. Reynolds. The discoveries of continuations. Lisp and Symbolic Computation, 6(3/4):233–247, December 1993.

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

[12] Mitchell Wand. Correctness of procedure representations in higher-order assembly language. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics, number 598 in Lecture Notes in Computer Science, pages 294–311, Pittsburgh, Pennsylvania, March 1991. Springer-Verlag.

Recent BRICS Report Series Publications

RS-00-33 Olivier Danvy and Lasse R. Nielsen. A Higher-Order Colon Translation. December 2000. 17 pp. To appear in Fifth International Symposium on Functional and Logic Programming, FLOPS ’01 Proceedings, LNCS, 2001.

RS-00-32 John C. Reynolds. What do Types Mean? - From Intrinsic to

Extrinsic Semantics. December 2000.

RS-00-31 Bernd Grobauer and Julia L. Lawall. Partial Evaluation of Pattern Matching in Strings, revisited. November 2000. 48 pp.

RS-00-30 Ivan B. Damgård and Maciej Koprowski. Practical Threshold RSA Signatures Without a Trusted Dealer. November 2000. 14 pp.

RS-00-29 Luigi Santocanale. The Alternation Hierarchy for the Theory of μ-lattices. November 2000. 44 pp. Extended abstract appears in Abstracts from the International Summer Conference in Category Theory, CT2000, Como, Italy, July 16–22, 2000.

RS-00-28 Luigi Santocanale. Free μ-lattices. November 2000. 51 pp. Short abstract appeared in Proceedings of Category Theory 99, Coimbra, Portugal, July 19–24, 1999. Full version to appear in a special conference issue of the Journal of Pure and Applied Algebra.

RS-00-27 ZoltánÉsik and Werner Kuich. Inductive^{∗}-Semirings. October 2000. 34 pp.

RS-00-26 František Čapkovič. Modelling and Control of Discrete Event Dynamic Systems. October 2000. 58 pp.

RS-00-25 Zoltán Ésik. Continuous Additive Algebras and Injective Simulations of Synchronization Trees. September 2000. 41 pp.

RS-00-24 Claus Brabrand and Michael I. Schwartzbach. Growing Languages with Metamorphic Syntax Macros. September 2000.

RS-00-23 Luca Aceto, Anna Ingólfsdóttir, Mikkel Lykke Pedersen, and Jan Poulsen. Characteristic Formulae for Timed Automata. September 2000. 23 pp.