Space-Profiling Semantics of the Call-by-Value
Lambda Calculus and the CPS Transformation
Yasuhiko Minamide
Institute of Information Sciences and Electronics
University of Tsukuba
Tsukuba 305-8573, Japan

Abstract
We show that the CPS transformation from the call-by-value lambda calculus to a
CPS language preserves space required for execution of a program within a constantfactor. For the call-by-value lambda calculus we adopt a space-proﬁling semantics
based on the proﬁling semantics of NESL by Blelloch and Greiner. However, wehave noticed their semantics has some inconsistency between the treatments of stackspace and heap space. This requires us to revise the semantics so that the semantics
treats space in more consistent manner in order to obtain our result.

1

Introduction

In the studies of program transformations it is indispensable to prove their correctness. However, so far it is not so common to discuss eﬀects on performance
formally; it is usually discussed only by benchmarks. This sometimes resultsin undesirable situation. Several researchers have noticed that some programtransformations are not safe with respect to space [1,3,10]. This clariﬁes thatspace safety of program transformations should be discussed formally.
To discuss space safety formally, we ﬁrst need a space-proﬁling semantics which formalizes how much memory a program requires for its execution.
However, it is not so easy to formulate such a semantics. Blelloch and Greiner
proposed a space-proﬁling semantics for the parallel programming language
NESL and discussed the space eﬃciency of an implementation of NESL [2]. As
far as we know, this is the only work that formalized a space-proﬁling semantics
of a programming language and discussed this topic formally. Their proﬁling
semantics is an extension of the standard natural semantics of the call-byvalue lambda calculus and seems suitable to study space safety of programtransformations on call-by-value functional languages. However, the problem
of formalizing space-proﬁling semantics is not completely solved. Their semantics is quite involved and it is not so clear that it models space required
for execution of a program properly.
This is a preliminary version. The final version will be published inElectronic Notes in Theoretical Computer Science
URL: www.elsevier.nl/locate/entcs

Minamide

In this paper we show that the CPS transformation from the call-by-value
lambda calculus to a CPS language preserves space within a constant factor by adopting a space-proﬁling semantics of Blelloch and Greiner for thelambda calculus. This result itself is signiﬁcant since it conﬁrms what we expected on space for the CPS transformation. Furthermore, this implies thatthe call-by-value lambda calculus has an implementation based on the CPS
transformation where space is preserved and thus the space-proﬁling semanticsof the lambda calculus models space required for execution of programs properly. However, during this study we have noticed that the semantics given by
Blelloch and Greiner has some inconsistency between the treatments of stackspace and heap space. This requires us to revise the semantics so that thesemantics treats space in more consistent manner in order to obtain our result.
The CPS language we consider is basically a simpliﬁed version of the language used in the study of SML/NJ [1]. The language does not require stack
to model execution of programs. This simpliﬁes its space-proﬁling semantics.
Furthermore, since the language is close to low level implementation we are
relatively sure that the space-proﬁling semantics we deﬁne for the language
models actual implementation. This is our motivation that we used the CPS
language as the target language into which the call-by-value lambda calculus
is translated.
This paper is organized as follows. We start by introducing the concept of
proﬁling semantics and discussing what properties a program transformation
should satisfy. As the property we discuss mainly in this paper we deﬁne spaceeﬃcient program transformations. In Section 3 we introduce the proﬁling semantics of the call-by-value lambda calculus given by Blelloch and Greiner anddiscuss inconsistency between the treatments of stack space and heap space.
In Section 4 the CPS language and its space-proﬁling semantics is introduced.
In Section 5 we show that the CPS transformation is space eﬃcient. We also
consider some variations of proﬁling semantics of the call-by-value lambda
calculus and the CPS language in Section 6. Finally we review related works
and give directions for future work.

2

Proﬁling semantics, space eﬃciency, and space safety

In this section we review what is proﬁling semantics and what properties
program transformations should satisfy on space. For simple functional languages the semantics can be deﬁned as a function eval(M) returning the resultof evaluation if it terminates:eval(M) = v
if the evaluation terminates and the result is the value v. Otherwise, eval(M)is undeﬁned. This semantics formalizes what should be the result of thecomputation of M, but does not give any information on how much time orspace the evaluation requires.
2Minamide

