Discovering Auxiliary Information for Incremental Computation

Yanhong A. Liu^{∗}  Scott D. Stoller^{†}  Tim Teitelbaum^{∗}

Department of Computer Science, Cornell University, Ithaca, New York 14853

{yanhong,stoller,tt}@cs.cornell.edu

Abstract

This paper presents program analyses and transformations that discover a general class of auxiliary information for any incremental computation problem. Combining these techniques with previous techniques for caching intermediate results, we obtain a systematic approach that transforms nonincremental programs into efficient incremental programs that use and maintain useful auxiliary information as well as useful intermediate results. The use of auxiliary information allows us to achieve a greater degree of incrementality than otherwise possible. Applications of the approach include strength reduction in optimizing compilers and finite differencing in transformational programming.

1 Introduction

Importance of incremental computation. In

essence, every program computes by fixed-point iteration, expressed as recursive functions or loops. This is why loop optimizations are so important. A loop body can be regarded as a program f parameterized by an induction variable x that is incremented on each iteration by a change operation ⊕. Efficient iterative computation relies on effective use of state, i.e., computing the result of each iteration using stored results of previous iterations. This is why strength reduction [2] and related techniques [48] are crucial for performance.

Given a program f and an input change operation ⊕, a program f′ that computes f(x ⊕ y) efficiently by using the result of the previous computation of f(x) is called an incremental version of f under ⊕. Sometimes, information other than the result of f(x) needs to be maintained and used for efficient incremental computation of f(x ⊕ y). We call a function that computes such information an extended version of f. Thus, the goal of computing loops efficiently corresponds to constructing an extended version of a program f and deriving an incremental version of the extended version under an input change operation ⊕.

In general, incremental computation aims to solve a problem on a sequence of inputs that differ only slightly from one another, making use of the previously computed output in computing a new output, instead of computing the new output from scratch. Incremental computation is a fundamental issue relevant throughout computer software, e.g., optimizing compilers [1, 2, 15, 20, 60], transformational program development [7, 17, 47, 49, 59], and interactive systems [4, 5, 9, 19, 27, 33, 53, 54]. Numerous techniques for incremental computation have been developed, e.g., [2, 3, 22, 28, 29, 30, 41, 48, 51, 52, 55, 58, 61, 64].

Deriving incremental programs. We are enga-

ged in an ambitious effort to derive incremental extended programs automatically (or semi-automatically) from nonincremental programs written in standard programming languages. This approach contrasts with many other approaches that aim to evaluate non-incremental programs incrementally. We have partitioned the problem (thus far) into three subproblems:

• P1. Exploiting the result, i.e., the return value, of f(x).

• P2. Caching, maintaining, and exploiting intermediate results of the computation f(x).

• P3. Discovering, computing, maintaining, and exploiting auxiliary information about x, i.e., information not computed by f(x).

Our current approaches to problems P1 and P2 are described in [41] and [40], respectively. In this paper, we address issue P3 for the first time and contribute:

• A novel proposal for finding auxiliary information.

• A comprehensive methodology for deriving incremental programs that addresses all three subproblems.

Some approaches to incremental computation have exploited specific kinds of auxiliary information, e.g., auxiliary arithmetic associated with some classical strength-reduction rules [2], dynamic mappings maintained by finite differencing rules for aggregate primitives in SETL [48] and INC [64], and auxiliary data structures for problems with certain properties like stable decomposition [52]. However, until now, systematic discovery of auxiliary information for arbitrary programs has been a subject completely open for study.

∗The author gratefully acknowledges the support of the Office of Naval Research under contract No. N00014-92-J-1973.

†Supported in part by NSF/DARPA Grant No. CCR-9014363, NASA/DARPA Grant NAG-2-893, and AFOSR Grant F49620-94-1-0198. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not reflect the views of these agencies.

*********************************************** Appears in Proceedings of POPL’96: the 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, January 21-24, 1996.

Auxiliary information is, by definition, useful information about x that is not computed by f(x). Where, then, can one find it? The key insight of our proposal is:

A. Consider, as candidate auxiliary information for f, all intermediate computations of an incremental version of f that depend only on x; such an incremental version can be obtained using some techniques we developed for solving P1 and P2.^{1}

How can one discover which pieces of candidate auxiliary information are useful and how they can be used? We propose:

B. Extend f with all candidate auxiliary information, then apply some techniques used in our methods for P1 and P2 to obtain an extended version and an incremental extended version that together compute, exploit, and maintain only useful intermediate results and useful auxiliary information.

Thus, on the one hand, one can regard the method for P3 in this paper as an extension to methods for P1 and P2. On the other hand, one can regard methods for P1 and P2 (suitably revised for their different applications here) as aids for solving P3. The modular components complement one another to form a comprehensive principled approach for incremental computation and therefore also for efficient iterative computation generally. Although the entire approach seems complex, each module or step is simple.

We summarize here the essence of our methods:

P1. In [41], we gave a systematic transformational approach for deriving an incremental version f′ of a program f under an input change ⊕. The basic idea is to identify in the computation of f(x⊕y) those subcomputations that are also performed in the computation of f(x) and whose values can be retrieved from the cached result r of f(x). The computation of f(x⊕y) is symbolically transformed to avoid reperforming these subcomputations by replacing them with corresponding retrievals. This efficient way of computing f(x ⊕ y) is captured in the definition of f′(x, y, r).

P2. In [40], we gave a method, called cache-and-prune, for statically transforming programs to cache all intermediate results useful for incremental computation. The basic idea is to (I) extend the program f to a program f̄ that returns all intermediate results, (II) incrementalize the program f̄ under ⊕ to obtain an incremental version f̄′ of f̄ using our method for P1, and (III) analyze the dependencies in f̄′, then prune the extended program f̄ to a program f̂ that returns only the useful intermediate results, and prune the program f̄′ to obtain a program f̂′ that incrementally maintains only the useful intermediate results.

P3. This paper presents a two-phase method that discovers a general class of auxiliary information for any incremental computation problem. The two phases correspond to A and B above. For Phase A, we have developed an embedding analysis that helps avoid including redundant information in an extended version, and we have exploited a forward dependence analysis that helps identify candidate auxiliary information. All the program analyses and transformations used in this method are combined with considerations for caching intermediate results, so we obtain incremental extended programs that exploit and maintain intermediate results as well as auxiliary information.

We illustrate our approach by applying it to problems in list processing, VLSI design, and graph algorithms.

The rest of this paper is organized as follows. Section 2 formulates the problem. Section 3 discusses discovering candidate auxiliary information. Section 4 describes how candidate auxiliary information is used. Two examples are given in Section 6. Finally, we discuss related work and conclude in Section 7.

2 Formulating the problem

We use a simple first-order functional programming language, with expressions given by the following grammar:

e ::= v  variable
| c(e_{1}, ..., e_{n})  constructor application
| p(e_{1}, ..., e_{n})  primitive function application
| f(e_{1}, ..., e_{n})  function application
| if e_{1} then e_{2} else e_{3} conditional expression
| let v = e_{1} in e_{2}  binding expression

A program is a set F of mutually recursive function definitions of the form

f(v_{1}, ..., v_{n}) = e  (1)

and a function f_{0} that is to be evaluated with some input x = ⟨x_{1}, ..., x_{n}⟩. Figure 1 gives some example definitions. The semantics of the language is strict.

An input change operation ⊕ to a function f_{0} combines an old input x = ⟨x_{1}, ..., x_{n}⟩ and a change y = ⟨y_{1}, ..., y_{m}⟩ to form a new input x′ = ⟨x′_{1}, ..., x′_{n}⟩ = x ⊕ y, where each x′_{i} is some function of x_{j}’s and y_{k}’s. For example, an input change operation to the function cmp of Figure 1 may be defined by x′ = x ⊕ y = cons(y, x).

We use an asymptotic cost model for measuring time complexity and write t(f(v_{1}, ..., v_{n})) to denote the asymptotic time of computing f(v_{1}, ..., v_{n}). Thus, assuming all primitive functions take constant time, it is sufficient to consider only the values of function applications as candidate information to cache. Of course, maintaining extra information takes extra space. Our primary goal is to improve the asymptotic running time of the incremental computation. We attempt to save space by maintaining only information useful for achieving this.

Given a program f_{0} and an input change operation ⊕, we use the approach in [41] to derive an incremental version f′_{0} of f_{0} under ⊕, such that, if f_{0}(x) = r, then whenever f_{0}(x ⊕ y) returns a value, f′_{0}(x, y, r) returns the same value and is asymptotically at least as fast.^{2} For example, for the function sum of Figure 1 and input change operation x ⊕ y = cons(y, x), the function sum′ in Figure 2 is derived.

f_{0}(⟨x_{1}, ..., x_{n}⟩ ⊕ ⟨y_{1}, ..., y_{m}⟩), f0^{′}(x, y, r) abbreviates f0^{′}(x_{1}, ..., x_{n},

1We use techniques developed for solving P1 and P2, instead of just P1, so that the candidate auxiliary information includes auxiliary information useful for efficiently maintaining the intermediate results.

2While f_{0}(x) abbreviates f_{0}(x_{1}, ..., x_{n}), and f_{0}(x⊕y) abbreviates y_{1}, ..., y_{m}, r). Note that some of the parameters of f0^{′} may be dead and eliminated [41].

cmp(x) = sum(odd(x)) ≤ prod(even(x)) — compare sum of odd and product of even positions of list x

o d d (x) = if null(x) then nil

else cons(car(x), even(cdr(x)))

even(x) = if null(x) then nil

else odd(cdr(x))

