Retraction Approach to CPS Transform^{∗}

Jakov Kučan

Department of Mathematics Massachusetts Institute of Technology Cambridge, MA 02139, USA

                (kucan@theory.lcs.mit.edu)

Abstract

We study the continuation passing style (CPS) transform and its generalization, the computational transform, in which the notion of computation is generalized from continuation passing to an arbitrary one. To establish a relation between direct style and continuation passing style interpretation of sequential call-by-value programs, we prove the Retraction Theorem which says that a lambda term can be recovered from its continuationized form via a λ-definable retraction. The Retraction Theorem is proved in the logic of computational lambda calculus for the simply typable terms.

1 Introduction

The notions of a continuation and a continuation passing style (CPS) transform have been introduced by a number of authors (see [Rey93] for a historical overview). The main motivation for the independent developments of these concepts seemed to be twofold: explaining the behavior of imperative features in functional languages, and compilation of programs with higher order procedures. Further research led to development of CPS denotational semantics [SW74] (see also [Sto77]), and later categorical semantics of computations [Mog89], as well as compilers based on the CPS transform [Ste78] (see also [App92]). In both kinds of applications one of the central goals of

5-1 the research has been to establish a relationship between original terms and their images under the transform.

∗This research was supported in part by: “Types and Algorithms”, Office of Naval Research (N00014-93-1-1015), “Computational efficiency of optimal reduction in lambda calculus”, National Science Foundation (CDA-9504288), and “Logic, Complexity, and Programming Languages”, National Science Foundation (CCR-9216185).

In this work we view the CPS transform as a formalization of the (continuation passing style) denotational semantics of a call-by-value programming language in the βη lambda calculus λ_{n}.

To model call-by-value evaluation in a programming language we choose Moggi’s [Mog88] computational lambda calculus, λ_{c}, for the two reasons: 1) the logic of λ_{c} is sound for call-by-value reasoning, and 2) the logic of λ_{c} is complete for the class of models (computational lambda models [Mog88]) in which most commonly used computational effects can be expressed.

One way of asserting the correctness of the CPS transform, as an interpretation of λ_{c} in λ_{n}, is the equational correspondence result due to Sabry and Felleisen [SF92].

Theorem 1.1 (Sabry-Felleisen). For any two lambda terms M and N,

λ_{c} ⊢ M = N iff λ_{n} ⊢ \overline{M} = \overline{N}.

The left-to-right implication in this theorem says that the CPS transform preserves equality, and the right-to-left implication says that the transform also preserves distinctions. Thus, the transform gives an accurate picture of λ_{c}-equivalence in λ_{n}.

To formalize the problem we are trying to solve we observe that the left-to-right implication of the theorem also says that the CPS transform defines a function, T , mapping the λ_{c}-equivalence classes of lambda terms to the λ_{n}-equivalence classes of lambda terms. The right-to-left implication can be understood as saying that T is injective, and therefore has a left inverse, T^{−1}. We ask the question whether functions T , or its inverse T^{−1}, are definable. More precisely,

• is there a lambda term P, such that λ_{n} ⊢ (P M) = \overline{M}, and

• is there a lambda term R, such that λ_{c} ⊢ (R \overline{M}) = M?

An elementary argument given in [MR] shows that the answer to the first question must be “no”. In this work we give an affirmative answer to the second question. More precisely we prove the following theorem:

Theorem 1.2 (Retraction, for the CPS transform). For any simple type σ there is a lambda term R_{σ}, such that for all closed lambda terms M of type σ,

λ_{c} ⊢ (R_{σ} \overline{M}) = M.

5-2 A version of the above Retraction Theorem was proven by Meyer and Wand [MW85], where the conclusion of the theorem holds in the logic of λ_{n}. However, as the authors themselves have pointed out to us, their result is misleading. We are interested in behavior of a term M under a call-by-value evaluation, and λ_{n} is not sound for call-by-value reasoning in presence of any computational effects.

An interesting point about the CPS transform, viewed as an interpretation of a call-by-value programs, is that not only it can interpret pure functional programs, but can also be extended to interpret programs with control operators such as call/cc and abort. Different extensions of a functional language with “impure” features can also be given denotational semantics using a similar transform. For example, an interpretation of programs in a language with mutable store can be given using the state passing style (SPS) transform. As shown by Moggi [Mog88], a number of such computational effects can be described by the notion of a monad, and the CPS and the SPS transforms can be generalized to, what we call, the computational transform [Wad90, SW96].

The equational correspondence for the computational transform holds as well [SW96], and it is natural to ask whether the Retraction Theorem (Theorem 1.2) generalizes. However, the computational transform maps lambda terms to the terms of the “monadic metalanguage”, λ_{ml} [Mog91]. The language of λ_{ml} is extended with new constructs that the logic of the computational lambda calculus has no axioms for, so the question of whether there is a lambda term, R, (even in the language of λ_{ml}) such that

λ_{c} ⊢ (R M^{∘}) = M,

where M^{∘} denotes the computational transform of M, is ill formed. In order to study the Retraction Theorem in an abstract setting that can be applied to other transforms, as well as to the CPS transform, we define a modified computational transform, T_{⋄}, mapping lambda terms to lambda terms extended with two constants E and R that satisfy axiom