Proﬁling semantics is introduced to discuss such properties formally. As
an extension of the standard semantics, proﬁling semantics can be given as afunction eval(M) below.
eval(M) = (v, n)This function gives the result of computation v and information n on resource
requirement. In this paper we focus on space as the resource. More specially,
we discuss not the space allocated totally, but the space required for execution
in the presence of garbage collection. As the values of n we use non-negative
integers that represent the size of space required for execution.
The next step is to formalize what property a program transformation
should satisfy on space. Let us consider that a program M is translated toa program M  by a program transformation and the proﬁling semantics forthe language after the transformation is given by eval (M  ). We say that a
program transformation is space eﬃcient if the following property holds.
There exist constants k1 and k2 such that for any program Meval(M) = (v, n) implies eval (M  ) = (v  , n ) for some n ≤ k1 n + k2 .
In this deﬁnition we admit constants k1 and k2 because they seem dependent
on the details of deﬁnition and not essential. It is clear that this condition
ensures that the program transformation does not raise the space complexityof a program. This is the property shown by Blelloch and Greiner for an
implementation of NESL [2] and we show this property for the CPS transformation.
However, this property might be too strong for some program transformations used in compilers. Appel discussed that a transformation is space safe
if it does not raise the space complexity of programs [1]. To formalize thisidea we have to consider programs with an input; we consider programs with
one free variable and use the free variable for input. One way of formalizing
space-safety is as follows:
For any program M with a free variable x, there exist constants k1 and k2
such that for any integer i the following holds:
eval(M[i/x]) = (v, n) implies eval (M  [i/x]) = (v  , n )for some n ≤ k1 n + k2
The key diﬀerence from space-eﬃciency is that the constants k1 and k2 areprogram-dependent. Minamide and Garrigue showed that this property withrespet to time complexity for a type-directed unboxing transformation, which
is not eﬃcient in terms of the deﬁnition above [10]. We should remark that
if we ignore inputs, the statement of space-safety gets trivial. The following
claim is trivial on requirement of space.
For any program M, there exist program-dependent constants k1 and k2 such3

Minamidethat the following holds:
eval(M) = (v, n) implies eval (M  ) = (v  , n ) for some n ≤ k1 n + k2
It might be suﬃcient that a program transformation used in compilers is
space safe. However, we think that it is interesting to show that a programtransformation is space eﬃcient, since it gives us a uniform constant independent of programs.

3

Lambda calculus and space-proﬁling semantics

In this section we introduce a space-proﬁling semantics of the call-by-value
λ-calculus based on the space-proﬁling semantics of NESL by Blelloch andGreiner [2]. Their semantics does not explicitly take account of garbage collection, but the maximum size of reachable space during evaluation. We havenoticed that this semantics has some inconsistency between the treatments ofheap space and stack space: it takes account of the size of each closure, but
ignores the size of each stack frame. This motivates us to revise the semantics
so that the semantics treats space in more consistent manner. As we will
see later, this revision is necessary to prove that the CPS transformation isspace eﬃcient. In this section we ﬁrst describe the semantics by Blelloch andGreiner. Then we explain the problem and revise the semantics to make it
more consistent.
We consider the following untyped call-by-value λ-calculus with a constantc.
M ::= x | c | λx.M | M1 M2
The proﬁling operational semantics is given as an extension of the standard
natural semantics. A value v is either a constant c or a location l. We use store
σ mapping locations to store values sv to express sharing of values. A store
value sv models a value allocated on heap memory and for this calculus it is
only a closure. A closure cl ρ, x, M consists of an environment ρ mapping
variables to values, a variable, and an expression.
v ::= c | l
sv ::= cl ρ, x, M
We denote the set of the free variables of M by F V (M) and for closures wewrite F V (cl ρ, x, M) for F V (M) \ {x}.
The operational semantics is deﬁned as a natural semantics with judgmentsof the following form
ρ, σ, R  M −→ v, σ; swhere ρ is environment, σ is store, R is a root set, and s is the maximum sizeof reachable space. A root set is a set of locations which is necessary after thiscomputation.
4

Minamide