sum(x) = if null(x) then 0

else car(x) + sum(cdr(x))

prod(x) = if null(x) then 1 else car(x) ∗ prod(cdr(x))

Figure 1: Example function definitions

In order to use also intermediate results of f_{0}(x) to compute f_{0}(x⊕y) possibly faster, we use the approach in [40] to cache useful intermediate results of f_{0} and obtain a program that incrementally computes the return value and maintains these intermediate results. For example, for the function cmp of Figure 1 and input change operation x ⊕ ⟨y_{1}, y_{2}⟩ = cons(y_{1}, cons(y_{2}, x)), the intermediate results sum(odd(x)) and prod(even(x)) are cached, and the functions ĉmp and ĉmp′ in Figure 2 are obtained.

However, auxiliary information other than the intermediate results of f_{0}(x) is sometimes needed to compute f_{0}(x⊕y) quickly. For example, for the function cmp of Figure 1 and input change operation x ⊕ y = cons(y, x), the values of sum(even(x)) and prod(odd(x)) are crucial for computing cmp(cons(y, x)) incrementally but are not computed in cmp(x). Using the method in this paper, we can derive the functions c̃mp and c̃mp′ in Figure 2 that compute these pieces of auxiliary information, use them in computing cmp(cons(y, x)), and maintain them as well. c̃mp′ computes incrementally using only O(1) time. We use this example as a running example.

Notation. We use <> to construct tuples that bundle intermediate results and auxiliary information with the original return value of a function. The selector nth returns the nth element of such a tuple.

We use x to denote the previous input to f_{0}; r, the cached result of f_{0}(x); y, the input change parameter; x′, the new input x ⊕ y; and f′_{0}, an incremental version of f_{0} under ⊕. We let f̄_{0} return all intermediate results of f_{0}, and let f̌_{0} return candidate auxiliary information for f_{0} under ⊕. We use ¯ ; ˇf_{0} to denote a function that returns all intermediate results and candidate auxiliary information; ¯ ; ř, the cached result of ¯ ; ˇf_{0}(x); and ¯ ; ˇf_{0}′, an incremental version of ¯ ; ˇf_{0} under ⊕. Finally, we use f̃_{0} to denote a function that returns only the useful intermediate results and auxiliary information; r̃, the cached result of f̃_{0}(x); and f̃_{0}′, a function that incrementally maintains only the useful intermediate results and auxiliary information. Note that (useful) intermediate results include the original return value. Figure 3 summarizes the notation.

3 Phase A: Discovering candidate auxiliary information

Auxiliary information is, by definition, useful information not computed by the original program f_{0}, so it can not be obtained directly from f_{0}. However, auxiliary information is information depending only on x that can speed up the comfunction return value denoted as

incremental function

f_{0}  original value  r  f′_{0}
f̄_{0}  all i.r.  r̄
f̌_{0}  candidate a.i.
¯ ; ˇf_{0}  all i.r. & candidate a.i.  ¯ ; ř  ¯ ; ˇf_{0}′
f̃_{0}  useful i.r. & useful a.i.  r̃  f̃_{0}′

Figure 3: Notation

putation of f_{0}(x ⊕ y). Seeking to obtain such information systematically, we come to the idea that when computing f_{0}(x ⊕ y), for example in the manner of f′_{0}(x, y, r), there are often subcomputations that depend only on x and r, but not on y, and whose values can not be retrieved from the return value or intermediate results of f_{0}(x). If the values of these subcomputations were available, then we could perhaps make f′_{0} faster.

To obtain such candidate auxiliary information, the basic idea is to transform f_{0}(x ⊕ y) as for incrementalization and to collect subcomputations in the transformed f_{0}(x⊕y) that depend only on x and whose values can not be retrieved from the return value or intermediate results of f_{0}(x). Note that computing intermediate results of f_{0}(x) incrementally, with their corresponding auxiliary information, is often crucial for efficient incremental computation. Thus, we modify the basic idea just described so that it starts with f̄_{0}(x ⊕ y) instead of f_{0}(x ⊕ y).

Phase A has three steps. Step 1 extends f_{0} to a function f̄_{0} that caches all intermediate results. Step 2 transforms f̄_{0}(x⊕y) into a function f̄_{0}^{‵} that exposes candidate auxiliary information. Step 3 constructs a function f̌_{0} that computes only the candidate auxiliary information in f̄_{0}^{‵}.

3.1 Step A.1: Caching all intermediate results

Extending f_{0} to cache all intermediate results uses the transformations in Stage I of [40]. It first performs a straightforward extension transformation to embed all intermediate results in the final return value and then performs administrative simplifications.

Certain improvements to the extension transformation are suggested, although not given, in [40] to avoid caching redundant intermediate results, i.e., values of function applications that are already embedded in the values of their enclosing computations, since these omitted values can be re-If sum(x) = r, then sum′(y, r) = sum(cons(y, x)). For x of length n, sum′(y, r) takes time O(1);

sum(cons(y, x)) takes time O(n).

cmp(x) = 1st(ĉmp(x)). For x of length n, ĉmp(x) takes time O(n);

cmp(x) takes time O(n).

If ĉmp(x) = r̂, then ĉmp′(y_{1}, y_{2}, r̂) = ĉmp(cons(y_{1}, cons(y_{2}, x))). For x of length n, ĉmp′(y_{1}, y_{2}, r̂) takes time O(1);

ĉmp(cons(y_{1}, cons(y_{2}, x))) takes time O(n).

cmp(x) = 1st(c̃mp(x)). For x of length n, c̃mp(x) takes time O(n);

cmp(x) takes time O(n).

If c̃mp(x) = r̃, then c̃mp′(y, r̃) = c̃mp(cons(y, x)). For x of length n, c̃mp′(y, r̃) takes time O(1);

c̃mp(cons(y, x)) takes time O(n).

| \begin{matrix}sum′(y, r) & = & y + r \\ ĉmp(x) & = & let v_{1} = sum(odd(x)) in let v_{2} = prod(even(x)) in < v_{1} ≤ v_{2}, v_{1}, v_{2} > \\ ĉmp′(y_{1}, y_{2}, r̂) & = & let v_{1} = y_{1} + 2nd(r̂) in let v_{2} = y_{2} ∗ 3rd(r̂) in < v_{1} ≤ v_{2}, v_{1}, v_{2} > \\ c̃mp(x) & = & let v_{1} = odd(x) in let u_{1} = sum(v_{1}) in let v_{2} = even(x) in let u_{2} = prod(v_{2}) in <u_{1} ≤ u_{2}, u_{1}, u_{2}, sum(v_{2}), prod(v_{1})> \\ c̃mp′(y, r̃) & = & <\begin{matrix}y+4th(r̃) ≤ 5th(r̃), \\ y+4th(r̃), 5th(r̃), 2nd(r̃), y∗3rd(r̃)> \end{matrix} \end{matrix}

Figure 2: Resulting function definitions

trieved from the results of the enclosing applications. These improvements are more important for discovering auxiliary information, since the resulting program should be much simpler and therefore easier to treat in subsequent analyses and transformations. These improvements also benefit the modified version of this extension transformation used in Step A.3.

We first briefly describe the extension transformation in [40]; then, we describe an embedding analysis that leads to the desired improvements to the extension transformation.

Extension transformation. Basically, for each func-

tion definition f(v_{1}, ..., v_{n}) = e, we construct a function definition

f̄(v_{1}, ..., v_{n}) = Ext[[e]]  (2)

where Ext[[e]] extends an expression e to return the values of all function calls made in computing e, i.e., it considers subexpressions of e in applicative and left-to-right order, introduces bindings that name the results of function calls, builds up tuples of these values together with the values of the original subexpressions, and passes these values from subcomputations to enclosing computations.

The definition of Ext is given in Figure 4. We assume that each introduced binding uses a fresh variable name. For a constructed tuple <>, while we use 1st to return the first element, which is the original return value, we use rst to return a tuple of the remaining elements, which are the corresponding intermediate results here. We use an infix operation @ to concatenate two tuples. For transforming a conditional expression, the transformation Pad[[e]] generates a tuple of ’s of length equal to the number of the function applications in e, where is a dummy constant that just occupies a spot. The length of the tuple generated by Pad[[e]] can easily be determined statically. The use of Pad ensures that each possible intermediate result appears in a fixed position independent of value of the Boolean expression.

Administrative simplifications are performed on the resulting functions to simplify tuple operations for passing intermediate results, unwind binding expressions that become unnecessary as a result of simplifying their subexpressions, and lift bindings out of enclosing expressions whenever possible to enhance readability.

The following improvements can be made to the above brute-force caching of all intermediate results. First, before applying the extension transformation, common subcomputations in both branches of a conditional expression are lifted out of the conditional. This simplifies programs in general. For caching all intermediate results, this lifting saves the extension transformation from caching values of common subcomputations at different positions in different branches, which makes it easier to reason about using these values for incremental computation. The same effect can be achieved by explicitly allocating, for values of common subcomputations in different branches, the same slot in each corresponding branch.

Next, we concentrate on major improvements. These improvements are based on an embedding analysis.

Embedding analysis. First, we compute embedding relations. We use Mf(f, i) to indicate whether the value of v_{i} is embedded in the value of f(v_{1}, ..., v_{n}), and we use Me(e, v) to indicate whether the value of variable v is embedded in the value of expression e. These relations must satisfy the following safety requirements:

if Mf(f, i) = true, then there exists an expression f_{i}^{−1}

such that, if u = f(v_{1}, ..., v_{n}), then v_{i} = f_{i}^{−1}(u)

