BRICS RS-01-30 L. R. Nielsen: A Selective CPS Transformation BRICS

Basic Research in Computer Science

A Selective CPS Transformation

Lasse R. Nielsen BRICS Report Series RS-01-30 ISSN 0909-0878 July 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, 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/01/30/

A Selective CPS Transformation^{∗}

Lasse R. Nielsen BRICS ^{†}

Department of Computer Science, University of Aarhus ^{‡}

July 2001

Abstract

The CPS transformation makes all functions continuation-passing, uniformly. Not all functions, however, need continuations: they only do if their evaluation includes computational effects. In this paper we focus on control operations, in particular “call with current continuation” and “throw”. We characterize this involvement as a control effect and we present a selective CPS transformation that makes functions and expressions continuation-passing if they have a control effect, and that leaves the rest of the program in direct style. We formalize this selective CPS transformation with an operational semantics and a simulation theorem à la Plotkin.

Keywords: CPS-transformation, program transformation, colon translation, correctness proof.

∗To appear the proceedings of MFPS XVII, ENTCS vol. 45 † Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

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

E-mail: lrn@brics.dk

Contents

1 Introduction 3 1.1 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 Definitions 4 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 The CPS transformation . . . . . . . . . . . . . . . . . . . . . 6

3 The selective CPS transformation 7 3.1 Annotated source language . . . . . . . . . . . . . . . . . . . 8 3.2 The Selective CPS Transformation . . . . . . . . . . . . . . . 10 3.3 Semantics of annotated syntax . . . . . . . . . . . . . . . . . 10

4 Proof of correctness 12 4.1 The selective colon-translations . . . . . . . . . . . . . . . . . 12 4.2 Colon-translation lemmas . . . . . . . . . . . . . . . . . . . . 15 4.3 Proof of correctness . . . . . . . . . . . . . . . . . . . . . . . 19

5 Conclusion 20 5.1 Perspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 5.2 Future work . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

List of Figures

1 Abstract syntax of the source language . . . . . . . . . . . . . 4 2 The typing rules of the source language. . . . . . . . . . . . . 5 3 Semantics of the source language . . . . . . . . . . . . . . . . 6 4 The CPS transformation . . . . . . . . . . . . . . . . . . . . . 7 5 Effect type system . . . . . . . . . . . . . . . . . . . . . . . . 10 6 The selective CPS transformation . . . . . . . . . . . . . . . . 11 7 The selective colon translation on expressions . . . . . . . . . 13 8 The selective colon translation on contexts. . . . . . . . . . . 14

1 Introduction

This paper defines, and proves correct, a selective Continuation-Passing Style (CPS) transformation, i.e., one that preserves part of the program in direct style. It uses information about a program’s effect-behavior to guide the transformation. The particular computational effect we use is the control-transfer effect exemplified by “call with current continuation” [3].

1.1 Related work

Selectively CPS transforming a program is not a new idea.

Danvy and Hatcliff defined a selective CPS transformation based on strictness analysis [6]. When dealing with the effect of non-termination, a strict function is indifferent to the evaluation order of its argument, and as such arguments of strict functions could be transformed by a call-by-value transformation while the rest of the program was transformed by a call-by-name transformation. The same authors also investigated CPS transformation based on totality information, defining a selective transformation [7]. There is no immediate generalization of strictness to other effects than nontermination, though, whereas triviality (the absence of effects) generalizes immediately to all other computational effects, as we have exemplified with control effects.

Kim, Yi, and Danvy implemented a selective CPS transformation for the core language of SML of New Jersey to reduce the overhead of their CPStransformation which λ-encoded the exception effects of SML [15]. The implementation is very similar to the present work, though they treat exceptions instead of control operations and base the annotation on a specific exception analysis.

Recent work has focused on selective transformations for different reasons.

Reppy introduced a local CPS transformation in an otherwise directstyle compiler to improve the efficiency of nested loops [18]. Kim and Yi defined coercions between direct style and CPS terms with no other effects than non-termination, allowing arbitrary subexpressions to be transformed, and facilitating interfacing to external code in both direct style and CPS. The selective transformation was proven correct [14].

The present paper defines a selective CPS transformation for the simply typed λ-calculus extended with recursive functions and computational effects, namely callcc and throw, into λ-calculus with only recursive functions, i.e., with only non-termination as an effect. The transformation is based on an effect analysis, and it is proven correct with respect to the dynamic behavior of the program. We conjecture that the methodology extends to other types of effects, only differing in the details of the encoding of effectful primitives into λ-expressions.

1.2 Overview

Section 2 gives the syntax and semantics of a small, typed functional language with control effects, and shows the traditional (non-selective) CPS transformation. Section 3 extends the language with effect annotations which are verified by an effect system, and defines the selective CPS transformation guided by these annotations. Section 4 proves the correctness of the selective CPS transformation using Plotkin-inspired colon translations, and Section 5 concludes.

2 Definitions

We define the source and target language of our selective CPS transformation, giving the syntax and type predicates as well as an operational semantics.

2.1 Syntax

The source language is a call-by-value typed functional language with recursive functions and the canonical control operators: callcc and throw. The syntax is given in Figure 1, where x and f range over a set of identifiers and c ranges over a set of constants.

e ::= c | x | fun f x.e | e @ e | callcc x.e | throw e e

Figure 1: Abstract syntax of the source language

We identify expressions up to renaming of bound variables, i.e., fun f x.x = fun g y.y. We use the shorthand λx.e for a function-abstraction fun f x.e where f does not occur in e.

We require expressions to be well typed with regard to the typing rules in Figure 2, similar to those given by Harper, Duba, and MacQueen [12].

The syntax of types is given by the grammar:

τ ::= b | τ→τ | ⟨τ⟩

where b ranges over a set of base types, and ⟨τ⟩ is the type of continuations expecting a value of type τ.

In the rules ConstType is a mapping from constants to base types, giving the type of a constant, and Γ is a mapping from identifiers to types.

