A New Criterion for Safe Program
Transformations
Yasuhiko Minamide
Institute of Information Sciences and Electronics
University of Tsukuba
and
PRESTOJapan Science & Technology Corporation
Email: minamide@score.is.tsukuba.ac.jp

Abstract
Previous studies on safety of program transformations with respect to performance
considered two criteria: preserving performance within a constant factor and preserving complexity. However, as the requirement of program transformations usedin compilers the former seems too restrictive and the latter seems too loose. We
propose a new safety criterion: a program transformation preserves performancewithin a factor proportional to the size of a source program. This criterion seems
natural since several compilation methods have eﬀects on performance proportional
to the size of a program. Based on this criterion we have shown that two semantics
formalizing the size of stack space are equivalent. We also discuss the connection
between this criterion and the properties of local program transformations rewriting
parts of a program.

1

Introduction

Recent compilers utilize advanced program transformations to obtain highperformance executable code. For these advanced program transformations,
it is not so straightforward to guarantee that they are safe with respect toperformance. In fact, some program transformations have been shown to
improve the performance of most programs, while degrading the performanceof some programs severely [9,12].
To remedy this situation, several papers have discussed the safety of program transformations based on semantics formalizing the performance of programs [7,6,11,2,8]. In those studies, two safety criteria for whole-programtransformations were discussed. However, these criteria do not seem appropriate to impose on program transformations used in compilers, for reasons weThis is a preliminary version. The final version can be accessed at
URL: http://www.elsevier.nl/locate/entcs/volume41.html

Minamide

discuss below. In this paper we focus on the space requirement of programs incall-by-value functional languages, but the general framework can be adopted
for other languages and performance metrics.
The ﬁrst of the above two criteria ensures that a program transformation
preserves space requirement within a constant factor. If a program transformation satisﬁes this property, we say that the program transformation isspace eﬃcient. Many program transformations seem to satisfy this criterion,
but there are some useful transformations that do not satisfy this criterion.
Furthermore, to show this criterion is satisﬁed we must formalize the details of semantics formalizing space requirements. In the study of the CPS
transformation, it was necessary to revise the space proﬁling semantics of acall-by-value functional language by Blelloch and Greiner [3], to show that
this transformation satisﬁes this criterion [8].
The second criterion is space safety: a program transformation is spacesafe if it does not raise the complexity of programs. Clearly, program transformations used in a compiler must satisfy this criterion. However, we thinkthat this criterion is too loose. This criterion does not impose any restriction for programs without inputs. However, showing space safety is simpler
than showing space eﬃciency, in the sense that it is possible to adopt a simpler proﬁling semantics that ignores details such as sizes of closures and stack
frames.
In this paper we propose a new criterion that falls between the above two
criteria. The new criterion is that a program transformation preserves thespace requirement within a factor proportional to the size of a source program.
Most useful transformations used in a compiler seem to satisfy this criterion.
This criterion seems natural because several compilation methods have eﬀects
on performance proportional to the size of a program. Furthermore, we canshow this criterion based on semantics ignoring some details as we show spacesafety.
Based on the new criterion we have shown that two semantics of a simple
call-by-value functional language proﬁling stack space are equivalent. One
models evaluation by an interpreter and the other models execution basedon compilation. They are not equivalent in the sense of space eﬃciency, butthey are equivalent in the sense of our new criterion. We also show that Anormalization preserves stack space modeled by the second semantics. Thisbacks the claim that the second semantics models stack space required forexecution based on compilation.
The criterion we propose is a property of a whole-program transformation.
On the other hand, some transformations used in compilers are based on local
program transformations. We therefore also study the connection between
the properties of local transformations and the properties of global transformations. We will show that some restricted class of local transformations
induces whole-program transformations satisfying our new criterion.
2

MinamideThis paper is organized as follows. We begin by reviewing the two safety
criteria discussed in previous studies and discussing why they are not suitable as the criterion we impose on the transformations used in a compiler.
In Section 3 we introduce our new safety criterion and the equivalence of semantics on a programming language induced by the criterion. In Section 4,
based on this new safety criterion, we show that two operational semantics
of a call-by-value functional language are equivalent. In Section 5 we discuss
the connection between the properties of local transformations and our new
criterion. Finally, we give our conclusions and directions for future work.

