Retraction Approach to CPS Transform.
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 CPS form via a -definable retraction. The Retraction Theorem is proved in the logic of computational lambda calculus for the simply typable terms.
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
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).
the research has been to establish a relationship between original terms and
their images under the transform.
In this work we view the CPS transform as a formalization of the (contin-
uation passing style) denotational semantics of a call-by-value programming
language in the fij 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 ,
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
-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
We ask the question whether functions T , or its inverse T
are definable. More precisely,
ffl is there a lambda term P , such that - n ' (P
ffl is there a lambda term R, such that - c ' (R
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 oe there is a lambda term R oe , such that for all closed lambda terms M
of type oe,
(R oe
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
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 \Pi , mapping lambda terms to lambda
terms extended with two constants E and R that satisfy axiom
(R
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).
Theorem 1.3 (Retraction, for T \Pi ). For any simple type oe there is a term
R oe , such that for all closed lambda terms M of type oe,
(R oe M \Pi
where M \Pi 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 oe, then the meaning of M and the
meaning of oe 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 trans-
form, 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.
Theorem 1.4. Assume terms e and r exist such that e and r are total
functions satisfying (in - c +(r-e))
(R (y (e x))))
Then for every term M ,
(R M \Pi
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.
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
(let x=M in N) to abbreviate the term ((-x:N) M ), and M ffi 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 if the equation can be derived using
the rules of lambda congruence from the axioms in -.
(let x=M in

Table

1: Axioms of - c .
For most part of this paper we consider equalities provable in Moggi's

Table

1), possibly extended with additional axioms for constants. In
particular we will use constants E and R satisfying axiom
(R
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 oe!- is a
type whenever oe and - are types. The type inference system consists of set
of rules (given in Table 2) for deriving sequents of the form \Gamma . M : oe, where
oe is called a typing assertion and \Gamma is a typing hypothesis, i.e. a set of
typing assertions of the form x where we always assume no variable x i
occurs more than once in \Gamma.
\Gamma; x: oe . x: oe (var)
. (M N
(app)
\Gamma; x: oe .
(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 \Pi ,
mapping pure lambda terms to lambda terms extended with two constants
E and R (see Table 3). The transform T \Pi 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 \Pi 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 \Pi .

Table

3: The modified computational transform, T \Pi .
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
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 hx 1
i=M in N)

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

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 oe (intuitively programs)
to terms of type T (oe 0 ) (intuitively computations), where T is a unary type
constructor (that depends on the particular transform), and oe 0 is defined
inductively using T to be -
0). This can be
made precise by defining the typed version of the transform mapping typing
sequents to typing sequents.
3 Retraction Theorem
In this section we state and prove the Retraction Theorem for the abstract
transform, T \Pi , as well as, for the CPS and the SPS transforms. While one
might not find the transform T \Pi 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 \Pi , 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,
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 oe) to terms representing computations (of type T (oe 0 )), in-
tuitively, we can understand the pairs of terms defined below as retraction-
embedding pairs between types oe and T (oe 0 ). One can also formally define
a notion of a type oe being a retract of a type - , and in the sense of such
definition, given below, we exhibit terms R oe and E oe that form a retraction-
embedding pair between types oe and T (oe 0 ). Moreover, we will show that
(suitable versions of) terms R oe define the required inverses of the transforms
we study.
Definition 3.1. A type oe is said to be a retract of a type - if there is a pair
of lambda terms R oe;- and E oe;- of types -!oe and oe!- respectively, such
that (R oe;- (E oe;-
Definition 3.2. For each simple type, oe, define terms e oe and r oe inductively
on the structure of oe as follows:
and at higher types we have
r
(R (f (e
Lemma 3.3. - c +(r-e) ' (r oe (e oe
Proof: Easy by induction on oe.
Note: Above lemma holds whenever we replace constants E and R with any
values E 0 and R 0 such that - c ' (R 0
Finally we define terms R (R x)) and E
Later we will show that R oe is an inverse of the transform T \Pi . To define an
inverse of the CPS transform we first define terms R K def
-xk:(k x). It is easy to show (in - c ) that (R K (E K
the retraction-embedding pair (R K
oe 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
represents some initial state of the store, and define terms R S
oe and E S
oe 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 fij-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,
ae, mapping variables to V(D) we define an interpretation (relative to ae) that
to each term M assigns an element JMKae of D. In addition we assume that
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 . The interpretation of
types will be defined (using the "-relation defined below) inductively:
set of all terms of the form
set of all M (of the form (E V )) such that 8N 2 JoeK:
(R - (R oe N))
Relating the interpretations: To relate meanings of terms and types,
instead of using the simple set-membership relation, we define an extended
2. 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 : oe is true (with respect to ae), written ae
JoeK. The notions of satisfaction and validity are defined in the
standard way relative to the definition of truth. Namely, ae satisfies a typing
hypothesis \Gamma, written ae every typing assertion in \Gamma is true with
respect to ae, and a typing sequent \Gamma . M : oe is valid,
is true for every ae that satisfies \Gamma.
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 " Joe!-K and N " JoeK:
(R (R oe N)); (z)
where R oe , 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 (y) and (z) 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,
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 ae be a substitution mapping variables to values. Define
the interpretation function J \DeltaK to be
JMKae
Definition 3.5. Type sets are sets of terms of the form
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:
It is easy to see that J(M
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
and
Definition 3.8. The interpretation of types is defined inductively on the
structure of type expressions. Namely,
set of all terms of the form
set of all M , of the form (E V ), such that 8N 2 JoeK,
(R - (R oe N))
Recall that 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 oe and any value V ,
Proof: Easy by induction on oe.
Lemma 3.10. For any two terms M and N such that M " Joe!-K and
and
(R (R oe 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 2 JoeK, and in the lemma we show that these two
statements hold for all N " JoeK. 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 \Gamma be a typing hypothesis and let ae be a
substitution that satisfies \Gamma. Let ae 0 be a substitution such that for each
and
(R oe ae(M \Pi
Proof: We prove the lemma by induction on the derivation of \Gamma . M : oe.
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 j -x:N and oe j
, and that \Gamma . -x:N
was derived from \Gamma; x: - 1
using the
(abs) rule.
To show (S.1), first observe that ae((-x:N) \Pi so we need
to show that ae((-x:N) \Pi any term in J- 1 K. Then
and therefore since aefV=xg satisfies \Gamma; x: - 1 , by induction hypothesis (S.1),
K. Moreover we can compute
(R -2 App(ae((-x:N) \Pi (R
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
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 \Pi ). For any closed term M of (simple)
type oe,
(R oe M \Pi
3.4 The CPS Transform
To prove the the Retraction Theorem for the CPS transform, as indicated be-
fore, 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
(R to be
It is easy to see that - c ' (R K (E K which is the only abstract
property of E and R we use.
We define the interpretation of terms (relative to a substitution ae) using
the CPS transform, that is,
JMKae
The application in the codomain of the transform is defined to be
so that (M Finally, we define the extended membership
relation, " K , to be
for some terms P i , a value V such that 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 (y) and (z) hold.
Lemma 3.13. For any two terms M and N such that M " K
Joe!-K and
App K (M;
and
(R K
oe!- M) (R K
oe
Proof: The proof is straightforward using the definitions and axioms of - c .
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 oe,
(R K
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 (y) and (z)
still hold. Recall that the terms E S and R S are defined to be
where init is some initial state of the store.
The interpretation of terms is defined using the SPS transform. Namely,
JMKae
The application in the codomain of the transform is define to be
so that (M N)  Finally we define the extended membership
for some terms P i , some value V such that
Furthermore, we interpret the definitions of type sets, interpretation of
types, and retraction-embedding pairs defined earlier, as if given using
in place of E , R, App and ". With the new definitions
we can show that conditions (y) and (z) 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 oe,
(R S
oe M
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 straight-
forward. 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 oe!- is added to - c , we need to make sure that if M " oe
then App(c \Pi ; 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 diver-
gence. In presence of divergence - n reasoning is no longer sound for call-
by-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, \Omega\Gamma that is added
to the language of - c as a constant, but it is not considered a value. The
axioms
for\Omega specify that an application diverges if either the operators or
the operand diverges. Moreover, these axioms identify all divergent terms.
The axioms
are:(\Omega
M)
=\Omega and (M \Omega\Gamma
One can verify that the resulting equational logic is consistent and that it
cannot
value V . The type system is extended with the
axiom
. \Omega\Gamma oe
which says
that\Omega has every type. The modified computational transform
is defined
on\Omega to be
has every type, to prove the Retraction Theorem for -
c+\Omega we need
to extend the Soundness Lemma for the case of typing
In other
words we need to show (S.1):
and (S.2): that (R
=\Omega
for every type oe. The second condition follows trivially from the definition
of\Omega \Pi and the axioms
To prove the first condition observe that
x=\Omega in (E (e oe x)));
and by Lemma 3.9, (E (e oe x)) 2 JoeK for every oe.
The very same reasoning can be applied to extend the Retraction Theorem
for the CPS transform to -
c+\Omega\Gamma where the CPS transform is defined
on\Omega to
-k:\Omega 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:oe (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
oe ) at new types. In particular how does one define e -t:oe and r -t:oe , 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 (-x:x x) \Pi (R
(R ((e - x) (e - x))))
To complete this derivation, one would like to have (e -
so we can continue
(R
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 , 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
r
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 ,
(R M \Pi
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-c97].
The recursive type system extends the simple types by adding type variables
and type expressions of the form -t:oe. The new inference rules are
(- I)
E)
One can understand these rules by considering the type -t:oe as the type - ,
satisfying equation oef-=tg. Thus we need to define the interpretation,
J-K-, of - such that it satisfies the equation
In other words J-K- should be a fixed point of the function
-S:JoeK-fS=tg:
(We assume the interpretation will satisfy JoeK-fJ-K-=tg.) The
difficulty lies in showing that for any oe and -, the function -S:JoeK-fS=tg
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:JoeK-fS=tg is a contraction, and thus, by Banach's Fixed-point
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 (typ-
ing sequents) ordered under discrete order, thus greatly simplifying general
purpose structures used in [MPS86].
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.
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
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
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 call-
by-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.



--R

Compiling with Continuations.
The Lambda Calculus: Its Syntax and Se- mantics
New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
Representing monads.
"Free Theorems"
type inference and containment.
Computational lambda-caluclus and monads
Computational lambda-caluclus and monads
Notions of computation and monads.
An ideal model for recursive polymorphic types.
Continuations may be unrea- sonable
Continuation semantics in typed lambda-calculi (summary)

The discoveries of continutions.
Isolating side effects in sequential languages.
Reasoning about programs in continuation-passing style
A compiler for Scheme.
Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory
A mathematical semantics for handling full jumps.
A reflection on call-by-value
Comprehending monads.
--TR

--CTR
Andrzej Filinski, On the relations between monadic semantics, Theoretical Computer Science, v.375 n.1-3, p.41-75, May, 2007
continuation passing style;continuations;CPS transform;monads;retractions