\frac{Γ(x) = τ}{Γ ⊢ x : τ}  \frac{ConstType(c) = b}{Γ ⊢ c : b}

\frac{Γ; x : τ_{1}; f : τ_{1}→τ_{2} ⊢ e : τ_{2}}{Γ ⊢ fun f x.e : τ_{1}→τ_{2}}

\frac{Γ ⊢ e_{1} : τ_{1}→τ_{2} Γ ⊢ e_{2} : τ_{1}}{Γ ⊢ e_{1} @ e_{2} : τ_{2}}

\frac{Γ; x : ⟨τ⟩ ⊢ e : τ}{Γ ⊢ callcc x.e : τ}  \frac{Γ ⊢ e_{1} : ⟨τ⟩ Γ ⊢ e_{2} : τ}{Γ ⊢ throw e_{1} e_{2} : τ_{2}}

Figure 2: The typing rules of the source language.

We define a program to be a closed expression of type b_{0}, an arbitrary base type, and we only prove the correctness of the transformation on entire programs.

2.2 Semantics

The source language has a left-to-right call-by-value(CBV) operational semantics given using evaluation contexts. We introduce an intermediate value to the syntax to represent captured continuations, and define the values and contexts recursively, and give the context-based reduction rules (Figure 3).

Notice that continuations are represented as contexts, so throwing a continuation amounts to reinstating a context.

This semantics uses evaluation contexts in a way similar to Felleisen [9], capturing the fact that for any expression, there is at most one enabled reduction at a time.

Subject reduction (e : τ and e → e′ implies e′ : τ where the rules have been extended to include contexts), can be proven by a completely standard proof, which has been omitted.

Extended expressions, values, and evaluation contexts:

e ::= … | ⟨E⟩
v ::= c | fun f x.e | ⟨E⟩
E ::= [ ] | E @ e | v @ E | throw E e | throw v E

Reduction rules:

E

[(fun f x.e) @ v]

→ E

[e [fun f x.e/f] [v/x]]
E ; [callcc x.e] → \begin{matrix}E \\ [ & e [⟨E⟩/x] & ] \end{matrix}

E

[throw ⟨E_{1}⟩ v]

→

E_{1}[v]

Figure 3: Semantics of the source language

2.3 The CPS transformation

The CPS transformation can be used to transform a program in the source language into a program in a similar language without callcc and throw, while preserving the computational behavior of the source program. That is, the translated program, when applied to an initial continuation, terminates if the source program did, and the result of the transformed program, which is of a base type, is the same as that of the original program.

The CPS-transformation has other interesting properties:

• It generates programs that can be evaluated under both a call-by-name (CBN) and a CBV semantics and yield the same result, which corresponds to the result of the source program. A number of CPS transformations exist, each corresponding to an evaluation-order for the source language [13].

• It generates programs where all applications are tail-calls, i.e., no application is in an argument position.

CPS transformations are used in many places, but primarily in compilers to give an intermediate representation [1, 21] and as a way to simplify the language of a program before applying other transformations or analyzes to it [4]. It is the last application that is the motivation for the present work.

The standard CBV CPS transformation is defined in Figure 4.

C[[c]] = λk.k @ C_{t}[[c]]
C[[x]] = λk.k @ C_{t}[[x]]
C[[fun f x.e]] = λk.k @ C_{t}[[fun f x.e]]
C[[e_{1} @ e_{2}]] = λk.C[[e_{1}]] @ λv.C[[e_{2}]] @ λv′.v @ v′ @ k
C[[callcc x.e]] = λk.λx.C[[e]] @ k @ k
C[[throw e_{1} e_{2}]] = λk.C[[e_{1}]] @ λv.C[[e_{2}]] @ v
C_{t}[[x]] = x
C_{t}[[c]] = c
C_{t}[[fun f x.e]] = fun f x.C[[e]]

Figure 4: The CPS transformation

The C_{t}[[·]] function is used to coerce values and identifiers into CPS form, which consists of transforming the bodies of function abstractions. Values and identifiers share the property that Reynolds called “being trivial” [19] and Moggi called “being a value” (as opposed to a computation) [16], in the sense that they have no computational effects, including nontermination. The C[[·]] function is used on expressions with potential effects, the “serious” expressions.

3 The selective CPS transformation

As stated in the previous section, we treat trivial and serious expressions differently. Trivial expressions are those that have no computational effects and serious expressions are those that might have effects. The safe approximation used by the standard CPS transformation assumes that any application might have effects, which is not unreasonable when one considers nontermination as an effect.

In the source language we have added control effects, and it makes sense only to focus on those, and let the termination behavior be preserved by only evaluating the result in a CBV semantics. If we do so, we can use an effect analysis to find the parts of the program that are guaranteed to be free of the control effects generated by callcc and throw. In the following we will use the words “trivial” and “non-trivial” about the absence or possible presence of control effects only, while ignoring the partiality effect of nontermination. That is, an expression that has an infinite reduction sequence can still be said to be “trivial” with regards to control effects. We are not aiming for evaluation-order independence, rather the source and target languages are assumed to have the same evaluation-order (call-by-value), so the translation need not take any measures to preserve or prevent nontermination in otherwise effect-free expressions.

This section defines effect-annotated expressions, an effect type system to check the consistency of the annotation, and a selective CPS transformation that keeps trivial applications in direct style.

3.1 Annotated source language

We annotate a program with annotations taken from the set {T, N}, which is a partial order with the ordering relation N < T.

We mark some applications as trivial, with a T, and some as (potentially) non-trivial, with an N. The trivial ones are kept in direct style, and as such do not expect to receive a continuation.

For an expression, an effect analysis can tell us one of three things:

• Some evaluation of the expression will certainly give rise to effects (meaning, in this case, the reduction sequence of the expression contains evaluations of callcc or throw expressions),

• no evaluation of the expression will give rise to effects, or

• we just don’t know either way, which can happen since the problem is generally undecidable.