Before giving the rules of the natural semantics we have to deﬁne reachable
locations and the space of a set of locations. The set of locations locs(l, σ)reachable from a location l in σ is deﬁned as follows 1 .
locs(l, σ) = {l} ∪ locs(σ(l), σ)locs(cl ρ, x, M, σ) = l∈L locs(l, σ) where L = ρ(F V (cl ρ, x, M))Loc
where SLoc is the set of locations included in a set of values S.
The size of space space(R, σ) reachable from a set of locations R is deﬁned
as follows:space(R, σ) = Σl∈locs (R,σ) size(σ(l))
size(cl ρ, x, M) = |F V (cl ρ, x, M)| + 1
The size of a closure is proportional to the size of the environment required for
M. This models the implementation of environments based on a ﬂat record.
The following are the rules of the operational semantics, which are basicallyobtained by simplifying those given by Blelloch and Greiner.
(con)ρ, σ, R  c −→ c, σ; space(R, σ)(var)
ρ, σ, R  x −→ ρ(x), σ; space(R ∪ {ρ(x)}Loc , σ)(abs)ρ, σ, R  λx.M −→ l, σ  ; space(R ∪ {l}, σ  )where l is a fresh location and σ  = σ[cl ρ, x, M/l](app)
ρ, σ, R ∪ ρ(F V (M2 ))  M1 −→ l, σ1 ; s1
ρ, σ1 , R ∪ {l}  M2 −→ v2 , σ2 ; s2
ρ [v2 /x], σ2 , R  M3 −→ v, σ3 ; s3
σ2 (l) = cl ρ , x, M3 ρ, σ, R  M1 M2 −→ v, σ3 ; max(s1 + 1, s2 + 1, s3 )The size of reachable space is only calculated in the leaves of a derivation. In
the rules (con), (var), and (abs) we have to take the root set R into accountto determine the reachable space. Thus in (con) the size of reachable space isdetermined by space(R, σ). In the rule of application we calculate the maximum size of reachable space by taking maximum of those of the subderivation.
We calculate the maximum of s1 + 1, s2 + 1, and s3 instead of s1 , s2 , and s3
where adding 1 to s1 and s2 is explained as the space for stack. However, theevaluation of M3 corresponds to a tail call. Thus we do not add 1 to s3 .
To deﬁne an evaluation function based on this natural semantics, we ﬁrst
deﬁne the observable values and the function oval(v) coercing values into1

We assume that there is no cycle in a store. That is ensured for this operational semantics.

5

Minamide

observable values as follows:oval(v) =ov ::= c | cls⎧⎨ c if v is a constant c⎩ cls if v is a location

The space-proﬁling semantics based on the natural semantics is deﬁned asfollows:
evalλBG (M) = (ov, s) if and only if ∅, ∅, ∅  M −→ v, σ; s and ov = oval(v).
This seems reasonable deﬁnition, but if we think the evaluation more carefully,
we will ﬁnd some inconsistency in the rules of the natural semantics. The
semantics takes account of the size of each closure, but it ignores the size ofeach stack frame. Let us consider the evaluation of application M1 M2 . During
the evaluation of M1 , we have to preserve the values of F V (M2 ) in the stack
frame, the size of which is not constant. However, this size is ignored in therule of application.
We revise the rule of application so that the size of stack frames is treatedin more consistent manner. The rule is revised as follows:
ρ, σ, R ∪ ρ(F V (M2 ))  M1 −→ l, σ1 ; s1
ρ, σ1 , R ∪ {l}  M2 −→ v2 , σ2 ; s2
ρ [v2 /x], σ2 , R  M3 −→ v, σ3 ; s3
σ2 (l) = cl ρ , x, M3 ρ, σ, R  M1 M2 −→ v, σ3 ; max(s1 + |F V (M2 )| + 1, s2 + 1, s3)
We adopt this rule hereafter and refer the proﬁling semantics based on this ruleevalλ (M). As we will see later, without this revision the CPS transformation
is not space eﬃcient.
These semantics evalλBG (M) and evalλ (M) are not equivalent in terms ofspace eﬃciency of program transformations: there is no constants k1 and k2
such thatevalλBG (M) = (ov, n) implies evalλ (M) = (ov, n ) for some n ≤ k1 n + k2 .
This is veriﬁed by constructing expressions Zn indexed by a natural number
n where the space required for the execution of Zn is proportional to n forevalλBG (M) and n2 for evalλ (M). The construction is given as follows:
Xn = (λx1 . . . xn .c)z1 . . . zn
Yn = (λy1 . . . yn .c)Xn . . . Xn
Zn = (λz1 . . . zn .Yn )c . . . c
where λx1 . . . xn .M is abbreviation of (λx1 .(λx2 .(. . . (λxn .M)))). The intuitionis that the evaluation of Zn requires n stack frames of size n and thus n2 spaceis necessary for evalλ (M), but only n space is necessary for evalλBG (M) since
the size of each stack frame is ignored.
6

Minamide

4

CPS language and space-proﬁling semantics