2

Safety criteria of program transformations

We review the safety criteria of program transformations with respect to performance discussed in previous studies. To formalize safety criteria we mustﬁrst develop semantics to formalize performance of programs. We call suchsemantics proﬁling semantics. For a simple programming language, proﬁling
semantics can be given as a partial function eval(M):eval(M) = (v, n)This function gives the computation result v and a non-negative integer n,which represents such performance values of programs as execution time orspace required for execution.
In this paper, to simplify our discussion, we focus on the space requirementof a program and ignore the computation result. For this purpose we deﬁnespace(M) as below:
space(M) = n iﬀ eval(M) = (v, n) for some v
This function is only deﬁned if the evaluation of M terminates. We callthis semantics for specifying space required for execution of a program spacesemantics.
Let us now review two space safety criteria of program transformations
discussed in previous work [1,3,8]. In this paper, we consider a program transformation as a binary relation between programs in a source language anda target language. Let us consider a program transformation ; between asource language and a target language that have space semantics space(M)and space  (M  ) respectively: M ; M  means that M is translated to M  bythe program transformation.
The ﬁrst criterion ensures that a program transformation preserves thespace required for execution of a program within a constant factor.
Definition 2.1 We say that a program transformation ; is space eﬃcient if
constants k1 and k2 exist such that:space(M) = n =⇒ space (M  ) ≤ k1 n + k2
3

Minamide

for any programs M and M  with M ; M  .
We admit constants k1 and k2 because they seem dependent on the detailsof deﬁnition of space semantics and not essential. Moreover, there are severaltransformations in which k1 > 1 is required to show this property. This
property was ﬁrst discussed by Blelloch and Greiner for an implementationof NESL [3]. Minamide also showed that the CPS transformation is spaceeﬃcient [8].
The second criterion is called space safety: a transformation is space safe
if it does not increase the space complexity of programs [1]. To formalize
this idea we must consider programs with an input; thus we can consider aprogramming language with input commands and the semantics space(M, I),
which formalizes the space required for execution of the program M for the
input I.
Definition 2.2 We say that a program transformation ; is space safe if forany programs M and M  such that M ; M  , constants k1 and k2 exist suchthat for any input I the following holds:
space(M, I) = n =⇒ space  (M  , I) ≤ k1 n + k2
The key diﬀerence from space eﬃciency is that the constants k1 and k2
are program-dependent. Space eﬃciency usually implies space safety because
space eﬃciency provides the constants k1 and k2 to show space safety without
depending on programs.
Although many program transformations used in compilers seem spaceeﬃcient, some useful transformations are not space eﬃcient, but only spacesafe. Furthermore, to show that a program transformation is space eﬃcient
we must consider too many details of the operational semantics of the source
language. In the study of the CPS transformation it was necessary to revise
the semantics proposed by Blelloch and Greiner [3] to show that the CPS
transformation was space eﬃcient [8].
Code motion is a typical example of a transformation that is space safe,
but not space eﬃcient. Consider the following expression where M is a pure
expression that contains the variable n but does not contain a function application:
fun loop 0 = ()| loop n = let val x = M

inloop (n - 1) end

The value of M is loop-invariant, thus we want to hoist the binding of x as
follows:
val x = M
fun loop 0 = ()| loop n = loop (n - 1)
This usually improves the performance of the program. However, if the func4

Minamidetion loop is used only as loop 0 or is not actually used, this transformation
results in extra computation of M. The extra time and space to evaluate M is
not uniformly bounded by a constant, but depends on M.
On the other hand, space safety seems too weak as a requirement of transformations used in compilers. Space safety is trivial for programs without
inputs. Even for programs with inputs, it is impossible to estimate the performance of a program since the constants k1 and k2 are program-dependent.
Thus in this paper we propose a new criterion that falls between space eﬃciency and space safety.

3

A new criterion

