BIB-VERSION:: CS-TR-v2.0
ID:: CORNELLCS//TR93-1384
ENTRY:: 1993-10-14
ORGANIZATION:: Cornell University, Computer Science Department
LANGUAGE:: English
TITLE:: Deriving Incremental Programs
AUTHOR:: Liu, Yanhong A.
AUTHOR:: Teitelbaum, Tim
DATE:: September 1993
PAGES:: 38
ABSTRACT::
A systematic transformational approach is given for deriving incremental 
programs from non-incremental programs. We exploit partial evaluation, other 
static analysis and transformation techniques, and domain-specific knowledge 
in order to provide a degree of incrementality not otherwise achievable by a 
generic incremental evaluator. Illustrative examples using the transformation 
approach are given.
END:: CORNELLCS//TR93-1384
BODY::
Deriving Incremental Programs
Yanhong Liu*
Tim Teitelbaum*
TR 93-1384
September 1993
Department of Computer Science
Cornell University
Ithaca NY 14853-7501
The authors gratefully acknowledge the support of the Office of Naval Research
under contract No. NOOOl 4-92-J-1 973.
Deriving Incren?enta1 Progran?s
Yanhong Lin			Tim Teitelbaum
Department of Computer Science, Cornell University, Ithaca, NY 14853
fyanhong, ttj(mctcs.cornell.edu
September 1993
Abstract
A systematic trausformational approach is given for deriving incremental programs from
non-incremental programs. ?Ve exploit partial evaluation other static analysis and transforma-
tion techniques, and domain-specific knowledge in order to provide a degree of incrementality
not otherwise achievable by a generic incremental evaluator. Illustrative examples using the
transformation approach are given.
1			Introduction
Incremental programs take advantage of repeated computations on inputs that differ only slightly
from one another, avoiding unnecessary duplication of conimon computations. Given a computa-
tion of f(x) with result r and a new input ? & to the program f, an incrementJ program f'
computes the result of f(x ? ?r) by making use of r, avoiding computations previously done by
f(x). Niethods of incremental computation have widespread application throughout software, e.g.,
optimizing compilers [1] [6] [7], trausformational programming [1.5] [32], interactive editing systems
[25] [3], etc. Based on the observation that explicitly incremental programs are hard to write, we
aim to provide incremental computation automatically from non - incremental programs.
In this paper, we present a technique for formally deriving an incremental program f' from a
non-incremental program f and input change ??. ?Ve exploit partial evaluation, other static analysis
and transformation techniques, and domain-specific knowledge in an attempt to provide a degree
of incrementality not otherwise achievable by a generic incremental evaluator. The technique is
presented as a four-step transformation: (1) &xpanding the computation f( x E 6x) to separate
computations on x from the rest, (2) introducing the cache parameter ? f(x) (3) replacing
The authors gratefully acknowledge the support of the Office of Naval Research under contract No. Nooo14-92-
J-1973
equivalent computations on x by retrieving results from r, and (4) eliminating redundant code.
In the third step, a subroutine called auxiliary generalized partial evaluation is employed to help
discover incrementalities. We also cast our derivation approach in terms of a generalized partial
evaluation point of view.
Paige's work on fInite differencing is the pioneering work on deriving incremental programs
[18] [14] [31] [5]. Whereas Paige's methods are for very high-level set-theoretic languages, our
techniques apply to general functional programs, as does Smith's approach in KIDS [32] [33]. For
further discussions and comparisons between these methods, see Section 8.
The rest of the paper is organized as follows: In Section 2, we give the defInition of incremental
programs. Our basic approach for the derivation of incremental programs is outlined in Section
3. The formalization of the problem with the language we are using is presented iii Section 4. In
Section 5, ?ve formalize the transformations for the derivation and argue that they preserve the
semantics of the programs. ?n example using the transformations is given iii Section 6 iii which
an insert program is derived from a sort program. Several related issties, including a limitation of
the approach and directions for remedying them, are discussed in Section 7. Finally, we discuss
related work in incremental computation iii Section 8.
2 Incremental Programs
Let f be a program and r an input for f. Let &` be a cIic?ng? in the value of x and ? a ch?ingc-
operation that combines value w and change ?x to produce a new input value r &. In general, the
domains of r and & need not be the same. For example consider a list of integers x, an integer
&, and x Q, & cons(&, x); i.e., x is changed by prepending integer & at the head of the list.
Let r f(x); i.e., r is the result of executing program f on input . We call r the caclied result
and aim to make use of it in computing f(x ? &). Let f), be a program such that whenever 7. is
the cached result f(x), fe'(x,&,r) computes f(x t' &) for all possible x and 6, i.e.,
(Vx)(V&)(Vr) [f(x) 1= r?f?(x,&'.,r)= f(xE?&)]			(1)
where f(x) I r nieans that f(x) tern?inates ?vith value `r. Then f4 is called aii inc'i?inental version
of f under e if, in additioii to satisfying (1), f2(x. kr, r) computes faster than f(x ? &) for almost
all x and & and makes non-trivial use of r. By computing faster. we mean that a computation takes
less time under some time model. By making non-trivial use of r we mean that the availability of
r is indispensable in obtaining the faster computation.
For &xample, assume the RAM modd and let sort(x) be a selection sort on a list x of numbers
2
that uses a naive select (which finds a least element in a list by traversing the list from the beginning
to the end). Then, sort(x) takes time 0(n2) for x of length n. Consider the change to the input x
given by x fD lii' cons(&,x), where 6x is a number. There exists a ?ort'(x, or. ,r) that, when r is
sort(r), computes sort(cons(&, x)) by inserting &. in r in 0(n) time. Then by definition, sort' is
an incremental version of sort. In particular, sort' makes non-trivial use of r since otherwise it is
impossible for a sort program to compute in 0(n) time. In contrast, consider a sort11(x, 6x, r) that
computes sort(cons(?,r)) by doing a merge sort on cons(?,r) and takes only 0(nlogn) time.
sort" is not an incremental version of sort since it gains its speedup without the use of r.
Suppose f? is an incremental version of f under O'. N\?e say that is a complete incremental
version if f? does not depend at all on the parameter x, i.e., f?(x,ar,r) f?(e,ar,r) for all x, or,
and constant c. Iii other words, f?(x, or, r) computes f(x D; 6x) but only uses the change parameter
or and the cached result r. In the sort exau?ple, sort' is a complete incremental version of sort
under ?.
For a formal definition of incremental programs, see [13]. ?Vhen no confusion arises, we simply
write f' for f?. For typographical convenience, we shall typically use y for the change parameter
rather than or. Also, throughout the paper, identifier r always refers to the cached result of a
previous computation f(x).
In [13], it is proved that in general, given a program f and an input change operation t,
whether an incremental version f' exists is undecidable. Accordingly we compromise by seeking an
approximation to an incremental version, which we call a diffei'entiated version? differentiated
version f' differs from an incremental version in that it only guarantees that f' computes at least
as fast as the onginal program for almost all inputs. while an incremental version computes strictly
faster than the original program for almost all inputs. If a differentiated version only uses the
change parameter or and the cached result r, then it is called a compThte differentiated version.
Obviously, a differentiated version f'(x, or, r) can be trivially defined to be f(x D ?). But then
no efficiency is gained by f', which is of no interest. The goal is to make f' as efficient as possible
by having it use the cached result r as much as possible.
3 Derivation Approach
Basic Ideas. We aim to identify in the computation of f(x ? y) those computations that are also
performed in the computation of f(x) and avoid recomputing them if possible.
More precisely, by expanding the computation of f(x G y) those computations on x in f(x Q' y)
3
can be separated out from the rest of the computation. Given the cached result r of a previous
computation of f(x), the results of some of the computations on x in f(x ? y) may be retrieved
more efficiently from 1 than computing them from scratch. This more efficient way to compute
f(x ? y) is captured in the definition of the differentiated version f?(x, y, r).
In order to explain the basic ideas further, we break the derivation approach into four steps.
Step I. Expanding the computation of f(x ? to separate out the computations on x from
the rest of computation. This is achieved by unfolding and simplifying function applications whose
arguments involve both x and y.
Step 2. Introducing the cached result r of the computation f(x). In this step, we define
f?(x, y, r) to be the expanded computation of f(x t y) obtained from Step 1. In particular, if an
application of f whose arguments involve both x and y occurs recursively in the expanded compu
tation of f(x 0 y), it is replaced by an instance of f*(x, y, ?), if possible. Thus, the computation of
f(x 0 y) is perlormed by f*(x, y, ??).
Step 3. Using the cached result r in the computation of f?(x y, r). Iii the definition of f?(r, y, r)
obtained from Step 2, we find computations that are also performed by f( x), and replace them by
retrievals from the cached result r where possible. As a straightforward example, an occurrence
of f(x) in the definition of f*(x, y, r) can be replaced by ?. iNloreover, within the context of a
subexpression in the definition of f*(x, y, r), the computation f(r) may have a specialized form. If
the subexpression has that specialized form, then it can also be replaced by ??.
Step 4. Eliminating redundant computations in the resulting definition obtained from Step 3.
This can be done using standard optimizations. In particular, since some computations depending
on x have been replaced by computations on r, part or all of parameter x may have become
redundant. Eliminating them results in a more efficient differentiated version f'(.%, y, ?) ?vhere ? is
x or the part of x that remains as a parameter.
Example. To illustrate the four?step derivation approach, we present a simple case of matrix
multiplication as an example. Let x be (C, 1?), where C and 1? are two lists of numbers. The
function mtxAiul(C, 1?) treats C as a column matrix, 1? as a row matnx, and returns the product
of the two matrices. The resulting matrix is represented as a list of rows, where each row is a list
of numbers. The auxiliary function `ro?vAiui(c, R) multiplies an element ct with each element in a
4
row I? and returns the product row. The function definitions are:
rntxfrlul(C, 1?)
rowMul(e, 1?) =
if null(C) then nil
else cons(iowAlui(car(C), II), mtxAIul(cd?( C), 1?))
if null(R) then nil
else cons(e * car(ft), rowAIul(e,cdr(R)))
(2)
Suppose r is the cached result rntxMul(C, 1?) and the new input to rntxMul, x ? y, is defined
as (C,R? ? y = (C,cons(y,1?)). We aim to compute m! AJui(C,cons(y,R)) more efficiently by
making use of r.
Step 1 considers
rnt Ai?Ll(C, cons(?, 1?)).
First, we unfold mt?AJul(C, cons( y, 1?)) siuce its arguments involve both x and y. We get
if null(C') then nil			(3)
else cons(rowAIni(ca??(C), co?is(y, R)), mtx?Iul( cd??( 0), cons( y, R))).
Then, we unfold ?owAJul(car(C),cons(y, 1?)) in (3) since its argumeuts also involve both x and y.
We get
if null(C) then nil
else cons(if null(cons(y, R)) then nil
else cons(car(C) * ca?(cons(y, II)), rowAful( car( 0), cd?(cofls(y, II)))),
mtxA'Iul(cdr(C), cons( y, R))).
(4)
Using the axioms of data types nuli(cons(h, t)) = false, ca?(cons(h, t)) = h, and cd?(cons(h, t)) =
t and specializing the false conditional expression in (4) to its false branch, we get
if null(C) then nil			(5)
else cons(cons(car(C) * `y, rowM'ul(car(C), 1?)), mtxAjul( cd7?( 0), cons(y, ft))).
The function application mtxAIul(cd?(0),cons(?, ft)) in (5) is not flirther unfolded since it is an
instance of mtA'Inl(0 cons(?j, R)), which has already been unfolded.
Step 2 defines mtxAIul?((0, 1?), y', ??) based on (5). The expression fl?txAiui(cd?(0), cons(y', 1?))
in (5) is equivalent to mtxAiui((cdr(c'), ft\) ? y). Repladng this application of mirMul with an
application of mtxMui?, we get
if null(0) then nil
else cons(cons(car(0) * y, ?owMui(cai(0). II)),
mtxMitl*( (cdi'(0), 1l?, y, mtxiliul( cdr(0), I?))),
5
(6)
which is then used as the initial definition of fl?.tx?Iu1*((C,R),y,?). Note the invariance that the
third parameter of rntxA?Iu1* is the application of mtxMul to the first parameter of mlxkiul*
Step 3 aims to use the cached result ? to compute (6) more efficiently. In particular, in the false
branch of the conditional expression, nuli(C) is false. b? this context, we specialize (2) and find
that
mtxAlul(C, 1?) cons( rowAlui(car(C), II), rn?xAIu1(cdr(C), R)). (7)
From the invariance mtxMul(C,1?) ?, We have cons(rowAlui(car(C),R), n?txAIzt1(cd?(C),J?))
= r, which implies,
rowAJul(car( C), 1?) = car( r) and mtAi%Ll( cd??( C' ) R)) = cdr( r).
After substitutions in (6) using the last two equations, we get
if nuII(C) then nil			(9)
else cons(cons(car(C) * y, car(?)), nitxA1nl?((cdr(C), R?, y,
which is a new definition of mtxAJul?((C, J??, y. r).
Step 4 eliminates redundant code in the definition (9) of mtAjul*. In particular, the parameter
1? of n?twA'Iul?((C, R?, y, r) is not used as data or for any control, except in the recursive call to
mtxMnl? itself as the corresponding argument. After eliminating it, we get a final definition
mtwA'Iul'(C, y, 7) = if null(C) then nil			(10)
else cons(cons(car((') * y, car(r)), n?tAinl'(cdr( 0), y,
Therefore, given that mtxiVlnl(C, 1?) = r, we have that n?txMnl'(C y, 7) n?t?Iul?((0, 1?), y, r)
--H mtxMnl(C, cons(y, 1?)). The function mixAjul' is a differentiated version of n?txiN4ui for the
given notion of input change. Note that it is not a complete differentiated version since 0 can not
be eliminated from (10).
Generalized Partial Evaluation. It is convenient and fruitful to view our derivation approach
as an instance of generalized partial evaluation (GPE). GPE is a semantic-based program transfor-
mation: given an expression e and an information set 1 that describes partial knowledge about e,
CPE produces a residual expression e' by specializing e using hiformation from I
The notion of GPE has appeared in [10] [37], where it was called generalized partial computa-
tion(GPC). It was originally proposed to overcome the drawbacks of conventional partial evaluation,
which only specializes programs given static values for certain arguments. The key idea of GPE
6
is to employ a theorem prover during the specialization to utilize information such as the logical
structure of programs, algebraic properties of primitive functions. and axioms for abstract data
types, etc.
Expanding the computation of f(x ? y) in Step 1 can be regarded as a special case of GPE in
which the expression e is f(z) and the information set states that is xQ)y and the cached result f(x)
is available. We call this use of GPE the onginal generalized partial evaThation (oGPE); the residual
expression of the oGPE is called the original residnal expression. In the matrix multiplication
example above, (5) is the original residual expression.
The spedalization of f(x) in a specific context in Step 3 can also be regarded as a special case
of GPE. We call this the auxiliary generalized partial evaluation (aGPE); a residnal expression of
the aGPE is called an auxiliary residual expression. For the example above, the specialization of
mtxMul(C, 1?) in the context where n'ull(C) is false is an aGPF that yields the right hand side of
(7).as an auxiliary residual expression.
In [10] and [37], GPE transformation methods for a restricted form of language (u-form) and
a lazy functional language are discussed, and small examples are given. In this paper, we see that
combining the idea of GPE transformations with other special transformation techniques results in
an effective transformation approach for deriving incremental programs.
4 Formalization of the Problem
First, we present the syntax of the simple language we use and give it a simple evaluation semantics.
Then, the derivation problem is described in terms of the language.
4.1 Language
We consider a pure first-order functional language with the following syntax.
Syntactic Domains
Va?
Con
PrirnFun
Fun
Exp
Abstract Syntax
For e E Exp,
e ::=v
c(ei, ..., en)
variables, ranged over by x, ......
constructors, ranged over by c, Co....
primitive functions, ranged over by P,Po,
functions, ranged over by f, ......
expressions, ranged over by e, e0,...
v C ??ar variable
c C (`on constructor application
7
p(ei
if e1 then e2 else e3
let v = e1 in ?2 end
p E PrimFun
f c Fun
primitive function application
function application
conditional expression
binding expression
A program is a set F of mutually recursive function definitions
 xn?) eili ? 1F1			(11)
where 1F is a finite index set satisfying 0 E 1F' The function fo with parameter W1?0 ?? the
expression to be evaluated in the context of these definitions. Note that, from this section on, J0
refers to the function for which we aim to derive a differentiated version, whereas f refers to an
arbitrary function in the set P. We assume that each v in a let expression is renamed so that it is
distinct from all other variables used in P.
A simple strict semantics for expressions can be given by semantic function t : Exp?Euv?Va1,
where Env and Val are semantic domains. In particular, constructor applications and primitive
function applications are strict. Val is the set of values, including constants and constructions.
Integers and Boolean vahies (T for true and F for false) are inchided an?ong the constants. Env is
a type-respecting mapping from variables to values. Formally, we give the semantic domains and
the semantic equations below, where D1 is the domain D extended with a value 1 that is bAow
all elements in D and v `?` d means that the variable v is bound to the value d. Sometimes, we use
as an abbreviation for [xi			d1n			dn].
Semantic Domains
Val Constants + Constructions, ranged over by d
where Constants = (Con)1,
Constructions = (Con x Va!)j + (Con x Va! x ?`?oi)i + + (Con x Vain)1 +
Fnv = Var			Va!, ranged over l)y p
Semantic Equations
p
??(c1,...,cn)? fi
p
?[if e1 then e2 else 63? p
--H p(v)
--H c(&c[ci?I?
--H p(?[ci?p,...,t??n?p)			if dj is of the right type for			off
--H uC[? p[x1			d1,..., X?			dn],
--H 1, otherwise,
where d? = &C,[[ei?p, for i = 1..n, and f is defined by f(x1			?n) =
--H ?[c2?, if d = T
--H ??e3?p, if d = F
--H I otherwise,
where d =
--H ??e2? p[v (1], if (! of the right type for v
--H 1, otherwise,
where d = ?[c1?p
??et v = e1 in ?2 end? p
4.2 Description of the Prob1en?
We are given a set F of function definitions, as in (11), and an input change operation D. The
operation D describes the change to the arguments of the function fo. It combines any tuple of
old arguments x			(x1X??1,2 and a tuple of variables y			(yi, ...,ym) to form a tuple of new
arguments x' (x'1, ..,X???? i.e., x' x 0 y. The operation D can be regarded as a tuple of n
separate single change operations Di, `..,Dn for x'1x? respectively, such that X'i x Di y for
each i 1,..., n. Each of the single change operations Di is defined in such a way that r'? is
computed as some function g? of parameters Xj'5 and Yk'5. Usually, g is a constructor application
or a primitive function application. The most typical y and D are the tuple v (viy?? and the
operation ? such that there exists a binary function g? of Xj and y?, such that ?` g?(x?, vi), for
each i --H 1 ,
Note that in order to keep our language simple, we do not include tuples as expressions.
However, tuples are used in the presentation as a notational convenience. In particular, if x
(xi,X??, y --H (vivm? D --H--H (DiDo) and x Di v is defined using a fuiiction 9i of x5,s
and Yk'5, then f0(x) is an abbreviation for fo(xiv?), f0*(r, v f0(x)) is an abbreviation for
f0*(xi, ..., X?? viYm, fo(xixn)), and r D v is an abbreviation for (x Di v o+.. X On v), where
x Di y is an abbreviation for g?(xi, .. X?, viYm)' These abbreviatioiis are used not only for
tuples of variables, but also for tuples of expressions.
We are only interested in using tlie caclied result if we can save time by doing so. Accordingly,
we must have a model that describes tlie tinie needed to compute expressions. We use T(e) to
denote the time needed to compute expression e. If r is the only free variable in an expression
e, then T(e) is described as "the tinie needed to retrieve the vaJue of e from caclied result r". If
e iii (e1, ...,e?), we use T(e) to denote the sum of the T(Cj)'5. The function T can be obtained
usmg fairly staiidard constructions [38] [27] [30]. Note that different primitive fliuctions iiiay take
different time to evaluate.
In general, given two expressions e1 and e2 that compute the saiue function of x, it is not
decidable whether e1 computes faster thau e2 for a given value of x. Therefore, we say that
T(e1) < T(e2) (or T(e1) ? T(e2)) for a giveli vaJue of x if we can effectively confirni the inequality
using heuristics for the function T. N\7e write t( ci) ? t(e2) to denote that we can effectively decide
that there exists a constant c such that for all x, T(ei) ? c.T(e2). In particular, we use t(e1) =< t(e2)
to denote that for all r, T(ei) ? T(e2). Notice that t(e1) ? t(e2) (or t(c1) ? t(e2)) is just notation
1In the following presentation we ose --Hrn' for identity.
2For sin?plicity the arity flo of fnnction fo referred to in (11) is denoted by o
9
2			Dt
3			St
4			standard optimizations
expanding fo(x ? y) to separate computations on x and y
introducing the cache parameter T
using the cache parameter
eliminating redundant code
as t itself is not defined.
As a matter of fact, we do not need to know the exact time needed to evaluate an expression.
Instead, we only care about comparing the times needed to evaluate two expressions. Therefore,
we can use heuristics to compare times. For example, if T(e) > i?(e1) + mawfT(e2),T(?3)1, then
T(e) > T(if e1 then e2 else e3). If T(?1) ? T(e2), then T(p(ei)) < T(p(e2)) for any applicable
primitive function p. In particular, if c1 is a subexpression of e2, then T(e1) < T(?2). For example,
T(ei) < T(car(cons(e1,e2))). We can also make use of the transitivities of various comparison
relations.
Given P, 0, and the time model T, we aim to apply a series of transformations to obtain a finite
set F' of function definitions ?f((x'1`??) ?`jj? E 1F'1, where 0 c TF and f01 is a differentiated
version of fo under O.
5 Formalization of the Transformations for the Derivation
In order make the formalization of the transformation approach tractable, we break it into four
steps:
step			descriptiontransformation
T
The definition of a differentiated version f0 of fo is obtained by transforming f0(x 0 u) with ?o, Dt,
and S? in turn. The final differentiated version f0, is obtained by applying standard optimizations,
especially redundant code elimination, on f0* and the other function definitions in the set F. In the
following, we discuss each step separately and argue (a) that together they preserve the semantics
of the program, and (b) that computations using tlie derived programs are at least as fast as using
the original programs. An example using the transformations is given in Section 6.
Since this formalization breaks the transformation into separate steps, it has some obvious
limitations and inefficiencies. For a characterization of this simple formalization and ideas for a
more general approach, see Section 7.
5.1 Information Sets
Section 3 introduced the GPE view of our derivation approach. GPE specializes an expression c
with respect to an information set 1. We use h?tjo to denote the domain of information sets. For
10
any I E Info, I is a set of equations whose conjunction represents the information with which an
expression is to be specialized. An equation is a pair of expressions and has type Ex1) x Exp, where
the two expressions are related by the Boolean primitive equality function. In this paper, we use
e e' to denote that e equals e' for two expressions e and e'. Usually, an iuformation set is collected
from the context of an expression. For example, let e be the expression
let v p(x) in if v < x then e1 else e2 end.
The information set for subexpression e2 in e is ?v l)(x), v < x
5.2 Underlying Logic
The key idea of GPE is to use a theorem prover to make inferences based on its logic and the
information collected about a program. ?Ve are only interested in logics that contain axioms,
inference rules, and basic formulas that are true for the language we are using. For any information
set I, let el be a Boolean-valued expression in our language that represents the information of the
set I. A logic is called an itnderlying logic [10] for our language if it is conipatibTh with the evaluation
semantics of our language, where compatibility is defined as follows:
Definition 5.1 A logic L is compatible with The evalantio?i seniantics ?of our Thnguage if and only
if, for any two inforniation sets I and I? such that the equations in I' are provable from those in I
based on the logic L, we have Vv,, ?[ei? [z vz] T ? t?ep]] [z Q] T, where 1, ...,Zk
are all the free variables in el and c1,.
In the transformations below, we assume that L0 is some fixed underlying logic of our language. In
principle, L0 can be any undedying logic, depending on the power we desire for making inferences
about our programs. b? this paper. we assume that a theorem prover based on the logic L0 is
available, and we write e H1 et to denote that a finite proof that e equals e' can be found by the
theorem prover using equations in the set I.
5.3 Step 1: Separating r and y
Step 1 specializes the function fo for arguments of the form x ffi y. The goal of this step is to expand
computations of f0(x 0 y) into computations on x and y separately in the hope that computations
on r alone can be avoided by making use of the cached result fo(x).
Step 1 unfolds function applications whose arguments involve computations on both x and y.
Conversely, function applications whose arguments depend purely on x or y are not unfolded. The
intuition behind this strategy is as follows: First, by unfolding and simplif\ing function applications
11
on arguments involving both r and y, we can hope to expose computations on x and on y sepa-
rately. Secondly, computations purely related to y are new and need to be carried out anyway. The
only purpose in unfolding such function applications would be to optimize them, but incremental-
ization, not optimization, is the subject of this paper. Thirdly, the intention in unfolding function
applications that depend only on x would be either to enable optimizations of such computations
or to help equate them with computations performed by f0(x). The former is not the subject of
this paper, as just mentioned. The latter is actually a theorem proving problem, which is not the
subject of this paper either. There is a fourth category of function applications, namely those that
depend on neither x nor y. Such computations allow a straightforward optimization, i.e. evaluation
by unfolding and simplification. However, this is a potential source of nontermination. NVe may
wish to omit such optimizations, as will be discussed later for the unfolding rule. In short, our
main concern is incrementality of Jo with respect to the new input x D y.
Step 1 is implemented by the transformation ?jo defined in Figure 1, where the type of ?? is
Exp Thfo Exp. Given an expression e ? Exp and an information set 1 c Info, Q specializes
e with respect to 1. By applying q0 to the expression f0(x ? y) and the null information set ?, we
obtain expression e0:
eo Y%[[ft?(x ? ?)? ?.			(12)
The body of function g0 consists of a set of cases conditioned on the structure of its argument
expression. The first column in Figure 1 gives a name for each case, where a description of the case
is encoded in the name:
v variable
c constructor application
I) primitive function application
f function application
if if-expression
let let-expression
Subscript i in a name indicates that subexpression i within the named construct is being reduced.
Subscript i-if or i-let indicates that the subexpression being reduced is an if or a let expression.
Subscript e indicates that an expression itself is reduced after all of its subexpressions have been
reduced. Suliscript n indicates that an expression is not further reducible. The last column gives
side conditions for the reduction rules.
The presentation of ?? is simplified by omitting detailed control structures that sequence
y0 through its argument subexpressions. Thus, we just present the case of q0 working on the
12
Name			Transformation			Condition
v			?o[[e? I
v			= c			if v v
v			= v			otherwise
Ct
Q--Ht'f
Ct?1?t
= c(ei
v			??j[p(eie?)? I
v,			= g0?v(ete??3,???e,?f,e,+1			v7t )( I
13,?,j			= ?0?f v11 then p(v1v,?l,v2,v,+1v,)
else p(v1v,?1,v3,v,+1v0)? I
= ?0?et v = v11 ill p(eiv??1 ., v,+1v,?) end? I
= ?0?Simp?[p(v1v?)?I? I
v			= p(v1v,,)
f			?o?f(v?v,,)? I
= ???f(v1v1?1 , ?0?v,'?I, v,+1v,,)? I
= ???f v11 then f(v1v,?1,v12,v,+1v,)
else f(v1v,?1 , v2, v,+1			v, )? I
f,--H1?t			= ???et v = e; in f(v1v,?1 , v2, v,+1			v,,) end? I
fv			= ?,,?v[r1 := e1x,, := v,,]? I
where! is defined as f(r1 ...,r,,) = v
fo			=f(v?v,,)
if
if1
if??q
if1 --Hlet
if2
if3
if23
let
let1
lvt1?v
lvt1?,j
?0?c(v1v,,)? I
= ?0?c(v1v,?1, ?0?v??I, v,+1v,,)? I			if v1v,?1 are irreducible. not if or let, but v, is reducible
= ?,?f e1 then v(v1v,-?1,v21,v,+1v,,)			if v1v,?1 are irreducible, not if or let, and
else c(e1v??1 , v31, v,+1v,,)? I			v is irreducible and v, is if v'1 then v21 else v2
= ?0?et v = v11 in c(v1v,?1, v21, v,+1e,,) end? I if v1v,?1 are irreducible, not if or let, and
v `s irreducible and v, is let v = v'1 in v21 end
otherwise
if v1v,?1 are irreducible, not if or let, but v, is reducible
if v1v,?1 are irreducible, not if or let, and
v, is irreducible and v, is if v1 then v21 else v21
if v1v,?1 are irreducible, not if or let, and
v, is irreducible and v, is let v = v'1 in v21 end
if v1 . . -, v? are irreducible, not if or let, but
p(v1 ..., v,,) can be simplified under I
otherwise
if v1v,?1 are irredudhle, not if or let, hut v, is redudblv
if v1 , ..v,?1 are irreducible, not if or let, and
v, 15 irreducible and v, is if v11 then v2 else
if v1v,?1 are irreducible, not if or let, and
v, is ineducible and v, is let v = v11 in v21 end
if v1v,, are irredudblv, ant if or let, but
the argument patteril is favorable and is not in the list I?
Also, put the argument pattem in the list It.
otherwise
v1 then v2 else v2? I
= ?0?f (?e?v??I) then e2 else v2? 1 if v1 is reducible
= ?0?f v11 then (if v21 then v2 else v?) else (if v21 then v2 else ?)? I
if v1 is irreducible and v? is if v11 then v21 else
= ?,?et v = v'1 in (if v21 then			v2 else v?) end? I			if v1			is irreducible and v1 is let v = v11 in v21 end
= ?0?v2? I			if v1			is irreducible and is ant if or let, and v1 ? T
= ?,?v2? I			if v1			is irreducible and is not if or let, and v1 ? F
= if v1 then Cj0?v2? (I u (v1			T)) else Cj,?v2? (Iu (v1
otherwise
lvt2??et = ?,?et v' = v1 in (let v = v21 in v? end) end? I
let2 = ?0?v2? I
let21 = let v = v1 in ?v??2? (I u (v v1)) end
?0?et v = v1 in v2 end? I
= ?0?et v = (?o?v1?I) in v2 endl I			if v1 is reducible
= ?0?v?[v := v'1? I			if v1 is irreducible and v1 is v'
= ?o?f v1 then (let v = v21 in v2 end) else (let v = v21 in v2 end)? I
if v1 is irreducible and v1 is if v11 then v2 else v2
if v1 is irreducible and v1 is let v' = v11 in v2 end
if v1 is irreducible and is not if or let, and v e1
otherwise
Figure 1: De?nition of ?v
13
ith subexpression of the top-level construct and condition it on the irrcdncibility of subexpressions
1 through ? --H 1. Operationally, when we say that subexpressions 1 through ? --H 1 are irreducible, we
mean that they are the result of having already applied Cj0 for subexpressions at those positions.
?Ve say that an expression ? is reducibTh if e is not irreducible.
The meaning of v rules are straightforward. A variable that can be shown to be equal to a
constant c under the assumptions of the given information set is replaced by c.
For a constructor application, ?o recursively reduces each argument in turn. If a reduced
argument expression is an if-expression or a let-expression, then the if or let is lifted out of the
constructor.
On a primitive function application, ?? first reduces each argument and, as iii the case of a
constructor application, lifts any if or let expressions. Then it uses the properties of the primitive
function to simplify the application. ?Ve say that a primitive function application p(e1, ...,
can be siniphfled (to e') under I if we can effectively find e' such that p(eien) 7 e' and
=< t(p(eien)). N\7e define Simp[p(ei, ...,e?)?I to be an expression e' if p(e1, ...,en) can be
simplified to e' under I but e' can not be further simplified under 1.
On a function application, Cj also first reduces each argument and, if necessary, lifts an if or a
let as in the case of a constructor application. Then, it considers whether the function application
needs to be unfolded. As this is the key point for Cj0, it will be discussed in detail bAow.
For an if-expression, Cj0 first reduces the Boolean expression. If the reduced Boolean expression
is another if or let-expression, then this if or let is lifted out of the original top-level if-expression.
Suppose the Boolean expression is reduced already and is not an if or a let-expression. Then if the
Boolean expression can be proved to be true (false) under the assumptions of the given information
set, the if structure simplifies to the true (faJse) branch alone, which is then reduced. Otherwise,
if the Boolean expression can not be proved to be true or false, the Boolean expression is left as
a residual and Cj0 reduces both the true and false branches. In this case, the assumption that the
Boolean expression equals true (false) is added into the information set for the true (false) branch
of the if-expression.
For a let-expression, ?? is similar to the case of an if-expression. It first reduces the binding
expression and, if necessary, lifts if and let-expressions. If the binding expression is reduced to
a variable, then a minor simplification is made by a variable substitutionSuppose the binding
expression is reduced already and is not an if-expression, a let-expression, or a variable. Then if the
variable v can be proved to be equal to the binding expression, then the let structure simplifies to
its body alone, which is then reduced. Otherwise. the binding is left as a residual and ?? reduces the
body of the let-expression with the information set enlarged by the binding. Recall that we assume
14
that all variables in let bindings are distinct, which guarantees the consistency of information sets.
We now return to the question of which function applications to unfold. Recall that we are
interested in unfolding function applications that depend on both the old input x and the change
parameter y.
Given an expression e, a single change operation ?j, and an information set I, we say that ? is
favorably decomposable (under I) into ej ? Cy if e depends on both r and y and we can find two
tuples of expressions, Cx and Cy, such that
x but not on
y and possibly on x, and
1) Cx depends on
2) Cy depends on
3) e ?I* Cx ?i Cy.
As a trivial but important example, if e Ci ti C2, where e1 depends on x but not on y and e2
depends on y, then e is favorably decomposable into e1 4?i C2 under any information set I.
Given the input change operation tT (ii,Wie??, we say that an expression C 15 most favorably
decomposable into Cx ?i Cy if e is favorably decomposable into Cy ?? Cy for some i and 1(Cy ?i Cy) ?
t(Cy' oj Cy') for all favorable decompositions Cy? ?,5 Cy1 of e for I 1,...,
In order to avoid unlimited unfoldings we associate an argument pattern with each function
application and unfold applications of a function at most once for each of its favorabTh argument
patterns. Consider a function application f(eiCn). Suppose that elC? have been reduced
and are not if or let-expressions. We say that f(eien) lias afrivorabTh argument patteni if at least
one of the Cj `5 either has a most favorable decomposition or depends on neither x nor y. Formally,
we associate an argument pattern (pati, ...,pctn? with the function application f(eien), where
[j]			if Cj is most favorably decomposable into Cix D5 Ciy for some 5
pat?			Cj			if Cj depends on neither x nor y
[0]			otherwise
We say that the argument pattern of a function application is favorabfr if not all of its components
are [0].
For each function f, we keep a list if of the argument patterns for which f has already been
unfolded. The unfolding rule fe of ?? unfolds an application of f if and only if its argument pattern
is favorable and does not occur in the list ij. Note that this is merely one of many possible unfolding
strategies; a discussion of unfolding strategies appears in Section 7.
The unfolding rule is the only possible source of nontermination. We can guarantee that q0 al-
ways terminates by forbidding the unfolding of flinction applications caused by arguments that
depend on neither x nor y, i.e., we could define pat to be [5] if Cj is most favorably decomposable
15
into C?x ?j ej? and [0] otherwise. For this notion of favorable argument pattern, each function has
only a fixed number of favorable argument patterns, so termination is assured. This choice omits
the class of straightforward optimization evalijation by unfolding and simplification. Of course,
allowing such unfoldings coupled with some heuristics to prevent divergence could be an effective
implementation strategy.
We can prove the following proposition by an induction on the structure of expressions, following
the ?? rules, and making use of the fact that the underlying logic is compatible with the evaluation
semantics of our language.
Proposition 5.2 For any expression e and information set I of e, let 1,..., Zk be all The free
variables in e ande1. If?0[e]]I tenninates, then, Vvz, if?[ei? [z?vz] T, thenVv, ?[e]] [z>?vz] 1=
v ? ?[[?0?e?I]] [? H Vz] ?= v and t(?0[e]]I) ?
Therefore, if the application of Cj0 on f0(x Q y) terminates and we get Co ?0?f0(x Q) y)]] ?, then
we have the following corollary.
Corollary 5.3 If ?0[f0(x ? y)? ? terminates with e0 y%[f0(x % y)? ? Then we have, Vv?, v,,, v,
C[f0(x ? y)]] [x			Vx, Y'" v,,] j--H v ? ?[e0? [x			v1, y			v,,] t= v
and t(e0) < t(fo(x 0
5.4 Step 2: Introducing the cached-resuit parameter r
Step 2 defines the function fS such that fj(x, y. r) computes f0(x 0 y) when r is the cached result
f0(x). The extra parameter r is introduced as an explicit name for the cached result f0(x). Our mo-
tivation for introducing r is so that, in a later step, some computations performed by f0(x 0 y) may
be replaced by expressions involving the cached result r provided that such expressions compute
the same values and are at least as fast as doing the original computations.
We define
f0(x, y r) e			(13)
where e* is a transformed version of C0. The transformation of e involves replacing some calls f0(e)
with recursive calls fo*(Cx, C,,, fo(Cx)), where Cx and e,, are a definition candidate pair for e, defined
below, such that Cx 0 e,, is equivalent to e. Note that this transformation preserves the invariant
that the third argument to fS is ahvays fo applied to the first argument of f0*. Also note that, in
16
the body of Jo* as defined in this step, parameter ? is not used in any substantive way; it will be
used by Step 3 to replace, in the body of j??, some computations on x by expressions involving r.
The transformation of e0 into e* is implemented by Dt, which has type Exp Info Exp.
Expression e*, the body of function j??, is obtained by applying Dt to e0 and the null information
set ?:
Dt?e0? ?.			(14)
Figure 2 defines Dt. The names of rules have the same meaning as for the Cj0 transformation, with
the addition that the subscript 5 indicates substitution of a function application.
Condtjon
Name			Transformation
v			Dtlv? I			=0
v			Dtlc(eie?)? I			= c(Dtlei)IDtle,?lI)
p			Dt?[p(eien)) I			= p(DtleillDtlen)I)
fs			Vt?f(eien)? I			= f;(e?,c?,J(e?)) if J Jo and (e?,e?) is adefinitioncandidatepah'for f(e?on)
Jn			= f(Dt?o?lIDtlenll) otherwise
if			Dtlif e1 then e2 else 03? I if VtleilI then Dtlo2l (lulei T)) else Dtle?l (IU ?vi F))
let			Dtlletv= e1 in e2			end) I = let v `tIcill in Vtle2l (Iu4u?c?)) end
Figure 2: Definition of Dt
All rules other than those dealing with function applications are straightforward. They just
collect and pass on information sets for the expressions being transformed. If there is no fuiiction
call to Jo in e0, then e* e0.
Consider a (recursive) function apphcation f0(e1, ..., en) in the expression Co with the collected
information I. Let e (eiC??. If there exist a pair of tuples e1. and e such that Ci is favorably
decomposable into Cx ?iCo under I for each i 1n and t(Cv Q e?) ? t(e), then we call (Cx,e??
a definition candidate pair for fo(e), and replace the occurrence of f0(e) with fS(ex, Co, fo(ew)).
Function fo? is not necessarily a differentiated version of Jo because, although transformation
Dt preserves semantics, it may actually result in a slower program. To compare the time of e
and Co, consider a function application fj(Cx, C?, f0(e1)) ill C* that replaces function application
f0(e) inc0. The fact that (ex,eo? is a definition candidate pair for fo(e) guarantees that computing
Cx and e0 is at least as fast as computing C. However, fo(ex) may need a substantiJ amount of
time to compute and hence transformation Dt produces a slower program. This apparent step
17
backwards is remedied in Step 3, whi4? restores fs(ex, Cy, fo(ex)) to fo(e) nuless it can be replaced
by f0*(ex, e?, er), where Cr computes fo(ex) rapidly using the cached value r and f0*(ex, e?, fo(ex))
can compute at least as fast as fo(e) by making use of e?
Note that, among various heunstics that can be used to find a definition candidate pair for f(e)
under information I, there are two special cases that are most useful:
1.			If there exists a right-reverse operation H? of ? such that y			a x iff x Q y --H __ and e 0 x
can be simplified element-wise under 1 to form Cy such that t(x 0 e?) <= t(e), then (x,e?? is
a definition candidate pair for fo(e). In this case, transformation `Pt may replace f0(e) by
f0*(x, Cy, f0(x)), and Step 3 can subsequently replace fo(r) by the cached result r.
2.			If there exists a left-reverse operation 0 of 0 such that x			? y iff v ? g --H z and e ? y
can be simplified dement-wise under 1 to form Cx sud? that er does not depend on y and
t(ex0y) <? t(e), then (ex, y? is a definition candidate pair for fo(e). b? this case, transformation
D? may replace fo(e) by fO(ex,y',f0(ex)).
For the transformation Dt described above, we have the foliowing proposition:
Proposition 5.4 With the fzLnction definition fs(x, y, ?) e?, we have Vvx, v?, V1, V2
?[e0? [x `" vx, y			vy] I vi A t'?e? [x >--H> Vx, Y			vy] I--H v2 ? v1			v2.
5.5 Cache sets
We would like to find, in the computatioll of f0(x 0 y) performed by f0(x, g. `r) e*, expressions
whose values can be retrieved quickly from the cached result r. Of course, literal occurrences of the
subexpression f0(x) in e* can be replaced by r. But we aim to locate many other opportunities to
use the cached result r. For example,
o+ Expressions that are provably equal to but not identical to fo( x) can be replaced by r.
o+ If f0(x) is provably equal to g(h(x)) and g has an inverse g?' sud? that t(g--H1(?)) ? t(h(x))
for fo(?) r, then any expressions provably equal to h(r) can be replaced by g--H'(?).
Such equalities need not hold globally throughout e*. Rather, they only need to hold in the local
context of the expression that is a candidate for replacement.
For e being a subexpression of e*, let Te be the information set at e, say as computed by Step
1 or 2. We associate a cache set Ce with e. We use Cache to denote the domain of cache sets. For
any Ce E Cache, Ce is a set of expression pairs (e', r'? such that,
18
1) e' ?? r', and
2) r is the only free variable of r'
In general, the expression pairs in Cc may have no relation to e other than their validity with respect
to le. Note that, although all pairs (e', r'? in Cc satisfy 1) and 2) above, Cc is not necessarily a
complete set of such pairs. The computation of Cc will be given in Step 3, where a cache set is
collected for the expression e and is then used to determine whether e can be replaced by a use of
the cached result r.
For any subexpression e of ??, r' is called a substitution candidate for e iff
1) ?e', e H*1 e' and (c', r) ? Cc, and
2) t(r') <
We use e HI*C r' to denote that r' is a substitution candidate for e and t(r') ? t(r") for all
substitution candidates ?? of e that we can find.
5.6 Step 3: Using the Cache
We are now ready to redefine function fS so that it makes use of the cached-result parameter `r.
Step 2 defined fJ by %?(r, y, r) e*. We now redefine
%(x, y, r)			et
where et is derived from e by transformation S?:
(15)
et			St[e?? () ?(fo(x) ???,			(16)
and St has type Exp Info Cache Exp. For each subexpression e of e*, St collects the
information set 1c from the context of e, computes the cache set C?, and, where possible, substitutes
e with its fastest substitution candidate.
Figure 3 defines St. The first column gives a name for each rule. The subscripts of rule names
have the same significance as those for (j0. The subscript r corresponds to a rule that does a direct
substitution using the cached result. The subscript rp corresponds to a rule that does a substitution
for a predicate application.
St works inductively on the structure of expressions. For each expression e, it substitutes e with
e ?*? r'. Otherwise, it examines e's subexpressions. Rule V? is the base case. Rule Cj involves
a straightforward application of St on each argument.
For a pnn?tive function application p(ei e?), if p is a predicate and p(ei, ...,e?) is predicate
substitutable by p(r'1r?'), then rule Prp replaces p(e1en) by p(r'1,?`) The formal notion
19
Nan?			Transfom?ation			Condition
v			St?? I C
v			= r?			if v
Jo
vn			= v			otherwise
St?c(eien)i I C
= c(St?ei?ICSt?en?1C)
p
J
f?p
fi,
if
if
if23
let
let
let3
if (c1e?)??0 r'
otherwise
St?p(e,ien)i I C			if p(eie,?) ??
= p(r31r?)			else if p(eie?) is predica - ubstitutable by p(r3r?) under I and C
= SimpSt?p(St?ei?1CSt?eniIC)? I C otherwise
St?f(e3e?)? I C
f(r1,rn')
= f(St?ei?1CSt?e??1C)
= St?j6(e)? I C
if f(e1e,)?10 `r
else if f(e3e?) is predicate substitutable by f(r1r?) under land C
else if f ? % or! = % and %(ei,...e?) is preferred
over the original function application J0(e)
otherwise
St?f e1 then e? else e3? I C
if if e1 then e2 else e3 ??
= if e31 then St?e??I?C? else St?e?iJ??C? otherwise
where e1 = St?iiIC, 12 = Iu fei Ti, c2 = C(C, 13), 13 = I u fei F), C3 = c(c, 13)
St?et v = e3 in e2 end? I 0
if let v = e1 in e2 end			v'
= let v = e3 in St?e?? 12 C'3 end otherwise
where e3' = St?ii1C, 13 = Iu fv			e1?, C3 = c(C, 13)
simp SimpSt?p(eien)? 1 0
simp,			= Simp?(eie,,)? 10
simpn			= e
if p(eie,,) can be simplified with substitution under I and 0
otherwise
Figure 3: De?nition of St
20
of predicate substitution will be explained later, but the idea is that p( e1e?) may be replaced
by p(r'1, ..., r?') even if each e? may not be replaced by r?. For example, if sorting a list x returns
a sorted list r, i.e., sort(x) r, then although, in general, x is not equivalent to r, nuli(x) is
equivalent to null(r) and thus can be replaced by null(r). If none of the rules Pr or Prp applies,
then p? applies St straightforwardly on each argument. 5in?)St simplifies the resulting primitive
function application by making use of cache C' and simpli?er Sirnp described in Step 1. It is defined
in rule simp. Given information set 1 and cache set C, let 1? denote the set IU te r (e, r? C C'?.
We say that primitive function application p(ei, ...,e?) can be sirnplified by substitution under
I and C if p(e1, ...,e?) can be simplified under 1C; we define SimpSt[p(ei, ...,en)? I C e' if
Sirnp[[p(e1,...,e?)? I?
For a function application f(ei, ... e?), if f is a Boolean function and f ? fJ, then frp also
tries a predicate substitution as rule Prp does. If f f0*, then, as a result of Step 2, f(eie?)
f0*(e?, e?, fo(ex)) for some e? and e?. In this case, S? makes sure that the function application of fJ
that eventually appears in et can be computed at least as fast as the original function application
of fo. Formally, if er St?fo(e?)?IC, we say that fj(e?,, e?, f0(e1?)) is preferred over the original
function application fo(e) if t(f0*(e?,e?,e?)) ? t(f0(e)). Testing for such preference requires us to
compare the definitions of f(; and fo; Proposition 5.5 gives a heunstic that can always be applied
for this purpose.
Proposition 5.5 For e0 as obMined from (12), if t(e0) ? i(fo(x Q y)) and t(Cr) ? t(e) for each
fo(e) in e0 that is replaced by f0*(e?,ey,er) in et, then wiU? fJ(x,y,r) e?, we have 1(et) < t(e0)
andt(fo*(ex,e?,er)) < t(f0(e)).
This heuristic requires that the time to compute e0 be no greater than the time to compute fo(xQy)
in an absolute sense, i.e., a slowdown by a constant factor is not allowed. Since the possible
slowdown is caused by computing argument expressions more than once after function unfoldings,
we only need to guarantee that these expressions can be simplified in context so that together
they take at most the time of computing the argument expressions once. If f(;(ex e?, fo(e?)) is
preferred over the original function application f0(e), then the function application of f(; is retained
in the resulting expression et and St is applied to each argument; otherwise, the original function
application f0(e) is restored and St is applied to it. Note that function applications are not further
unfolded by S?, as all necessary unfoldings have been done by ? in Step 1.
For if and let -expressions, St applies similar ideas. It collects information from the logical
structure of the expression in the set I, enlarges the cache C' using a closure-like function C defined
21
below, and continues making substitutions in the two branches of an if-expression or the body of
a let-expression, respectively.
In order to define the notion of predicate substitution and the function C, we need the aGFE
transformation Va as a subroutine. Given an expression e' and an information set 1, Va[e'?I
specializes e' with respect to 1. The basic idea of using Va is this: given an expression e in the
context of information 1, if there is (e', r') ? C such that Va[e'?I e, then e can be replaced by r'
provided that 1(r') <
Given a primitive function application or a function application P(e1en) for some predicate
P, let land C be the information set and cache set of P(e1, ...,Cn). N\?e say that P(e1, ...,en) is
predicate substitutabTh with P(r'1,..., r?') under I and C if there are (C'j, r?') ? C' such that
1)Va[[P(e'1,...,en')?(IUtP(e1,...,en)?TY)--H?T,
Va[[P(C1C?')? (IufP(e1,en)?F))
2) P(e'1, ?.,C'?) is defined if and only if P(e1, ...,Cn) is defined,
3) t(P(r'1,...,r?')) < t(P(e1,...,en)).
and			(17)
In the matrix multiplication example of Section 3. consider null(C) in expression (9). ?Ve have
(mtx?Inl(C, 1?), r) in the caclie set, and
Va[[nuli(mtxAiul(C,R))? ?null(C) Ti T, Va?nuli(mtxAIul(C,J?))? (null(C)
since when null(C) equals T, iiitxAiul(C, I?) is specialized to nil and thus null(nitxAlul(C, 1?)
to T, and when null(C) equals P, rntAiul(C, 1?) is specialized to a cons structure and thus
null(nitxMul(C, 1?) to P. Therefore, the expression null(C?) can actually lie replaced by null(r).
The function C used in if and let rules has type Cache hifo--HCache. For any C E Cache,I c
Info, we call C(C,I) the closure of c' under I and define C(C,I) 0 u 0' u CII, where
0' ((Va[[e'?I, r") (e', r'? E
Cl' ((e'1,g--H1(r')) (e', r'? E 0 Va[e11 --H7 g(e'1 )Y.
(18)
For any (e', r') c 0, if Va specializes Cl to e11 under I, then (el', r') is added ijito 0'. If Cl' is provably
equal to 9(e'1) for some primitive function g and g has an inverse g?', then (e'1,g--H1(r')) is added
into CII. In particular, if el' c(e'1 ..., e'?) for some constructor c and c's corresponding destructors
are CT1 ,5, then (e,'.,c7'(r')) is added into 0" for i 1 n. In the matnx multiplication example
of Section 3, the expression in the false branch of expression (6) has J (null(C) PJ and
0 ((mtxAlul(C, 1?), r)J. Then 0' ((cons( rowAiul(car(C), 1?), nitAI'ul(cdr(C), 1?) ))? by (7)
22
and C" ?(?owMnI(car(C), II), car(r)?, (mtxAIul(cdr(C), 1?)), cdr(r)?? by (8). Thus, the cache
set associated with that expression would be C u 0' u 0" by (18).
From the above definitions, we see how ?a transformations are used. The goal is to help find
more expressions whose values can be retrieved from a cached result. Therefore, an unfolding
by ?? is beneficial for this purpose only if the unfolded expression can be specialized to a new
expression under the given information I. In general, the new expression can be obtained in one
of the following two ways:
1) simplification of primitive function applications using Sirnp as rule Pe in Y%;
2) specialization of if or let expressions using rules like if2 if3, or !?t2 in Cj0.
Therefore, we unfold a function application only if the unfolded expression can be simplified using
Simp or specialized to a strict subexpression of itself. Other than the unfolding rule, ?a does most
of the other transformations and simplifications in a fashion similar to ?d
Figure 4 defines Cia, whid? has type Exp Info Exp. The delinitiou of ?ja is mostLy the same
as for C?; it differs only in its treatment of function applications and let-expressions. The notion
of irreducibility for Ca is similar to irreducibility for Y%.
Name			Transformation			Condition
f			t'alf(eien)? I
= ??le[ei := e1			:= e?]? I
where J is defined by f(x1			c
let			?allet a = e1 in e2 end? I
let1?			< this case is deleted >
let2			= ??le?[a := e1? I			othenvise
all other rules are the same as those for t'?.
if e1e, are irreducible, not if or let, but
f(e?e,?) is expandable.
Figure 4: Definition of Ca
Consider a function application f(c1e?) in the context of information set I, where the ej's
are already reduced by Ca and are not if or let-expressions. Suppose ?j is the expression obtained
by unfolding f on (e1, ...,en). N\7e say that f(?i?n) is expandable by Ca if e can be simplified
by Simp under 1 or specialized to be a strict subexpression of itself under I. C0 unfolds a function
application f(e1en) if and only if it is expandable. Recall that C unfolds f(e1,e?) if and
only if its argument pattern is favorable and occurs the first time for f. Here again, the unfolding
rule fe is a potential source of nontermination.
For a let-expression, Ca applies rules let1, leti?if, iet1?1?t, let2 in turn, if possible. At the end,
instead of leaving the binding in the residual expression as Ca does, Ca replaces occurrences of each
23
defined variable v in e2 by its defining expression e1. This is merely an implementation strategy
so that, when using the cache set, we do not have to keep track of equations introduced by the
bindings of let-expressions. When a program has many let-expressions, this may cause code blow-
up. However, when a program has a lot of let-expressions, we expect that many of them can be
eliminated by the let2 rule in the context of the information collected for the ?a transformation.
We can prove the following proposition by induction on the structure of expressions:
Proposition 5.6 For any expression e and information set I of e, let 1zk be all the free
variables in e and el. If ga?e?I terminates, then we have Vw, if ?[ei? [z ` Vz] --H T then Vv,
?[[e? [z `?" vz] ? v ? ?[?a([e?I? [z vz] 1= v
Corollary 5.7 For any cache set C and inforniation set I, let zi, ..., Zk be all the free variables ?n
ci and e' and r''s for all (C,r") E C. Then we have Vv? if?[ei? [z v?? T and V(e',r'? e
??e'? [z Vz] $= ??r'? [z `,` vz] I, then V(e' r'? ? C(C, f), ?[e'? [z >? v?? --H--H ?[[r'? [z vz] I.
We redefine f0* to be f0*(x, y, r) --H et. We have the following proposition for St transformation:
Proposition 5.8 For any expression e, infoniiation set I and cache set G' of e,. let 1,,Zk be all
the free variables in e, CJ, and e' and r' `s for all (e1, r'? C C'. Let e1 iii Dt[e?I. IfSt ?e1?IC terminates
with e2 St?ei?IC, then with the definition f0*(x,y,r) et, we have Vv?, if??e1? [z?vz? T and
E C, ??e'? [z?v?] 1= ?[[r'? [z>?v?] I thenVv1,v2, cC,[[e? [z?Qj I--H viA?[e2? [z?v?] I--H--H
v2 ? v1			v2 and t(e2) < t(e)
Therefore, if the ?a transformations issued by St terminate and we get et St?e?? ? ?(fo(r), r??,
then we have the following corollary:
Corollary 5.9 If St[e?? ? ((fo(x), r?? terminates with et			St[[e?? ? ?(fo(r), r??, then with the
definition f0*(r, y, i?) et, we have VVx, `Vy, vr, v1, `?)2, f t'?[[fo(r )? [x v?] --H v_ then
?[e0? [x `" Vx, y v?] ?= v1 A ?[et? [x v?, y ` vy, r vr] ?= v2 ? v1 v2.
and t(et) < t(e0).
Finally, we have our main result, which follows directly from Corollary 5.3 and Corollary 5.9: the
semantics of the programs are preserved by the series of transformations above and computations
using the differentiated versions are at least as fast as computations using the original programs.
Theorem 5.10 If the oCPE and aUPE transformations terminate then wiU? the function defini-
tion f0*(x,y,r) --H et we have,
24
(1) VVx,Vy,VT, if?[[f0(x)? [x >--H? Vx] t--H Vr, then Vvi,v2,
?[[f0(x 0 y)? [x >--H+ Vx, Y'" vy] 1= v1 A ?[fs(x, y, r)? [x Vx, Y Vy, r vr] I--H v2 ? v1 v2,
(2) t(f0*(x, y, ? t(fo(x 0 y)).
5.7 Step 4: Redundant Code Elimination
The purpose of this last step is to optimize the function f(;(x, y, ?) --H et in the context of the set of
functions P. The optimizations mainly involve redundant code elimination. At least the following
three kinds of code may become redundant as a result of the above transformations.
First, some function definitions in P may have become irrelevant to the evaluation of f0*(x, y, r).
This is because: After f0(x 0 y) is expanded into e0 by Step 1, fC with ? is introduced in Step
2 to form e* and then used in Step 3 to replace some expressions in e* to form et. The replaced
expressions may be function applications. If all calls to a function are replaced, then the definition
of the function becomes redundant. In particular, some flinction calls to the flinction fo are possibly
As a result fo may become redundant even without substitutions
replaced in Step 2 by calls to fS
in Step 3.
Second, some computations inside remaining flinctions may also have become redundant. This
is obvious. Since some expressions are replaced by calls to fS or expressions involving i?, some other
expressions whose results are used for the computations of these replaced expressions may simply
become unnecessary.
Third, some parameters of remaining functions may also have become redundant. This occurs
because some computations dependent on the parameter x are altered by the replacements in Step
3 to be dependent on the cache parameter r. Hence all or part of tlie parameter x may have become
irrelevant to the final computation.
There has been considerable work on such optimizations [1]. Standard data-flow and control-
flow analysis algorithms can be adapted to reason about the dependencies within the programs and
recognize the redundant code to be eliminated.
After optin?zatiou, we get the resulting flinction definition j01( y, r) e', where 27 (xj
1 < i1 < . < ?k < n, in the context of a set, say F' (including f4), of function definitions. f0, is
a differentiated version of fo. If the correctuess of these standard optimizations guarantees that
VVx, V2, Vr, V,
y, ?)? [x Vx, Y v2 r Vr] I--H--H v ??f?(.i, y, ?)? [x v?, y v2, v vr] I--H v
and t(f0,(x, y, v)) < t(f0*(x, y, v)), then combining this with Theorem 5.10. we have Vvx, vy, Vr, if
25
?[jb(x)? [x			Vx] I Vr, then Vv1,v2,
??f6(x ? y)? [x:: Vx, Y			vy] 1= v1 A ?([%`(x?, y, r)? [x:' Vx, Y			Vy,			vr] t--H v2 ? v1			v2,
and t(i?(?, y, r)) < t(f0(x ?
Note that the optimizations of this last step try to make the resulting function f0, depend as
little on the input x as possible by eliminating those Xi'5 with `i ? fi, ..., --H fii, .., ikY. If x can
be entirety eliminated, then ft(?? r) is a complete differentiated version of fo.
6 Example: Derivation of Insert from Sort
Suppose we are given a program for select sort consisting of the function definitions for sort, least
and rest. Sort takes a list ? of numbers and returns a sorted list r of these numbers. Let the change
in the input of sort be that an extra dernent i is added at the beginning of the list x. EormJly,
we have
function definition:
soTt(x) =			if null(x) then nil
else Jet k = teast(x)
in con8(k, ?ort(re?t(x. k))) end
lea?t(x) = if null(cdr(x)) then car(r)
else let 8 = 1ea?t(cdr(x))
in if ca?(x) < 8 then ca?(x) else 8 end
re?t(c, k) = if k = cer(x) then cdr(r)
else con?(car(x), re?t(cdr(x), k))
cached result:
8oT?(x) = T
change in input:
= cons(i, x)
We apply the series of transformations discussed in Section 5 to derive a differentiated version of
sort. li?stead of sorting the new input co??s( i x) from scratch, the derived program actually inserts
the element i into the sorted list r. Therefore, it is a complete differentiated version of sort. In
fact, the derived program is also a complete incrementj version of sort.
Step 1. Applying ?? on sort(cons(i,x)) produces the foliowing transformations. The most sub-
stantial steps are marked with ?.
?0?ort(con?(i, x))l?
--H t'0?f null(cons(i, x)) then nil
else let k = least(cons(i,x))
in cons(k, ?ort(re?t(con?(i, i), k)))
end?l
--H ?0?et k = lee?t(con?(i ?))
in con?(k, ?ort(?e?t(con?(i, x), k)))
end?l
--H ?0?[Iet k = ?o?ee?t(con?(i,x))ll
in cons(k, ?ort(re??(con?(i, x), k)))
(if3)
26
end?l			then
--H ?0?et k = ?0?f nutl(cdr(cons(i, x))) car cons 1
else let s = least(cdr(cons(i, x)))
in if car(cons(i,x)) < s then car(cons(i,x))
else s
end?l
in cons(k, sort(rest(cons(i, x), k)))
end?l
--H Q?[Iet k = ??f null(x) then i
else let s = least(x)
in if i < s then i else s
end?l
in cons(k, sort(rest(cons(i, x), k)))
end?l
--H ???et k = if null(x) then i
else let s = least(x)
in if i < s then i else 5
end
in cons(k, sort(rest(cons(i, e), k)))
end?l
--H ?0?f nvll(x) then let k = i
in cons(k, sort(rest(cons(i, x), k)))
end
else let k = let s = least(x)
in if i < s then i else s
end
in cons(k,sort(rest(cons(i,x),k)))
end?ll
--H if null(x) then ???et k = i
in cons(k, sort(rest(cons(i T) k)))
end?(null(x)
else ?0?et k = let 5 = least(x)
in if i < s then i else 5
end
in cons(k, sort(rest(cons(i, x), k)))
end?(null(x)
--H if null(x) then ???con5(i, sort(rest(cons(i,x),i)))
?(null(x)
else ?0?et 5 = least(x)
in let k = if i < s then i else s
in cons(k,sort(rest(cons(i x),k)))
end
end?(null(x)
--H if null(x) then ???cons(i. sort(rest(cons(i,x),i)))
?(nvll(x)
else let s = least(x)
in ?0?et k = if i < s then i else s
in cons(k,sort(rest(cons(i,x),k)))
end?fnull(x) F,s least(x)?
end
--H if null(x) then ?0?cons(i, sort(?0?[rest(cons(i, nil), i)
?(null(x) T?))](null(x)
else let s = least(x)
in QoWff i < s then let k = i
in cons(k, sort(rest(cons(i, r), k)))
end
else let k = s
in cons(k, sort(rest(cons(i, x), k)))
end?(null(x) F, s least(i))
end
--H if null(x) then ??(cons(i, sort(nil)?(nnll(?)
else let s = least(x)
in if i < s then ?0?et k = i
in cons(k,sort(rest(cons(i,r) k)))
end?I2
(let1)
(p?,iJ23,v?,let2,J?,if23,v?,v?)
(let1 --H,j
(if23)
(let1?v Ieti?i?t)
(let3')
(p2,f1,p2,v?,Iet1?j)
else ?0?et k = s
in cons(k, sort(rest(cons(i, x), k)))
27
end?j?
(A,i!2,i!23)
end
where 12 = ?nuU(x) F,s least(x),i < s
13 = ?null(x) F, s least(x) i < s
--H if null(?) then cons(i, nil)
else let s = least(x)
in if i < s then ?0?cons(i,sort(rest(cons(i,x),i)))? 12
else ???cons(s, sort(rest(cons(i, x), s)))? 13
end
--H if null(x) then cons(i, nil)
else let s = least(x)
in if i < s then ?0?ons(i,?ort(x))? 12
else ?0?cons(s, sort(rest(cons(i, x), s)))? 13
end
--H if null(x) then cons(i, nil)
else let s = least(x)
in if < s then cons(i, sor?(x))
else ???cons(s, sort(?0?rest(con?(i, x), s)? 13 ))? 13
end
--H if null(x) then cons(i, nil)
else let s = least(x)
in if < s then cons(i, sort(x))
else ?0?cons(s, sort(???f s = ca??(cons(i, x))
then cdr(cons(i, x))
else cons(car(cons(i, x))
?est(cdr(con?(i, x)), s))
?1l ))113
end
--H if nnll(x) then cons(i, nil)
else let s = least(x)
in if i < s then cons(i, 3ort(x))
else ?o?cons(?, sort(if s = i then x
else cons(i, ?est(r,s))))l13
end
--H if nttll(x) then cons(i, nil)
else let s = leas?(x)
in if i < s then cons(i, sort(x))
else ?0?f s = i then cons(s, 3oT?(x))
else cons(s, ?ort(con?(i ?e?t(x, 3))))l13
end
--H if nnll(x) then cons(i, nil)
else let s = least(x)
in if i < s then cons(i, sort(x))
else if s = i then cons(s, ?ort(x))
else cons(3, ?ort(con?(i, rest(i, s))))
end
(f??if2,let1??,let1??)
(f?,iJ2)
(pn,Jn,p2,J1)
(p?,?23,p?, f?,v?)
(J1--H?f'P2--H?f)
(iJ23,p?,f?,vn)
Step 2. Define sort5(x,i,?), where r sort(x), to be e0 with sort(cons(i,rest(w,s))) in e0
replaced by ?ort5 (rest(x, s), i, sort( rc-?t( w, ?))). N\7e get
sort?(x,i, ,)
--H Dt?e0l ?
--H if nnll(x) then cons(i, nil)
else let s = least(x)
in if i < s then cons(i, so?t(x))
else if s = i then cons(s, so?'t(x))
else cons(s, ?o?t?(re?t(x, 3), i, ?ort(rest(i, s))))
end
Step 3. First, we itemize here those Lj? translormations that are needed.
28
???ort(x)??nutt(x)
--H nit
?a??ort(e)j?nutt(x)
--H g??et k = tee?t(x) in cons(k, sort(rest(x, k))) end
?Inutt(x)
--H ?a?con3(tea3t(x), sort(rest(x, tee?t(x))))end
??nutt(x)
--H con3(tea?t(?), 3ort(re?t(?, teast(x))))
Then, apply the transformation S? on
I ?(?ort(x),r))
= St?f nnlt(x) then con3(i,nit)
else let s = teast(x)
in if i < s then cons(i, soTt(x))
else if s = i then cons(s, 3ort(x))
else cons(s, 3ort?(re?t(x, s), i, 3ort(te?t(r, s))))
end? I 1(3oTt(x),T)Y
= if Cond then St?on3(i,ni1)? ?nutt(x)
?(sort(x),r), (R2, ?))
else St [[let s = teast(x)
in if i < s then cons(i, sort(x))
else if s = i then con3(?, sort(x))
else con3(?, ?ort?(?e?t(x, s), i, ?o?t(re?t(x, s))))
end? ?nntt(?) F? C
where Cond = St?nutt(x)? I I(?ort(x),r)) =
C = 4(?o?t(x),r),(R3,r),(R31,car(r)).(R32,cdr(r))?
R2 = ???3oTt(x)J 4nutt(x) = nit,
R3 = ???3oTt(x)J 4nutt(x)
= cons(teast(x), ?ort(re?t(x, teast(x))))
R31 = tee?t(x), and
`?32 = 3ort(re?t(x,tea?t(x)))
= if nntt(r) then cons(i, nit)
else let s = Rst
in St?f i < s then cons(i, 3ort(x))
else if s = i then cons(s, 3oTt(x))
else cons(s, 3ort*(rett(x, s), 3o?t(te3t(?, s))))
end? I C
where Rst = St?ea?t(x)J ?nutt(x)			F) C
--H car(?)
I = fnntt(?) F, s teast(x), 3 RstY
= if nutt(r) then cons(i, nit)
else let s = car(r)
in if i < 3 then St?con3(i, ?ort(x))? (I u ? , T)) c'
else St?f 3 = i then cons(s, sort(x))
else cons(s, ?ort?(?e?t(x, s), i, 3oTt(Test(x, 3))))
? (Iu?i<3?F)) C
end
= if nutt(r) then cons(i, nit)
else let s = car(r)
in if i < ? then cons(i, r)
else if s = i then St?con3(3, ?ort(x))? (I u 13 = i T)) C
else St ?on3(3, 3ort (re3t(t?, s), i, ?o?t(re?t(x, s))))
? (I u Ii < 3 F) u Ii 3 F)) C
end
= if nutt(r) then con?(i nit)
else let 3 =
in if i < 3 then cons(i, r)
else if 3 = i then cons(s, ?)
else cons(s, ?ort?(re?t(x, s), i, cdr(r)))
(f,, if2)
(fe, if3)
(tet2,)
(pn, fn, ve)
(if23)
(pn, tet2)
(Jr)
(Pr,, if23)
(p,, f,,iJ23)
end
(p,, fr'p, f?, Jr)
et
29
Step 4. Apply standard optimizations on sort*(x, i, r) et. The fuiiction definitions sort, least,
rest, and the argument x to the function sort* are eliminated eventually.
(merge conditional branches)
sort?(x, jr)
--H if nntt(r) then cons(i, nit)
else let s = cer(r)
in if i < s then cons(i, r)
else cons(s, sort?(rest(?, s), i, cdr(r)))
end
(eliminate redundant argument x to sort to get sort?)
sort'(i, r)
--H if nutt(r) then cons(i, nit)
else let s = car(r)
in if i < s then cons(i, r)
else cons(s, sort'(i, cdr(r)))
end
(miscellaneous: let can be either saved or not)
sort'(i, r)
--H if nntt(r) then cons(i, nit)
else if i < car(r) then cons(i, r)
else cons(cer(r), sort'(i, cdr(r)))
Analysis. For x of length n, the time complexity of sort(x) is 0(n2) and thus sort(cons(?,x))
takes 0(n2) time. But sort' inserts the element i into the sorted list r in O( n) time. Thus, ?? have
obtained a linear speedup by making use of the cached result r.
7			Discussion
In our presentation, we have emphasized conveying basic ideas and exposing basic problems. At
severJ places in the transformation algonthins need to be further studied in order to make the
transformation approach efficient. Moreover effective Jgorithms are also important for achieving
a higher degree of incrementality in the derived programs, which is the main concern of this paper.
Issues related to the degree of incrementality. Informally, we say that a derived program
has a higher degree of incrementality if more of its computation is avoided by using the caclied
result. There are two main issues in the transformation approach that relate to the degree of
incrementality achievable in derived programs.
First, unfolding strategies affect the degree of incrementality that can be derived. Since unre
stricted unfoldings may lead to nonterniination, coiiditions are attached to unfolding rules. How
ever, at the same time that these conditions restrict unfoldings. they may also mask opportunities
for discovering a higher degree of incrementality. In q0, we only unfold calls to a function at most
once for each of its favorable argument patterns. Thus, some computations depending purely on x
may not be separated out in Step 1 and hence can not be replaced by their substitution candidates
in Step 3. In ?a, we only unfold function calls that are expandable. At a result, some auxiliary
30
residual expressions with substitution candidates may not be found by ?a Therefore, in both
transformations, more lenient unfolding conditions could be studied to help achieve a higher degree
of incrementality in the derived programs.
Second, fleunstics for time comparisons affect tbe effectiveness of the transformations and hence
the degree of incrementality that can be discovered. At several places in the transformations,
especially in the St transformation, we ru'i into situations where we need to decide whether 1(ei) <
1(r1) or 1(e1) < 1(r1), and if so, replace Ci with r1. A quick heuristic may simply give negative
answers to most comparisons. Thus, no replacement would occur in these situations and there
would be less use of cached results. So good timing heuristics are important for the derivation of
a higher degree of incrementality. Note, however, that a more accurate heuristic may take a long
time, making the transformation inefficient. Therefore, fast heuristics are also important for the
efficiency of the transformation.
On the other hand, these issues are of concern because the problems are intractable in the
general setting. If we give up generabty a lot of work can be done to frame the classes of domam
problems that need to be solved and/or the features of programming languages that can be used for
coding the domain problems. Then we can study efficient algorithms for these frameworks without
sacrificing the degree of incrementality that can be derived. Of course, relating this potential work
with existing work in incremental computation is itself anotber important task.
Applicability and limitation. The transformation approach presented here can only derive a
set F' of function definitions such that in the set P', f6 is a differentiated version of fo, and each
function other than fo in the original set P is either efiminated in Step 4 (if all fuiiction calls to
them are either unfolded in Step 1 or substituted out in Step 3) or kept unchanged in F'
The reason for this limitation is as follows: Basically, y0 of Step 1 naively decides whether a
function application is unfolded or not using rule fe. For any function, if rule fe does not apply
at one of its calls and this function application does not have a substitution candidate, then the
definition of this function is needed as a whole and is kept unchanged henceforth. During the whole
transformation, the function fo is derived towards its differentiated version ft under the change
0. But this is only made possible through the iiitroductioii of the function f with the application
of transformation Dt. For any function other than fo say g, if g is debued recursively and there
exists some function applications of g that do not have substitution candidates, then without an
appllcation of transformation Dj on 9, its definition has to be kept unchanged for recursive calls to
itself. In summary, the limitation of the approach above is the result of tlie naive decision about
function unfoldings by the rule fe of ?? as well as the naive separation and sequential execution of
31
the four basic steps as presented above.
Overcoming tbe limitation. Suppose we are given a flinction fo in the context of a set F
of function definitions and an input change operation ?, and we want to derive a differentiated
version f01 of fo in the context of a set P' of function definitions. In general, any function g in F may
have its differentiated versions in P' from the derivation. These differentiated versions may also
be incremental versions of g under certain change operations caused by ?. In order to obtain such
incrementality in the derived programs, we need to modif, the basic unfolding rules and combine
the four basic steps in a more organic way.
We propose the following idea of focusing and switching: During the transformation, the focus
is on the function application that is presently transformed, say the flinction is g, and the goal
is to apply the four-step transformation to this application of g. If there is no function call in
g, then, all four steps can be applied subsequently and we are done with this application of g.
Otherwise, if g has a function call at some point, say to the function h, then we first apply the
four-step transformation on the part of g before the call point to h, then we switch attention to the
application of h, which means that the goal now is to focus on this application of h and apply the
four-step transformation on it. This procedure is applied recursive? to all function calls. When
we are done with this application of h, we switch our focus back from h to ? to continue the
transformation on g. We apply the four-step transformation 011 the part of of g after the call point
to h until we meet another function call or we finish the transformation on this application of g.
Of course, we start with function J0.
To implement the above approach, we propose that the four-step transformation presented in
Section 5 be modified as follows: Associate with each function A in F a list of its differentiated
versions, initially empty. These differentiated versions are hitroduced at some calls to h that depend
on both x and y. The transformation works as follows: At a call A(c1c?) that depends on both
r and y, if we can not use any of h's differentiated versions that have previously been introduced
in A's list (in a fashion similar to the way that Dt uses its rule f3 to replace a call to f with a call
to f*), then we introduce a new function definition A for this caJI (iii a fashion similar to the way
Step 2 introduces f*), add A to the list of differentiated versions of h and proceed to transform on
the unfolded function body of this A*. Of course, more special care is needed to deal with recursive
function applications.
A thorough presentation of the focusing-and-switching technique sketched here is forthcoming.
32
8 Related Work
A comprehensive guide to the titerature on incrementj computation has appeared in [23]. Despite
the relatively diverse categories discussed in [23], most of the work can be divided into three classes,
The first class includes particular incremental algorithms that deal with particular input changes
to particular problems. Examples are incremental attribute evaluation [26] [39] [12], incremental
data-flow analysis [29] [28], incremental circuit evaluation [2], incremental shortest path problems
[22], etc. The study of dynamic algorithms [40] [8] [24] can be viewed as falling into this class.
Although efforts in this class are directed towards particular incremental algorithms, they apply to
a broad class of problems, e.g., any attribute grammar, any circuit, etc.
In the second class, rather than manualiy developing particular incremental algoritlims for par-
ticular problems, general evaluation frameworks are pursued for achieving incremental computation
automatically, e.g., incremental computation via function caching [21]. formJ program manipula-
tions like traditional partial evaluation [36] [35] [9], and incrementj computation as a program
abstraction [11], etc. Note that, when attribute grammars are used as a general description lan-
guage for applications, the attribute evaluation framework can be viewed as falling into this class
too. The characteristic of work in this class is that a general incremental evaluation model is run
for any given application program and no explicitly incremental version of the program is derived
and run autonomously by a standard evaluator. For this reason, these solutions to the incremental
computation problem for particular applications are not readily comparable with explicitly derived
incremental algorithms such as those in the first class [36] [20].
In the third class, explicitly incremental programs are derived from non-incremental programs
by formal transformation techniques such as finite differencing [18] [41]. Typically, programs are
written in very high-level languages with aggregate data structures, e.g., sets and bags, and fixed
rules are offered for transforming aggregate operations into more efficient incremental operations.
What is not provided is a method for deriving an incremental program from a non-incremental
program written in standard programming languages like Pascal or Lisp.
Our work is closest in spirit to the finite differencing techniques of the third class. The name "fi-
nite differencing" was originally given by Paige and Koenig [14] [18]. Their work generalizes Cocke's
method of strength reduction [6] and provides a convenient framework with which to implement
a host of program transformations including Earley's "iterator inversion" [7]. They develop a set
of rules for differentiating set-theoretic expressions and combine them using a chain rule to derive
inexpensive incrementA programs. Such techniques are indispensable as part of an optimizing
compiler for programs written in very high-level languages like SETL or APL [17] [5]. The APTS
33
[16] program transformation system has been developed for suCh purposes. Our technique differs
from that work in that it applies to programs written in a standard language like Lisp. In general,
such programs are written at a lower abstraction level so that a fixed set of rules for differentiating
expressions involving complex objects like sets is not sufficient. The technique we propose can be
regarded as a principle and a systematic approach. Using this approach, incrementalities can be
discovered in existing programs written in standard languages.
KIDS [32] [33] is a semiautomatic program development system that aims to derive programs
from high-level specifications, as is APTS. The system performs Jgorithm design [34], deductive
inference, program simplification, partial evaluation, finite differencing, data type refinement, etc.
Its version of finite differencing is developed for the optimization of its derived functional programs
and it has two basic operations: abstraction and simplification. Abstraction of a function F(x)
with respect to E(x) results a function F(x, c) with the invariance c E(x) and changes function
calls P(U(x)) to F(U(x), E(U(x))). Simplification uses the invanance to simplify F by replacing
occurrences of E(x) with c and, in particular, aims to compute ( U(x)) using tlie invariance
c E(x). As is pointed out in [32] [33], the real benefit of this optimization comes fiom the
potential use of c E(x) in the computation of E(U(x)). However, iio special technique is provided
except the observation that distributive laws can often be applied to E(U(x)) yielding U'((x)) and
then U'(c). Note that the essence of this optimization is to compute  (used by F) incrementally
under the change U (caused by F), which is exactly what our work is aimed at. Also note that
U(x) is not an accurate description of the change expression, which can actually have other free
variables, say y. As far as we know, KIDS has no formal notion of incremental programs of E(x)
with respect to U(x, y), as we give with our notation for f(.v) with respect to x (T) y, and, other
than the distributive laws, offers no special treatment for achieviiig incrementalities of F(U(x, y))
using c			E(x), as we do for computing f(x ? y) using r			f(x) with our transformations ?o, Dt,
St and ??. The Munich CIP project [19] has a finite differeiicing strategy similar to that of KIDS.
Each of the three classes of work discussed above emphasizes a different, although important,
aspect of incremental computation. But none can be regarded as a general model that subsumes the
others. A general model M for incremental computation would be one that, given a non-incremental
program f written in some language  and an input change F?g (which is also describable in ),
derives f', an incremental version of f under D. Such an			can be viewed as a general model that
addresses all three approaches discussed above for the following reasons: First, the development
of particular incremental algoritlims in the first class is a special case of \4 where f and t' are
fixed according to the particular problems being studied. Secondly, work in the second class can be
34
regarded as a specialization of M to deal with a special class of input change, namely, the change
operation Q that always takes an old input x and returns a new input x' with part of x retained
in x' and the rest of x' being new parameters y. Thirdly, work in the third class is exactly the
study of M where the language ` for describing the programs and the changes is limited to very
high-level languages.
Our work attacks the problem of deriving incremental programs from non-incremental programs
written in a standard programming language. It begins the study of a general model for incremental
computation along lines unique and distinct from all other approaches. Although this problem is,
in general, very hard, we have shown that effective approaches can be developed to derive efficient
incremental programs by combining particular program transformation techniques. By studying
general techniques, we aim to better understand the essence of incremental computation. We also
aim to establish a general framework in which different ideas 011 incrementaj computation can be
integrated. By specializing the general techniques to different applications, we will be able to obtain
particular incremental algorithms, particular incremental computation techniques, and particular
incremental computation languages. Their applications could include most problems discussed ill
the literature [23] on incremental computation.
References
[1] A. V. Aho, R. Sethi, and J. D. Uliman. CompiThrs, Princq?Ths, Techniques and Tools. Addison-
Wesley series in Computer Science. Addison-Wesley Publishing Company, 1986.
[2] B. Alpern, R. Hoover, B. Rosen, P. Sweeney, and K. Zadeck. Incremental evaluation of com-
putational circuits. In Proceedings of the First Annual ACAL-SLIAl Sgmposium on Discrete
Algorithnis, pages 32--H42, San Francisco, California, January 1990.
[3] R. A. Baliance, 5. L. Graham, and M. L. V. D. Vanter. The Pan language-based editing
system. ACAl Transactions on Programming Languages and Systems, 1(1):95--H127, January
1992.
[4] B. Bj?rner, A. P. Ershov, and N. D. Jones, editors. Partial EvaThation and Ajixed Compumtion.
North-Holland, 1988. Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Niixed
Computation, Gammel Avern?s, Denmark, October 1987.
[5] J. Cal and R. Paige. Program derivation by ?xed point computationScience of Computer
Programming, 11:197--H261, September 1988/89.
35
[6] J. Cocke and K. Kennedy. An algorithm for reduction of operator strength. Commun?cations
of the ACM, 20(11):850--H856, November 1977.
[7] J. Earley. High level iterators and a method for automatically designing data structure repre-
sentation. Journal of Computer Languages, 1:321--H342, 1976.
[8] D. Eppstein, Z. Galil, G. Italiano, and A. Nissenzweig. Sparsification a technique for speeding
up dynamic graph Jgorithms. In Proceedings of the 33rd Annual IEEE Symposium on FOCS,
Pittsburgh, Pennsylvania, October 1992.
[9] J. Field and T. Teitelbaum. Incremental reduction in the lambda calculus. In Proceedings of
the ACM `90 Conference on LISP and Functional Programming, pages 307--H322, 1990.
[10] Y. Futamura and K. Nogi. Generalized partial evaluation. h? Partial EvaThation and A/fixed
Computation, pages 133--H151. North-Hollaud, 1988. In [4].
[11] R. Hoover. Alphonse: Incremental computation as a programming abstraction. In Proceedings
of the ACM SICPLAN `92 Conference on PLDJ, pages 261--H272, California, June 1992.
[12] P. Lipps, U. M5ncke, M. 01k, and R. ?VilhAm. Attribute (re)evaluation in OPTRAN. Acta
Informatica, 26:213--H239, 1988.
[13] Y. A. Liu. Theoretical results on deriving incremental programs. Unpublished notes, 1992.
[14] R. Paige. Formal Differentiation: A Program SynThesis Technique, volume 7 of Computer
Science. Artificial h?telligence. UMI Research Press, Ann Arbor, Michigan, 1981. Revision of
Ph.D. Thesis - New York University, 1979.
[15] R. Paige. Transformational programming - applications to algorithms and systems. In Con-
ference Record of the 10th Annual ACAl Symposium on POPL, pages 73 87, January 1983.
[16] R. Paige. Symbolic finite differencing - part I. In Proceedings of the 3rd ESOP, pages 36--H56,
Copenhagen, Denmark, May 1990. Springer-Verlag. LNCS 432.
[17] R. Paige and F. Henglein. Mechanical translation of set theoretic problem specifications into
efficient ram code - a case study. Journal of Symbolic Computation, 4(2):207--H232, 1987.
[18] R. Paige and 5. Koenig. Finite differencing of computable expressions. A CAl Transactions on
Programming Languages and Systems, 4(3):402--H4.54, July 1982.
36
[19] H. A. Partsch. Specification and Transt'ormation of Prngrarns - A Formal Apprnach to Software
Development. Texts and Monographs in Computer 5cience. Springer-Verlag, 1990.
[20] W. Pugh. Comments on `incremental computation via partial evaluation'. Private communi-
cations, March 1991.
[21] W. Pugh and T. Teitelbaum. Incremental computation via flinction caching. In Conference
Record of the 16th Annual ACAl S?mpos?um on POPL, pages 315--H328, January 1989.
[22] G. Ramalingam and T. Reps. On the computationJ complexity of incremental algonthms.
Technical Report TR- 1033, Computer Sciences Department, University of Wisconsin,, Madi-
son, Wisconsin, August 1991.
[23] G. Ramalingam and T. Reps. A categorized bibliography on incremental computation. In
Conftrence Record of the 20th AnnualACAiSymposium on POPL pages 502--H510 Charleston,
South Carolina, January 1993.
[24] M. Ranch. Fully dynamic biconnectivity in graphs. In Proceedings of the 33rd Annual IEEE
Symposium on FOCS, pages 50 59, Pittsburgh Pennsylvania. October 1992.
[25] T. Reps and T. Teitdbaum. The Synthesizer Cenerator: A System for Constructing Language-
Based Editors. Springer-Verlag, New York, 1988.
[26] T. Reps, T. Teitelbaum, and A. Demers. Incremental context-dependent analysis for language-
based editors. ACM Transactions on Programming Languages and Systems, 5(3):449 477, July
1983.
[27] M. Rosendahl. Automatic complexity analysis. In Proceedings of the 4th International C'on-
frrence on FPCA, pages 144--H156, London, September 1989.
[28] B. Ryder, T. MaHowe, and Ni. Paull. Conditions for incremental iteration: examples and
counterexamples. Science of Computer Programming, 11(i):i 15, 1988.
[29] B. Ryder and M. Paull. h?cremental data flow analysis algorithmsAl Transactions on
Programming Languages and Systems, 10(1):1--H50, January 1988.
[30] D. Sands. Complexity analysis for a lazy higher-order language. In Proceedings of the 3rd
ESOP, pages 361--H376, Copenhagen, Denmark, May 1990. Springer-Verlag. LNCS 432.
[31] NI. Sharir. Some observations concerning formal differentiation of set theoretic expressions.
ACAl Transactions on Programming Languages and Systems, 4(2):196--H225, Apnl 1982.
37
[32] D. R. Smith. KIDS: A semiautomatic program devdopment system. IFFE Transactions on
Software Engineering, 16(9)1024--H1043, September 1990.
[33] D. R. Smith. KIDS a knowledge-based software development system. Ii? M. R. Lowry and
R. D. MacCartney, editors, Automating Software Design, chapter 19, pages 483--H514. AAAI
Press/The MIT Press, 1991. Proceedings of the Workshop on Automating Software Design,
AAAI `88.
[34] D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer
Programming, 14:305--H321, 1990.
[35] R. Sundaresh. Building incremental programs using partial evaluation. In Proceedings of the
ACM SICPLAN Symposium on PEPAL, pages 83--H93, Yale University, June 1991.
[36] R. Sundaresh and P. lludak. Incremental computation via partial evaluation. In Conference
Record of the 18th Annual ACAf Sympos?um on POPL, pages 1--H13, January 1991.
[37] A. Takano. Generalized partial computation for a lazy functional ianguage. In Proceutings of
the Symposium on PEPAI, pages 1--H11, Yale University, June 1991.
[38] B. Wegbreit. Mechanical program analysis. Commun?cations of the ACAf', 18(9):528--H538,
September 1975.
[39] D. Yeh and U. Kastens. Improvements on an incremental evajuation algorithm for ordered
attribute grammars. SIGPLAN ATotices, 23(12):45 50,1988.
[40] D. M. Yellin. Speeding up dynamic transitive closure for bounded degree graphs. Acta Infor-
matica, 30(4) :369--H384, July 1993.
[41] D. M. Yellin and R. E. Strom. INC: A language for incremental computations. ACM Trans-
actions on Programming Languages and Systems, 13(2):211--H236, Apnl 1991.
38