As we saw in the previous section, it is delicate to formalize the space-proﬁling
semantics even for the simple call-by-value λ-calculus. Thus in this section
we consider a space-proﬁling semantics of a simpler CPS language where a
program is expressed in continuation passing style. The language is basically a simpliﬁed version of the language used in the SML/NJ compiler [1].
The proﬁling semantics is deﬁned based on the abstract machine proposedby Flanagan et al. [6] and does not require stack to model execution. That
simpliﬁes its space-proﬁling semantics.
The syntax of the CPS language is deﬁned as follows:
V ::= x | c
M ::= xV1 , . . . , Vn  | let x = λx1 . . . xn .M1 in M2
A value expression V is either a variable x or a constant c. An expression
M is either an application xV1 , . . . , Vn  with n-arguments V1 , . . . , Vn or a letexpression introducing a lambda abstraction. For readability we use k, k1 , . . .
as variables of the CPS language for continuation.
We deﬁne the operational semantics based on the abstract machine proposed by Flanagan et al. [6] by extending it with locations and stores. The
deﬁnition of store values, values, stores, and environments is similar to thosefor the semantics of the lambda calculus.
sv ::= cl ρ, x1 . . . xn , Mv ::= l | c | stop
The value stop is used to represent the initial continuation. We sometimes use
an environment ρ as a function from value expressions to values by extending
ρ with ρ(c) = c.
The operational semantics is deﬁned as transition of a state Q consistingof a store, an environment, and an expression: σ, ρ, M. The rules of thetransition σ, ρ, M −→ σ  , ρ , M   are deﬁned as follows:(app)
σ, ρ, xV1 , . . . , Vn  −→ σ, ρ [ρ(V1 ), . . . , ρ(Vn )/z1 , . . . , zn ], Mwhere σ(ρ(x)) = cl ρ , z1 . . . zn , M.
(abs)
σ, ρ, let x = λx1 . . . xj .M1 in M2  −→σ[cl ρ, x1 . . . xj , M1 /l], ρ[l/x], M2 
where l is a fresh location.
As for the proﬁling operational semantics of the lambda calculus, we deﬁne
the reachable locations and its space. The set of locations locs(l, σ) reachable
7

Minamide

from l in σ is deﬁned as follows.
locs(l, σ) = {l} ∪ locs(σ(l), σ)locs(cl ρ, x1 . . . xn , M, σ) = l∈L locs(l, σ)
where L = ρ(F V (M) \ {x1 , . . . , xn })Loc .
The size of space reachable from a set of locations R is deﬁned as follows:space(R, σ) = Σl∈locs (R,σ) size(σ(l))
size(cl ρ, x1 . . . xn , M) = |F V (M) \ {x1 , . . . , xn }| + 1
The set of locations and the size of space reachable from a state σ, ρ, M
deﬁned as follows:
where L = ρ(F V (M))Loc
locs(σ, ρ, M) = l∈L locs(l, σ)space(σ, ρ, M) = space(locs(σ, ρ, M), σ)We write Q1 −→∗s Qn if Q1 −→∗ Qn and s = max1≤i≤n (space(Qi )). Let M
be a program with a variable k for the initial continuation. Then we deﬁne
the proﬁling semantics of M as follows:
evalcps (M) = (ov, s)
if and only if∅, [stop/k], M −→∗s σ, ρ, k  V 
and oval(ρ(V )) = ov and ρ(k  ) = stop.

5

CPS transformation is space eﬃcient

In this section we will consider a CPS transformation from the lambda calculus
to the CPS language and show that the transformation is space eﬃcient. The
proof simultaneously shows that the transformation preserves the observablebehavior of programs and is space eﬃcient.
We deﬁne the CPS transformation as a deductive system with judgmentsof the form of k  M
M  which means M is transformed to M  by usingk as a variable for continuation. The rules of the transformation are given as
follows:k  λx.M
k  M1 M2

kx

kx

kc

kc

M
kM
let f = λxk.M  in kf 

k1  M1
M1
k2  M2
M2
let k1 = λf.let k2 = λa.f ak in M2 in M1

We use the CPS language as the target language of the transformation instead of the lambda calculus and for readability we introduce fresh variables
8Minamide

for continuation in the transformation of applications. This is basically thestandard CPS transformation by Fischer and Plotkin [5,13].
The following lemma determines the set of the free variables of a CPStransformed expression.
M  , then F V (M  ) = F V (M) ∪ {k}.

Lemma 5.1 If k  M

In the transformation of application, the continuation for M1 is the following expression.
λf.let k2 = λa.f ak in M2
The set of free variables of the expression is (F V (M2 )\{k2 })∪{k} = F V (M2 )∪{k}. Thus the size of the closure for this expression is not a constant, but|F V (M2 )| + 2. This is the reason why we need the revised space-proﬁling
semantics of the lambda calculus to show that the CPS transformation isspace eﬃcient.
The following theorem claims that the CPS transformation is space eﬃcientfor the constant K = 3.
Theorem 5.2 Let k  M(ov, s) and s ≤ Ks.