if Me(e, v) = true, then there exists an expression e_{v}^{−1}

such that, if u = e, then v = e_{v}^{−1}(u)

(3)

For each function definition f(v_{1}, ..., v_{n}) = e_{f}, we define Mf(f, i) = Me(e_{f} , v_{i}), and we define Me recursively as in Figure 5. For a primitive function p, ∃p_{i}^{−1} denotes true if p has an inverse for the ith argument, and false otherwise. For a conditional expression, if_{e_{2}e_{3}}^{e_{1}} denotes true if the value of e_{1} can be determined statically or inferred from the value

Ext[[v]]  = < v >
Ext[[g(e_{1}, ..., e_{n})]] where g is c or p

= let v_{1} =Ext[[e_{1}]] in ... let v_{n} =Ext[[e_{n}]] in

< g(1st(v_{1}), ..., 1st(v_{n})) > @ rst(v_{1}) @ ... @ rst(v_{n})

Ext[[f(e_{1}, ..., e_{n})]] = let v_{1} =Ext[[e_{1}]] in ... let v_{n} =Ext[[e_{n}]] in

let v =f̄(1st(v_{1}), ..., 1st(v_{n})) in

< 1st(v) > @ rst(v_{1}) @ ... @ rst(v_{n}) @ < v >

Ext[[if e_{1} then e_{2} else e_{3}]]

= let v_{1} =Ext[[e_{1}]] in

if 1st(v_{1}) \begin{matrix}then & \begin{matrix}let v_{2} =Ext[[e_{2}]] in \\ < 1st(v_{2}) > @ rst(v_{1}) @ rst(v_{2}) @ Pad[[e_{3}]] \end{matrix} \\ else & \begin{matrix}let v_{3} =Ext[[e_{3}]] in \\ < 1st(v_{3}) > @ rst(v_{1}) @ Pad[[e_{2}]] @ rst(v_{3}) \end{matrix} \end{matrix}

Ext[[let v =e_{1} in e_{2}]]

= let v_{1} =Ext[[e_{1}]] in

let v =1st(v_{1}) in \begin{matrix}let v_{2} =Ext[[e_{2}]] in \\ < 1st(v_{2}) > @ rst(v_{1}) @ rst(v_{2}) \end{matrix}

Figure 4: Definition of Ext