In this section, we propose a new safety criterion for program transformations. First, to simplify our discussion, we compare two space semantics of aprogramming language.
Let us consider two space semantics space1(M) and space2(M) of a programming language. As a natural extension of space eﬃciency, we can consider
the following property: there exists a polynomial f such thatspace 1 (M) = n =⇒ space 2(M) ≤ f(n)However, this property is not suitable as a criterion that space 2 (M) is safewith respect to space 1 (M). By extending the language and the semantics
with inputs, we have the following property:
space 1(M, I) = n =⇒ space 2(M, I) ≤ f(n)Even if this holds, it might happen that for an input of size n space 1 requires
n space, but space 2 requires n2 space, because f(x) = x2 . Thus, this extended
property does not imply safety and is therefore not suitable as a criterion thatspace 2 is safe with respect to space 1 .
When we consider various semantics of a language, the diﬀerence in space
usage often depends on the size of a program. Thus, it is natural to consider
the following relation of semantics.
Definition 3.1 We say that the semantics space 1 is weakly simulated by
space 2 ifspace 1 (M) = n =⇒ space 2(M) ≤ f1 (|M |)n + f2 (|M |)where f1 (x) and f2 (x) are polynomials with positive coeﬃcients and |M | isthe size of M.
Hereafter in this paper we simply say “a polynomial” for “a polynomialwith positive coeﬃcients.”
This relation induces equivalence of semantics as follows.
5Minamide

Definition 3.2 We say that semantics space 1 is weakly space equivalent tospace 2 if space 1 is weakly simulated by space 2 and space 2 is weakly simulated
by space 1 .
Most reasonably deﬁned semantics of a language seem weakly space equivalent. Moreover, it is possible to deﬁne simpler semantics weakly space equivalent to the semantics considered in previous studies.
Example 3.3 Let space 1 be a semantics of a functional language that accounts for the sizes of closures: the size of a closure with n free variables isn + 1. Let space 2 be a semantics where the sizes of closures are ignored: thesizes of closures are always 1. Then space 1 and space 2 are weakly equivalent,since the sizes of the closures constructed during evaluation of a program arebounded by the size of the program.
Example 3.4 Let space 1 and space 2 be a semantics that accounts for the sizeof each stack frame and a semantics that ignores the size of each stack frame,
respectively. Then space 1 and space 2 are weakly equivalent, since the sizes ofthe stack frames constructed during evaluation of a program are bounded by
the size of the program.
Although these examples are rather straightforward, they show that we
can adopt a simple space semantics when we consider weak simulation. We
will also show that two space semantics proﬁling stack space are equivalent in
Section 4. The proof of this equivalence requires detailed analysis of the spacesemantics.
Now we extend weak simulation as a safety criterion for program transformations. Consider a program transformation ; between a source language
and a target language that have space semantics space(M) and space  (M  ),respectively, as before.
Definition 3.5 We say that a program transformation ; is weakly spaceeﬃcient if polynomials f1 (x) and f2 (x) exist such that:space(M) = n =⇒ space  (M  ) ≤ f1 (|M |)n + f2 (|M |)for any programs M and M  with M ; M  .
This criterion clearly falls between space eﬃciency and space safety. It
admits that a program transformation degrades performance within a factor
dependent on the size of a program. This gives us much more freedom todesign program transformations used in compilers than is possible with spaceeﬃciency.
To construct a compiler that is a weakly eﬃcient transformation as a whole,
the composition of transformations must be weakly space eﬃcient since actual
compilers consist of many phases. To make the composition weakly space
6