(R (E M)) = M.  (r-e)

The modified computational transform satisfies the equational correspondence result for the closed terms, and we prove the Retraction Theorem in the logic of λ_{c} extended with the axiom (r-e).

5-3 Theorem 1.3 (Retraction, for T_{⋄}). For any simple type σ there is a term R_{σ}, such that for all closed lambda terms M of type σ,

λ_{c}+(r-e) ⊢ (R_{σ} M^{⋄}) = M,

where M^{⋄} stands for the modified computational transform of M.

The proof of the above theorem consists of defining interpretations of types and terms, as well as an ε-relation between the interpretations, and proving that if a term M has a type σ, then the meaning of M and the meaning of σ are related by the ε-relation. This framework is in many ways similar to, and was inspired by, the type inference models developed in [Mit88].

Even though the transforms of interests, namely the CPS transform and the SPS transform, are not special cases of the modified computational transform, we benefit from studying the abstract transform in that we obtain a proof that does not depend on details of a particular transform, and can be applied, by modifying definitions appropriately, to either the CPS or the SPS transform. Hence, we obtain the Retraction Theorems for the CPS and the SPS transforms.

The fore mentioned results apply only to simply typed closed terms. To extend the applicability of these results we can proceed in two directions: we can extend the computational lambda calculus with new language constructs and axioms that define equational behavior of the new terms, and we can extend the type system so that our results apply to a larger class of terms.

Our results can be easily extended to a calculus, extending λ_{c}, with a datatype such as natural numbers and primitive operators on natural numbers. A more important class of extensions consists of those extensions which introduce a computational effect to λ_{c}. We have been able to extend the Retraction Theorem to λ_{c} extended with a divergent element. However, we stop short of proving the Retraction Theorem for λ_{c} terms extended with recursion.

In an attempt to prove the Retraction Theorem for all (untyped) closed terms, we extend the type system with recursive types and prove the following result. Call a term F a total function if for any value V, F (V) is λ_{c}-equivalent to a value.

5-4 Theorem 1.4. Assume terms e and r exist such that e and r are total functions satisfying (in λ_{c}+(r-e))

\begin{aligned}(e y) & = & λx.(E (e (y (r x)))) \\ (r y) & = & λx.(r (R (y (e x)))) \\ (r (e x)) & = & x. \end{aligned}

Then for every term M,

λ_{c}+(r-e) ⊢ (r (R M^{⋄})) = M.

Analogous theorems also hold for the CPS and the SPS transforms. The assumption of the above theorem is quite strong, and it remains to be seen whether such terms e and r exist. One should also investigate whether such elements exist in models that would allow interesting applications of the theorem.

2 Definitions

We assume the reader is familiar with elementary concepts of a lambda calculus. For details one is referred to [Bar84]. In this section we will provide concise definitions in order to disambiguate our notation.

2.1 Lambda calculus

Lambda terms are terms formed over an infinite set of variables by lambda abstraction and application. We will use a number of standard conventions when writing lambda terms, such as that application associates to the left, and in general, use parentheses freely to make terms easier to read. We will write (let x=M in N) to abbreviate the term ((λx.N) M), and M ∘ N for the term λx.(M (N x)). For most part (but not exclusively) we use letters M, N, P, etc. to range over arbitrary lambda terms, and letters U, V and W to range over values, that is lambda terms that are either variables, lambda abstractions or constants. Lower-case letters, x, y, z etc. will be used for variables.

We study provable equality between untyped lambda terms. If λ is a set of axions we write λ ⊢ M = N if the equation M = N can be derived using the rules of lambda congruence from the axioms in λ.

5-5

((λx.M) V) = M{V/x}  (β_{v})

λx.V x = V , x ∉ FV(V)  (η_{v})

(let x=M in x) = M  (unit)

(let x_{2}=(let x_{1}=M_{1} in M_{2}) in M) = (let x_{1}=M_{1} in (let x_{2}=M_{2} in M)) , x_{1} ∉ FV(M) (assoc)

(M N) = (let x=M in (x N))  (let.1)

(V M) = (let y=M in (V y))  (let.2)

Table 1: Axioms of λ_{c}.

For most part of this paper we consider equalities provable in Moggi’s λ_{c} (see Table 1), possibly extended with additional axioms for constants. In particular we will use constants E and R satisfying axiom

(R (E x)) = x.  (r-e)

2.2 Typing system

We consider a type system for assigning types to untyped lambda terms. Simple types are defined over a base type ı, i.e. ı is a type and σ→τ is a type whenever σ and τ are types. The type inference system consists of set of rules (given in Table 2) for deriving sequents of the form Γ ▷ M: σ, where M: σ is called a typing assertion and Γ is a typing hypothesis, i.e. a set of typing assertions of the form x_{i}: σ_{i}, where we always assume no variable x_{i} occurs more than once in Γ.

5-6

Γ, x: σ ▷ x: σ  (var)

\frac{Γ ▷ M: σ→τ, Γ ▷ N: σ}{Γ ▷ (M N): τ}  (app)

\frac{Γ, x: σ ▷ M: τ}{Γ ▷ λx.M: σ→τ}  (abs)

Table 2: Type inference rules for simple types.

2.3 Transforms