Me(u, v)  = \{ \begin{matrix}true & if v = u \\ false & otherwise \end{matrix}
Me(c(e_{1}, ..., e_{n}), v)  = Me(e_{1}, v) ∨ ... ∨ Me(e_{n}, v)
Me(p(e_{1}, ..., e_{n}), v)  = (∃p_{1}^{−1} ∧ Me(e_{1}, v)) ∨ ... ∨ (∃p_{n}^{−1} ∧ Me(e_{n}, v))
Me(f(e_{1}, ..., e_{n}), v)  = (Mf(f, 1) ∧ Me(e_{1}, v)) ∨ ... ∨ (Mf(f, n) ∧ Me(e_{n}, v))
Me(if e_{1} then e_{2} else e_{3}, v) = if_{e_{2}e_{3}}^{e_{1}} ∧ (e_{1} ⊢Me(e_{2}, v)) ∧ (e_{1} ⊢Me(e_{3}, v))
Me(let u = e_{1} in e_{2}, v)  = Me(e_{2}, v) ∨ (Me(e_{1}, v) ∧ Me(e_{2}, u))

Figure 5: Definition of Me

of if e_{1} then e_{2} else e_{3}, and false otherwise. For example, if_{e_{2}e_{3}}^{e_{1}} is true if e_{1} is T (for true) or F (for false), or if the two branches of the conditional expression return applications of different constructors. For a Boolean expression e_{1}, e_{1} ⊢ Me(e, v) means that whenever e_{1} is true, the value of v is embedded in the value of e. In order that the embedding analysis does not obviate useful caching, it considers a value to be embedded only if the value can be retrieved from the value of its immediately enclosing computation in constant time; in particular, this constraint applies to the retrievals when ∃p_{i}^{−1} or if_{e_{2}e_{3}}^{e_{1}} is true.

We can easily show by induction that the safety requirements (3) are satisfied. To compute Mf, we start with Mf(f, i) = true for every f and i and iterate using the above definitions to compute the greatest fixed point in the pointwise extension of the Boolean domain with false ⊑ true. The iteration always terminates since these definitions are monotonic and the domain is finite.

Next, we compute embedding tags. For each function definition f(v_{1}, ..., v_{n}) = e_{f}, we associate an embedding tag Mtag(e) with each subexpression e of e_{f}, indicating whether the value of e is embedded in the value of e_{f}. Mtag can be defined in a similar fashion to Me. We define Mtag(e_{f}) = true, and define the true values of Mtag for subexpressions e of e_{f} as in Figure 6; the tags of other subexpressions of e_{f} are defined to be false. These tags can be computed directly once the above embedding relations are computed. Finally, we use the embedding tags to compute, for each function f, an embedding-all property Mall(f) indicating whether all intermediate results of f are embedded in the value of f. We define, for each function f(v_{1}, ..., v_{n}) = e_{f},

Mall(f) = ⋀_{all function applications g(e_{1}, ..., e_{n}) occurring in e_{f}} Mtag(g(e_{1}, ..., e_{m})) ∧ Mall(g)

(4)

where Mtag is with respect to e_{f}. To compute Mall, we start with Mall(f) = true for all f and iterate using the definition in (4) until the greatest fixed point is reached. This fixed point exists for similar reasons as for Mf.

Improvements. The above embedding analysis is used to improve the extension transformation as follows. First, if Mall(f) = true, i.e., if all intermediate results of f are embedded in the value of f, then we do not construct an extended function for f. This makes the transformation for caching all intermediate results idempotent.

If there is a function not all of whose intermediate results are embedded in its return value, then an extended

if Mtag(c(e_{1}, ..., e_{n})) = true  then Mtag(e_{i}) = true, for i = 1..n
if Mtag(p(e_{1}, ..., e_{n})) = true  then Mtag(e_{i}) = true if ∃p_{i}^{−1}, for i = 1..n
if Mtag(f(e_{1}, ..., e_{n})) = true  then Mtag(e_{i}) = true if Mf(f, i), for i = 1..n
if Mtag(if e_{1} then e_{2} else e_{3}) = true then Mtag(e_{i}) = true if if_{e_{2}e_{3}}^{e_{1}}, for i = 1, 2, 3
if Mtag(let v =e_{1} in e_{2}) = true  then Mtag(e_{2}) = true; Mtag(e_{1}) = true if Me(e_{2}, v)

Figure 6: Definition of Mtag

function for it needs to be defined as in (2). We modify the definition of Ext[[f(e_{1}, ..., e_{n})]] as follows. If Mall(f) = true, which includes the case where f does not contain function applications, then, due to the first improvement, f is not extended, so we reference the value of f directly:

Ext[[f(e_{1}, ..., e_{n})]]

= let v_{1} =Ext[[e_{1}]] in ... let v_{n} =Ext[[e_{n}]] in let v =f(1st(v_{1}), ..., 1st(v_{n})) in < v > @ rst(v_{1}) @ ... @ rst(v_{n}) @ < v > (5)

Furthermore, if Mall(f) = true, and Mtag(f(e_{1}, ..., e_{n})) = true, i.e, the value of f(e_{1}, ..., e_{n}) is embedded in the value of its enclosing application, then we avoid caching the value of f separately:

Ext[[f(e_{1}, ..., e_{n})]]

= let v_{1} =Ext[[e_{1}]] in ... let v_{n} =Ext[[e_{n}]] in <f(1st(v_{1}), ..., 1st(v_{n}))> @ rst(v_{1}) @ ... @ rst(v_{n}) (6)

To summarize, the transformation Ext remains the same as in Figure 4 except that the rule for a function application f(e_{1}, ..., e_{n}) is replaced with the following: if Mall(f) = true and Mtag(f(e_{1}, ..., e_{n})) = true, then define Ext[[f(e_{1}, ..., e_{n})]] as in (6); else if Mall(f) = true but Mtag(f(e_{1}, ..., e_{n})) = false, then define Ext[[f(e_{1}, ..., e_{n})]] as in (5); otherwise define Ext[[f(e_{1}, ..., e_{n})]] as in Figure 4. Note that function applications f(e_{1}, ..., e_{n}) such that Mall(f) = true and Mtag(f(e_{1}, ..., e_{n})) = true should not be counted by Pad. The lengths of tuples generated by Pad can still be statically determined.

For the function cmp of Figure 1, this improved extension transformation yields the following functions:

\overline{cmp}(x) = let v_{1} = odd(x) in let u_{1} = \overline{sum}(v_{1}) in let v_{2} = even(x) in let u_{2} = \overline{prod}(v_{2}) in < 1st(u_{1}) ≤ 1st(u_{2}), v_{1}, u_{1}, v_{2}, u_{2} >

\overline{sum}(x) = if null(x) then < 0, > else \begin{matrix}let v_{1} = \overline{sum}(cdr(x)) in \\ < car(x) + 1st(v_{1}), v_{1} > \end{matrix}

\overline{prod}(x) = if null(x) then < 1, > else \begin{matrix}let v_{1} = \overline{prod}(cdr(x)) in \\ < car(x) ∗ 1st(v_{1}), v_{1} > \end{matrix}

(7)

Functions odd and even are not extended, since all their intermediate results are embedded in their return values.

3.2 Step A.2: Exposing auxiliary information by incrementalization

This step transforms f̄_{0}(x ⊕ y) to expose subcomputations depending only on x and whose values can not be retrieved from the cached result of f̄_{0}(x). It uses analyses and transformations similar to those in [41] that derive an incremental program f̄_{0}′(x, y, r̄), by expanding subcomputations of f̄_{0}(x ⊕ y) depending on both x and y and replacing those depending only on x by retrievals from r̄ when possible.

Our goal here is not to quickly retrieve values from r̄, but to find potentially useful auxiliary information, i.e., subcomputations depending on x (and r̄) but not y whose values can not be retrieved from r̄. Thus, time considerations in [41] are dropped here but are picked up after Step A.3, as discussed in Section 5.

In particular, in [41], a recursive application of a function f is replaced by an application of an incremental version f′ only if a fast retrieval from some cached result of the previous computation can be used as the argument for the parameter of f′ that corresponds to a cached result. For example, if an incremental version f′(x, y, r) is introduced to compute f(x ⊕ y) incrementally for r = f(x), then in [41], a function application f(g(x)⊕h(y)) is replaced by an application of f′ only if some fast retrieval p(r) for the value of f(g(x)) can be used as the argument for the parameter r of f′(x, y, r), in which case the application is replaced by f′(g(x), h(y), p(r)). In Step A.2 here, an application of f is replaced by an application of f′ also when a retrieval can not be found; in this case, the value needed for the cache parameter is computed directly, so for this example, the application f(g(x) ⊕ h(y)) is replaced by f′(g(x), h(y), f(g(x))). It is easy to see that, in this case, f(g(x)) becomes a piece of candidate auxiliary information.

Since the functions obtained from this step may be different from the incremental functions f′ obtained in [41], we denote them by f^{‵}.

For the function \overline{cmp} in (7) and input change operation x ⊕ y = cons(y, x), we transform the computation of \overline{cmp}(cons(y, x)), with \overline{cmp}(x) = r̄:

1. unfold \overline{cmp}(cons(y, x))

= let v_{1} = odd(cons(y, x)) in let u_{1} = \overline{sum}(v_{1}) in let v_{2} = even(cons(y, x)) in let u_{2} = \overline{prod}(v_{2}) in < \begin{matrix}1st(u_{1}) ≤ 1st(u_{2}), \\ v_{1}, u_{1}, v_{2}, u_{2} > \end{matrix}

2. unfold odd, \overline{sum}, even and simplify

= let v′_{1} = even(x) in let u′_{1} = \overline{sum}(v′_{1}) in let v_{2} = odd(x) in let u_{2} = \overline{prod}(v_{2}) in < \begin{matrix}y+1st(u′_{1}) ≤ 1st(u_{2}), \\ cons(y, v′_{1}), <y+1st(u′_{1}), u′_{1} >, v_{2}, u_{2} > \end{matrix}

3. replace applications of even and odd by retrievals

= let v′_{1} = 4th(r̄) in let u′_{1} = \overline{sum}(v′_{1}) in let v_{2} = 2nd(r̄) in let u_{2} = \overline{prod}(v_{2}) in < \begin{matrix}y+1st(u′_{1}) ≤ 1st(u_{2}), \\ cons(y, v′_{1}), <y+1st(u′_{1}), u′_{1} >, v_{2}, u_{2} > \end{matrix}

Simplification yields the following function \overline{cmp}^{‵} such that, if \overline{cmp}(x) = r̄, then \overline{cmp}^{‵}(y, r̄) = \overline{cmp}(cons(y, x)):

\overline{cmp}^{‵}(y, r̄) = let u′_{1} = \overline{sum}(4th(r̄)) in let u_{2} = \overline{prod}(2nd(r̄)) in <\begin{matrix}y+1st(u′_{1})≤1st(u_{2}), \\ cons(y, 4th(r̄)), < y+1st(u′_{1}), u′_{1} >, \\ 2nd(r̄), u_{2} > \end{matrix} (8)

3.3 Step A.3: Collecting candidate auxiliary information

This step collects candidate auxiliary information, i.e., intermediate results of f̄_{0}^{‵}(x, y, r̄) that depend only on x and r̄. It is similar to Step A.1 in that both collect intermediate results; they differ in that Step A.1 collects all intermediate results, while this step collects only those that depend only on x and r̄.

Forward dependence analysis. First, we use a

forward dependence analysis to identify subcomputations of f̄_{0}^{‵}(x, y, r̄) that depend only on x and r̄. The analysis is in the same spirit as binding-time analysis [32, 37] for partial evaluation, if we regard the arguments corresponding to x and r̄ as static and the rest as dynamic. We compute the following sets, called forward dependency sets, directly.

For each function f(v_{1}, ..., v_{n}) = e_{f}, we compute a set Σ_{f} that contains the indices of the arguments of f such that, in all uses of f, the values of these arguments depend only on x and r̄, and, for each subexpression e of e_{f}, we compute a set Σ_{[e]} that contains the free variables in e that depend only on x and r̄. The recursive definitions of these sets are given in Figure 7, where F V (e) denotes the set of free variables in e and is defined as follows:

F V (v)  = {v}
F V (g(e_{1}, ..., e_{n}))  = F V (e_{1}) ∪ ... ∪ F V (e_{n})

where g is c, p, or f

F V (if e_{1} then e_{2} else e_{3}) = F V (e_{1}) ∪ F V (e_{2}) ∪ F V (e_{3})
F V (let v = e_{1} in e_{2})  = F V (e_{1}) ∪ (F V (e_{2}) \ {v})

To compute these sets, we start with Σf̄_{0}_{‵} containing the indices of the arguments of f̄_{0}^{‵} corresponding to x and r̄, and, for all other functions f, Σ_{f} containing the indices of all arguments of f, and iterate until a fixed point is reached. This iteration always terminates since, for each function f, f has a fixed arity, Σ_{f} decreases, and a lower bound ∅ exists.

For the running example, we obtain Σ\overline{cmp}^{‵} = \{2\} and Σ\overline{sum} = Σ\overline{prod} = \{1\}. For every subexpression e in the definition of \overline{cmp}^{‵}(y, r̄), r̄ ∈ Σ_{[e]}. For every subexpression e in the definitions of \overline{sum}(x) and \overline{prod}(x), Σ_{[e]} = \{x\}.

Collection transformation. Next, we use a collec-

tion transformation to collect the candidate auxiliary information. The main difference between this collection transformation and the extension transformation in Step A.1 is that, in the former, the value originally computed by a subexpression is returned only if it depends only on x and r̄, while in the latter, the value originally computed by a subexpression is always returned.

Basically, for each function f(v_{1}, ..., v_{n}) = e called in the program for f̄_{0}^{‵} and such that Σ_{f} ≠ ∅, we construct a function definition

f̌(v_{i_{1}}, ..., v_{i_{k}}) = Col[[e]]  (9)

where Σ_{f} = {i_{1}, ..., i_{k}} and 1 ≤ i_{1} < ... < i_{k} ≤ n. Col[[e]] collects the results of intermediate function applications in e that have been statically determined to depend only on x and r̄. Note, however, that an improvement similar to that in Step A.1 is made, namely, we avoid constructing such a collected version for f if Σ_{f} = {1, ..., n} and Mall(f) = true.

The transformation Col always first examines whether its argument expression e has been determined to depend only on x and r̄, i.e., F V (e) ⊆ Σ_{[e]}. If so, Col[[e]] = Ext[[e]], where Ext is the improved extension transformation defined in Step A.1. Otherwise, Col[[e]] is defined as in Figure 8, where Pǎd[[e]] generates a tuple of ’s of length equal to the number of the function applications in e, except that function applications f(e_{1}, ..., e_{n}) such that Σ_{f} = ∅, or Σ_{f} = {1, ..., n} but Mall(f) = true and Mtag(f(e_{1}, ..., e_{n})) = true are not counted. Note that if e has been determined to depend only on x and r̄, then 1st(Col[[e]]) is just the original value of e; otherwise, Col[[e]] contains only values of intermediate function applications.

Although this forward dependence analysis is equivalent to binding time analysis, the application here is different from that in partial evaluation [31]. In partial evaluation, the goal is to obtain a residual program that is specialized on a given set of static arguments and takes only the dynamic arguments, while here, we construct a program that computes only on the “static” arguments. In this respect, the resulting program obtained here is similar to the slice obtained from forward slicing [63]. However, our forward dependence analysis finds parts of a program that depend only on certain information, while forward slicing finds parts of a program that depend possibly on certain information. Furthermore, our resulting program also returns all intermediate results on the arguments of interest.

For the function \overline{cmp}^{‵} in (8), collecting all intermediate results that depend only on its second parameter yields

čmp(r̄) = < \overline{sum}(4th(r̄)), \overline{prod}(2nd(r̄)) > (10)

We can see that computing čmp(r̄) is no slower than computing cmp(x). We will see that this guarantees that incremental computation using the program obtained at the end is at least as fast as computing cmp from scratch.

4 Phase B: Using auxiliary information

Phase B determines which pieces of the collected candidate auxiliary information are useful for incremental computation of f_{0}(x ⊕ y) and exactly how they can be used. The For each function f(v_{1}, ..., v_{n}) = e_{f} , define Σ_{[e_{f}]} = {v_{i} | i ∈Σ_{f} } and, for each subexpression e of e_{f},

if e is c(e_{1}, ..., e_{n}) or p(e_{1}, ..., e_{n}) then Σ_{[e_{1}]} = ... = Σ_{[e_{n}]} = Σ_{[e]}
if e is f_{1}(e_{1}, ..., e_{n})  then Σ_{[e_{1}]} = ... = Σ_{[e_{n}]} = Σ_{[e]} and Σ_{f_{1}} ={i | F V (e_{i}) ⊆ Σ_{[e]}} ∩ Σ_{f_{1}}
if e is if e_{1} then e_{2} else e_{3}  then Σ_{[e_{1}]} = Σ_{[e_{2}]} = Σ_{[e_{3}]} = Σ_{[e]}
if e is let v = e_{1} in e_{2}  then Σ_{[e_{1}]} = Σ_{[e]} and Σ_{[e_{2}]} = \begin{cases}Σ_{[e]} ∪ \{v\} & if F V (e_{1}) ⊆ Σ_{[e]} \\ Σ_{[e]} \ \{v\} & otherwise \end{cases}

Figure 7: Definition of Σ

Col[[v]]  = <>
Col[[g(e_{1}, ..., e_{n})]] where g is c or p = Col[[e_{1}]] @ ... @ Col[[e_{n}]]
Col[[f(e_{1}, ..., e_{n})]] = let v_{1} =Col[[e_{1}]] in ... let v_{n} =Col[[e_{n}]] in e′_{1} @ ... @e′_{n} @ e′

where e′_{i} = \begin{cases}rst(v_{i}) & if i ∈ Σ_{f} \\ v_{i} & otherwise \end{cases}

e′ = \begin{cases}<> & if Σ_{f} = ∅ \\ <f̌(1st(v_{i_{1}}), ...,1st(v_{i_{k}}))> & otherwise \end{cases}

where Σ_{f} = {i_{1}, ..., i_{k}} and 1≤ i_{1} <...<i_{k} ≤ n

Col[[if e_{1} then e_{2} else e_{3}]]

= let v_{1} =Col[[e_{1}]] in

if 1st(v_{1}) \begin{matrix}then & \begin{matrix}let v_{2} =Col[[e_{2}]] in \\ rst(v_{1}) @ v_{2} @ Pǎd[[e_{3}]] \end{matrix} \\ else & \begin{matrix}let v_{3} =Col[[e_{3}]] in \\ rst(v_{1}) @ Pǎd[[e_{2}]] @ v_{3} \end{matrix} \end{matrix}

if F V (e_{1}) ⊆ Σ_{[e_{1}]}

= let v_{1} =Col[[e_{1}]] in let v_{2} =Col[[e_{2}]] in let v_{3} =Col[[e_{3}]] in v_{1} @ v_{2} @ v_{3}  otherwise

Col[[let v =e_{1} in e_{2}]]

= let v_{1} =Col[[e_{1}]] in

let v =1st(v_{1}) in \begin{matrix}let v_{2} =Col[[e_{2}]] in \\ rst(v_{1}) @ v_{2} \end{matrix}

if F V (e_{1}) ⊆ Σ_{[e_{1}]}

= let v_{1} =Col[[e_{1}]] in \begin{matrix}let v_{2} =Col[[e_{2}]] in \\ v_{1} @ v_{2} \end{matrix}  otherwise

Figure 8: Definition of Col

basic idea is to merge the candidate auxiliary information with the original computation of f_{0}(x), derive an incremental version for the resulting program, and determine the least information useful for computing the value of f_{0}(x ⊕ y) in that incremental version.

However, we want the incremental computation of f_{0}(x⊕

y) to have access to the auxiliary information in addition to the intermediate results of f_{0}(x). Thus, we merge the candidate auxiliary information in f̌_{0}(x, r̄) with f̄_{0}(x) instead of f_{0}(x). After deriving an incremental version for the resulting program, we prune out the useless auxiliary information and the useless intermediate results.

Phase B has three steps. Step 1 merges f̌_{0} with f̄_{0} to form a function ¯ ; ˇf_{0} that returns candidate auxiliary information as well as all intermediate results. It also determines a projection Π_{0} that projects the return value of f_{0} out of ¯ ; ˇf_{0}. Step 2 incrementalizes ¯ ; ˇf_{0} under ⊕ to obtain an incremental version ¯ ; ˇf_{0}′. Step 3 prunes out of ¯ ; ˇf_{0} and ¯ ; ˇf_{0}′ the intermediate results and auxiliary information that are not useful.

4.1 Step B.1: Combining intermediate results and auxiliary information

To merge the candidate auxiliary information with f̄_{0}, we could simply attach it onto f̄_{0} by defining ¯ ; ˇf_{0} to be the pair of f̄_{0} and f̌_{0}:

¯ ; ˇf_{0}(x) = let r̄ = f̄_{0}(x) in let ř = f̌_{0}(x, r̄) in < r̄, ř >

and use the projection Π_{0}(¯ ; ř) = 1st(1st(¯ ; ř)) to project out the original return value of f_{0}. However, we can do better by using a transformation to integrate the computation of f̌_{0} more tightly into the computation of f̄_{0}, as opposed to carrying out two disjoint computations. The integrated computation is usually more efficient; so is its incremental version.

We do not describe the integration in detail. Basically, it uses traditional transformation techniques [13] like those used in tupling tactic [21, 50, 14]. We require only that Π_{0}(¯ ; ˇf_{0}(x)) always project out 1st(f̄_{0}(x)), which is the value of f_{0}(x), and that the values of all other components of f̄_{0}(x) and f̌_{0}(x, r̄) are embedded in the value of ¯ ; ˇf_{0}(x). This allows re-arranging the order of the components in the return value.

For the functions \overline{cmp} in (7) and čmp in (10), we first define a function

\begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}(x) = let r̄ = \overline{cmp}(x) in let ř = čmp(r̄) in < r̄, ř >