Minamideeﬃcient we should restrict program transformations so that the expansion of
the size of a program is limited by some polynomial.
Definition 3.6 We say that a program transformation M ; M  is polynomial size safe if |M  | ≤ f(|M |) for all programs M where f(x) is a polynomialof x.
This is a natural restriction because actual compilers already avoid exponential blowup of code size. We can now construct a weakly space eﬃcientcompiler by composing weakly space eﬃcient and polynomial size safe transformations.
Theorem 3.7 Let ;1 and ;2 be program transformations from L1 to L2 andfrom L2 to L3 respectively. If ;1 is weakly space eﬃcient and polynomial size
safe, and ;2 is weakly space eﬃcient, then their composition ;1 ◦ ;2 is aweakly space eﬃcient transformation from L1 to L3 .
Proof. Let M ;1 ◦ ;2 N. Then P exists such that M ;1 P and P ;2 N.
By weak space eﬃciency we have:space 2 (P ) ≤ f11 (|M |)space 1 (M) + f21 (|M |)space 3 (N) ≤ f12 (|P |)space 2 (P ) + f22 (|P |)By polynomial size safety we have |P | ≤ g(|M |). Then:
space 3 (N) ≤ f12 (g(|M |))(f11 (|M |)space 1 (M) + f21 (|M |)) + f22 (g(|M |))Here, f12 (g(x))f11(x) and f12 (g(x))f21 (x) + f22 (g(x)) are clearly polynomials ofx.
2This proof clariﬁes why we adopted a polynomial instead of a linear function in the deﬁnition of weakly eﬃcient transformation. Even if two transformations are bounded by linear functions of the size of a program, theircomposition is not necessarily bounded by some linear function.

4

Weak equivalence on stack space

In this section we consider two space semantics proﬁling stack space for a
simple call-by-value functional language. One semantics models evaluation by
an interpreter and the other models evaluation based on compilation. Bothsemantics properly model tail calls. We show that although they allocate
diﬀerent numbers of stack frames during evaluation, the semantics are weakly
space equivalent. Furthermore, it is shown that A-normalization preserves
stack space for the second semantics.
7

MinamideE  c ↓1 c E  x ↓1 E(x) E  λx.M ↓1 cl E, x, M
E  M1 ↓l cl E  , x, M E  M2 ↓m v2 E [v2/x]  M ↓n v
E  M1 M2 ↓max(l+1,m+1,n) v
Fig. 1. Operational semantics proﬁling stack size (interpreter-based)

4.1

Equivalence of two semantics proﬁling stack space

We consider the following untyped call-by-value λ-calculus with a constant c:
M ::= x | c | λx.M | M1 M2
We deﬁne two space semantics spaceλ1 (M) and spaceλ2 (M) by deductive systems. For the deﬁnition of the deductive systems, we ﬁrst deﬁne values: avalue v is either a constant c or a closure cl E, x, M consisting of an environment E mapping variables to values, a variable and an expression.
v ::= c | cl E, x, M
The space semantics spaceλ1 (M) models evaluation by an interpreter and isdeﬁned by the deductive system given in Figure 1.
spaceλ1 (M) = n iﬀ ∅  M ↓n v
The space semantics spaceλ2 (M) models stack space required for execution
based on compilation and is deﬁned by the deductive system given in Figure 2.
spaceλ2 (M) = n iﬀ ∅ t2 M ↓n v
The deductive system is deﬁned mutually inductively by the following two
judgments: E t2 M ↓n v models execution at tail call positions and E n2
M ↓n v models execution at non-tail call positions. The application at a tailcall position does not allocate a new stack frame. In the ﬁgure, we writeE 2 M ↓n v for E t2 M ↓n v and E n2 M ↓n v.
We have shown that the two semantics spaceλ1 (M) and spaceλ2 (M) are
weakly equivalent.
Theorem 4.1 If ∅  M ↓i v and ∅ t2 M ↓i v, then i + 1 ≤ i ≤ |M | · (i + 1).
To prove this theorem we must generalize the claim so that non-empty
environments can be treated. To treat non-empty environments we deﬁne the8MinamideE 2 c ↓0 c E 2 x ↓0 E(x) E 2 λx.M ↓0 cl E, x, ME n2 M1 ↓l cl E  , x, M E n2 M2 ↓m v2 E  [v2/x] t2 M ↓n v
E n2 M1 M2 ↓max(l,m,n+1) v
E n2 M1 ↓l cl E  , x, M E n2 M2 ↓m v2 E  [v2/x] t2 M ↓n v
E t2 M1 M2 ↓max(l,m,n) v
Fig. 2. Operational semantics proﬁling stack size (compiler-based)