In this work we concentrate on three transforms mapping lambda terms to lambda terms. First we study the modified computational transform, T_{⋄}, mapping pure lambda terms to lambda terms extended with two constants E and R (see Table 3). The transform T_{⋄} can be viewed as an abstract transform which captures, for our purposes, important properties of the CPS and the SPS transforms. Namely, in the transform M^{⋄} of a term M, the order of evaluation (left-to-right and call-by-value) is made explicit. However, the additional structure that makes, in particular, the CPS transform attractive to compiler designers, is not reflected in the definition of T_{⋄}.

x^{⋄} =^{def} (E x)
(λx.M)^{⋄} =^{def} (E λx.M^{⋄})
(M N)^{⋄} =^{def} (let f=(R M^{⋄}), x=(R N^{⋄}) in (f x))

Table 3: The modified computational transform, T_{⋄}.

The next transform we study is the call-by-value version of the Fischer-Reynolds CPS transform. The definition we use (as well as the overline notation) is taken from [Plo75] (see Table 4).

Analogous to the CPS transform, used to give a denotational semantics of programs with mutable store, instead of control operators, is the state passing style transform (SPS). In the definition, given in Table 5, we used the pairing constructs as abbreviations. Namely, (let ⟨x_{1}, x_{2}⟩=M in N)

5-7

\overline{x} =^{def} λk.k x
\overline{λx.M} =^{def} λk.k λx.\overline{M}
\overline{(M N)} =^{def} λk.\overline{M} (λm.\overline{N} (λn.m n k))

Table 4: The CPS transform.

abbreviates the expression

(let x=M in (let x_{1}=π_{1}(x) in (let x_{2}=π_{2}(x) in N))).

x^{∗} =^{def} λs.⟨x, s⟩
(λx.M)^{∗} =^{def} λs.⟨λx.M^{∗}, s⟩
(M N)^{∗} =^{def} λs.(let ⟨x_{1}, s_{1}⟩=(M^{∗} s),
⟨x_{2}, s_{2}⟩=(N^{∗} s_{1}) in (x_{1} x_{2} s_{2}))

Table 5: The SPS transform.

Even though we give untyped definitions of the transforms, we believe the transforms should be understood in the context of a typed language. This view is supported by the monadic framework, developed by Moggi [Mog88], in which programs are interpreted as “computations”. We leave out the details of Moggi’s monadic interpretation, as well as the definitions of the typed transforms, since they are not central to our development, but rather sketch the intuitive picture to help motivate some of our definitions.

We think of a transform mapping terms of type σ (intuitively programs) to terms of type T (σ′) (intuitively computations), where T is a unary type constructor (that depends on the particular transform), and σ′ is defined inductively using T to be ı′ = ı and (τ_{1}→τ_{2})′ = τ′_{1}→T (τ′_{2}). This can be made precise by defining the typed version of the transform mapping typing sequents to typing sequents.

5-8

3 Retraction Theorem

In this section we state and prove the Retraction Theorem for the abstract transform, T_{⋄}, as well as, for the CPS and the SPS transforms. While one might not find the transform T_{⋄} interesting in itself, for us it serves the purpose. More precisely, we develop a framework which enables us to prove the Retraction Theorem for the transform T_{⋄}, and is free of the details specific to the CPS and the SPS transforms. Nevertheless, the framework can be effortlessly modified to prove the Retraction Theorem for each of these transforms. Thus we believe that focusing on the more abstract transform, T_{⋄}, improves the clarity of our presentation.

3.1 Retractions

The Retraction Theorem asserts the definability of the inverse of the CPS transform (as well as other transforms of interest). We now give a construction of the type-indexed family of lambda terms that define the retraction. Note that we give the following definitions using terms E and R, but the definitions should be understood as parameterized by these terms. That is, the inverse of the modified computational transform will be defined using constants E and R, and in the definition of the inverse of the CPS transform, these constants will be replaced by the terms E^{K} and R^{K}. Likewise for the SPS transform, terms E^{S} and R^{S} will be used.

If we think of transforms in the context of a typed language, mapping terms (of type σ) to terms representing computations (of type T (σ′)), intuitively, we can understand the pairs of terms defined below as retractionembedding pairs between types σ and T (σ′). One can also formally define a notion of a type σ being a retract of a type τ, and in the sense of such definition, given below, we exhibit terms R_{σ} and E_{σ} that form a retractionembedding pair between types σ and T (σ′). Moreover, we will show that (suitable versions of) terms R_{σ} define the required inverses of the transforms we study.

Definition 3.1. A type σ is said to be a retract of a type τ if there is a pair of lambda terms R_{σ,τ} and E_{σ,τ} of types τ→σ and σ→τ respectively, such that (R_{σ,τ} (E_{σ,τ} x)) = x is provable.

Definition 3.2. For each simple type, σ, define terms e_{σ} and r_{σ} inductively on the structure of σ as follows:

e_{ı} =^{def} r_{ı} =^{def} λx.x,

5-9 and at higher types we have

\begin{matrix}e_{τ_{1}→τ_{2}} & =^{def} & λf.λx.(E (e_{τ_{2}} (f (r_{τ_{1}} x)))) \\ r_{τ_{1}→τ_{2}} & =^{def} & λf.λx.(r_{τ_{2}} (R (f (e_{τ_{1}} x)))). \end{matrix}