and a projection Π_{0}(¯ ; ř) = 1st(1st(¯ ; ř)). Next, we transform \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}(x) to integrate the computations of \overline{cmp} and čmp,

1. unfold \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}, then \overline{cmp} and čmp

= let r̄ = let v_{1} = odd(x) in let u_{1} = \overline{sum}(v_{1}) in let v_{2} = even(x) in let u_{2} = \overline{prod}(v_{2}) in < \begin{matrix}1st(u_{1}) ≤ 1st(u_{2}), \\ v_{1}, u_{1}, v_{2}, u_{2} > in \end{matrix} let ř = < \begin{matrix}\overline{sum}(4th(r̄)), \\ \overline{prod}(2nd(r̄)) > in \end{matrix} < r̄, ř >

2. lift bindings for v_{1}, u_{1}, v_{2}, u_{2}, and simplify

= let v_{1} = odd(x) in let u_{1} = \overline{sum}(v_{1}) in let v_{2} = even(x) in let u_{2} = \overline{prod}(v_{2}) in let r̄ = <\begin{matrix}1st(u_{1}) ≤ 1st(u_{2}), \\ v_{1}, u_{1}, v_{2}, u_{2} > in \end{matrix} let ř = < \begin{matrix}\overline{sum}(v_{2}), \\ \overline{prod}(v_{1}) > in \end{matrix} < r̄, ř >

3. unfold bindings for r̄ and ř

= let v_{1} = odd(x) in let u_{1} = \overline{sum}(v_{1}) in let v_{2} = even(x) in let u_{2} = \overline{prod}(v_{2}) in < \begin{matrix}<\begin{matrix}1st(u_{1}) ≤ 1st(u_{2}), \\ v_{1}, u_{1}, v_{2}, u_{2} >, \end{matrix} \\ < \overline{sum}(v_{2}), \overline{prod}(v_{1}) >> \end{matrix}

Simplifying the return value and Π_{0}, we obtain the function

\begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}(x) = let v_{1} = odd(x) in let u_{1} = \overline{sum}(v_{1}) in let v_{2} = even(x) in let u_{2} = \overline{prod}(v_{2}) in < \begin{matrix}1st(u_{1}) ≤ 1st(u_{2}), \\ v_{1}, u_{1}, v_{2}, u_{2}, \overline{sum}(v_{2}), \overline{prod}(v_{1}) > \end{matrix} (11)

and the projection Π_{0}(¯ ; ř) = 1st(¯ ; ř).

4.2 Step B.2: Incrementalization

To derive an incremental version ¯ ; ˇf_{0}′ of ¯ ; ˇf_{0} under ⊕, we can use the method in [41], as sketched in Section 1. Depending on the power expected from the derivation, the method can be made semi-automatic or fully automatic.

For the function \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix} in (11) and input change operation
x ⊕ y = cons(y, x), we derive an incremental version of \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}
under ⊕:

1. unfold \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}(cons(y, x))

= let v_{1} = odd(cons(y, x)) in let u_{1} = \overline{sum}(v_{1}) in let v_{2} = even(cons(y, x)) in let u_{2} = \overline{prod}(v_{2}) in < \begin{matrix}1st(u_{1}) ≤ 1st(u_{2}), \\ v_{1}, u_{1}, v_{2}, u_{2}, \overline{sum}(v_{2}), \overline{prod}(v_{1}) > \end{matrix}

2. unfold odd, \overline{sum}, even, \overline{prod} and simplify

= let v′_{1} = even(x) in let u′_{1} = \overline{sum}(v′_{1}) in let v_{2} = odd(x) in let u_{2} = \overline{prod}(v_{2}) in let u′_{4} = \overline{prod}(v′_{1}) in <\begin{matrix}y + 1st(u′_{1}) ≤ 1st(u_{2}), \\ cons(y, v′_{1}), <y+1st(u′_{1}), u′_{1} >, v_{2}, u_{2}, \\ \overline{sum}(v_{2}), <y∗1st(u′_{4}), u′_{4} >> \end{matrix}

3. replace all applications by retrievals