These three options corresponds to a three pointed domain, where both certainty of effects and certainty of absence of effects are above the uncertainty. The present transformation aims to keep the expressions in the second case in direct style. Since any effectful expression must be put into CPS, we must treat the first and third cases equally, and they are both marked N. Unifying these two cases gives rise to the stated ordering where greater means more information is known: certainty of the absence of effects as opposed to only possible presence, only losing information when the two cases are unified.

A ::= T | N
e ::= c | x | fun^{A} f x.e | (e @^{A} e)^{A} | callcc x.e | throw e e

These are the minimal annotations needed for our purpose. We treat values and identifiers (the traditional trivial expressions) as if they were annotated as such, i.e., (e)^{T} is a match for any trivial expression, just as (e)^{N} matches the two control operators.

We require that an expression annotated as trivial actually is so, i.e., whenever it is evaluated, the reduction sequence contains no steps corresponding to reductions of callcc or throw expressions. Since we use this annotation as a basis for the selective CPS transformation, we will want to CPS transform all expressions that are not marked trivial.

We have to treat functions and applications with special care. When a lambda abstraction is applied at an application point, the body of the abstraction is also evaluated at that point. If the body is not trivial, then neither is the application, and after selective CPS transformation, the transformed application must pass a continuation to the transformed body, and the body should expect a continuation.

In a higher-order program, more than one abstraction can be applied at the same application point, and after transformation, all of these abstractions must either expect a continuation or not. That means that all functions that can end up in a given application must be transformed in the same way. That divides the abstractions into two groups, those transformed into CPS, i.e., expecting a continuation, and those kept in direct style, i.e., not expecting a continuation. Some abstractions with a trivial body might be transformed to expect a continuation in order to match the other abstractions that reach the same application points.

We will say that the annotation is “consistent” (with regards to the behavior of the program) if:

• All expressions marked trivial are trivial,

• all abstractions marked trivial, or non-trivial, are only applied at application points marked trivial, or non-trivial respectively, and

• all abstractions whose body are marked non-trivial, are themselves marked as non-trivial.

To check all this, we use an extension of the type system to an effect type system that guarantees that the annotation is consistent. The types are also annotated, so the grammar of types is:

τ ::= b | τ→^{A}τ | ⟨τ⟩

The effect system is shown in Figure 5.

If an expression is typeable in the original type system, then there exists at least one annotation that is typeable in the effect system, namely the one where all functions and applications are marked non-trivial.

\frac{Γ(x) = τ}{Γ ⊢ x : τ, T}  \frac{ConstType(c) = b}{Γ ⊢ c : b, T}

\frac{Γ[x : τ_{1}][f : (τ_{1}→^{A_{1}}τ_{2})] ⊢ e : τ_{2}, A A_{1} ≤ A}{Γ ⊢ fun f x.e : τ_{1}→^{A_{1}}τ_{2}, T}

\frac{Γ ⊢ e_{1} : τ_{1}→^{A_{3}}τ_{2}, A_{1} Γ ⊢ e_{2} : τ_{1}, A_{2} A ≤ min(A_{1}, A_{2}, A_{3})}{Γ ⊢ e_{1} @ e_{2} : τ_{2}, A}

\frac{Γ[x : ⟨τ⟩] ⊢ e : τ, A}{Γ ⊢ callcc x.e : τ, N}  \frac{Γ ⊢ e_{1} : ⟨τ⟩ , A_{1} Γ ⊢ e_{2} : τ, A_{2}}{Γ ⊢ throw e_{1} e_{2} : τ_{2}, N}

Figure 5: Effect type system

The ≤ in the rule for function abstractions is exactly due to the restriction on which functions can flow where. Functions with trivial bodies can be annotated with an N, allowing them to flow into an application expecting to pass a continuation, but this is reflected in the type, which is the only thing that is known at the application point. There are two different annotated function types, one for each annotation, and only one of these is allowed at each application point.

The ≤ on the rule for applications is discussed in the next section, We only consider well-annotated expressions from here on, i.e., expres-

sions that are allowed by the effect typing rules.

3.2 The Selective CPS Transformation

We define a CPS transformation that transforms well-annotated expressions and leaves trivial applications in direct style (Figure 6).

3.3 Semantics of annotated syntax

We do not change the semantics of the language, since the annotation is just a mark on the expressions, and it is only used by the CPS transformation. Still, in order to prove the correctness of the transformation, we define a reduction relation on annotated expressions that updates the annotation as well.

S[[e^{T}]] = k @ S_{t}[[e^{T}]]
S[[(e_{1} @^{N} e_{2})^{N}]] = λk.S[[e_{1}]] @ (λv.S[[e_{2}]] @ (λv′.v @ v′ @ k))
S[[(e_{1} @^{T} e_{2})^{N}]] = λk.S[[e_{1}]] @ (λv.S[[e_{2}]] @ (λv′.k @ (v @ v′)))
S[[callcc x.e]] = λk.(λx.S[[e]] @ k) @ k
S[[throw e_{1} e_{2}]] = λk.S[[e_{1}]] @ (λv.S[[e_{2}]] @ v)
S_{t}[[x]] = x
S_{t}[[c]] = c
S_{t}[[fun^{N} f x.e]] = fun f x.S[[e]]
S_{t}[[fun^{T} f x.e]] = fun f x.S_{t}[[e]]
S_{t}[[(e_{1} @^{T} e_{2})^{T}]] = S_{t}[[e_{1}]] @ S_{t}[[e_{2}]]

Figure 6: The selective CPS transformation

E[((fun^{A^{1}} f x.(e)^{A^{3}}) @^{A^{2}} v)^{A}] → E[(e)^{A^{3}} [fun^{A^{1}} f x.(e)^{A^{3}}/f] [v/x]]
E[callcc x.(e)^{A}] → E[(e)^{A} [⟨E⟩/x]]
E[throw ⟨E′⟩ v] → {E′ \atop [v]}

The point of this reduction relation is that values and identifiers are always marked trivial, and no expression marked trivial can ever reduce to one marked as non-trivial.