Lemma 3.3. λ_{c}+(r-e) ⊢ (r_{σ} (e_{σ} x)) = x

Proof: Easy by induction on σ.

Note: Above lemma holds whenever we replace constants E and R with any values E′ and R′ such that λ_{c} ⊢ (R′ (E′ x)) = x.

Finally we define terms R_{σ} = λx.(r_{σ} (R x)) and E_{σ} = λx.(E (e_{σ} x)). Later we will show that R_{σ} is an inverse of the transform T_{⋄}. To define an inverse of the CPS transform we first define terms R^{K} =^{def} λx.(x λz.z) and E^{K} =^{def} λxk.(k x). It is easy to show (in λ_{c}) that (R^{K} (E^{K} x)) = x. We define the retraction-embedding pair (R_{σ}^{K}, E_{σ}^{K}) using terms R^{K} and E^{K} instead of constants R and E in the above definitions. Similarly for the SPS transform we define terms R^{S} =^{def} λx.(π_{1} (x init)) and E^{S} =^{def} λxs.⟨x, s⟩, where init represents some initial state of the store, and define terms R_{σ}^{S} and E_{σ}^{S} using these terms instead.

3.2 Interpretations of Terms and Types

The framework we develop to prove the Retraction Theorem is closely related to Mitchell’s type inference models [Mit88]. As in the definition of a type inference model we define interpretations of terms and types, as well as a relation between the two. However, the definition of a type inference model assumes one works with the full βη-equality, and we need to relax the definitions to accommodate reasoning in the weaker logic of λ_{c}.

We will first sketch the definitions for the general framework and then fill in the details that apply to each particular transform we study.

Interpretation of terms: Assume (D, App) is an applicative structure, that is, D is a set and App is a binary operation on D. Assume also that there is a distinguished subset, V(D) ⊆ D, of values. Given an environment, ρ, mapping variables to V(D) we define an interpretation (relative to ρ) that to each term M assigns an element ⟦M⟧ρ of D. In addition we assume that

⟦(M N)⟧ρ = App(⟦M⟧ρ, ⟦N⟧ρ).

5-10

In particular we will define D to be the set of equivalence classes of terms and the set of values to be the equivalence classes of terms that are values. (Note: below, we may be informal and identify terms with their equivalence classes.) The interpretation function will then be defined by the transform in consideration.

Interpretation of types: The types will be interpreted as certain subsets of D called type sets.

In particular we will chose type sets to contain only the equivalence classes of terms of the form (E V) for some value V. The interpretation of types will be defined (using the ε-relation defined below) inductively:

⟦ı⟧ =^{def} set of all terms of the form (E V)
⟦σ→τ⟧ =^{def} set of all M (of the form (E V)) such that ∀N ∈ ⟦σ⟧:
• App(M, N) ε ⟦τ⟧
• (R_{τ} App(M, N)) = ((R_{σ→τ} M) (R_{σ} N))

Relating the interpretations: To relate meanings of terms and types, instead of using the simple set-membership relation, we define an extended membership relation ε ⊇ ∈. This relation will in general depend on the structure of the transform in consideration, and intuitively, will serve the purpose of separating out “important” part of the transformed term.

Truth and validity: Having defined the above notions, we say that a typing assertion M: σ is true (with respect to ρ), written ρ ⊧ M: σ, if ⟦M⟧ρ ε ⟦σ⟧. The notions of satisfaction and validity are defined in the standard way relative to the definition of truth. Namely, ρ satisfies a typing hypothesis Γ, written ρ ⊧ Γ, if every typing assertion in Γ is true with respect to ρ, and a typing sequent Γ ▷ M: σ is valid, written Γ ⊧ M: σ, if M: σ is true for every ρ that satisfies Γ.

Our aim is to prove a soundness lemma for the type inference system that would imply the Retraction Theorem. Before we state the lemma, we single out two conditions that are necessary for the lemma to hold. Namely we require that for all M ε ⟦σ→τ⟧ and N ε ⟦σ⟧:

App(M, N) ε ⟦τ⟧  (†)

(R_{τ} App(M, N)) = ((R_{σ→τ} M) (R_{σ} N)),  (‡)

5-11 where R_{σ}, etc. are defined in Section 3.1 and equality is provable equality in λ_{c}+(r-e). The main reason why these two conditions are singled out is that, having proved the Retraction Theorem for the modified computational transform, we modify the definition of the interpretations of terms and types, as well as the ε-relation, to reflect properties of the CPS transform, and only the conditions (†) and (‡) need to be proved again to show that the Retraction Theorem holds for the CPS transform. Similarly for the SPS transform.

3.3 Modified Computational Transform

In the previous section we outlined the definitions of our framework, and we can now fill in the details. The following definitions are given, in particular, to prove the Retraction Theorem for the modified computational transform, T_{⋄}, but we will also indicate how these definitions need to be changed in the subsequent sections to prove the Retraction Theorem for the CPS and the SPS transforms.

We write “=” to denote an equality provable in λ_{c}+(r-e).

Definition 3.4. Let ρ be a substitution mapping variables to values. Define the interpretation function ⟦·⟧ to be

⟦M⟧ρ =^{def} ρ(M^{⋄}).