= let v′_{1} = 4th(¯ ; ř) in let u′_{1} = 6th(¯ ; ř) in let v_{2} = 2nd(¯ ; ř) in let u_{2} = 7th(¯ ; ř) in let u′_{4} = 5th(¯ ; ř) in <\begin{matrix}y + 1st(u′_{1}) ≤ 1st(u_{2}), \\ cons(y, v′_{1}), <y+1st(u′_{1}), u′_{1} >, v_{2}, u_{2}, \\ 3rd(¯ ; ř), <y∗1st(u′_{4}), u′_{4} >> \end{matrix}

Simplification yields the following incremental version \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}′ such that, if \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}(x) =¯ ; ř, then \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}′(y,¯ ; ř) = \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}(cons(y, x)):

\begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}′(y,¯ ; ř) = <\begin{matrix}y+1st(6th(¯ ; ř)) ≤ 1st(7th(¯ ; ř)), \\ cons(y, 4th(¯ ; ř)), <y+1st(6th(¯ ; ř)), 6th(¯ ; ř)>, \\ 2nd(¯ ; ř), 7th(¯ ; ř), \\ 3rd(¯ ; ř), <y∗1st(5th(¯ ; ř)), 5th(¯ ; ř)>> \end{matrix}

(12)

Clearly, \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}′(y,¯ ; ř) computes \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}(cons(y, x)) in only O(1) time.

4.3 Step B.3: Pruning

To prune ¯ ; ˇf_{0} and ¯ ; ˇf_{0}′, we use the analyses and transformations in Stage III of [40]. A backward dependence analysis determines the components of¯ ; řand subcomputations of ¯ ; ˇf_{0}′ whose values are useful in computing Π_{0}(¯ ; ˇf_{0}′(x, y,¯ ; ř)), which is the value of f_{0}. A pruning transformation replaces useless computations with . Finally, the resulting functions are optimized by eliminating the components, adjusting the selectors, etc.

For the functions \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix} in (11) and \begin{matrix}¯ & ¯ \\ ˇ cmp \end{matrix}′ in (12), we obtain

c̃mp(x) = let v_{1} = odd(x) in let u_{1} = \overline{sum}(v_{1}) in let v_{2} = even(x) in let u_{2} = \overline{prod}(v_{2}) in < \begin{matrix}1st(u_{1}) ≤ 1st(u_{2}), \\ , < 1st(u_{1}), >, , < 1st(u_{2}), >, \\ < 1st(\overline{sum}(v_{2})), >, < 1st(\overline{prod}(v_{1})), >> \end{matrix}

c̃mp′(y,¯ ; ř) = <\begin{matrix}y+1st(6th(¯ ; ř)) ≤ 1st(7th(¯ ; ř)), \\ , < y+1st(6th(¯ ; ř)), >, \\ , < 1st(7th(¯ ; ř)), >, \\ < 1st(3rd(¯ ; ř)), >, < y∗1st(5th(¯ ; ř)), >> \end{matrix}

Optimizing these functions yields the final definitions of c̃mp and c̃mp′, which appear in Figure 2:

5 Discussion

Correctness. Auxiliary information is maintained incrementally, so at the step of discovering it, we should not be concerned with the time complexity of computing it from scratch; this is why time considerations were dropped in Step A.2. However, to make the overall approach effective, we must consider the cost of computing and maintaining the auxiliary information. Here, we simply require that the candidate auxiliary information be computed at least as fast as the original program, i.e., t(f̌_{0}(x, r̄)) ≤ t(f_{0}(x)) for r̄ = f̄_{0}(x). This can be checked after Step A.3. We guarantee this condition by simply dropping pieces of candidate auxiliary information for which it can not be confirmed. Standard constructions for mechanical time analysis [57, 62] can be used, although further study is needed. Automatic space analysis and the trade-off between time and space are problems open for study.

Suppose Step B.1 projects out the original value using 1st. With the above condition, in a similar way to [40], we can show that, if f_{0}(x) = r, then

1st(f̃_{0}(x)) = r and t(f̃_{0}(x)) ≤ t(f_{0}(x))  (13)

and if f_{0}(x ⊕ y) = r′ and f̃_{0}(x) = r̃, then

\begin{matrix}1st(f̃_{0}′(x, y, r̃)) = r′, f̃_{0}′(x, y, r̃) = f̃_{0}(x ⊕ y), \\ and t(f̃_{0}′(x, y, r̃)) ≤ t(f_{0}(x ⊕ y)). \end{matrix}  (14)

i.e., the functions f̃_{0} and f̃_{0}′ preserve the semantics and compute asymptotically at least as fast. Note that f̃_{0}(x) may terminate more often than f_{0}(x), and f̃_{0}′(x, y, r̃) may terminate more often than f_{0}(x ⊕ y), due to the transformations used in Steps B.2 and B.3.

Multi-pass discovery of auxiliary informa-

tion. The function f̃_{0} can sometimes be computed even faster by maintaining auxiliary information useful for incremental computation of the auxiliary information already in f̃_{0}. We can obtain such auxiliary information of auxiliary information by iterating the above approach.

Other auxiliary information. There are cases

where the auxiliary information discovered using the above approach is not sufficient for efficient incremental computation. In these cases, classes of special parameterized data structures are often used. Ideally, we can collect them as auxiliary information parameterized with certain classes of data types. Then, we can systematically extend a program to compute such auxiliary information and maintain it incrementally. In the worst case, we can code manually discovered auxiliary information to obtain an extended program f̃_{0}, and then use our systematic approach to derive an incremental version of f̃_{0} that incrementally computes the new output using the auxiliary information and also maintains the auxiliary information.

6 Examples

The running example on list processing illustrates the application of our approach to solving explicit incremental problems for, e.g., interactive systems and reactive systems. Other applications include optimizing compilers and transformational programming.

This section presents an example for each of these two applications. The examples are based on problems in VLSI design and graph algorithms, respectively.

6.1 Strength reduction in optimizing compilers: binary integer square root

This example is from [45], where a specification of a nonrestoring binary integer square root algorithm is transformed into a VLSI circuit design and implementation. In that work, a strength-reduced program was manually discovered and then proved correct using Nuprl [16]. Here, we show how our method can automatically derive the strength reductions. This is of particular interest in light of the recent Pentium chip flaw [24].

The initial specification of the l-bit non-restoring binary integer square root algorithm [23, 45], which is exact for perfect squares and off by at most 1 for other integers, is

m := 2^{l−1}

for i := l − 2 downto 0 do p := n − m^{2}; if p > 0 then

m := m + 2^{i}

else if p < 0 then m := m − 2^{i}

(15)

In hardware, multiplications and exponentials are much more expensive than additions and shifts (doublings or halvings), so the goal is to replace the former by the latter.

To simplify the presentation, we jump to the heart of the problem, namely, computing n − m^{2} and 2^{i} incrementally in each iteration under the change m′ = m ± 2^{i} and i′ = i − 1. Let f_{0} be

f_{0}(n, m, i) = pair(n − m^{2}, 2^{i})

where pair is a constructor with selectors fst(a, b) = a and snd(a, b) = b, and let input change operation ⊕ be

⟨n′, m′, i′⟩ = ⟨n, m, i⟩ ⊕ ⟨ ⟩ = ⟨n, m ± 2^{i}, i − 1⟩

Step A.1. We cache all intermediate results of f_{0}, obtaining

f̄_{0}(n, m, i) = let v = m^{2} in < pair(n − v, 2^{i}), v >

Step A.2. We transform f̄_{0} under ⊕, obtaining

\begin{matrix}f̄_{0}^{‵}(n, m, i, r̄) \\ = \begin{matrix}let v = 2nd(r̄) ± 2∗m∗snd(1st(r̄)) + (snd(1st(r̄)))^{2} in \\ < pair(n − v, snd(1st(r̄))/2), v > \end{matrix} \end{matrix}

Step A.3. We collect candidate auxiliary information, obtaining

f̌_{0}(n, m, i, r̄) = < 2∗m∗snd(1st(r̄)), (snd(1st(r̄)))^{2} > (16)

Step B.1. We merge the collected candidate auxiliary information with f̄_{0}, obtaining Π_{0}(¯ ; ř) = 1st(¯ ; ř) and

¯ ; ˇf_{0}(n, m, i) = let v = m^{2} in let u = 2^{i} in <pair(n − v, u), v, 2∗m∗u, u^{2} >

Step B.2. We derive an incremental version of ¯ ; ˇf_{0} under ⊕, obtaining

¯ ; ˇf_{0}′(n, m, i,¯ ; ř) = let v = 2nd(¯ ; ř) ± 3rd(¯ ; ř) + 4th(¯ ; ř) in let u = snd(1st(¯ ; ř))/2 in < \begin{matrix}pair(fst(1st(¯ ; ř)) ∓ 3rd(¯ ; ř) − 4th(¯ ; ř), u), \\ v, 3rd(¯ ; ř)/2 ± 4th(¯ ; ř), 4th(¯ ; ř)/4 > \end{matrix}

Step B.3. We prune the functions ¯ ; ˇf_{0} and ¯ ; ˇf_{0}′, eliminating their second components and obtaining

\begin{matrix}f̃_{0}(n, m, i) \\ = let u = 2^{i} in < pair(n − m^{2}, u), 2∗m∗u, u^{2} > \end{matrix} (17)

\begin{matrix}f̃_{0}′(n, m, i, r̃) \\ = < \begin{matrix}pair(fst(1st(r̃)) ∓ 2nd(r̃) − 3rd(r̃), snd(1st(r̃))/2), \\ 2nd(r̃)/2 ± 3rd(r̃), 3rd(r̃)/4 > \end{matrix} \end{matrix}