M  . If evalλ (M) = (ov, s), then evalcps (M  ) =The constant K is determined as follows. Let us consider the evaluationof M1 M2 which is translated into the following expression.
let k1 = λf.let k2 = λa.f ak in M2 in M1
When we evaluate M2 , the current continuation is cl ρ, a, f ak for someenvironment ρ. The size of this closure is 3 since the set of the free variables is{f, k}. This size should correspond to the size of the stack frame to evaluate
M2 which is 1 in the rule for application in the deﬁnition of evalλ (M). Thus
we adopt 3 for K.
In order to prove this theorem we have to generalize the claim of thetheorem. First, in order to show that the CPS transformation preserves theobservable behavior of programs, we deﬁne the relations ≈ between values,
store values, environments, and stores of the lambda calculus and the CPS
language as follows:c≈cl≈lcl ρ, x, M ≈ cl ρ , xk, M   if ρ ≈ ρ and k  MMρ ≈ ρ
if ρ(x) ≈ ρ (x) for all x ∈ Dom(ρ)σ ≈ σ

if σ(l) ≈ σ  (l) for all l ∈ Dom(σ)

Since a store σ  of the CPS language includes locations pointing closures forcontinuation, we ignore the locations not included in the domain of σ of the9Minamide

lambda calculus in this deﬁnition.
The following lemma guarantees that for the related stores the set of reachable locations and the size of reachable space coincide.
Lemma 5.3 Let σ ≈ σ  and R be a set of locations with R ⊆ Dom(σ). Thenlocs(R, σ) = locs(R, σ  ) and space(R, σ) = space(R, σ  ).
Secondly, we have to distinguish locations of the CPS language for continuation from those corresponding closures of the lambda calculus. Let σ andσ  be the stores of the lambda calculus and the CPS language respectively.
The locations corresponding to continuation klocs(vk , σ, σ  ) and the locations
corresponding to heap hlocs(vk , σ, σ  ) are deﬁned as follows:
klocs(vk , σ, σ  ) = locs(vk , σ  ) \ Dom(σ)
hlocs(vk , σ, σ  ) = locs(vk , σ  ) ∩ Dom(σ)
Then the size of space corresponding to continuation kspace(vk , σ, σ  ) is deﬁned
as follows:
kspace(vk , σ, σ  ) = space(klocs(vk , σ, σ  ), σ  )The main theorem is generalized to the following lemma. The proof of thelemma appears in the appendix. The theorem is obtained by considering theempty stores for σ and σ  , the empty environments for ρ and ρ , the empty
set for R, and the initial continuation stop for vk .
M  , σ ≈ σ  , ρ ≈ ρ , and hlocs(vk , σ, σ  ) =Lemma 5.4 Let k  M
locs(R, σ).
If ρ, σ, R  M −→ v, σ0 ; s, then σ  , ρ [vk /k], M   →∗s σ0 , ρ [vk /k], kV  andσ0 ≈ σ0 and v ≈ ρ (V ) and s ≤ Ks + kspace(vk , σ, σ  ).

6

Variations of proﬁling semantics

In this section we consider some variations of proﬁling semantics of the callby-value lambda calculus and the CPS language.
In the proﬁling semantics of the λ-calculus, we have not considered muchabout constant factor on the stack space. When we evaluate M2 of application
M1 M2 , it is actually considered that the space of size 2 is necessary at least for
the value l of M1 and the return address. Then the rule is revised as follows:
ρ, σ, R ∪ ρ(F V (M2 ))  M1 −→ l, σ1 ; s1
ρ, σ1 , R ∪ {l}  M2 −→ v2 , σ2 ; s2
ρ [v2 /x], σ2 , R  M3 −→ v, σ3 ; s3
σ2 (l) = cl ρ , x, M3 ρ, σ, R  M1 M2 −→ v, σ3 ; max(s1 + |F V (M2 )| + 1, s2 + 2, s3)
If we adopt this rule, the constant K that is used to show that the CPS transformation is space eﬃcient can be reduced to 2. In this sense it is consideredthat K = 3 is overestimated. However, the concrete value of this constant K
will depend on the details of implementations anyway.
10

Minamide