Definition 3.5. Type sets are sets of terms of the form (E V), where V is a value.

Note: this definition is to be understood as parameterized by the term E, that is, when we consider, say, the CPS transform we will use the term E^{K} instead.

Definition 3.6. If M and N are terms, we define the application in the codomain of the transform as follows:

App(M, N) =^{def} (let f=(R M), x=(R N) in (f x)).

It is easy to see that ⟦(M N)⟧ρ = App(⟦M⟧ρ, ⟦N⟧ρ).

Definition 3.7. Let S be a type set and let M be a term. We write M ε S if there is a value V and terms P_{1}, …, P_{k} such that

M = (let x_{1}=P_{1}, …, x_{k}=P_{k} in (E V)),

and (E V) ∈ S.

5-12 Definition 3.8. The interpretation of types is defined inductively on the structure of type expressions. Namely,

⟦ı⟧ =^{def} set of all terms of the form (E V)
⟦σ→τ⟧ =^{def} set of all M, of the form (E V), such that ∀N ∈ ⟦σ⟧,
• App(M, N) ε ⟦τ⟧
• (R_{τ} App(M, N)) = ((R_{σ→τ} M) (R_{σ} N))

Recall that R_{σ} = r_{σ} ∘ R.

Note: We should understand this definition as parameterized by E, R, App, and ε. When we consider the CPS or the SPS transform, the appropriate definitions will be used instead.

Equipped with the definitions we can prove the Soundness Lemma, but first we need some auxiliary results.

Lemma 3.9. For each type σ and any value V, (E (e_{σ} V)) ∈ ⟦σ⟧.

Proof: Easy by induction on σ.

Lemma 3.10. For any two terms M and N such that M ε ⟦σ→τ⟧ and N ε ⟦σ⟧,

App(M, N) ε ⟦τ⟧,

and

(R_{τ} App(M, N)) = ((R_{σ→τ} M) (R_{σ} N)).

Proof: First observe that the statement of this lemma is stronger than what is given in Definition 3.8 above. The definition only requires that the two statements hold only for N ∈ ⟦σ⟧, and in the lemma we show that these two statements hold for all N ε ⟦σ⟧. Both conditions can be easily proved using the definitions and axioms of λ_{c}+(r-e).

The Soundness Lemma consists of two parts, (S.1) and (S.2). The first part asserts the soundness of our interpretation with respect to typing rules of the simply typed lambda calculus, and the second part is, in fact, the statement of the Retraction Theorem.

Lemma 3.11 (Soundness). Let Γ be a typing hypothesis and let ρ be a substitution that satisfies Γ. Let ρ′ be a substitution such that for each x_{i}: σ_{i} ∈ Γ, ρ′(x_{i}) = (r_{σ_{i}} x_{i}). Then, if Γ ▷ M: σ,

5-13

Γ ⊧ M: σ  (S.1)

and

λ_{c}+(r-e) ⊢ (R_{σ} ρ(M^{⋄})) = ρ′(M)  (S.2)

Proof: We prove the lemma by induction on the derivation of Γ ▷ M: σ. The (var) case follows by assumptions, and the (app) case follows directly by Lemma 3.10 and induction hypotheses.

The (abs) case is slightly more involved. Assume M ≡ λx.N and σ ≡ τ_{1}→τ_{2}, and that Γ ▷ λx.N: τ_{1}→τ_{2} was derived from Γ, x: τ_{1} ▷ N: τ_{2} using the (abs) rule.

To show (S.1), first observe that ρ((λx.N)^{⋄}) = (E ρ(λx.N^{⋄})), so we need to show that ρ((λx.N)^{⋄}) ∈ ⟦τ_{1}→τ_{2}⟧. Let (E V) be any term in ⟦τ_{1}⟧. Then

App(ρ((λx.N)^{⋄}), (E V)) = ρ{V/x}(N^{⋄}),

and therefore since ρ{V/x} satisfies Γ, x: τ_{1}, by induction hypothesis (S.1), App(ρ((λx.N)^{⋄}), (E V)) ε ⟦τ_{2}⟧. Moreover we can compute

(R_{τ_{2}} App(ρ((λx.N)^{⋄}), (E V))) = ((R_{τ_{1}→τ_{2}} ρ((λx.N)^{⋄})) (R_{τ_{1}} (E V))),

using the definition of the retraction-embedding pairs, and both induction hypotheses (S.1) and (S.2). This establishes (S.1). To show (S.2) simply compute

(R_{τ_{1}→τ_{2}} ρ((λx.N)^{⋄})) = ρ′(λx.N)

using properties of retraction-embedding pairs, Lemma 3.9 and induction hypothesis (S.2).

The Retraction Theorem follows directly from this lemma.

Theorem 3.12 (Retraction, for T_{⋄}). For any closed term M of (simple) type σ,

λ_{c}+(r-e) ⊢ (R_{σ} M^{⋄}) = M.

5-14

3.4 The CPS Transform

To prove the the Retraction Theorem for the CPS transform, as indicated before, we will use exactly the same framework, but will modify the definitions using appropriate definitions of application in the codomain of the transform and ε-relation. First recall that we define the retraction-embedding pair (R^{K}, E^{K}) to be

E^{K} =^{def} λxk.(k x) and R^{K} =^{def} λx.(x (λz.z)).