(18)

The expensive multiplications and exponentials have been completely replaced with additions and shifts. We even discover that an unnecessary shift is done in [45]. Thus, a systematic approach such as ours is desirable not only for automating designs and guaranteeing correctness, but also for reducing costs.

6.2 Transformational programming: path sequence problem

This example is from [7]. Given a directed acyclic graph, and a string whose elements are vertices in the graph, the problem is to compute the length of the longest subsequence in the string that forms a path in the graph. We focus on the second half of the example, where an exponential-time recursive solution is improved (incorrectly in [7], correctly in [8]).

The function llp defined below computes the desired length. The input string is given explicitly as the argument to llp. The input graph is represented by a predicate arc such that arc(a, b) is true iff there is an edge from vertex a to vertex b in the graph. The primitive function max returns the maximum of its two arguments.

llp(l) = if null(l) then 0 else max(llp(cdr(l)), 1+f(car(l), cdr(l)))

f(n, l) = if null(l) then 0 else if arc(n, car(l)) then max(f(n, cdr(l)), 1+f(car(l), cdr(l))) else f(n, cdr(l))

(19)

The problem is to compute llp incrementally under the input change operation l⊕i = cons(i, l). Using the approach described in this paper, we obtain

l̃lp(l) = if null(l) then <0> else let v = f̃(car(l), cdr(l)) in <max(llp(cdr(l)), 1+1st(v)), v >