With these reduction rules, an expression marked non-trivial can reduce to one marked trivial, typically by reducing it to a value. If that happens to one of the subexpressions of an application, we can suddenly be in the situation where both of the subexpressions are trivial as well as the bodies of the functions expected to be applied there, and the entire application could now be consistently annotated as trivial. The weakening in the effect-typing rule for applications is there to avoid that such a change would mandate changes to annotations not local to the reduction taking place.

All these properties make a proof of Subject Reduction a trivial extension of the proof for the unannotated syntax.

One reason for having both annotations and an effect system, and not, e.g., only the effect system, is for ease of representation. Even if a reduced program allows a more precise effect-analysis than the original program, the transformation is based on the original program, and the annotated reduction keeps the original annotation throughout the reduction sequence.

4 Proof of correctness

To prove the correctness of the transformation, we must first specify a notion of correctness. In this case we require that the transformed program reduces to the same result as the original program.

Theorem 1 (Correctness of the Selective CPS Transformation) If e is a closed and well-annotated expression of type b_{0} then

e →^{∗} v ⇔ S[[e]] @ (λx.x) →^{∗} v

In Plotkin’s original proof, the result of the transformed program would be S_{t}[[v]], but since the program has a type where the only values are constants, and all constants satisfy S_{t}[[c]] = c, we can state the theorem as above.

4.1 The selective colon-translations

The proof uses a method similar to Plotkin’s in his original proof of the correctness of the CPS transformation [17]. It uses a so-called “colontranslation” to bypass the initial administrative reductions and focus on the evaluation point.

The intuition that drives the normal CPS transformation is that if e reduces to v then (C[[e]] @ k) should evaluate to (k @ C_{t}[[v]]). Plotkin captured this in his colon translation where if e → e′ then e : k →^{∗} e′ : k, and at the end of the derivation, values satisfied v : k = k @ Ψ(v), where Ψ(·) is what we write S_{t}[[·]].

The idea of the colon translation is that in e : k, the k represents the context of e, which in the transformed program has been collected in a continuation: a function expecting the result of evaluating e. The colon separates the source program to the left and the transformed program to the right of it. In the selective CPS transform, some contexts are not turned into continuations, namely the contexts of expressions marked trivial, since such expressions are not transformed to CPS expressions, and as such does not expect a continuation.

Therefore we have two colon translations, one for non-trivial expressions, with a continuation function after the colon, and one for trivial expressions with an evaluation context after the colon. The definition is shown in Figure 7. In both cases, what is to the left of the colon is a piece of source syntax, and what is to the right is a representation of the context of that expression in the source program translated to the target language. If the expression is trivial, the source context is represented by a context in the target language, and the translation of the expression is put into this context. If the expression is not trivial, then the source context is represented by a continuation function which is passed to the translation of the expression.

e^{T} : k = e^{T} : [k @ [ ]]
(e_{1} @^{N} e_{2})^{N} : k = e_{1} : λv.S[[e_{2}]] @ (λv′.v @ v′ @ k)  e_{1} not a value
(v_{1} @^{N} e_{2})^{N} : k = e_{2} : λv′.S_{t}[[v_{1}]] @ v′ @ k  e_{2} not a value
(v_{1} @^{N} v_{2})^{N} : k = S_{t}[[v_{1}]] @ S_{t}[[v_{2}]] @ k
(e_{1} @^{T} e_{2})^{N} : k = e_{1} : λv.S[[e_{2}]] @ (λv′.k @ (v @ v′)) e_{1} not a value
(v_{1} @^{T} e_{2})^{N} : k = e_{2} : λv′.k @ (S_{t}[[v_{1}]] @ v′)  e_{2} not a value
(v_{1} @^{T} v_{2})^{N} : k = k @ (S_{t}[[v_{1}]] @ S_{t}[[v_{2}]])
callcc x.e : k = (λx.S[[e]] @ k) @ k
throw e_{1} e_{2} : k = e_{1} : λv.S[[e_{2}]] @ v  e_{1} not a value
throw v_{1} e_{2} : k = e_{2} : S_{t}[[v_{1}]]  e_{2} not a value
throw v_{1} v_{2} : k = S_{t}[[v_{1}]] @ S_{t}[[v_{2}]]
x : E = {E \atop [x]}
c : E = E [c]
fun^{N} f x.e : E = \begin{matrix}E \\ [ & fun f x.S[[e]] & ] \end{matrix}
fun^{T} f x.e : E = \begin{matrix}E \\ [ & fun f x.S_{t}[[e]] & ] \end{matrix}
(e_{1} @^{T} e_{2})^{T} : E = e_{1} : E[([ ] @^{T} S_{t}[[e_{2}]])^{T}]  e_{1} not a value
(v_{1} @^{T} e_{2})^{T} : E = e_{2} : E[(S_{t}[[v_{1}]] @^{T} [ ])^{T}]  e_{2} not a value
(v_{1} @^{T} v_{2})^{T} : E = E[(S_{t}[[v_{1}]] @^{T} S_{t}[[v_{2}]])^{T}]

Figure 7: The selective colon translation on expressions

In Plotkin’s colon translation, v : k = k @ Φ(v). This also holds for this colon translation pair, since v : k = v : [k @ [ ]], since v is trivial, and v : [k @ [ ]] = k @ v by the definition of the e : E-translation.

The e : E-translation is not as significant as the e : k-translation, since all it does is apply the S_{t}-function to the argument, i.e., if e is a trivial expression then e : E = E[S_{t}[[e]]]. There are no administrative reductions to bypass in direct style.

We plan to use the colon translations on the result of reducing on the annotated expressions, so we extend it to work on continuation values, ⟨E⟩, which are values and as such trivial.

⟨E′⟩ : E = E[E′ : id]

where id = λx.x and E : k defines either a continuation function or a context as displayed in Figure 8, in which E^{T} represents any non-empty context with a top-most annotation as trivial.