It is easy to see that λ_{c} ⊢ (R^{K} (E^{K} x)) = x, which is the only abstract property of E and R we use.

We define the interpretation of terms (relative to a substitution ρ) using the CPS transform, that is,

⟦M⟧ρ =^{def} ρ(\overline{M}).

The application in the codomain of the transform is defined to be

App^{K}(M, N) =^{def} λk.M (λm.N (λn.m n k)),

so that \overline{(M N)} = App^{K}(\overline{M}, \overline{N}). Finally, we define the extended membership relation, ε^{K}, to be

M ε^{K} S iff M = λk.((let x_{1}=P_{1}, …, x_{l}=P_{l} in (E^{K} V)) k),

for some terms P_{i}, a value V such that (E^{K} V) ∈ S, and a fresh variable k.

It should be understood that all the definitions used in the preceding section are now defined using E^{K}, R^{K}, App^{K} and ε^{K}, instead of E, R, App and ε.

With the new definitions, we prove the following lemma, analogous to Lemma 3.10, asserting that conditions (†) and (‡) hold.

Lemma 3.13. For any two terms M and N such that M ε^{K} ⟦σ→τ⟧ and N ε^{K} ⟦σ⟧,

App^{K}(M, N) ε^{K} ⟦τ⟧,

and

(R_{τ}^{K} App^{K}(M, N)) = ((R_{σ→τ}^{K} M) (R_{σ}^{K} N)).

Proof: The proof is straightforward using the definitions and axioms of λ_{c}.

5-15 Having shown the above lemma, the rest of the proof of the Soundness Lemma for the CPS transform is exactly the same as in the case of the modified computational transform, and as a corollary we obtain the retraction result.

Theorem 3.14 (Retraction, for the CPS transform). For any closed term M of (simple) type σ,

λ_{c} ⊢ (R_{σ}^{K} \overline{M}) = M.

3.5 The SPS Transform

To adopt our framework to the SPS transform we define E^{S}, R^{S}, App^{S} and ε^{S} in place of E, R, App and ε, and prove that the conditions (†) and (‡) still hold. Recall that the terms E^{S} and R^{S} are defined to be

E^{S} =^{def} λxs.⟨x, s⟩ and R^{S} =^{def} λx.(π_{1} (x init)),

where init is some initial state of the store.

The interpretation of terms is defined using the SPS transform. Namely,

⟦M⟧ρ =^{def} ρ(M^{∗}).

The application in the codomain of the transform is define to be

App^{S}(M, N) =^{def} λs.(let ⟨x_{1}, s_{1}⟩=(M^{∗} s), ⟨x_{2}, s_{2}⟩=(N s_{1}) in (x_{1} x_{2} s_{2})),

so that (M N)^{∗} = App^{S}(M^{∗}, N^{∗}). Finally we define the extended membership relation, ε^{S}, as follows:

M ε^{S} S iff M = λs.(let x_{1}=P_{1}, … x_{l}=P_{l} in ⟨V, s⟩),

for some terms P_{i}, some value V such that (E^{S} V) ∈ S, and fresh s.

Furthermore, we interpret the definitions of type sets, interpretation of types, and retraction-embedding pairs defined earlier, as if given using E^{S}, R^{S}, App^{S} and ε^{S}, in place of E, R, App and ε. With the new definitions we can show that conditions (†) and (‡) are still satisfied. This yields the Retraction Theorem for the SPS transform.

Theorem 3.15 (Retraction, for the SPS transform). For any closed term M of (simple) type σ,

λ_{c} ⊢ (R_{σ}^{S} M^{∗}) = M.

5-16

3.6 Extensions

Thus far we have only proved the retraction results for the pure simply typed terms. In order to make these results more applicable we would like to extend the theorems to a larger class of terms. We have essentially two directions in which we can proceed. We can extend the class of terms by adding constants or term constructors (including possibly new axioms that define functional behavior of the new terms), and secondly, we can extend the type system to one that can type a larger class of terms.

Extending the Retraction Theorem to an extension of λ_{c} with constants of a base type and primitive operators such as numerals is quite straightforward. However, adding arbitrary constants of higher order types may be more difficult. The difficulty lies in ensuring the closure conditions imposed on type sets by the addition of such constants are satisfied. For example if a constant c of type σ→τ is added to λ_{c}, we need to make sure that if M ε σ then App(c^{⋄}, M) ε τ. While such closure conditions are determined based on the type of new constants, the proof they are satisfied will, in general, depend on the functional behavior of the new constants.

Divergence: The difference between call-by-name and call-by-value evaluation strategies becomes apparent only in presence of actual computational effects. So far we have only considered pure simply typed terms. In this setting every closed term is equivalent to a value in both logics of λ_{c} and λ_{n}. Therefore, if we were to stop here, it would be unjustified to claim significant improvement over the original Meyer-Wand Retraction Theorem.

The simplest computational effect we can add to the language is divergence. In presence of divergence λ_{n} reasoning is no longer sound for callby-value languages, so for any applications in λ_{c} extended with divergence, we really need the stronger version of the Retraction Theorem provable in the weaker logic of λ_{c}. While extension of the Retraction Theorem to a language with divergence, which we now present, is quite straightforward, it is important since it illustrates the difference between Meyer and Wand’s and our formulation of the Retraction Theorem.