In this paper we have taken an approach to counting the size of closuresand stack frames to make the semantics of the lambda calculus consistent.
However, it is also possible to ignore the size of both closures and stack frames.
Even if we take this approach, we believe that the CPS transformation is spaceeﬃcient. However, this approach will make some transformation which is not
space eﬃcient if we take the size of closures and stack frames into account spaceeﬃcient. That is against our intuition and we consider that this approach isundesirable.
In the space-proﬁling semantics of the CPS language, we have taken account of only the size of reachable locations as the size of a state and ignored
the size of the environment ρ of the state. If we consider the size of the environment, the deﬁnition of the space of a state (ρ, σ, M) is revised as follows:space  (ρ, σ, M) = |F V (M)| + space(locs(ρ, σ, M))Here, we add |F V (M)| instead of |Dom(ρ)| to discard the space for the values
that are not necessary to evaluate M. This deﬁnition space  (Q) is also a
reasonable deﬁnition and it is not so clear which deﬁnition we should take.
The two semantics are not equivalent in the sense of space eﬃciency. However,
if we restrict programs to those obtained by the CPS transformation, twosemantics are equivalent. Let evalcps(M) be the proﬁling semantics deﬁned
M  , the following holds.
based on this deﬁnition. If k  M
If evalcps (M  ) = (v, n) and evalcps(M  ) = (v, n ), then n ≤ 2n + 3.

This means the two proﬁling semantics are equivalent in the sense of spaceeﬃciency for the programs obtained by the CPS transformation.

7

Related work

We have concentrated on issues of space in this paper, but it is also important to discuss execution time formally. A semantics proﬁling time is relatively
easy to formulate and several researchers have studied eﬀect of program transformations on execution time [14,7,2]. Even for time some advanced programtransformation was shown that it may raise time complexity of a program. Minamide and Garrigue showed that the type-directed unboxing transformation
proposed by Leroy [9] has this problem. They proposed a reﬁnement of thistransformation and proved that their reﬁnement preserves time complexity by
the method of logical relations [10].
Several researchers have noticed that some program transformations are
not safe with respect to space and proposed reﬁnements of the transformations
to avoid that problem [15,10]. Shao and Appel proposed a closure conversion
with a sophisticated environment representation that is space safe [15]. Minamide and Garrigue expected that their reﬁnement of unboxing transformation preserves space complexity with respect to heap space as well as timecomplexity [10]. However, no proof is given in both studies.
Blelloch and Greiner proposed two proﬁling semantics of NESL: one based
11

Minamideon natural semantics and the other based on an abstract machine [2]. They
showed that the implementation based on the latter semantics is time andspace eﬃcient with respect to the former semantics. However, as we discussed
in this paper the treatment of stack space and heap space on both semantics
seems inconsistent and diﬀerent from ours. In another recent eﬀort to address
space-safety formally, Gustavsson and Sands has developed a theory of a space
improvement relation for a call-by-need programming languages and showed
space safety of inlining of aﬃne-linear bindings [8].
Morrisett et al. proposed an operational semantics where various methodsof garbage collection can be discussed formally [11,12]. In this paper we haveignored details of garbage collection and focused on the size of reachable spaceas Blelloch and Greiner did. It is desirable to show the connection of the sizeof reachable space and the space required for execution of a program formally.

8

Future work

We have considered the standard CPS transformation which introduces administrative redexes [13]. However, it might be more natural to consider anadvanced CPS transformation as implementation of the call-by-value lambda
calculus, where administrative redexes are eliminated at time of the CPS
transformation. Thus we think that it is important to show such a CPS
transformation is also space eﬃcient. For such a CPS transformation, it is
not straightforward to preserve tail calls [4]. By showing that such a CPS
transformation is space eﬃcient, we can indirectly show that tail calls arepreserved.
The CPS language we considered is close to low level implementation.
However, actual compilers still use other program transformations such as
closure conversion to obtain executable code. To ensure that the proﬁling
semantics of the call-by-value lambda calculus models execution properly weshould prove that such transformations are also space eﬃcient.
In this paper we have considered space eﬃciency of program transformations. However, there will be program transformations used in compilers
which are not space eﬃcient, but only space safe. It will be interesting toclarify which program transformations are not space eﬃcient, but space safe.

Acknowledgement
We would like to thank Manuel Chakravarty and the anonymous reviewers fortheir many helpful comments. This work is partially supported by the Ministryof Education, Science, Sports and Culture, Grant-in-Aid for Encouragementof Young Scientists of Japan, No. 11780216, 1999.
12

Minamide