[ ] : k = k
E^{T} : k = E^{T} : [k @ [ ]]
(E @^{N} e_{2})^{N} : k = E : λv.S[[e_{2}]] @ (λv′.v @ v′ @ k)
(E @^{T} e_{2})^{N} : k = E : λv.S[[e_{2}]] @ (λv′.k @ (v @ v′))
(v_{1} @^{N} E)^{N} : k = E : (λv′.S_{t}[[v_{1}]] @ v′ @ k)
(v_{1} @^{T} E)^{N} : k = E : (λv′.k @ (S_{t}[[v_{1}]] @ v′))
throw E e_{2} : k = E : λv.S[[e_{2}]] @ v
throw v_{1} E : k = E : S_{t}[[v_{1}]]
[ ] : E = E
(E @^{T} e_{2})^{T} : E′ = E : \begin{matrix}E′ \\ [ & [ ] @ S_{t}[[e_{2}]] & ] \end{matrix}
(v_{1} @^{T} E)^{T} : E′ = E : \begin{matrix}E′ \\ [ & S_{t}[[v_{1}]] @ [ ] & ] \end{matrix}

Figure 8: The selective colon translation on contexts.

The E : k-translation yields either continuation functions or contexts, depending on the annotation of the innermost levels of the context argument, and the E : E-translation always gives a context, but requires that the first argument’s outermost annotation is trivial.

These colon-translations satisfy a number of correspondences.

Proposition 1 For all contexts E_{1}, E_{2}, and E_{3}, and continuation functions (closed functional values) the following equalities hold.

E_{1} \left[{E_{2} \atop [ ]}\right] : k = E_{2} : (E_{1} : k)
E_{1} \left[{E_{2} \atop [ ]}\right] : E_{3} = E_{2} : (E_{1} : E_{3})

Proof: The proof is by simple induction on the context E_{1}.

• If E_{1} = [ ] then (\begin{matrix}E_{1} \\ [ & E_{2} [ ] & ] \end{matrix} : k) = (E_{2} : k) = (E_{2} : (E_{1} : k)) and (\begin{matrix}E_{1} \\ [ & E_{2} [ ] & ] \end{matrix} : E_{3}) = (E_{2} : E_{3}) = (E_{2} : (E_{1} : E_{3})).

• If E_{1} = [(E @^{N} e_{2})^{N}] then

E_{1} \left[{E_{2} \atop [ ]}\right] : k = (E[E_{2}] @^{N} e_{2})^{N} : k
= E [E_{2}] : λv.S[[e_{2}]] @ (λv′.v @ v′ @ k)  (def. of E : k)
= E_{2} : (E : λv.S[[e_{2}]] @ (λv′.v @ v′ @ k)) (I.H.)
= E_{2} : ([(E @^{N} e_{2})^{N}] : k)  (def. E : k)

• The remaining cases are similar.

One would expect that similar equalities hold for the colon translations on expressions, i.e., E [e] : k = e : (E : k) and E [e] : E′ = e : (E : E′), and indeed these equalities hold in most cases. The exception is when E is nonempty and the “innermost” expression of the context is not annotated as trivial, e.g., E_{1}[([ ] @ e_{1})^{N}] for some context E_{1} and expression e_{1}, and e is a value. Normally the e : k translation descends the left-hand side and rebuilds the context on the right hand side, either as a continuation function or as a context, depending on the annotation. The exception mentioned, E [e] : k, the focus of the colon translation, the expression on the left hand side of the colon, would never descend all the way down to a value. We have made special cases for v @ e to bypass administrative reductions, so E [v] : k would not equal v : (E : k), because the latter introduces an administrative reduction. Reducing that administrative reduction, applying k to S_{t}[[v]], does lead to v : (E : k) again in one or more reduction steps. That is, if e is a value and E is not a trivial context then e : (E : k) = (E : k) @ S_{t}[[e]] →^{∗} E [e] : k, and likewise for the e : E-relation.

Proposition 2 For all contexts E and E′, expressions e, and continuation functions k

e : (E : k) →^{∗} E [e] : k
e : (E : E′) →^{∗} E [e] : E′ (if e trivial)

and →^{∗} is →^{0}, i.e., equality, if e is not a value.

Proof: Omitted.

4.2 Colon-translation lemmas

Plotkin used four lemmas to prove his simulation and indifference theorems. We only prove simulation, which corresponds to Plotkin’s simulation, since we already know that indifference does not hold for a selective CPS transformation (at least unless the selectivity is based on the effect of nontermination as well).

Lemma 1 (Substitution) If Γ[x : τ_{1}] ⊢ e : τ_{2}, A and ⊢ v : τ_{1}, T is a closed value then

S[[e]] [S_{t}[[v]]/x] = S[[e [v/x]]]
S_{t}[[e]] [S_{t}[[v]]/x] = S_{t}[[e [v/x]]] (if e is trivial)

Proof: The proof is by induction on the structure of e, using the distributive properties of substitution and taking the trivial cases before the non-trivial ones (because the S[[·]] translation defers trivial subexpressions to the S_{t} transformation). The details have been omitted.

Lemma 2 (Initial reduction) If Γ ⊢ e : τ, A and k is a continuation function of appropriate type then

S[[e]] @ k →^{∗} e : k
\begin{matrix}E \\ [ & S_{t}[[e]] & ] \end{matrix} = e : E (if e is trivial)

Proof: Again, the proof is by induction on the structure of e with the S[[·]] case taken after the S_{t} case for trivial expressions.

The E[S_{t}[[·]]] = · : E case: There are four cases covering all trivial expressions:

• If e is a value or an identifier then e : E = E[S_{t}[[e]]] by definition of e : E.

• If e = (e_{1} @^{T} e_{2})^{T} (e_{1} not a value) then

(e_{1} @^{T} e_{2})^{T} : E = e_{1} : \begin{matrix}E \\ [ & [ ] @ S_{t}[[e_{2}]] & ] \end{matrix} (def. e : E)
= \begin{matrix}E \\ [ & S_{t}[[e_{1}]] @ S_{t}[[e_{2}]] & ] \end{matrix} (I.H.)
= E[S_{t}[[(e_{1} @^{T} e_{2})^{T}]]] (def. Ψ)