Divergence is represented by the divergent element, Ω, that is added to the language of λ_{c} as a constant, but it is not considered a value. The axioms for Ω specify that an application diverges if either the operators or the operand diverges. Moreover, these axioms identify all divergent terms. The axioms are:

(Ω M) = Ω and (M Ω) = Ω.

5-17 One can verify that the resulting equational logic is consistent and that it cannot prove Ω = V for any value V. The type system is extended with the axiom

Γ ▷ Ω: σ  (Ω)

which says that Ω has every type. The modified computational transform is defined on Ω to be

Ω^{⋄} =^{def} Ω.

Since Ω has every type, to prove the Retraction Theorem for λ_{c}+Ω we need to extend the Soundness Lemma for the case of typing axiom (Ω). In other words we need to show (S.1): that Ω^{⋄} ε ⟦σ⟧, and (S.2): that (R_{σ} Ω^{⋄}) = Ω for every type σ. The second condition follows trivially from the definition of Ω^{⋄} and the axioms for Ω. To prove the first condition observe that

Ω = (let x=Ω in (E (e_{σ} x))),

and by Lemma 3.9, (E (e_{σ} x)) ∈ ⟦σ⟧ for every σ.

The very same reasoning can be applied to extend the Retraction Theorem for the CPS transform to λ_{c}+Ω, where the CPS transform is defined on Ω to be \overline{Ω} =^{def} λk.Ω k.

Recursive types: It is well known that all terms can be typed using the recursive type system. In order to extend the Retraction Theorem to all closed terms we study the recursive types.

The recursive type discipline introduces types of the form μt.σ (where we use t to denote a type variable). In order to extend our results to λ_{c} extended with recursive types we need to define retraction-embedding pairs (r_{σ}, e_{σ}) at new types. In particular how does one define e_{μt.σ} and r_{μt.σ}, or even e_{t} and r_{t}?

To motivate a solution, consider the following example. Let τ = μt.t→t. Then in the recursive type discipline one can type ▷(λx.x x): τ→τ. Assume we have defined terms e_{τ} and r_{τ}, and we try to compute

(r_{τ→τ} (R (λx.x x)^{⋄})) = (r_{τ→τ} (R (E λx.x x)))
= (r_{τ→τ} λx.x x)
= λx.(r_{τ} (R ((e_{τ} x) (e_{τ} x))))
= ?

5-18 To complete this derivation, one would like to have (e_{τ} x) = E ∘ e_{τ} ∘ x ∘ r_{τ}, so we can continue

\begin{aligned}⋯ & = & λx.(r_{τ} (R (E (e_{τ} (x (r_{τ} (e_{τ} x))))))) \\ & = & λx.x x \end{aligned}

What we see from this example is that the two occurrences of x in λx.x x “act” as having types τ→τ and τ, respectively. Similarly, we would like the two occurrences of e_{τ} in λx.(r_{τ} (R ((e_{τ} x) (e_{τ} x)))) to “act” as e_{τ→τ} and e_{τ}. A solution to our problem is to find a uniform definition for e’s and r’s at all types. Namely, we want a retraction-embedding pair (r, e) that satisfies the following definition.

Definition 3.16. A term F is called a total function if F is a value and, for any value V, (F V) is provably equal to a value.

A pair of total functions (r, e) is a uniform retraction-embedding pair if e and r satisfy system of equations

\begin{aligned}(r x) & = & r ∘ R ∘ x ∘ e \\ (e x) & = & E ∘ e ∘ x ∘ r \\ r ∘ e & = & λx.x. \end{aligned}  (⋆)

While it remains open whether there is a pair of terms satisfying the above conditions, we will assume we are given such a pair of functions and, under this assumption, show how the Retraction Theorem can be extended to recursive types. Moreover, since the recursive type system can type all terms, as a corollary we obtain the following theorem.

Theorem 3.17. Assume total functions e and r exist that satisfy equations (⋆). Then, for any closed lambda term M,

λ_{c} ⊢ (r (R M^{⋄})) = M.

Of course, the analogous theorems hold for the other transforms as well.

Here we only sketch the main idea in the proof of the above theorem. A detailed proof can be found in [Kuč97].

The recursive type system extends the simple types by adding type variables and type expressions of the form μt.σ. The new inference rules are

\frac{Γ ▷ M: σ\{μt.σ/t\}}{Γ ▷ M: μt.σ}  (μ I)

5-19

\frac{Γ ▷ M: μt.σ}{Γ ▷ M: σ\{μt.σ/t\}}  (μ E)

One can understand these rules by considering the type μt.σ as the type τ, satisfying equation τ = σ{τ/t}. Thus we need to define the interpretation, ⟦τ⟧ν, of τ such that it satisfies the equation

⟦τ⟧ν = ⟦σ{τ/t}⟧ν.

In other words ⟦τ⟧ν should be a fixed point of the function

λS.⟦σ⟧ν{S/t}.