size of a value and an environment as follows:|c|v = 0|cl E, λx.M |v = max(|E|v , |M |v )|E|v = e max{|E(x)|v | x ∈ Dom(E)}Then the theorem is generalized to the following lemma. This lemma is provedby induction on the derivation of evaluation.
Lemma 4.2 Let K be a constant such that |M | ≤ K and |E|v ≤ K.
(i) If E  M ↓i v and E t2 M ↓i v, then i + 1 ≤ i ≤ K · (i + 1).
(ii) If E  M ↓i v and E n2 M ↓i v, then i ≤ i ≤ K · i + |M |.
4.2

Preservation of stack space by A-normalization

In this section we show that A-normalization preserves stack space given by
spaceλ2 (M) and thus spaceλ2 (M) actually models execution based on compilation. This also shows that A-normalization is weakly space eﬃcient withrespect to spaceλ1 (M).
We deﬁne the syntax of the language of A-normal forms as follows:
ValuesV ::= x | λx.M

Expressions M ::= V | V1 V2 | let x = V1 V2 in M
The application V1 V2 represents tail calls and the application in let x =V1 V2 in M represents non-tail calls.
The semantics of this language is naturally given by the Ca EK Machinedeﬁned in Figure 3 [5]. In this operational semantics continuation clearly
9Minamide

State S = M, E, K
Continuation K = stop | ar x, M, E, K
Transition Rules:
v, E, ar x, M, E  , K  → M, E  [γ(v, E)/x], K 
let x = V1 V2 in M, E, K → M  , E  [V2 /x], ar x, M, E, K 
where γ(V1 , E) = cl x, M , E  V1 V2 , E, K → M  , E  [V2 /x], K
where γ(V1 , E) = cl x, M , E  γ(V, E) =⎧⎨ E(x)

if V ≡ x⎩ cl x, M, E if V ≡ λx.M

Fig. 3. The Ca EK Abstract Machinecorresponds to stack. The size of continuation is naturally deﬁned as follows:size(stop) = 0
size(ar x, M, E, K) = size(K) + 1

In this deﬁnition we ignore the size of each frame because it is bounded by
the size of the program and we discuss weak space eﬃciency in this paper. To
discuss space eﬃciency it is natural to count the number of free variables ofM.
The stack space of state M, E, K is deﬁned by size(K). Then we deﬁne
the space semantics of this language as follows: space A (M) = n if M, ∅, stop →∗V, E  , stop and n is the maximum size of the states in the transition.
A-normalization can be deﬁned as one pass translation [5,4]. In the following deﬁnition, we use a two-level lambda calculus where λ and @ are meta-level
abstraction and application. ||M ||A κ translates expressions at non-tail callpositions and ||M ||A translates expressions at tail call positions. The entire
10Minamide

program is translated by ||M ||A .
|x|A = x|λx.M |A = λx.||M ||A||V ||A κ = k@|V |A||M1M2 ||A κ = ||M1||A (λx1.||M2||A (λx2.let z = x1x2 in κ@z))||v||A = |v|A||M1M2 ||A = ||M1||A (λx1.||M2||A (λx2.x1x2 ))Then it is shown that the stack space required for execution is preserved by
A-normalization.
Theorem 4.3 If spaceλ2 (M) = n, then spaceA (||M ||A ) = n.
This theorem shows that spaceλ2 (M) models the stack space required forexecution based on compilation. Furthermore, since spaceλ2 (M) is weakly
equivalent to spaceλ1 (M), it is enough to consider spaceλ1 (M) even when we
consider weak eﬃciency of program transformations with respect to execution
based on compilation.

5

Local transformations

In this section we discuss the connection between our new criterion and theproperties of local program transformations. We show that some class of local
transformations induces weakly space eﬃcient transformations.
Based on the classiﬁcation of local transformations by Gustavsson andSands [7] we deﬁne two classes of local transformations.
Definition 5.1 Let R be a relation on terms of a programming language.
(i) We say that R is a strong improvement relation if we have:space(C[M ]) = n =⇒ space(C[N ]) ≤ n
for all (M, N) ∈ R and all context C[·] producing a whole program for
M and N.
(ii) We say that R is a weak improvement relation if there exists some linear
function f such that the following holds for all (M, N) ∈ R and all context
C[·] producing a whole program for M and N.
space(C[M ]) = n =⇒ space(C[N ]) ≤ f(n)11Minamide