• If e = (v_{1} @^{T} e_{2})^{T} (e_{2} not a value) then

(v_{1} @^{T} e_{2})^{T} : E = e_{2} : \begin{matrix}E \\ [ & S_{t}[[v_{1}]] @ [ ] & ] \end{matrix} (def. e : E)
= \begin{matrix}E \\ [ & S_{t}[[v_{1}]] @ S_{t}[[e_{2}]] & ] \end{matrix} (I.H.)
= E[S_{t}[[(v_{1} @^{T} e_{2})^{T}]]] (def. Ψ)

• If e = (v_{1} @^{T} v_{2})^{T} then

(v_{1} @^{T} v_{2})^{T} : E = \begin{matrix}E \\ [ & S_{t}[[v_{1}]] @ S_{t}[[v_{2}]] & ] \end{matrix} (I.H.)
= E[S_{t}[[(v_{1} @^{T} v_{2})^{T}]]] (def. Ψ)

This accounts for all trivial expressions.

The S[[·]] @ k →^{∗} · : k case: There is one sub-case for each non-trivial expression, and one case for all trivial expressions:

• If e is trivial then S[[e]] @ k = k @ S_{t}[[e]] = e : [k @ [ ]] = e : k from the above cases and the definition of e : k.

• If e = (e_{1} @^{N} e_{2})^{N} (e_{1} not a value) then

S[[(e_{1} @^{N} e_{2})^{N}]] @ k

→ S[[e_{1}]] @ (λv.S[[e_{2}]] @ (λv′.v @ v′ @ k)) (def. S[[·]])
→^{∗} e_{1} : (λv.S[[e_{2}]] @ (λv′.v @ v′ @ k))  (I.H.)
= (e_{1} @^{N} e_{2})^{N} : k  (def. e : k)

• If e = (v_{1} @^{N} e_{2})^{N} (e_{2} not a value) then

S[[(v_{1} @^{N} e_{2})^{N}]] @ k

→ S[[v_{1}]] @ (λv.S[[e_{2}]] @ (λv′.v @ v′ @ k)) (def. S[[·]])
→ (λv.S[[e_{2}]] @ (λv′.v @ v′ @ k)) @ S_{t}[[v_{1}]] (def. S[[v]])
→ S[[e_{2}]] @ (λv′.S_{t}[[v_{1}]] @ v′ @ k)
→^{∗} e_{2} : λv′.S_{t}[[v_{1}]] @ v′ @ k  (I.H.)
= (v_{1} @^{N} e_{2})^{N} : k  (def. e : k)

• If e = (v_{1} @^{N} v_{2})^{N} then the proof is similar to the previous case except two values need to be applied to continuations instead of just one.

• If e = (e_{1} @^{T} e_{2})^{N} then the proofs are similar to the ones for e = (e_{1} @^{T} e_{2})^{N} except that the innermost application is k @ (v @ v′) instead of (v @ v′) @ k.

• If e = callcc x.e_{1} then S[[callcc x.e_{1}]] @ k → (λx.S[[e_{1}]] @ k) @ k = callcc x.e_{1} : k.

• If e = throw e_{1} e_{2} the proofs are similar to the ones for application.

Lemma 3 (Simulation) If E[e] → E′[e′] is one of the reduction rules for the annotated language, then

E [e] : id →^{∗} E′[e′] : id

and if the reduction is not of a throw expression, then the →^{∗} is actually one or more steps.

Proof: Counting annotations, there are five cases:

• If e = (fun^{N} f x.e_{1} @^{N} v)^{N} then

E[(fun^{N} f x.e_{1} @^{N} v)^{N}] : id

= (fun^{N} f x.e_{1} @^{N} v)^{N} : (E : id)  (Prop. 2)
= S_{t}[[fun^{N} f x.e_{1}]] @ S_{t}[[v]] @ (E : id)  (def. e : k)
= fun f x.S[[e_{1}]] @ S_{t}[[v]] @ (E : id)  (def. Ψ)
→ S[[e_{1}]] [S_{t}[[fun^{N} f x.e_{1}]]/f] [S_{t}[[v]]/x] @ (E : id)
= S[[e_{1} [fun^{N} f x.e_{1}/f] [v/x]]] @ (E : id)  (Lemma 1)
→^{∗} e_{1} [fun^{N} f x.e_{1}/f] [v/x] : (E : id)  (Lemma 2)
→^{∗} E[e_{1} [fun^{N} f x.e_{1}/f] [v/x]] : id  (Prop. 2)

• If e = (fun^{T} f x.e_{1} @^{T} v)^{N} then we know that e_{1} is trivial, since otherwise the function would be annotated N, and E : k is a continuation since E has no trivial inner sub-contexts.

E[(fun^{T} f x.e_{1} @^{T} v)^{N}] : id

= (fun^{T} f x.e_{1} @^{T} v)^{N} : (E : id)  (Prop. 2)
= (E : id) @ (S_{t}[[fun^{T} f x.e_{1}]] @ S_{t}[[v]])  (def. e : k)
= (E : id) @ (fun f x.S_{t}[[e_{1}]] @ S_{t}[[v]])  (def. Ψ)
→ (E : id) @ S_{t}[[e_{1}]] [S_{t}[[fun^{T} f x.e_{1}]]/f] [S_{t}[[v]]/x]
= (E : id) @ S_{t}[[e_{1} [fun^{T} f x.e_{1}/f] [v/x]]]  (Lemma 1)
→^{∗} e_{1} [fun^{T} f x.e_{1}/f] [v/x] : [(E : id) @ [ ]]  (Lemma 2, e_{1} trivial)
= e_{1} [fun^{T} f x.e_{1}/f] [v/x] : (E : id)  (def. e : k)
→^{∗} E[e_{1} [fun^{N} f x.e_{1}/f] [v/x]] : id  (Prop. 2)

• If e = (e_{1} @^{T} e_{2})^{T} then either E : k is a context or a continuation. If it is a continuation the proof proceeds just as the previous case. If it is a context then