(We assume the interpretation will satisfy ⟦σ{τ/t}⟧ν = ⟦σ⟧ν{⟦τ⟧ν/t}.) The difficulty lies in showing that for any σ and ν, the function λS.⟦σ⟧ν{S/t} always has a fixed point. To do so, we define a metric on the space of all type sets so that the resulting metric space is complete. Then we show that each function λS.⟦σ⟧ν{S/t} is a contraction, and thus, by Banach’s Fixedpoint Theorem, has a unique fixed point. Mac Queen et al. [MPS86] have developed such a framework, of which our development can be viewed as a special case. Namely, our domain consists only of finite elements (typing sequents) ordered under discrete order, thus greatly simplifying general purpose structures used in [MPS86].

4 Concluding Remarks

In this work, we have established a relation between direct style and CPS terms using definable retraction functions. The Retraction Theorem shows that a term can be recovered, up to λ_{c}-equivalence, from its image under the CPS transform. Therefore, the retraction approach, in fact, only provides a relation between equivalence classes of terms. To contrast our results with others that provide, perhaps even stronger relation between lambda terms and their CPS forms (e.g. [SW96]), we should emphasize that the inverse of the CPS transform we obtain is definable. Another important point is that the conclusion of our version of the Retraction Theorem is an equation provable in the logic of λ_{c}, which is a call-by-value logic, unlike the results in [MW85] and [Fil94] which give similar equalities, but in a call-by-name logic. As a consequence, our results are applicable even where call-by-name reasoning is not sound.

5-20 Some open questions: In all practical applications, functional programming languages are equipped with some form of recursion. Therefore, to make the retraction approach applicable in practice, we need to extend our results to a language with recursion. This can be done in two ways: By extending the type system so that the fixed-point operator is definable in the pure language, or by adding a language construct such as constant Y, letrec, etc. The first approach, with some partial results, has been discussed earlier.

One difficulty in adding fixed-point operator Y, or a similar language construct, is that additional closure conditions are needed in the definition of type sets, and we haven’t been able to construct type sets satisfying these conditions. The other difficulty is determining the correct axiomatization of a fixed-point operator. It appears that the axiom

(Y V) = (V (Y V))  (fix)

does not suffice. In models of λ_{c}, fixed-point operator can be defined using the so called fixpoint object. Crole and Pitts [CP92] define such an object in models of λ_{c}, and discuss a logical system for reasoning about fixpoint computations, which may hold the answer to above questions.

Another class of extensions is motivated by the application of the Retraction Theorem developed by Riecke and Viswanathan [RV95], where they show how one can isolate effects of an extension of a language with assignment or control from interfering with pure functional code. A natural question arises, whether it is possible to extend this approach to isolate one computational effect from interfering with code possibly containing a different computational effect. For instance, if M is a program in, say callby-value PCF with assignment, can we define an operator, call it encap, so that, in an extension of call-by-value PCF with both assignment and control, (encap M) will behave the same as M behaves in the extension of call-by-value PCF with assignment. We believe that an appropriate extension of the Retraction Theorem to a programming language with imperative features may give us such results.

References

[App92] Anrew W. Appel. Compiling with Continuations. Cambridge Universisty Press, 1992.

5-21 [Bar84] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Se-

mantics, volume 103 of Studies in Logic. North-Holland Publishing Co., Amsterdam, second edition, 1984.

[CP92] Roy L. Crole and Andrew M. Pitts. New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic. Information and Computation, 98(2):171–210, jun 1992.

[Fil94] Andrzej Filinski. Representing monads. In Symposium on Principles of Programming Languages, pages 446–457, Portland, Oregon, January 1994.

[Kuč97] Jakov Kučan. Metatheorems about Convertibility in Typed Lambda Calculi: Applications to CPS Transform and ”Free Theorems”. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, U.S.A., February 1997.

[Mit88] John C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76:211–249, 1988.

[Mog88] Eugenio Moggi. Computational lambda-caluclus and monads. Technical Report ECS-LFCS-88-86, University of Edinburgh, October 1988.

[Mog89] Eugenio Moggi. Computational lambda-caluclus and monads. In LICS, 1989.

[Mog91] Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991.

[MPS86] David MacQueen, Gordon Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. Information and Control, 71(1/2):95–130, October/November 1986.

[MR] Albert R. Meyer and Jon G. Riecke. Continuations may be unreasonable. In Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pages 63–71.

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

5-22 [Plo75] G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus.

Theoretical Computer Science, 1(2):125–159, December 1975.

[Rey93] John C. Reynolds. The discoveries of continutions. Lisp and Symbolic Computation, 6(3/4), November 1993.

[RV95] Jon G. Riecke and Ramesh Viswanathan. Isolating side effects in sequential languages. In In Proceedings of Symposium on Principles of Programming Languages, 1995.

[SF92] Amr Sabry and Mathias Felleisen. Reasoning about programs in continuation-passing style. Technical Report COMP TR 92-180, Rice University, 1992.

[Ste78] Guy L. Steele. Rabbit: A compiler for Scheme. Technical Report AI-TR-474, MIT Artificial Intelligence Laboratory, 1978.

[Sto77] Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA, 1977.

[SW74] C. Strachey and C. P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Technical Report PRG–11, Oxford University Computing Laboratory, 1974.

[SW96] Amr Sabry and Philip Wadler. A reflection on call-by-value. In International Conference on Functional Programing, Philadelphia, May 1996. ACM Press.

[Wad90] Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2(4):461–493, December 1990.

5-23