References[1] A. W. Appel. Compiling with Continuation. Cambridge University Press, 1992.
[2] G. E. Blelloch and J. Greiner.
A provably time and space eﬃcient
implementation of NESL. In Proc. of ACM SIGPLAN International Conference
on Functional Programming, pages 213–225, 1996.
[3] D. R. Chase. Safety consideration for storage allocation optimization. In
Proc. of ACM SIGPLAN Conference on Programming Language Design and
Implementation, pages 1–10, 1988.
[4] O. Danvy and A. Filinski. Representing control: a study of the CPS
transformation. Mathematical Structures in Computer Science, 2(4):361 – 391,
1992.
[5] M. Fischer. Lambda calculus schemata. In Proc. of the ACM Conference on
Proving Assertions About Programs, SIGPLAN Notices, 7(1), 1972.
[6] C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compilingwith continuations. In Proc. of ACM SIGPLAN Conference on Programming
Language Design and Implementation, pages 237–247, 1993.
[7] J. Greiner and G. E. Blelloch. A provably time-eﬃcient parallel implementationof full speculation. In Proc. of ACM Symposium on Principles of Programming
Languages, pages 309 – 321, 1996.
[8] J. Gustavsson and D. Sands. A foundation for space-safe transformations ofcall-by-need programs. In Proc. of the Third International Workshop on Higher
Order Operational Techniques in Semantics (HOOTS99), 1999.
[9] X. Leroy. Unboxed objects and polymorphic typing. In Proc. of ACM
Symposium on Principles of Programming Languages, pages 177 – 188, 1992.
[10] Y. Minamide and J. Garrigue. On the runtime complexity of type-directed
unboxing. In Proc. of ACM SIGPLAN International Conference on Functional
Programming, pages 1–12, 1998.
[11] G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory
management. In Proc. of ACM Symposium on Functional Programming
Languages and Computer Architecture, pages 66–77, 1995.
[12] G. Morrisett and R. Harper.
Semantics of memory management forpolymorphic languages. Technical report, School of Computer Science, Carnegie
Mellon University, 1996. CMU-CS-96-176.
[13] G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. TheoreticalComputer Science, 1(2):125–159, December 1975.
[14] D. Sands. Complexity analysis for a lazy higher-order language. In Proc. ofEuropean Symposium on Programming, pages 361 – 375, 1990.
[15] Z. Shao and A. W. Appel. Space-eﬃcient closure representations. In Proc. of
ACM Conference on Lisp and Functional Programming, pages 150–161, 1994.

13

MinamideA

Proof of Lemma 5.4.

Proof. By induction on the derivation of ρ, σ, R  M −→ v, σ0 ; s. We only
present the cases for applications and abstractions. The cases for the constantand variables are similar to the case of abstractions.
Case: ρ, σ, R  λx.M −→ l, σ0 ; space(R∪{l}, σ0 ) where σ0 = σ[clρ, x, M/l].
The expression is translated to let f = λxk.M  in kf . Then,ρ [vk /k], σ  , let f = λxk.M  in kf  −→ρ [vk /k][l/f ], σ  [cl ρ , xk, M  /l], kf 
where σ[cl ρ, x, M/l] ≈ σ  [cl ρ , xk, M  /l] and l ≈ l. Let us name thestates above as follows:
Q1 ≡ ρ [vk /k], σ  , let f = λxk.M  in kf 
Q2 ≡ ρ [vk /k][l/f ], σ  [cl ρ , xk, M  /l], kf 
We can calculate locs(Q2 ) as follows:locs(Q2 ) = klocs(vk , σ, σ  ) ∪ hlocs(vk , σ, σ  ) ∪ locs(l, σ  )= klocs(vk , σ, σ  ) ∪ (locs(R, σ) ∪ locs(l, σ  ))Hence
space(Q2 ) ≤ s + kspace(vk , σ, σ  )This completes the proof of this case since space(Q1 ) ≤ space(Q2 ).
Case: ρ, σ, R  M1 M2 −→ v, σ0 ; s is derived from ρ, σ, R1  M1 −→ l, σ1 ; s1and ρ, σ1 , R2  M2 −→ v2 , σ2 ; s2 and ρ3 [v2 /x], σ2 , R  M3 −→ v, σ0 ; s3
where σ1 (l) = cl ρ3 , x, M3  and s = max(s1 + |F V (M2 )| + 1, s2 + 1, s3 ).
The expression is translated to the following expression
let k1 = λf.let k2 = λa.f ak in M2 in M1
where k1  M1
M1 and k2  M2
M2 . Let ρ0 be ρ [vk /k]. We have thefollowing transition.
ρ0 , σ, let k1 = λf.let k2 = λa.f ak in M2 in M1  −→ρ0 [lk1 /k1 ], σ  [vk1 /lk1 ], M1 
where vk1 = cl ρ0 , f, let k2 = λa.f ak in M2  and σ1 = σ  [vk1 /lk1 ].
Let R1 = R ∪ ρ(F V (M2 )). Thenhlocs(vk1 , σ, σ1 ) = hlocs(vk , σ, σ  ) ∪ locs(ρ0 (F V (M2 )))= R ∪ locs(ρ(F V (M2 )), σ) = R1
and ρ ≈ ρ0 . By induction hypothesis for M1 ,ρ0 [lk1 /k1 ], σ1 , M1  −→∗s1 ρ [lk1 /k1 ], σ1 , kx