E[(fun^{T} f x.e_{1} @^{T} v)^{T}] : id

= (fun^{T} f x.e_{1} @^{T} v)^{T} : (E : id)  (Prop. 2)
= (E : id)[S_{t}[[fun^{T} f x.e_{1}]] @ S_{t}[[v]]]  (def. e : k)

= (E : id)

[fun f x.S_{t}[[e_{1}]] @ S_{t}[[v]]]

(def. Ψ)

→ (E : id)[S_{t}[[e_{1}]] [S_{t}[[fun^{T} f x.e_{1}]]/f] [S_{t}[[v]]/x]]
= (E : id)[S_{t}[[e_{1} [fun^{T} f x.e_{1}/f] [v/x]]]]  (Lemma 1)
→^{∗} e_{1} [fun^{T} f x.e_{1}/f] [v/x] : (E : id)  (Lemma 2, e_{1} trivial)
→^{∗} E[e_{1} [fun^{N} f x.e_{1}/f] [v/x]] : id  (Prop. 2)

• If e = callcc x.e_{1} then

E [callcc x.e_{1}] : id

= callcc x.e_{1} : (E : id)  (Prop. 2)
= (λx.S[[e_{1}]] @ (E : id)) @ (E : id) (def. e : k)
→ S[[e_{1}]] @ (E : id) [(E : id)/x]
= S[[e_{1}]] [(E : id)/x] @ (E : id)  (E : k is closed)
= S[[e_{1}]] [S_{t}[[⟨E⟩]]/x] @ (E : id)  (def. S_{t}[[⟨E⟩]])
= S[[e_{1} [⟨E⟩/x]]] @ (E : id)  (Lemma 1)
→^{∗} e_{1} [⟨E⟩/x] : (E : id)  (Lemma 2)
→^{∗} \begin{matrix}E \\ [ & e_{1} [⟨E⟩/x] & ] \end{matrix} : id  (Prop. 2)

• If e = throw ⟨E′⟩ v then

E[throw ⟨E′⟩ v] : id = S_{t}[[⟨E′⟩]] @ S_{t}[[v]]  (def. e : k)
= (E′ : id) @ S_{t}[[v]] (def. S_{t}[[⟨E⟩]])
= v : [( @ E′ : id)[ ]] (def. v : E)
= v : (E′ : id)  (def. (e)^{T} : k)
→^{∗} \begin{matrix}E′ \\ [ & v & ] \end{matrix} : id  (Prop. 2)

In all cases except throw, there is at least one reduction step.

4.3 Proof of correctness

To prove the correctness of the selective CPS transformation, we use the simulation lemma in two ways.

Proof: The proof of e →^{∗} c ⟹ S[[e]] @ id →^{∗} c follows directly from the lemma 2 and repeated use of lemma 3. Assume e →^{∗} c.

S[[e]] @ id →^{∗} e : id  (Lemma 2)
→^{∗} c : id  (Lemma 3, repeated)
= c : [id @ [ ]] (def. (e)^{T} : k)
= id @ c  (def. c : E)
→ c

.

The other direction of correctness, S[[e]] @ id →^{∗} c ⟹ e →^{∗} c, is shown by contraposition. Assuming that for no c does e →^{∗} c, that is, e diverges, allows us to show that the same holds for S[[e]].

The proof that transformation preserves divergence also follow from Lemmas 2 and 3. Since S[[e]] @ id →^{∗} e : id it suffices to show that e : id has an arbitrary long reduction sequence.

Assume that e diverges. We show that for any n there exists an m such that if e →^{m} e_{1} then (e : id) →^{∗} (e_{1} : id) in n or more reduction steps.

This is proven by induction on n. The base case (n = 0) is trivial. For the induction case (n + 1) look at the n case. There exists m such that e →^{m} e_{1} and e : id →^{∗} e_{1} : id. Look at the reduction sequence from e_{1}.

• If the first reduction step (e_{1} → e_{2}) is not the reduction of a throw expression, then e_{1} : id →^{+} e_{2} : id, and m + 1 gives us our n + 1 or longer reduction sequence of e : id.

• If the first reduction step (e_{1} → e_{2}) is of a throw expression, then e_{1} : id →^{∗} e_{2} : id. In that case we look at the next step in the same way. Either we find a reduction that is not a throw, and we get the m needed for the proof, or there is nothing but reductions of throw expressions in the infinite reduction sequence of e_{1}.

There can not be an infinite sequence of reductions of throw expressions, since reducing a throw expression necessarily reduces the size of the entire program. A substitution into a context corresponds to the application of a linear function, and it reduces the size of the expression if one counts it as, e.g., number of distinct subexpressions or number of throw-expressions.

That means that e : id has an infinite reduction sequence.

5 Conclusion

We have proven the correctness of a selective CPS transformation based on an effect analysis. Similar proofs can be made for other λ-encodings and computational effects (e.g., with monads), where the immediate choice would be the effect of non-termination. This is the effect that is encoded by the traditional CPS transformation of languages with no other effects, and if one has an annotation of such a program, marking terminating (effect-free) expressions to keep in direct style, then the method works just as well.

5.1 Perspectives

Danvy and Hatcliff’s CPS transformation after strictness analysis [6] generalizes the call-by-name and the call-by-value CPS transformations. The same authors’ CPS transformation after totality analysis [7] generalizes the call-by-name CPS transformation and the identity transformation. In the same manner, the present work generalizes the call-by-value CPS transformation and the identity transformation, and proves this generalization correct.

Danvy and Filinski introduced the one-pass CPS-transformation [5] that removes the administrative reductions from the result by performing them at transformation time. This optimization can be applied to the selective CPS-transformation presented here as well. A proof of the correctness of the one-pass CPS-transformation also using Plotkin’s colon translation exists [8]. We expect that the methods used for proving correctness of the selectiveand the one-pass CPS transformations are orthogonal, and can easily be combined.