We should remark that there is one subtle diﬀerence in our deﬁnition of
weak improvement from that of Gustavsson and Sands. They deﬁned a single
weak improvement relation as follows. M  N if some linear function f exists≈

such that for all contexts C[·] the following holds:
space(C[M ]) = n =⇒ space(C[N ]) ≤ f(n)The relation  is the union of all the weak improvement relations. However,≈this relation  itself is not a weak improvement relation in our sense.
≈

To discuss the connection between these properties and the propertiesof global transformations, we ﬁrst deﬁne the induced global transformation
M ;R N as follows: M ;R N if some C[·], M  and N  exist such that
M = C[M  ], N = C[N  ], and (M  , N ) ∈ R. Then we immediately obtain thefollowing theorem.
Theorem 5.2 If R is a weak or strong improvement relation, ;R is spaceeﬃcient.
On the other hand, the relation  does not induce a space eﬃcient trans≈

formation. This is because there is no single linear function f such thatspace(C[N ]) ≤ f(space(C[M ])) for all M  N.
≈

The theorem above is still not enough to use a local transformation in acompiler. In a compiler we usually apply local transformations n times in one
phase of a compiler where n is proportional to the size of a program. Evenfor such composition, a strong improvement relation induces a space eﬃcienttransformation.
Theorem 5.3 If R is a strong improvement relation, ;∗R is space eﬃcient.
On the other hand, a weak improvement relation does not necessarily induce a weakly space eﬃcient transformation. Consider the following sequenceof transformations where R is a weak improvement relation with space(C[N ]) ≤kspace(C[M ]) for all (M, N) ∈ R.
M0 ;R M1 ;R M2 ;R M3 ;R . . . ;R Mn
The space requirement of Mn can be calculated as follows:space(M2 ) ≤ kspace(M1 )space(M3 ) ≤ kspace(M2) ≤ k 2 space(M1 )space(Mn ) ≤ k n space(M1 )12Minamide

Then it is clear that there is no single linear function f such that:space(N) ≤ f(space(M))
for M ;∗R N. Even if we restrict the number of repetitions to |M0 |, k n is nota polynomial of |M0 |. Thus, it is not even weakly space eﬃcient.
We therefore must consider stricter conditions on local transformations.
In the following deﬁnition a local transformation is permitted to add only aconstant amount of extra space.
Definition 5.4 We say that R is a semi-strong improvement relation if someconstant k exists such that:space(C[M ]) = n =⇒ space(C[N ]) ≤ n + k
for all (M, N) ∈ R and all context C[·] producing a whole program for M andN.
It can be shown that this class of local transformations induces weakly
space eﬃcient transformations if the number of applications of the transformation is limited by the size of a source program. We write M →R N if
M ;nR N where n ≤ |M |.
Theorem 5.5 If R is a semi-strong improvement relation, M →R N is
weakly eﬃcient.
Although this theorem relates a semi-strong improvement relation to weakly
eﬃcient transformations, semi-strong improvement relations seem too restrictive. There are many useful transformations R that are not semi-strong improvement relations, but →R seem weakly space eﬃcient. The following transformation is an example.
λx.let y = M in N ⇒ let y = M in λx.N
We have not shown formally that this transformation is weakly space eﬃcient.
For such proof we think that we require further study on the connections
between global transformations and local transformations.

6

Discussion and future work

We have shown weak eﬃciency only for stack space for two semantics of asimple functional language. It will not be very diﬃcult to deal with execution
time or heap space. For example, the proof that the CPS transformation isspace eﬃcient [8] can easily be modiﬁed to show that the CPS transformation
is weakly space eﬃcient with respect to a simpler space semantics of the source
language that ignores the sizes of closures and stack frames.
13

Minamide