and σ1 ≈ σ1 and l ≈ ρ (x) and s1 ≤ Ks1 +kspace(vk1 , σ, σ1 ). Thus ρ (x) = l
and σ1 (l) must be the form of cl ρ3 , xk, M3  and k  M3
M3 .
14

Minamide

Let v1 be ρ (x).
ρ [vk1 /k1 ], σ1 , kx −→s1 ρ0 [l/f ], σ1 , let k2 = λa.f ak in M2 −→ρ0 [l/f ][lk2 /k2 ], σ1 [vk2 /lk2 ], M2 

where vk2 = cl ρ [l/f ], a, f ak.
Let R2 = R ∪ {l}. We havehlocs(vk2 , σ2 , σ2 ) = hlocs(vk , σ, σ  ) ∪ {l} = R2
and ρ ≈ ρ0 [l/f ]. By induction hypothesis on M2 ,ρ0 [l/f ][vk2 /k2 ], σ1 [vk2 /lk2 ], M2  −→∗s2 ρ2 [vk2 /k2 ], σ2 , kyand σ2 ≈ σ2 and v2 ≈ ρ2 (y) and s2 ≤ Ks2 + kspace(vk2 , σ2 , σ2 ).
Let v2 be ρ2 (y).
ρ2 [vk2 /k], σ2 , ky −→ ρ0 [l/f ][v2 /a], σ2 , f ak
−→ ρ3 [v2 /x][vk /k], σ2 , M3 
Since ρ3 [v2 /x] ≈ ρ3 [v2 /x], by induction hypothesis on the evaluation of M3
ρ3 [v2 /x][vk /k], σ2 , M3  −→∗s3 ρ3 [vk /k], σ0 , kz
and σ0 ≈ σ0 and v ≈ ρ3 (z) and s3 ≤ s3 + klocs(vk , σ2 , σ2 ).
By summarizing, we have the following transition.
Q0 = ρ0 , σ, let k1 = λf.let k2 = λa.f ak in M2 in M1 
↓


Q0 =
ρ0 [lk1 /k1 ], σ  [vk1 /lk1 ], M1 
s
↓∗1
Q1 =
ρ [lk1 /k1 ], σ1 , kx↓ρ0 [l/f ], σ1 , let k2 = λa.f ak in M2 
Q1 =↓ρ0 [l/f ][lk2 /k2 ], σ1 [vk2 /lk2 ], M2 
s
↓∗2
Q2 =
ρ2 [vk2 /k2 ], σ2 , ky↓Q2 =ρ0 [l/f ][v2 /a], σ2 , f ak↓ρ3 [v2 /a][vk /k], σ2 , M3 s↓∗3ρ3 [vk /k], σ0 , kz
By checking reachable locations from the states above, we obtain thefollowing relations.
space(Q0 ) ≤ space(Q0 ) ≤ s1
space(Q1 ) ≤ space(Q1 ) ≤ s1
space(Q2 ) ≤ space(Q2 ) ≤ s215

Minamide

Hence we obtainσ  , ρ [vk /k], M   →∗s σ0 .ρ [vk /k], kx
for s = max(s1 , s2 , s3 ).
Then the following calculation completes the proof of this case.
s1 ≤ Ks1 + kspace(lk1 , σ, σ  [vk1 /lk1 ])= Ks1 + kspace(vk , σ, σ  ) + |F V (M2 )| + 2≤ Ks + kspace(vk , σ, σ  )s2 ≤ Ks2 + kspace(lk2 , σ1 , σ1 [vk2 /lk2 ])= Ks2 + kspace(vk , σ, σ  ) + 3≤ Ks + kspace(vk , σ, σ  )s3 ≤ Ks3 + kspace(vk , σ2 , σ2 )≤ Ks + kspace(vk , σ, σ  )16