The selective CPS transformation presented here is based on an effect analysis and should generalize to other computational effects than control, e.g., state or I/O. The proof will not carry over to other effects, since it relies on the choice of λ-encoding of the effect primitives, but we expect that the structure of the proof can be preserved.

The approach taken is “Curry-style” in the sense that we have given a language and its operational meaning, and only after the fact we have associated types and effect annotation to the untyped terms. A “Church-style” approach, such as Filinski’s [10, 11], would have defined the language with explicit types and effect annotation, so that only well-typed, consistently annotated programs are given a semantics.

5.2 Future work

It is possible to prove results similar to the present ones for other choices of effects and combinations of effects. A sensible choice would be a monadic effect of state and control, since it is sufficient to implement all other choices of layered monads [11]. A proof similar to the present one for both state and control effects would be a logical next step.

Acknowledgments: The method of extending the colon translation to selective CPS transformation was originally developed in cooperation with Jung-taek Kim and Kwangkeun Yi from KAIST in Korea, and with Olivier Danvy from BRICS in Denmark. The present work would not have been possible without their inspiration. Thanks are also due to Andrzej Filinski and to the anonymous referees for their comments.

References

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

[2] Hans-J. Boehm, editor. Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, Portland, Oregon, January 1994. ACM Press.

[3] William Clinger, Daniel P. Friedman, and Mitchell Wand. A scheme for a higher-level semantic algebra. In John Reynolds and Maurice Nivat, editors, Algebraic Methods in Semantics, pages 237–250. Cambridge University Press, 1985.

[4] Daniel Damian and Olivier Danvy. Syntactic accidents in program analysis. In Philip Wadler, editor, Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming, pages 209–220, Montréal, Canada, September 2000. ACM Press.

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

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

[7] Olivier Danvy and John Hatcliff. On the transformation between direct and continuation semantics. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Proceedings of the 9th Conference on Mathematical Foundations of Programming Semantics, number 802 in Lecture Notes in Computer Science, pages 627–648, New Orleans, Louisiana, April 1993. Springer-Verlag.

[8] Olivier Danvy and Lasse R. Nielsen. A higher-order colon translation. In Herbert Kuchen and Kazunori Ueda, editors, Fifth International Symposium on Functional and Logic Programming, number 2024 in Lecture Notes in Computer Science, pages 78–91, Tokyo, Japan, March 2001. Springer-Verlag. Extended version available as the technical report BRICS RS-00-33.

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

[10] Andrzej Filinski. Representing monads. In Boehm [2], pages 446–457.

[11] Andrzej Filinski. Representing layered monads. In Alex Aiken, editor, Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Programming Languages, pages 175–188, San Antonio, Texas, January 1999. ACM Press.

[12] Robert Harper, Bruce F. Duba, and David MacQueen. Typing first-class continuations in ML. Journal of Functional Programming, 3(4):465–484, October 1993.

[13] John Hatcliff and Olivier Danvy. A generic account of continuationpassing styles. In Boehm [2], pages 458–471.

[14] Jung-taek Kim and Kwangkeun Yi. Interconnecting Between CPS Terms and Non-CPS Terms. In Sabry [20].

[15] Jung-taek Kim, Kwangkeun Yi, and Olivier Danvy. Assessing the overhead of ML exceptions by selective CPS transformation. In Greg Morrisett, editor, Record of the 1998 ACM SIGPLAN Workshop on ML and its Applications, Baltimore, Maryland, September 1998. Also appears as BRICS technical report RS-98-15.

[16] Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science, pages 14–23, Pacific Grove, California, June 1989. IEEE Computer Society Press.

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

[18] John Reppy. Local CPS conversion in a direct-style compiler. In Sabry [20].

[19] John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363– 397, 1998. Reprinted from the proceedings of the 25th ACM National Conference (1972).

[20] Amr Sabry, editor. Proceedings of the Third ACM SIGPLAN Workshop on Continuations CW’01, number 545 in Technical Report, Computer Science Department, Indiana University, Bloomington, Indiana, December 2000.

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

Recent BRICS Report Series Publications

RS-01-30 Lasse R. Nielsen. A Selective CPS Transformation. July 2001. 24 pp. To appear in Brookes and Mislove, editors, 27th Annual Conference on the Mathematical Foundations of Programming Semantics, MFPS ’01 Proceedings, ENTCS 45, 2000. A preliminary version appeared in Brookes and Mislove, editors, Preliminary Proceedings of the 17th Annual Conference on Mathematical Foundations of Programming Semantics, MFPS ’01, (Aarhus, Denmark, May 24–27, 2001), BRICS Notes Series NS-01-2, 2001, pages 201–222.

RS-01-29 Olivier Danvy, Bernd Grobauer, and Morten Rhiger. A Unifying Approach to Goal-Directed Evaluation. July 2001. 23 pp. To appear in New Generation Computing, 20(1), November 2001. A preliminary version appeared in Taha, editor, 2nd International Workshop on Semantics, Applications, and Implementation of Program Generation, SAIG ’01 Proceedings, LNCS 2196, 2001, pages 108–125.

RS-01-28 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. A Fully Equational Proof of Parikh’s Theorem. June 2001.

RS-01-27 Mario Jose Cáccamo and Glynn Winskel. A Higher-Order Calculus for Categories. June 2001. Appears in Boulton and Jackson, editors, Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs ’01 Proceedings, LNCS 2152, 2001, pages 136–153.

RS-01-26 Ulrik Frendrup and Jesper Nyholm Jensen. A Complete Axiomatization of Simulation for Regular CCS Expressions. June 2001. 18 pp.

RS-01-25 Bernd Grobauer. Cost Recurrences for DML Programs. June 2001. 51 pp. Extended version of a paper to appear in Leroy, editor, Proceedings of the 6th ACM SIGPLAN International Conference on Functional Programming, 2001.

RS-01-24 ZoltánÉsik and Zoltán L. Németh. Automata on Series-Parallel Biposets. June 2001. 15 pp. To appear in Kuich, editor, 5th International Conference, Developments in Language Theory DLT ’01 Proceedings, LNCS, 2001.