We have shown no examples of local program transformations that are
weak improvement relations or semi-strong improvement relations. We areplanning to show that various optimizations formalized as local program transformations have these kinds of properties. In this area, Gustavsson and Sands
have developed a theory of space improvement relations for call-by-need programming languages and have shown that several local transformations are
weak improvements [7]. Their work will be also applicable to call-by-value
languages.
We think that the framework we have developed in this paper requires
further reﬁnement. For example, although intuitively clear, it is not provedthat space safety, weak space eﬃciency and space eﬃciency ensure that the
space complexity of programs is preserved. Bakewell and Runciman discussed
these kinds of issues more formally in their study on the comparison of space
usage of lazy evaluators [2]. They modeled lazy evaluators by graph rewriting
systems. This kind of uniform formalization of semantics may help develop atheory of safe program transformations.
There is an implementation strategy of ML that is not space eﬃcient, but
is space safe. That is the implementation strategy that uses types as parameters at runtime [10,13]. This is because the extra work and space necessary
for type parameters cannot be bounded by any constant. Furthermore, this
implementation strategy is not even weakly space eﬃcient, because the types
appearing in the typing derivation of a program may have a size exponential to the size of the program. However, if we take the sum of the size ofa program and the maximum size of types appearing in typing derivation of
the program as the size of the program, this implementation strategy can beconsidered weakly space eﬃcient. By choosing the deﬁnition of the size of aprogram in this way we can control the class of transformations that can beused in compilers of the language.

Acknowledgement
This work is partially supported by the Ministry of Education, Science, Sports
and Culture, Grant-in-Aid for Encouragement of Young Scientists of Japan
No. 11780216, 1999. We would like to thank anonymous reviewers for their
many helpful comments and suggestions.

References[1] Appel, A. W., “Compiling with Continuation,” Cambridge University Press,
1992.
[2] Bakewell, A. and C. Runciman, A model for comparing the space usage oflazy evaluators, in: 2nd International Conference on Principles and Practiceof Declarative Programming (PPDP 2000), 2000.

14

Minamide[3] Blelloch, G. E. and J. Greiner, A provably time and space eﬃcient
implementation of NESL, in: Proc. of ACM SIGPLAN International Conference
on Functional Programming, 1996, pp. 213–225.
[4] Danvy, O. and A. Filinski, Representing control: a study of the CPS
transformation, Mathematical Structures in Computer Science 2 (1992), pp. 361– 391.
[5] Flanagan, C., 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, 1993, pp. 237–247.
[6] Greiner, J. and G. E. Blelloch, A provably time-eﬃcient parallel implementationof full speculation, in: Proc. of ACM Symposium on Principles of Programming
Languages, 1996, pp. 309 – 321.
[7] Gustavsson, J. 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), ENTCS 26, 1999.
[8] Minamide, Y., A space-proﬁling semantics of call-by-value lambda calculus andthe CPS transformation, in: Proc. of the Third International Workshop on
Higher Order Operational Techniques in Semantics (HOOTS99), ENTCS 26,
1999.
[9] Minamide, Y. and J. Garrigue, On the runtime complexity of type-directed
unboxing, in: Proc. of ACM SIGPLAN International Conference on Functional
Programming, 1998, pp. 1–12.
[10] Ohori, A. and N. Yoshida, Type inference with rank 1 polymorphism for
type-directed compilation of ML, in: Proc. of ACM SIGPLAN International
Conference on Functional Programming, 1999, pp. 160– 171.
[11] Santos, A. L., “Compilation by Transformation in Non-strict Functional
Languages,” Ph.D. thesis, Department of Computing Science, University ofGlasgow (1995).
[12] Shao, Z., Flexible representation analysis, in: Proc. of ACM SIGPLAN
International Conference on Functional Programming, 1997, pp. 85 – 98.
[13] Tarditi, D., G. Morrisett, P. Cheng, C. Stone, R. Harper and P. Lee, TIL:
A type-directed optimizing compiler for ML, in: Proc. of ACM SIGPLAN
Conference on Programming Language Design and Implementation, 1996, pp.
181–192.

15