f̃(n, l) = if null(l) then <0> else let u = f̃(car(l), cdr(l)) in if arc(n, car(l)) then <max(f(n, cdr(l)), 1+1st(u), u> else <f(n, cdr(l)), u>

(20) and

l̃lp′(i, l, r̃) = if null(l) then <1, <0>> else let v = f̃′(i, l, 2nd(r̃)) in <max(1st(r̃), 1+1st(v)), v >

f̃′(i, l, r̃_{1}) = if null(cdr(l)) then if arc(i, car(l)) then <1, <0>> else <0, <0>> else let v = f̃′(i, cdr(l), 2nd(r̃_{1})) in if arc(i, car(l)) then <max(1st(v), 1+1st(r̃_{1})), r̃_{1} > else <1st(v), r̃_{1} >

(21)

Computing llp(cons(i, l)) from scratch takes exponential time, but computing l̃lp′(i, l, r̃) takes only O(n) time, where n is the length of l, since l̃lp′(i, l, r̃) calls f̃′, which goes through the list l once.

Finally, we use these derived functions to compute the original function llp. Note that llp(l) = 1st(l̃lp(l)) and, if l̃lp(l) = r̃, then l̃lp′(i, l, r̃) = l̃lp(cons(i, l)). Using the definition of l̃lp′ in (21) in this last equation, we obtain:

l̃lp(cons(i, l)) = if null(l) then <1, <0>> else let r̃ = l̃lp(l) in let v = f̃′(i, l, 2nd(r̃)) in <max(1st(r̃), 1+1st(v)), v >

Using this equation and the base case l̃lp(nil) = < 0 >, we obtain a new definition of l̃lp:

l̃lp(l) = if null(l) then <0> else if null(cdr(l)) then <1, <0>> else let r̃ = l̃lp(cdr(l)) in let v = f̃′(car(l), cdr(l), 2nd(r̃)) in <max(1st(r̃), 1+1st(v)), v > (22)

where f̃′ is defined in (21). This new l̃lp takes only O(n^{2}) time, since it calls f̃′ only O(n) times.

7 Related work and conclusion

Work related to our analysis and transformation techniques has been discussed throughout the presentation. Here, we take a closer look at related work on discovering auxiliary information for incremental computation.

Interactive systems and reactive systems often use incremental algorithms to achieve fast response time [4, 5, 9, 19, 27, 33, 53, 54]. Since explicit incremental algorithms are hard to write and appropriate auxiliary information is hard to discover, the general approach in this paper provides a systematic method for developing particular incremental algorithms. For example, for the dynamic incremental attribute evaluation algorithm in [55], the characteristic graph is a kind of auxiliary information that would be discovered following the general principles underlying our approach. For static incremental attribute evaluation algorithms [34, 35], where no auxiliary information is needed, the approach can cache intermediate results and maintain them automatically [40].

Strength reduction [2, 15, 60] is a traditional compiler optimization technique that aims at computing each iteration incrementally based on the result of the previous iteration. Basically, a fixed set of strength-reduction rules for primitive operators like times and plus are used. Our method can be viewed as a principled strength reduction technique not limited to a fixed set of rules: it can be used to reduce strength of computations where no given rules apply and, furthermore, to derive or justify such rules when necessary, as shown in the integer square root example.

Finite differencing [46, 47, 48] generalizes strength reduction to set-theoretic expressions for systematic program development. Basically, rules are manually developed for differentiating set expressions. For continuous expressions, our method can derive such rules directly using properties of primitive set operations. For discontinuous set expressions, dynamic expressions need to be discovered and rules for maintaining them derived. How to discover these dynamic expressions remains to be studied, but once discovered, our method can be used to derive rules that maintain them. In general, such rules apply only to very-high-level languages like SETL; our method applies also to lower-level languages like Lisp.

Maintaining and strengthening loop invariants has been advocated by Dijkstra, Gries, and others [18, 25, 26, 56] for almost two decades as a standard strategy for developing loops. In order to produce efficient programs, loop invariants need to be maintained by the derived programs in an incremental fashion. To make a loop more efficient, the strategy of strengthening a loop invariant, often by introducing fresh variables, is proposed [26]. This corresponds to discovering appropriate auxiliary information and deriving incremental programs that maintain such information. Work on loop invariants stressed mental tools for programming, rather than mechanical assistance, so no systematic procedures were proposed.

Induction and generalization [10, 44] are the logical foundations for recursive calls and iterative loops in deductive program synthesis [42] and constructive logics [16]. These corpora have for the most part ignored the efficiency of the programs derived, and the resulting programs “are often wantonly wasteful of time and space” [43]. In contrast, the approach in this paper is particularly concerned with the efficiency of the derived programs. Moreover, we can see that induction, whether course-of-value induction [36], structural induction [10, 12], or well-founded induction [10, 44], enables derived programs to use results of previous iterations in each iteration, and generalization [10, 44] enables derived programs to use appropriate auxiliary information by strengthening induction hypotheses, just like strengthening loop invariants. The approach in this paper may be used for systematically constructing induction steps [36] and strengthening induction hypotheses.

The promotion and accumulation strategies are proposed by Bird [7, 8] as general methods for achieving efficient transformed programs. Promotion attempts to derive a program that defines f(cons(a, x)) in terms of f(x), and accumulation generalizes a definition by including an extra argument. Thus, promotion can be regarded as deriving incremental programs, and accumulation as identifying appropriate intermediate results or auxiliary information. Bird illustrates these strategies with two examples. However, we can discern no systematic steps being followed in [7]. As demonstrated with the path sequence problem, our approach can be regarded as a systematic formulation of the promotion and accumulation strategies. It helps avoid the kind of errors reported and corrected in [8].

Other work on transformational programming for improving program efficiency, including the extension technique in [17], the transformation of recursive functional programs in the CIP project [11, 6, 49], and the finite differencing of functional programs in the semi-automatic program development system KIDS [59], can also be further automated with our systematic approach.

In conclusion, incremental computation has widespread applications throughout computing. This paper proposes a systematic approach for discovering a general class of auxiliary information for incremental computation. It is naturally combined with incrementalization and reusing intermediate results to form a comprehensive approach for efficient incremental computation. The modularity of the approach lets us integrate other techniques in our framework and reuse our components for other optimizations.

Although our approach is presented in terms of a firstorder functional language with strict semantics, the underlying principles are general and apply to other languages as well. For example, the method has been used to improve imperative programs with arrays for the local neighborhood problems in image processing [39]. A prototype system, CA-CHET [38], based on our approach is under development.

References

[1] A. V. Aho, R. Sethi, and J. D. Ullman. Compilers, Principles, Techniques, and Tools. Addison-Wesley Series in Computer Science. Addison-Wesley Publishing Company, Reading, Massachusetts, 1986.

[2] F. E. Allen, J. Cocke, and K. Kennedy. Reduction of operator strength. In S. S. Muchnick and N. D. Jones, editors, Program Flow Analysis, chapter 3, pages 79– 101. Prentice-Hall, Englewood Cliffs, New Jersey, 1981.

[3] B. Alpern, R. Hoover, B. Rosen, P. Sweeney, and K. Zadeck. Incremental evaluation of computational circuits. In Proceedings of the 1st Annual ACM-SIAM Symposium on Discrete Algorithms, pages 32–42, San Francisco, California, January 1990.

[4] R. Bahlke and G. Snelting. The PSG system: From formal language definitions to interactive programming environments. ACM Transactions on Programming Languages and Systems, 8(4):547–576, October 1986.

[5] R. A. Ballance, S. L. Graham, and M. L. Van De Vanter. The Pan language-based editing system. ACM Transactions on Software Engineering and Methodology, 1(1):95–127, January 1992.

[6] F. L. Bauer, B. Möller, H. Partsch, and P. Pepper. Formal program construction by transformations— computer-aided, intuition-guided programming. IEEE Transactions on Software Engineering, 15(2):165–180, February 1989.

[7] R. S. Bird. The promotion and accumulation strategies in transformational programming. ACM Transactions on Programming Languages and Systems, 6(4):487–504, October 1984.

[8] R. S. Bird. Addendum: The promotion and accumulation strategies in transformational programming. ACM Transactions on Programming Languages and Systems, 7(3):490–492, July 1985.

[9] P. Borras and D. Clément. CENTAUR: The system. In Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, pages 14–24, Boston, Massachusetts, November 1988. Published as SIGPLAN Notices, 24(2).

[10] R. S. Boyer and J. S. Moore. A Computational Logic. ACM Monograph Series. Academic Press, New York, 1979.

[11] M. Broy. Algebraic methods for program construction: The project CIP. In P. Pepper, editor, Program Transformation and Programming Environments, volume 8 of NATO Advanced Science Institutes Series F: Computer and System Sciences, pages 199–222. Springer-Verlag, Berlin, 1984. Proceedings of the NATO Advanced Research Workshop on Program Transformation and Programming Environments, directed by F. L. Bauer and H. Remus, Munich, Germany, September 1983.

[12] R. M. Burstall. Proving properties of programs by structural induction. The Computer Journal, 12(1):41– 48, 1969.

[13] R. M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44–67, January 1977.

[14] W.-N. Chin. Towards an automated tupling strategy. In Proceedings of the ACM SIGPLAN Symposium on PEPM, Copenhagen, Denmark, June 1993.

[15] J. Cocke and K. Kennedy. An algorithm for reduction of operator strength. Communications of the ACM, 20(11):850–856, November 1977.

[16] R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.

[17] N. Dershowitz. The Evolution of Programs, volume 5 of Progress in Computer Science. Birkhäuser, Boston, 1983.

[18] E. W. Dijkstra. A Discipline of Programming. Prentice-Hall Series in Automatic Computation. Prentice-Hall, Englewood Cliffs, New Jersey, 1976.

[19] V. Donzeau-Gouge, G. Huet, G. Kahn, and B. Lang. Programming environments based on structure editor: The Mentor experience. In D. R. Barstow, H. E. Shrobe, and E. Sandewall, editors, Interactive Programming Environments, pages 128–140. McGraw-Hill, New York, 1984.

[20] J. Earley. High level iterators and a method for automatically designing data structure representation. Journal of Computer Languages, 1:321–342, 1976.

[21] M. S. Feather. A system for assisting program transformation. ACM Transactions on Programming Languages and Systems, 4(1):1–20, January 1982.

[22] J. Field and T. Teitelbaum. Incremental reduction in the lambda calculus. In Proceedings of the ACM ’90 Conference on LFP, pages 307–322, 1990.

[23] I. Flores. The Logic of Computer Arithmetic. Prentice-Hall International Series in Electrical Engineering. Prentice-Hall, Englewood Cliffs, New Jersey, 1963.

[24] J. Glanz. Mathematical logic flushes out the bugs in chip designs. Science, 267:332–333, January 20, 1995.

[25] D. Gries. The Science of Programming. Texts and Monographs in Computer Science. Springer-Verlag, New York, 1981.

[26] D. Gries. A note on a standard strategy for developing loop invariants and loops. Science of Computer Programming, 2:207–214, 1984.

[27] A. N. Habermann and D. Notkin. Gandalf: Software development environments. IEEE Transactions on Software Engineering, SE-12(12):1117–1127, December 1986.

[28] R. Hoover. Alphonse: Incremental computation as a programming abstraction. In Proceedings of the ACM SIGPLAN ’92 Conference on PLDI, pages 261–272, California, June 1992.

[29] S. Horwitz and T. Teitelbaum. Generating editing environments based on relations and attributes. ACM Transactions on Programming Languages and Systems, 8(4):577–608, October 1986.

[30] F. Jalili and J. H. Gallier. Building friendly parsers. In Conference Record of the 9th Annual ACM Symposium on POPL, pages 196–206, Albuquerque, New Mexico, January 1982.

[31] N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, Englewood Cliffs, New Jersey, 1993.

[32] N. D. Jones, P. Sestoft, and H. Søndergaard. An experiment in partial evaluation: The generation of a compiler generator. In J.-P. Jouannaud, editor, Rewriting Techniques and Applications, volume 202 of Lecture Notes in Computer Science, pages 124–140, Dijon, France, May 1985. Springer-Verlag, Berlin.

[33] G. E. Kaiser. Incremental dynamic semantics for language-based programming environments. ACM Transactions on Programming Languages and Systems, 11(2):168–193, April 1989.

[34] U. Kastens. Ordered attributed grammars. Acta Informatica, 13(3):229–256, 1980.

[35] T. Katayama. Translation of attribute grammars into procedures. ACM Transactions on Programming Languages and Systems, 6(3):345–369, July 1984.

[36] S. C. Kleene. Introduction to Metamathematics. Van Nostrand, New York, 1952. Tenth reprint, Wolters-Noordhoff Publishing, Groningen and North-Holland Publishing Company, Amsterdam, 1991.

[37] J. Launchbury. Projections for specialisation. In Partial Evaluation and Mixed Computation, pages 299–315. North-Holland, 1988.

[38] Y. A. Liu. CACHET: An interactive, incrementalattribution-based program transformation system for deriving incremental programs. In Proceedings of the 10th Knowledge-Based Software Engineering Conference, Boston, Massachusetts, November 1995. IEEE Computer Society Press.

[39] Y. A. Liu. Incremental Computation: A Semantics-Based Systematic Transformational Approach. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, January 1996. To appear as Cornell Technical Report, October, 1995.

[40] Y. A. Liu and T. Teitelbaum. Caching intermediate results for program improvement. In Proceedings of the ACM SIGPLAN Symposium on PEPM, pages 190–201, La Jolla, California, June 1995.

[41] Y. A. Liu and T. Teitelbaum. Systematic derivation of incremental programs. Science of Computer Programming, 24(1):1–39, February 1995.

[42] Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems, 2(1):90–121, January 1980.

[43] Z. Manna and R. Waldinger. Fundamentals of deductive program synthesis. IEEE Transactions on Software Engineering, 18(8):674–704, August 1992.

[44] Z. Manna and R. Waldinger. The Deductive Foundations of Computer Programming. Addison-Wesley, Reading, Massachusetts, 1993.

[45] J. O’Leary, M. Leeser, J. Hickey, and M. Aagaard. Nonrestoring integer square root: A case study in design by principled optimization. In R. Kumar and T. Kropf, editors, Proceedings of TPCD ’94: the 2nd International Conference on Theorem Provers in Circuit Design— Theory, Practice and Experience, volume 901 of Lecture Notes in Computer Science, pages 52–71, Bad Herrenalb (Black Forest), Germany, September 1994. Springer-Verlag, Berlin, 1995.

[46] B. Paige and J. T. Schwartz. Expression continuity and the formal differentiation of algorithms. In Conference Record of the 4th Annual ACM Symposium on POPL, pages 58–71, January 1977.

[47] R. Paige. Transformational programming—applications to algorithms and systems. In Conference Record of the 10th Annual ACM Symposium on POPL, pages 73–87, January 1983.

[48] R. Paige and S. Koenig. Finite differencing of computable expressions. ACM Transactions on Programming Languages and Systems, 4(3):402–454, July 1982.

[49] H. A. Partsch. Specification and Transformation of Programs—A Formal Approach to Software Development. Texts and Monographs in Computer Science. Springer-Verlag, Berlin, 1990.

[50] A. Pettorossi. A powerful strategy for deriving efficient programs by transformation. In Proceedings of the ACM ’84 Symposium on LFP, Austin, Texas, August 1984.

[51] L. L. Pollock and M. L. Soffa. Incremental global reoptimization of programs. ACM Transactions on Programming Languages and Systems, 14(2):173–200, April 1992.

[52] W. Pugh and T. Teitelbaum. Incremental computation via function caching. In Conference Record of the 16th Annual ACM Symposium on POPL, pages 315– 328, January 1989.

[53] S. P. Reiss. An approach to incremental compilation. In Proceedings of the ACM SIGPLAN ’84 Symposium on Compiler Construction, pages 144–156, Montreal, Canada, June 1984. Published as SIGPLAN Notices, 19(6).

[54] T. Reps and T. Teitelbaum. The Synthesizer Generator: A System for Constructing Language-Based Editors. Texts and Monographs in Computer Science. Springer-Verlag, New York, 1988.

[55] 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.

[56] J. C. Reynolds. The Craft of Programming. Prentice-Hall, 1981.

[57] M. Rosendahl. Automatic complexity analysis. In Proceedings of the 4th International Conference on FPCA, pages 144–156, London, U.K., September 1989.

[58] B. G. Ryder and M. C. Paull. Incremental data flow analysis algorithms. ACM Transactions on Programming Languages and Systems, 10(1):1–50, January 1988.

[59] D. R. Smith. KIDS: A semiautomatic program development system. IEEE Transactions on Software Engineering, 16(9):1024–1043, September 1990.

[60] B. Steffen, J. Knoop, and O. Rüthing. Efficient code motion and an adaption to strength reduction. In Proceedings of the 4th International Joint Conference on TAPSOFT, volume 494 of Lecture Notes in Computer Science, pages 394–415, Brighton, U.K., 1991. Springer-Verlag, Berlin.

[61] R. S. Sundaresh and P. Hudak. Incremental computation via partial evaluation. In Conference Record of the 18th Annual ACM Symposium on POPL, pages 1–13, January 1991.

[62] B. Wegbreit. Mechanical program analysis. Communications of the ACM, 18(9):528–538, September 1975.

[63] M. Weiser. Program slicing. IEEE Transactions on Software Engineering, SE-10(4):352–357, July 1984.

[64] D. M. Yellin and R. E. Strom. INC: A language for incremental computations. ACM Transactions on Programming Languages and Systems, 13(2):211–236, April 1991.