Systematic Derivation of Incremental Programs^{∗}

Yanhong A. Liu^{†}, Tim Teitelbaum

Department of Computer Science, Cornell University, Ithaca, NY 14853, USA

Abstract A systematic approach is given for deriving incremental programs from non-incremental programs written in a standard functional programming language. We exploit a number of program analysis and transformation techniques and domain-specific knowledge, centered around effective utilization of caching, in order to provide a degree of incrementality not otherwise achievable by a generic incremental evaluator.

1 Introduction

Incremental programs take advantage of repeated computations on inputs that differ only slightly from one another, avoiding unnecessary duplication of common computations. Given a program f and a certain input change ⊕, a program f′ that computes the value of f(x ⊕ y) efficiently by making use of the value of f(x) is called an incremental version of f under ⊕. The parameter y can be regarded as a change δx to the input x. Methods of incremental computation have widespread applications, e.g., loop optimizations in optimizing compilers [1, 24, 9, 10] and transformational programming [26, 38], interactive systems like editors [3, 35] and programming environments [34, 21], and dynamic systems like distributed databases [8, 20] and real-time systems [45].

A comprehensive guide to the literature on incremental computation has appeared in [33]. Despite the relatively diverse categories discussed in [33], most of the work can be divided into three classes.

The first class includes particular incremental algorithms designed for particular problems dealing with particular input changes. Examples are incremental parsing [15, 18], incremental attribute evaluation [35, 48], incremental data-flow analysis [37], incremental circuit evaluation [2], incremental constraint solving [44, 13], etc. The study of dynamic graph algorithms, e.g., [49], 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 manually developing particular incremental algorithms, application programs are run in a general incremental execution framework so that incremental computation is achieved automatically, e.g., incremental attribute evaluation frameworks [34], incremental computation via function caching [32], formal program manipulations using traditional partial evaluation [42, 41], incremental lambda reduction [12], the change detailing network of INC [50], incremental computation as a program abstraction [16], etc. In this class, often no explicitly incremental version of an application program is derived and run autonomously by a standard evaluator. Moreover, any input change to an application program is mapped to whatever the framework can handle, which is fixed for each framework. Therefore, 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.

∗This is a reformatted version with minor typographical corrections of the article that appeared in Science of Computer Programming, 24(1):1–39, February 1995. The authors gratefully acknowledge the support of the Office of Naval Research under contract No. N00014-92-J-1973.

†Corresponding author. Email address: yanhong@cs.cornell.edu

In the third class, systematic approaches are studied to derive explicitly incremental programs from nonincremental programs using program transformation techniques like finite differencing [25, 30]. Examples are high level iterators [10], finite differencing of set expressions in SETL [30], optimizing relational database operations [17, 27], incremental fixed point computation [7], differentiation of functional programs in KIDS [38, 39], etc. In most of these works, 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. In other work, only high-level strategies are proposed. What is not provided is an effective procedure for deriving incremental programs from non-incremental programs written in a standard language like Lisp.

Our work attacks the problem of discovering incrementality for programs written in a standard functional programming language. We give an effective procedure for deriving incremental programs from nonincremental programs written in a standard functional programming language. The basic derivation idea is to expand the computation of f on the new input so that subcomputations whose values can be efficiently retrieved from the previously computed result of f are replaced by corresponding retrievals. We exploit a number of program analysis and transformation techniques and domain-specific knowledge, centered around effective utilization of caching, in order to provide a degree of incrementality not otherwise achievable by a generic incremental evaluator. We also show how our approach can be extended to address caching auxiliary information for increasing incrementality.

The paper is organized as follows. Section 2 defines the derivation problem. Section 3 outlines the derivation procedure. Basic techniques for incrementalization by simplification and replacement are described in Section 4, with emphasis on techniques for discovering incrementality. Analysis and manipulation of recursive function applications are discussed in Section 5. Section 6 summarizes the derivation procedure and addresses a number of important issues, including correctness, termination, auxiliary information, and mechanization. A number of examples are given in Section 7. Finally, we compare our approach with closely related work and conclude in Section 8.

2 Defining the Problem

For simplicity of exposition, we use a simple first-order functional programming language. The expressions of our language are 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} end 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}⟩.

Example definitions are given in Figure 1. Each constructor c, primitive function p, and user-defined function f has a fixed arity. In general, c_{i}^{−1} denotes the i-th selector corresponding to the constructor c. The semantics of the language is strict.

An input change ⊕ to the 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, in Figure 1, an input change ⊕ to the function out can be defined by ⟨C′, R′⟩ = ⟨C, R⟩ ⊕ ⟨i, a⟩ = ⟨C, insert(i, a, R)⟩. For typographical convenience, we shall always use x to refer to the previous input to f_{0}, r the cached result of f_{0}(x), and y the change parameter to the input x.

We are only interested in using a cached result if we can save time by doing so. Accordingly, we need a time model T such that T (e) describes the time needed to compute expression e. The function T can be

out(C, R) : compute the outer product of lists C and R
out(C, R) = if null(C) then nil
else cons(row(car(C), R), out(cdr(C), R))
row(c, R) = if null(R) then nil
else cons(c ∗ car(R), row(c, cdr(R)))

| \begin{matrix}insert(i, a, R) & : & insert a in list R at position i \\ insert(i, a, R) & = & if i ≤ 1 then cons(a, R) \\ & & else if null(R) then cons(a, nil) \\ & & else cons(\begin{matrix}car(R), \\ insert(i − 1, a, cdr(R))) \end{matrix} \end{matrix}

Figure 1: Example function definitions

obtained from standard constructions [46, 36]. In general, given two expressions e_{1} and e_{2}, it is not decidable whether e_{2} computes faster than e_{1} for given values of their variables. Therefore, we say T (e_{2}) ≤ T (e_{1}) if we can effectively confirm the inequality. Suppose v_{1}, ..., v_{k} are all the variables in e_{1} and e_{2}, and P is some predicate on these variables, we write

t(e_{2}) ≤_{P} t(e_{1})  (2)

to denote that we can effectively decide there is a constant k such that, for any values of v_{1}, ..., v_{k}, if P holds then T (e_{2}) ≤ kT (e_{1}), and we say that e_{2} is asymptotically at least as fast as e_{1}. During our derivation, P always represents the equations that hold at the occurrence of the expression currently under consideration; therefore, it will be omitted for simplicity.

Given a program f_{0} and an input change ⊕, we aim to derive f′_{0}, an incremental version 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.^{1} Obviously, we can trivially define f′_{0}(x, y, r) to be f_{0}(x ⊕ y), but this is of no interest. The goal is to make f′_{0} as efficient as possible by having it use the cached result r of f_{0}(x) as much as possible.

We will use the example in Figure 1 as a running example. At the end, we will obtain the incremental functions shown in Figure 2.

If out(C, R) returns r, then

out′(C, i, a, r) computes out(C, insert(i, a, R)).

For C of length m and R of length n, out′(C, i, a, r) takes time O(m ∗ min(i, n)); out(C, insert(i, a, R)) takes time O(m ∗ n).

|  \begin{matrix}out′(C, i, a, r) & = & if null(r) then nil \\ & & else cons(\begin{matrix}row′(car(C), i, a, car(r)), \\ out′(cdr(C), i, a, cdr(r))) \end{matrix} \\ row′(c, i, a, r_{1}) & = & if i ≤ 1 then cons(c ∗ a, r_{1}) \\ & & else if null(r_{1}) then cons(c ∗ a, nil) \\ & & else cons(\begin{matrix}car(r_{1}), \\ row′(c, i − 1, a, cdr(r_{1}))) \end{matrix} \end{matrix}

Figure 2: Derived function definitions

3 Overview of the Derivation Procedure

The basic derivation idea is to symbolically expand the computation of f_{0}(x⊕y) and replace subcomputations whose values can be efficiently retrieved from the cached result r of f_{0}(x) by corresponding retrievals.

Derivation Procedure. The derivation procedure recursively follows function applications in the computation of f_{0}(x ⊕ y) and aims to replace these applications by uses of new functions introduced to compute the applications incrementally.

1While f_{0}(x) abbreviates f_{0}(x_{1}, ..., x_{n}), and f_{0}(x ⊕ y) abbreviates f_{0}(⟨x_{1}, ..., x_{n}⟩ ⊕ ⟨y_{1}, ..., y_{m}⟩), f′_{0}(x, y, r) abbreviates f′_{0}(x_{1}, ..., x_{n}, y_{1}, ..., y_{m}, r). Note that some of the parameters of f′_{0} may be dead and eliminated, as discussed in Section 5.

To introduce a new function f′ to compute a function application f(e_{1}, ..., e_{n}) incrementally, we collect an information set I_{f} describing the context of the application, and a cache set C_{f} indicating how the values of certain relevant computations can be retrieved from a cached result under certain conditions. Then, we obtain a definition of f′ by the following three steps. First, we unfold [6] (also called expand [47]) the application. Second, we incrementalize the unfolded application. Basically, we consider each subexpression e of the unfolded application in applicative order and (a) collect an information set I_{[e]} from e’s context based on I_{f}, and extend the cache set C_{f} under the condition that the facts in I_{[e]} are valid, (b) recursively apply this procedure if e is a function application, (c) apply simplification using I_{[e]} and replacement by efficient retrieval using the extended C_{f}. Third, we eliminate dead code mainly related to dead parameters of f′. If the function f′ so obtained is suitably fast, then f(e_{1}, ..., e_{n}) can be replaced by an application of f′. Other applications of f that are subsequently analyzed may also be replaced by applications of this f′, if appropriate.

The derivation procedure starts by considering the function application f_{0}(x ⊕ y), with an empty information set and a cache set containing only f_{0}(x) = r. We maintain a global data structure for the set D of functions introduced during the derivation procedure. We take special care of recursive function applications to help the derivation procedure terminate naturally and, at the same time, discover as much incrementality as possible. When finished, we have the original set of functions F and the set D of functions introduced during the derivation procedure, including f′_{0}. We then eliminate dead functions in F and D not needed in computing f′_{0}.

A function IncApply implements the recursive procedure on a function application f(e_{1}, ..., e_{n}) with information set I, cache set C, and global definition set D:

IncApply[[f(e_{1}, ..., e_{n})]] I C D = ⟨f′(e′_{1}, ..., e′_{m}), D′⟩  (3)

f′ is an introduced function such that f′(e′_{1}, ..., e′_{m}) computes f(e_{1}, ..., e_{n}) incrementally under I and C. The global set D may be extended to D′ as a side effect.

Two Main Issues. The derivation procedure has two main tasks. First, incrementalizing an unfolded function application, i.e., discovering and replacing subcomputations whose values can be efficiently retrieved from cached results. Second, analyzing recursive function applications and introducing incremental versions that are used to replace these applications.

The first task corresponds to maintaining cache sets under collected information sets at subexpressions of an unfolded application and applying simplification and replacement to these subexpressions using these sets. The second task corresponds to maintaining a global set of functions introduced to compute function applications incrementally and replacing function applications with appropriate applications of these introduced functions.

The two main issues are addressed in Sections 4 and 5, respectively. Finally, the derivation procedure is summarized in Section 6.

4 Incrementalization

We define two notions, information sets and cache sets. Given an information set I and an initial cache set C relevant to a function application, we describe how to use them in incrementalizing the unfolded application, i.e., collecting information sets at subexpressions, extending the cache set with respect to the collected information sets, and using them to simplify subexpressions and replace subexpressions whose values can be efficiently retrieved from cached results.

4.1 Information Sets and Simplification

An information set I_{[e]} at the occurrence of an expression e is a collection of equations that hold in the context of e. We write e_{1} ↔ e_{2} to denote that two expressions e_{1} and e_{2} are equal. For example, if f_{0}(x ⊕ y) is unfolded to be expression e as follows:

let v =e_{1} in ( if v =0 then 0 else e_{2} ) end

then I_{[e]} = ∅, I_{[e_{1}]} = ∅, I_{[v=0]} = {v ↔ e_{1}}, and I_{[e_{2}]} = {v ↔ e_{1}, v =0 ↔ F }.

Given an information set at a top-level expression, it is simple to compute information sets at occurrences of subexpressions:

if e is g(e_{1}, ..., e_{n}), where g is a constructor or a (primitive) function, then I_{[e_{i}]} = I_{[e]} for i=1..n; if e is if e_{1} then e_{2} else e_{3}, then I_{[e_{1}]} = I_{[e]}, I_{[e_{2}]} = I_{[e]} ∪ {e_{1}↔T }, and I_{[e_{3}]} = I_{[e]} ∪ {e_{1}↔F }; if e is let v =e_{1} in e_{2} end, then I_{[e_{1}]} = I_{[e]}, and I_{[e_{2}]} = I_{[e]} ∪ {v↔e_{1}}.

An underlying logic L_{0} is used to make inferences based on the facts in an information set. We require that L_{0} be compatible with the semantics of the programming language we are using [14], i.e., if two expressions are proved to be equal under L_{0}, then they compute the same value. In this paper, we assume that a theorem prover based on L_{0} is available, and we write e_{1} ↔_{I}^{∗} e_{2} to denote that a finite proof that e_{1} equals e_{2} can be found by the theorem prover using equations in set I.

Simplification. We can simplify expressions using information sets and the underlying logic, as summarized in Figure 3. Given an expression e and an information set I, we say e can be simplified under I to e′ if the corresponding condition cond(I) holds.

expression e  expression e′  condition cond(I)
v  c  v ↔_{I}^{∗} c
c(e_{1}, ..., e_{n})  e_{c}  \begin{matrix}e ↔_{I}^{∗} c(c_{1}^{−1}(e_{c}), ..., c_{n}^{−1}(e_{c})) \\ and t(e_{c})≤t(e) \end{matrix}
p(e_{1}, ..., e_{n}) e_{p}

e can be simplified to e_{p} under I using properties of p

f(e_{1}, ..., e_{n}) \begin{matrix}e_{f}[e_{1}/v_{1}, \\ ... , \\ e_{n}/v_{n}] \end{matrix} e can be unfolded under I and f is defined as f(v_{1},...,v_{n})=e_{f}

e_{2}  e_{1} ↔_{I}^{∗} T
if e_{1} then e_{2} else e_{3}  e_{3}  e_{1} ↔_{I}^{∗} F
e_{2} (or e_{3}) \begin{matrix}e_{2} ↔_{I}^{∗} e_{3} and \\ t(e_{2})≤t(e_{3}) (or t(e_{3})≤t(e_{2})) \end{matrix}

let v =e_{1} in e_{2} end \frac{e_{2}[v_{1}/v]}{e_{2}[e_{1}/v]} (e_{1} ↔_{I}^{∗} v_{1}) / (e can be unfolded under I)

Figure 3: Simplification

Basically, the simplification is as conventional, except with the identity relation generalized everywhere to the equality under I relation. Simplification of a function application f(e_{1}, ..., e_{n}) unfolds the application if the resulting expression (or its context) can be computed as least as fast (through appropriate simplification corresponding to the context). To automate this in practice, heuristic conditions such as the following are used:

1) f is not recursively defined, and unfolding f(e_{1}, ..., e_{n}) does not duplicate non-trivial computations, i.e., for each i, either t(e_{i}) ≤ t(v_{i}) or v_{i} occurs at most once on every (syntactic) execution path in e_{f}.

2) f(e_{1}, ..., e_{n}) is an argument to a primitive function p, and this application of p can be simplified after unfolding f using properties of p.

Simplification of a binding expression let v = e_{1} in e_{2} end unfolds it to e_{2}[v_{1}/v] if e_{1} equals a variable v_{1} under I. Otherwise, it treats the expression as f(e_{1}), with f defined by f(v)=e_{2}.

Given an expression e and an information set I, we define Simp[[e]]I to be e′ if e can be simplified under I to e′, and e otherwise.

4.2 Cache Sets and Replacement

A cache set C for an unfolded application is a set of tuples ⟨e_{1}, e_{2}, I⟩ such that

1) expression e_{1} depends only on x, expression e_{2} depends only on r, and,

2) if the equations in information set I hold, then e_{1} and e_{2} compute the same value.

For example, if f_{0}(x ⊕ y) is unfolded to be e, then the initial cache set for e is {⟨f_{0}(x), r, ∅⟩}.

Intuitively, an element ⟨e_{1}, e_{2}, I⟩ in a cache set C says that if the equations in I hold, then the value of e_{1} can be retrieved from a cached result by computing e_{2}. Given a cache set and an occurrence of an expression e with information set I_{[e]}, we can extend the cache set at e under I_{[e]}. This extension requires techniques for discovering more expressions whose values can be retrieved from cached results, i.e., discovering incrementality, as described below.

Discovering Incrementality. The schematic diagrams of Figure 4 help explain the basic ideas. The leftmost rectangle depicts the expanded computation of f_{0}(x ⊕ y). Clearly, if f_{0}(x) occurs anywhere as a

f_{0}(x ⊕ y) ; ⋮ ; f_{0}(x) ; ⋮ ; g(e_{1}) I_{1} ; : ; e_{1} I_{1} ; ⋮ ; h(e_{2}) I_{2} ; :  \begin{matrix}f_{0}(x)  I_{1} ; g(e_{1}) = r \\ e_{1} = g^{−1}(r) \end{matrix}  \begin{matrix}h(f_{0}(x)) I_{2}∪\{h(e_{2})↔T \} ; T = h(r) \\ h(f_{0}(x)) I_{2}∪\{h(e_{2})↔F \} ; F = h(r) \end{matrix}

Figure 4: Discovering incrementality

subcomputation, then its value can be straightforwardly retrieved from r. However, we seek to discover other subcomputations whose values can also be retrieved from r. Suppose g(e_{1}) occurs somewhere as a subcomputation and it is not f_{0}(x). If we collect the context information I_{1} at the occurrence of g(e_{1}), and find that f_{0}(x) can be specialized to g(e_{1}) under I_{1}, as depicted in the middle rectangle, then the value of g(e_{1}) at the occurrence can also be retrieved from r. Moreover, if g is a function with an inverse g^{−1}, then the value of e_{1} can be retrieved from g^{−1}(r), wherever I_{1} holds. In a special situation, suppose h(e_{2}) occurs as a subcomputation but neither h(e_{2}) nor e_{2} is f_{0}(x), g(e_{1}), or e_{1}. If h is a Boolean valued function defined on all inputs, and h(f_{0}(x)) can be specialized to true (false) when h(e_{2}) equals true (false), as depicted in the right rectangles, then the value of h(e_{2}) can be retrieved from h(r).

The specializations shown in the middle and right rectangles in Figure 4 employ an auxiliary specializer G. Given an expression e and an information set I, G[[e]]I specializes e under I, and whenever e computes a value, G[[e]]I computes the same value. The specialization is achieved by unfolding and simplification, and will be defined at the end of this section. Here, we use G as a subroutine to help discover more subcomputations whose values can be retrieved from cached results.

We formalize the basic ideas as follows. Given a cache set C and an occurrence of an expression e with information set I_{[e]}, we can extend C at e under I_{[e]} to be C(C, e, I_{[e]}), where C(C, e, I) is called the closure of C at e under I and is defined as follows. Given C, e, and I, let

\begin{matrix}F_{1}(C) = \{⟨e′_{1}, & e_{2}, & I⟩ | & ⟨e_{1}, e_{2}, I′⟩ ∈C, I ⇒ I′, G[[e_{1}]]I =e′_{1}\}, \\ F_{2}(C) = \{⟨e′_{1}, & g^{−1}(e_{2}), & I⟩ | & ⟨e_{1}, e_{2}, I′⟩ ∈C, I ⇒ I′, e_{1} =g(e′_{1})\}, and \\ F_{3}(C) = \{⟨ e, & h(e_{2}), & I⟩ | & ⟨e_{1}, e_{2}, I′⟩ ∈C, I ⇒ I′, G[[h(e_{1})]](I ∪\{e↔\begin{matrix}T \\ F \end{matrix}\}) =\begin{matrix}T \\ F \end{matrix}\}, \end{matrix}  (4)

where g is a constructor or primitive function that has a known inverse g^{−1}, and h is a Boolean valued function defined on all inputs. Note that g and h can be straightforwardly generalized to include functions with two or more parameters. As a particular example for F_{2}, if e_{1} = c(e′_{1}, ..., e′_{n}), then ⟨e′_{i}, c_{i}^{−1}(e_{2}), I⟩ ∈ F_{2}(C) for i = 1..n. Just as F_{2}(C) extends C when e_{1} is a constructor or a special primitive function application, the following sets extend C when e_{1} is a binding expression or a special conditional expression:

F_{21}(C) = {⟨e′′_{2}, e_{2}, I⟩ | ⟨let v = e′_{1} in e′_{2} end, e_{2}, I′⟩ ∈C, I ⇒ I′, e′_{2}[e′_{1}/v] = e′′_{2}},
F_{22}(C) = {⟨e′_{3}, e_{2}, I⟩ | ⟨if e′_{1} then e′_{2} else e′_{3}, e_{2}, I′⟩ ∈C, I ⇒ I′, G[[e′_{3}]](I ∪{e′_{1}↔T }) = e′_{2}},
F_{23}(C) = {⟨e′_{2}, e_{2}, I⟩ | ⟨if e′_{1} then e′_{2} else e′_{3}, e_{2}, I′⟩ ∈C, I ⇒ I′, G[[e′_{2}]](I ∪{e′_{1}↔F }) = e′_{3}}.

(5)

We let F_{2}(C) also include the elements in these sets, and define C(C, e, I) to be C ∪ C′ ∪ F_{3}(C ∪ C′), where C′ is the least set such that F_{1}(C) ⊆ C′ and F_{2}(C′) ⊆ C′.

The set C′ can be computed using a worklist algorithm. First, initialize C′ to be ∅ and worklist L to be F_{1}(C). Then, repeatedly move any element ⟨e_{1}, e_{2}, I′⟩ from L to C′ and, if e_{1} is g(e′_{1}), add ⟨e′_{1}, g^{−1}(e_{2}), I′⟩ into L, if e_{1} is let v = e′_{1} in e′_{2} end, add ⟨e′_{2}[e′_{1}/v], e_{2}, I′⟩ into L, etc. This stops when L is empty, at which time we have obtained the final set C′. Optimizations to the computation of the closure are possible. For example, we can group elements that have the same information sets into units, and maintain a tree of these units so that, if I_{1} ⇒ I_{2}, then the unit with I_{1} is a descendent of the one with I_{2}. Every time we compute the closure, we only need to look at elements in the units that are closest to the leaves and whose information sets are implied by the current information set.

Example. Using the example in Figure 1, let e be the unfolded application of out(C, insert(i, a, R))

if null(C) then nil

else cons(row(car(C), insert(i, a, R)), out(cdr(C), insert(i, a, R))) (6)

with information set I_{[e]} = ∅ and initial cache set C_{out} = {⟨out(C,R), r, ∅⟩}.

Let e_{1} be the false branch of e. Given C_{out} = {⟨out(C,R), r, ∅⟩}, consider extending C_{out} at e_{1} with I_{[e_{1}]} ={null(C)↔F }. Specializing out(C, R) under I_{[e_{1}]}, we get the expression e_{2} below:

cons(row(car(C), R), out(cdr(C), R))  (7)

Thus,

C(C_{out}, e_{1}, I_{[e_{1}]}) = C_{out} ∪ {⟨e_{2}, r, I_{[e_{1}]}⟩, ⟨row(car(C),R), car(r), I_{[e_{1}]}⟩, ⟨out(cdr(C),R), cdr(r), I_{[e_{1}]}⟩}. (8)

Given C_{out} ={⟨out(C,R), r, ∅⟩}, consider extending C_{out} at the Boolean subexpression null(C) in e with I_{[null(C)]} = ∅. When null(C)↔T holds, out(C, R) is specialized to nil and thus null(out(C, R)) equals T; when null(C)↔F holds, out(C, R) is specialized to e_{2} and thus null(out(C, R)) equals F. Thus

C(C_{out}, null(C), ∅) = C_{out} ∪ {⟨null(C), null(r), ∅⟩}.  (9)

Replacement. We say that expression e can be replaced by e′ under I and C, denoted as e →_{IC}^{∗} e′, if

( ∃⟨e_{1}, e′, I_{1}⟩ ∈ C) [ e ↔_{I}^{∗} e_{1} ∧ I ⇒ I_{1} ∧ t(e′) ≤ t(e) ].

Given a non-conditional and non-binding expression e, an information set I, and a cache set C, if e can be replaced by e′ under I and C, then we do so. Otherwise, we extend the cache set to be C(C, e, I), and, if e can be replaced by e′′ under I and the extended cached set C(C, e, I), then we do so. As a result, the cache set may be extended as a side effect of a replacement. We define a function Repl for replacement as follows:

Repl[[e]]IC = \{ \begin{matrix}⟨e, C⟩ & if e is a conditional or binding expression \\ ⟨e′, C⟩ & else if e →_{IC}^{∗} e′ \\ ⟨e′′, C′⟩ & else if e →_{IC′}^{∗} e′′, where C′ = C(C, e, I) \\ ⟨e, C′⟩ & otherwise, where C′ is as above \end{matrix}  (10)

Another use of a cache set for replacement is as follows. Suppose an expression e can not be replaced by any expression under I and C, but

∃ ⟨if e_{1} then e_{2} else e_{3}, e_{4}, I_{1}⟩ ∈ C, I ⇒ I_{1}

such that e can be replaced by e_{T} (respectively, e_{F}) under I ∪{e_{1}↔T } (respectively, I ∪{e_{1}↔F }) and the correspondingly extended cache set. Then we can replace e by if e_{1}then e_{T} else e_{F} provided t(if e_{1}then e_{T} else e_{F}) ≤t(e). For example, if e is e_{3}, and e_{1} takes unit time, then we can replace e by if e_{1}thene elsee_{4}. We extend the function Repl for replacement to include this case, i.e., we replace the last case of (10) by the following two cases:

\begin{cases}⟨if e′_{1} then e_{T} else e_{F} , C′′′⟩ \\ if ∃ ⟨if e_{1} then e_{2} else e_{3}, e_{4}, I_{1}⟩ ∈ C′, I ⇒ I_{1}, t(if e′_{1} then e_{T} else e_{F}) ≤ t(e) \\ where & e′_{1} = \{ \begin{matrix}e′′_{1} & if e_{1} →_{IC′′}^{∗} e′′_{1} \\ e_{1} & otherwise \end{matrix} , where C′′ = C(C′, e_{1}, I) e_{B} =\{ \begin{matrix}e′_{B} & if e →_{I_{B}C′′′}^{∗} e′_{B} \\ e & otherwise \end{matrix}, where I_{B} = I ∪ \{e′_{1}↔B\}, for B = T, F C′′′ = C(C′′, e, I_{T}) ∪ C(C′′, e, I_{F}) \\ ⟨e, C′′′⟩ otherwise, where C′′′ is as above \end{cases} (11)

4.3 Incrementalization Using Simplification and Replacement

To incrementalize an unfolded application, a function Inc applies simplification and replacement on subexpressions in applicative order. The cache set for the current unfolded application may be extended as a side effect of replacement using Repl. In particular, Inc calls IncApply to consider subexpressions that are function applications. The global set of introduced functions may be extended as a side effect of using IncApply.

We refer to the application of simplification and replacement by Inc as reduction. Thus Inc does innermost leftmost reduction. If a subexpression is reduced to a conditional expression, then the condition is lifted out of the enclosing expression. Similarly, if a subexpression is reduced to a binding expression, then the binding is lifted. A function Subl is used by Inc to recursively reduce subexpressions and perform necessary lifting, as defined in Figure 5.

The presentation of Subl is simplified by omitting detailed control structures that sequence Subl through its subexpressions. We just present the case of Subl working on the ith subexpression of the top-level construct and condition it on that the subexpressions 1 through i − 1 have been reduced. Operationally, we say that a subexpression is reduced, if it is the result of having already applied Inc for the subexpression at that position; otherwise, it is not reduced. For a conditional expression if e_{1}then e_{2} else e_{3}, Inc reduces e_{2} (respectively, e_{3}) with the assumption that e_{1} equals true (respectively, false) added into the information set.

Name  Transformation  Condition

(g) Subl[[g(e_{1}, ..., e_{n})]] I C D where g is c, p, or f (g_{i}) = Subl[[g(e_{1}, ..., e_{i−1}, e′_{i}, e_{i+1}, ..., e_{n})]] I C′ D′ if e_{1}, ..., e_{i−1} are reduced, not if or let, but

where ⟨e′_{i}, C′, D′⟩ = Inc[[e_{i}]] I C D e_{i} is not reduced

(g_{i−if}) = Subl[[if e′_{1} then g(e_{1}, ..., e_{i−1}, e′_{2}, e_{i+1}, ..., e_{n}) if e_{1}, ..., e_{i−1} are reduced, not if or let,

else g(e_{1}, ..., e_{i−1}, e′_{3}, e_{i+1}, ..., e_{n})]] I C D e_{i} is reduced, but e_{i} is if e′_{1} then e′_{2} else e′_{3}

where e′_{1} is reduced and is not if or let

(g_{i−let}) = Subl[[let v =e′_{1} in g(e_{1}, ..., e_{i−1}, e′_{2}, e_{i+1}, ..., e_{n}) end]] I C D if e_{1}, ..., e_{i−1} are reduced, not if or let,

where e′_{1} is reduced and is not if or let e_{i} is reduced, but e_{i} is let v =e′_{1} in e′_{2} end

(g_{n}) = ⟨g(e_{1}, ..., e_{n}), C, D⟩ otherwise (if) Subl[[if e_{1} then e_{2} else e_{3}]] I C D (if_{1}) = Subl[[if e′_{1} then e_{2} else e_{3}]] I C′ D′ if e_{1} is not reduced

where ⟨e′_{1}, C′, D′⟩ = Inc[[e_{1}]] I C D

(if_{1−if}) = Subl[[if e′_{1} then (if e′_{2} then e_{2} else e_{3}) if e_{1} is reduced, and e_{1} is if e′_{1} then e′_{2} else e′_{3}

else (if e′_{3} then e_{2} else e_{3})]] I C D

where e′_{1} is reduced and is not if or let

(if_{1−let}) = Subl[[let v =e′_{1} in (if e′_{2} then e_{2} else e_{3}) end]] I C D if e_{1} is reduced, and e_{1} is let v =e′_{1} in e′_{2} end

where e′_{1} is reduced and is not if or let

(if_{n}) = ⟨if e_{1} then e′_{2} else e′_{3}, C′′, D′′⟩ otherwise

where ⟨e′_{2}, C′, D′ ⟩ = \begin{cases}⟨e_{2}, C, D⟩ & if e_{1}↔_{I}^{∗}F \\ Inc[[e_{2}]] (I ∪\{e_{1}↔T \}) C D & otherwise \end{cases} ⟨e′_{3}, C′′, D′′⟩ = \begin{cases}⟨e_{3}, C′, D′⟩ & if e_{1}↔_{I}^{∗}T \\ Inc[[e_{3}]] (I ∪\{e_{1}↔F \}) C′ D′ & otherwise \end{cases}

(let) Subl[[let v =e_{1} in e_{2} end]] I C D (let_{1}) = Subl[[let v =e′_{1} in e_{2} end]] I C′ D′ if e_{1} is not reduced

where ⟨e′_{1}, C′, D′⟩ = Inc[[e_{1}]] I C D

(let_{1−if}) = Subl[[if e′_{1} then (let v =e′_{2} in e_{2} end) if e_{1} is reduced, and e_{1} is if e′_{1} then e′_{2} else e′_{3}

else (let v =e′_{3} in e_{2} end)]] I C D

where e′_{1} is reduced and is not if or let

(let_{1−let}) = Subl[[let v′ =e′_{1} in (let v =e′_{2} in e_{2} end) end]]I C D if e_{1} is reduced, and e_{1} is let v′ =e′_{1} in e′_{2} end

where e′_{1} is reduced and is not if or let

(let_{n}) = ⟨let v =e_{1} in e′_{2} end, C′, D′⟩ otherwise

where ⟨e′_{2}, C′, D′⟩ = Inc[[e_{2}]] (I ∪{v↔e_{1}}) C D

Figure 5: Definition of Subl Similarly, for a binding expression let v =e_{1}in e_{2} end, Inc reduces e_{2} with the assumption that v equals e_{1} added into the information set. At the end, all subexpressions are reduced with necessary lifting performed.

Finally, we define the function Inc as in (12), where I^{C} denotes the set I ∪{e_{1}↔e_{2} | ⟨e_{1}, e_{2}, I′⟩∈C, I ⇒I′}. We need I^{C} instead of I because Inc does applicative order reduction, during which some subexpressions may be replaced by retrievals, and thus the equations in I may involve the cache parameter. As a result, the underlying logic needs to know the equality relation involving the cache parameter to make inferences. For example, to reduce the expression e in (6), first null(C) is reduced to null(r) according to (9), and thus I_{[e_{1}]} ={null(r)↔F } for the expression e_{1} in the false branch of e. Now to specialize out(C, R) at e_{1}, we use the information set {null(r)↔F } ∪ {null(x)↔null(r)}, and we obtain the same expression as in (7).

Inc[[e]]ICD = ⟨e′′′, C′′, D′′⟩, where ⟨e′′′, C′′⟩ = Repl[[Simp[[e′′]]I^{C′}]]I^{C′}C′ ⟨e′′, D′′⟩ = \{ \begin{matrix}IncApply[[e′]]I^{C′}C′D′ & if e′ is f(e_{1}, ..., e_{n}) \\ ⟨e′, D′⟩ & otherwise \end{matrix} ⟨e′, C′, D′⟩ = \{ \begin{matrix}Subl[[e]]ICD & if e is not v \\ ⟨e, C, D⟩ & otherwise \end{matrix}  (12)

The function Inc proceeds as follows. First, if an expression e has subexpressions, then Inc calls Subl to recursively reduce the subexpressions in turn. The cache set and definition set may be changed while reducing subexpressions. Then if the resulting expression is a function application, Inc calls IncApply and aims to replace the application with an application of an introduced function that computes incrementally. The definition set may be changed by IncApply. Finally, Inc uses Simp to simplify the top-level expression, and then calls Repl to replace the resulting expression by a retrieval from a cached result, if possible. The cache set may be changed by Repl.

Auxiliary Specializer. The auxiliary specializer G is defined in a way similar to Inc, but is much simpler. It simplifies subexpressions in applicative order and lifts conditions and bindings as Inc does, but there are no cache sets or definitions sets involved. If simplification of a function application unfolds the application, then G is applied to the unfolded application. Let Subl′ be Subl except that Subl′ takes only an expression and an information set as arguments, returns only an expression, and calls G instead of Inc. Then G is defined as follows:

G[[e]]I = \{ \begin{matrix}G[[e′′]]I & if e′ is f(e_{1}, ..., e_{n}) and e′′ ≠ e′ \\ e′′ & otherwise \end{matrix}, where e′′ = Simp[[e′]]I e′ = \{ \begin{matrix}Subl′[[e]]I & if e is not v \\ e & otherwise \end{matrix}  (13)

5 Manipulating Recursive Function Applications

We define the definition set, which is a global set of functions introduced during the derivation procedure to compute function applications incrementally. We describe how to maintain the definition set when introducing functions and how to use the introduced functions to replace appropriate function applications.

5.1 Definition Set

The definition set D is a set of tuples ⟨f(e_{1}, ..., e_{n}), f′(v_{1}, ..., v_{k}), C⟩, where C is a single-element cache set {⟨e_{c}, e_{r}, I⟩}, such that

1) f is a function in the original set F, expressions e_{1}, ..., e_{n} depend on x and possibly on y, f′ is a new function introduced in the set D, and v_{1}, ..., v_{k} are variables in e_{1}, ..., e_{n}, e_{c}, and e_{r},

2) if the cache set C is valid, i.e., the equations in the information set I hold, and e_{c} = e_{r}, then whenever f(e_{1}, ..., e_{n}) terminates with a value, f′(v_{1}, ..., v_{k}) terminates with the same value, and 3) a definition of f′ is obtained by incrementalizing the unfolded f(e_{1}, ..., e_{n}) using I and C, and some of the parameters of f′ may be dead and eliminated after the incrementalization.

For example, given out(C, R) = r with empty information set at the initial application out(C, insert(i, a, R)), we introduce a new function out′, and we get the initial definition set

{⟨out(C, insert(i, a, R)), out′(C, i, a, R, r), {⟨out(C, R), r, ∅⟩}⟩}  (14)

where a definition of out′ is to be obtained by incrementalizing the unfolded out(C, insert(i, a, R)) using out(C, R) = r.

Intuitively, an element in the definition set D says that a new function f′ is introduced such that, if the equations in the information set I hold, and the value of e_{c} can be retrieved from a cached result by computing e_{r}, then f′(v_{1}, ..., v_{k}) computes f(e_{1}, ..., e_{n}) incrementally. To obtain a definition of f′, we unfold f(e_{1}, ..., e_{n}), incrementalize the unfolded application using the sets I and C, and then eliminate dead parameters. While we incrementalize the unfolded f(e_{1}, ..., e_{n}), we may encounter other function applications before we obtain a final definition of f′. We say f′ is fully defined if, for every introduced function g′ in D that f′ (transitively) depends on, a final definition of g′ has been obtained.

Note the restriction that the cache set C contains only one element, which reflects our main heuristic for introducing new functions. In general, a function application has its context information set and a current cache set. Any element in these sets might be used in incrementalizing the unfolded application. But we do not know a priori, before examining the unfolded application, what elements are used and how. Therefore, any dynamic decision must be an approximation. Our one-cache-element heuristic is based on the observation that, in a well-structured program, a function application is expected to be computed incrementally based on the cached result of a corresponding previous computation. As a consequence of our way of choosing the single cache element, as described below, there is only one variable in the expression e_{r}. This variable depends on r and is introduced as a parameter of f′. We call it the current cache parameter during the process of incrementalizing the unfolded f(e_{1}, ..., e_{n}).

A function f may correspond to multiple introduced functions, since there may be multiple occurrences of applications of f during the derivation, and different applications may correspond to different introduced functions.

5.2 Generalization for Function Introduction

Given a function application f(e_{1}, ..., e_{n}), let I be the information set at f(e_{1}, ..., e_{n}), and C the current cache set for the unfolded application that contains f(e_{1}, ..., e_{n}). To introduce a function f′ to compute f(e_{1}, ..., e_{n}) incrementally, the main task is to decide, based on I and C, a valid and relevant cache element that is to be used to incrementalize the computation of f(e_{1}, ..., e_{n}). An interaction with this comes from using a version of generalization that enables f′ to be used in more general settings and, at the same time, does not impede the discovery of incrementality.

Considerations. Our use of generalization ignores substructures of expressions to introduce functions for more general uses. For example, consider the function application

row(car(C), insert(i, a, R)) with ⟨row(car(C), R), car(r), {null(C)↔F }⟩ ∈ C_{out}  (15)

and I = {null(C) ↔ F } in the false branch of (6). Instead of introducing

⟨row(car(C), insert(i, a, R)), row′(C, i, a, R, r), {⟨row(car(C), R), car(r), {null(C)↔F }⟩}⟩  (16)

and replacing the application by row′(C, i, a, R, r), we introduce

⟨row(c, insert(i, a, R)), row′(c, i, a, R, r_{1}), {⟨row(c, R), r_{1}, I′⟩}⟩  (17)

where I′ = {null(C) ↔ F, car(C) ↔ c}, and replace the application by row′(car(C), i, a, R, car(r)). We say that c generalizes car(C), and r_{1} generalizes car(r). Obviously, the latter row′ is more general than the former and can be used in more general settings.

Basically, the largest common super-expression of all occurrences of a variable is generalized by a single (new) variable. However, there are two considerations. First, generalization should not impede the discovery of incrementality. For example, if we consider row(car(C), insert(i, a, R)) in (15), then insert(i, a, R) is not generalized by a variable, since we want to separate subcomputations depending only on x from the rest so that the former can possibly be replaced by retrievals. Therefore, one guideline is to generalize as much as possible, but not cross the boundary between subexpressions depending only on x and the rest.

The second consideration is associated with the main task of deciding a valid and most relevant cache element to be used to incrementalize the computation of f(e_{1}, ..., e_{n}). For example, among the valid cache elements in (8), the element in (15) is used to incrementalize row(car(C), insert(i, a, R)). To arrive at this choice, consider row(car(C), insert(i, a, R)) together with the two expressions in a cache element. With the element in (15), we can generalize more than with any other element in (8). Also, the information set becomes I′, as in (17), since it relates I with the new variable c. Therefore, the guideline is to generalize the function application together with the two expressions in each valid cache element, choose the element that allows most generalization, and relate the information set with the new variables.

To summarize, our use of generalization does not impede the discovery of incrementality and helps obtain the most relevant cache element. We should note that these are online techniques for the generalization.

Generalization. We present the above ideas formally as follows. Given expressions e_{1}, ..., e_{m}, let u_{1}, ..., u_{k} be all the variables in them. Let {u_{l}, u_{j_{1}}, ..., u_{j_{h}}} ⊆ {u_{1}, ..., u_{k}} but u_{l} ∉ {u_{j_{1}}, ..., u_{j_{h}}}. An expression e is the largest common u_{l}\{u_{j_{1}}, ..., u_{j_{h}}}-cover expression of e_{1}, ..., e_{m} if e is the largest common super-expression of all occurrences of u_{l} in the e_{i}’s, such that u_{j_{1}}, ..., u_{j_{h}} do not appear in e.

Given f(e_{1}, ..., e_{n}) with I and C, suppose u^{r} is the current cache parameter. Let u_{1}, ..., u_{m} be all the variables other than u^{r} in e_{1}, ..., e_{n}. Let u_{1}^{x}, ..., u_{p}^{x} be those u_{i}’s that depend only on x, and u_{1}^{y}, ..., u_{q}^{y} be the rest of u_{i}’s. Let ⟨e_{c}, e_{r}, I_{1}⟩ be any element in C such that I ⇒I_{1} and all the variables in e_{c} are in {u_{1}^{x}, ..., u_{p}^{x}}, and thus the element is valid and relevant.

Let E be a set of non-overlapping expressions e such that e is the largest common u^{r}\{u_{1}, ..., u_{m}}-cover or u_{j}^{x}\{u^{r}, u_{1}^{y}, ..., u_{q}^{y}}- or u_{k}^{y}\{u^{r}, u_{1}^{x}, ..., u_{p}^{x}}-cover expression of e_{1}, ..., e_{n}, e_{c}, and e_{r} for some u_{j}^{x} or u_{k}^{y}. Let

θ = {e/v | e ∈ E}  (18)

where v’s are distinct new variable names,^{2} then θ is a substitution corresponding to these largest common cover expressions of e_{1}, ..., e_{n}, e_{c}, and e_{r}. Using the inverse substitution θ^{−1} = {v/e | e/v ∈ θ}, we obtain e′_{1}, ..., e′_{n}, e′_{c}, and e′_{r} such that e′_{i} = e_{i}θ^{−1} for i = 1, ..., n, c, r, and we obtain an information set I′ such that I′ is Iθ^{−1} extended with equations induced by θ that are relevant to Iθ^{−1}, i.e.,

I′ =Iθ^{−1} ∪ {e↔v | e/v ∈ θ, a variable in e occurs in Iθ^{−1}}.

We say that ⟨e′_{1}, ..., e′_{n}, e′_{c}, e′_{r}, I′⟩ is a generalization for ⟨f(e_{1}, ..., e_{n}), I, C⟩ with substitution θ. For any e/v in θ, we say variable v generalizes expression e. It is clear that such a generalization obeys the first consideration.

A tuple ⟨f(e_{1}, ..., e_{n}), I, C⟩ may have more than one generalization if there are more than one element in C or there are more than one set of non-overlapping largest common covers for a cache element. Suppose A_{1} and A_{2} are two generalizations with substitutions θ_{1} and θ_{2}, respectively. We say A_{1} is more general than A_{2} if every expression in {e | e/v ∈ θ_{2}} is a subexpression of some expression in {e | e/v ∈ θ_{1}}. We say A_{1} is most general if no other generalization is more general. This incorporates the second consideration.

2If an expression e in the set E is a variable u, then the corresponding variable v can be u, i.e., v does not have to be a new variable in this case.

5.3 Function Introduction and Replacement

Given a function application f(e_{1}, ..., e_{n}), let I be the information set at f(e_{1}, ..., e_{n}), C the current cache set for the unfolded application that contains f(e_{1}, ..., e_{n}), and D the current definition set. If we can use a previously introduced function f′ in D to compute f(e_{1}, ..., e_{n}) incrementally, then f(e_{1}, ..., e_{n}) is replaced by an application of f′. Otherwise, we introduce a new function f′ into D to compute f(e_{1}, ..., e_{n}) incrementally and, if f′ computes fast, replace f(e_{1}, ..., e_{n}) by an application of this f′, otherwise, leave f(e_{1}, ..., e_{n}) unchanged; as a result, the definition set is changed as a side effect. This process is achieved by IncApply, first introduced in Section 3. It is defined in Figure 6 and explained below.

IncApply[[f(e_{1}, ..., e_{n})]] I C D = ⟨f′(v_{i_{1}}θ, ..., v_{i_{j}} θ), D⟩ if ∃ ⟨f(e′_{1}, ..., e′_{n}), f′(v_{i_{1}}, ..., v_{i_{j}}), {⟨e′_{c}, e′_{r}, I′⟩}⟩ ∈ D with a substitution θ s.t.

f(e_{1}, ...., e_{n}) ↔_{I}^{∗} f(e′_{1}θ, ..., e′_{n}θ), I ⇒ I′θ, e′_{c}θ →_{IC}^{∗} e′_{r}θ, and

if f′ is fully defined, t(f′(v_{i_{1}}θ, ..., v_{i_{j}} θ)) ≤ t(f(e_{1}, ..., e_{n}));

= ⟨f′(v_{i_{1}}θ, ..., v_{i_{j}} θ), D′′′⟩ else if f(e_{1}, ..., e_{n}) depends on x but can not be replaced by a retrieval, and, after obtaining a definition of f′ as follows, if f′ is fully defined, t(f′(v_{i_{1}}θ, ..., v_{i_{j}} θ)) ≤ t(f(e_{1}, ..., e_{n})); introduce d=⟨f(e′_{1}, ..., e′_{n}), f′(v_{1}, ..., v_{k}), C′⟩ with θ, where C′={⟨e′_{c}, e′_{r}, I′⟩}, and obtain f′(v_{i_{1}}, ..., v_{i_{j}}), to be defined as some e′′′, by the following steps:

1) e′ = e[e′_{1}/v_{1}, ..., e′_{n}/v_{n}], where f is defined by f(v_{1}, ..., v_{n}) = e

2) ⟨e′′, C′′, D′′⟩ = Inc[[e′]] I′ C′ D′, where D′ = D ∪ {d}

3) ⟨f′(v_{i_{1}}, ..., v_{i_{j}}), D′′′⟩ = Elim[[f′(v_{1}, ..., v_{k})]] D′′, where f′(v_{1}, .., v_{k}) is defined as e′′

= ⟨f(e_{1}, ..., e_{n}), D′′′′⟩ otherwise, where D′′′′ is D′′′ as above if it is computed and D otherwise

Figure 6: Definition of IncApply

Function Replacement. Since an introduced function f′ is associated with a cache element as an invariant, to use f′, we need to justify the corresponding invariant. We say that a function application f(e_{1}, ..., e_{n}) with I, C, and D can be replaced by an application of a previously introduced function f′ if there is ⟨f(e′_{1}, ..., e′_{n}), f′(v_{i_{1}}, ..., v_{i_{j}}), {⟨e′_{c}, e′_{r}, I′⟩}⟩ in D and there is a substitution θ over the variables in e′_{1}, ..., e′_{n}, e′_{c}, e′_{r}, and I′ such that

1) f(e_{1}, ..., e_{n}) equals f(e′_{1}θ, ..., e′_{n}θ), the invariant I′θ holds, e′_{c}θ can be replaced by e′_{r}θ, and
2) if f′ is fully defined, f′(v_{i_{1}}θ, ..., v_{i_{j}}θ) is asymptotically at least as fast as f(e_{1}, ..., e_{n}).

In this case, f(e_{1}, ..., e_{n}) can be replaced by f′(v_{i_{1}}θ, ..., v_{i_{j}}θ), and the definition set D remains unchanged. For example, given the definition set (14), the application

out(cdr(C), insert(i, a, R)), with ⟨out(cdr(C), R), cdr(r), {null(C)↔F }⟩ ∈ C_{out}  (19)

in the false branch of (6) can be replaced by out′(cdr(C), i, a, R, cdr(r)).

Function Introduction. If f(e_{1}, ..., e_{n}) with I, C, and D can not be replaced by an application of a previously introduced function in D, then we introduce a new function f′ into D to compute f(e_{1}, ..., e_{n}) incrementally. Following the basic derivation idea, we introduce f′ only if f(e_{1}, ..., e_{n}) depends on x but can not be replaced by a retrieval from a cached result.

Given f(e_{1}, ..., e_{n}) with I and C, let ⟨e′_{1}, ..., e′_{n}, e′_{c}, e′_{r}, I′⟩ be a most general generalization with substitution θ. Let v_{1}, ..., v_{k} be all the variables in e′_{1}, ..., e′_{n}, e′_{c}, and e′_{r}. We introduce ⟨f(e′_{1}, ..., e′_{n}), f′(v_{1}, ..., v_{k}), C′⟩, where C′ = {⟨e′_{c}, e′_{r}, I′⟩}, into D to get D′, and we obtain a definition of f′ by the following three steps:

1) unfold the application f(e′_{1}, ..., e′_{n}) to get e′;

2) incrementalize e′ with information set I′, cache set C′, and definition set D′ to get e′′;

3) eliminate dead parameters of f′, defined by f′(v_{1}, ..., v_{k})=e′′, in computing f′(v_{1}, ..., v_{k}).

Note that the second step uses the function Inc, which may use IncApply recursively for function applications. After the third step, if we obtain f′(v_{i_{1}}, ..., v_{i_{j}}) and, if f′ is fully defined, t(f′(v_{i_{1}}θ, ..., v_{i_{j}}θ))≤t(f(e_{1}, ..., e_{n})), then we replace f(e_{1}, ..., e_{n}) by f′(v_{i_{1}}θ, ..., v_{i_{j}}θ). The set D is changed as a side effect.

Dead Parameter Elimination. After the second step above, f′(v_{1}, ..., v_{k}) computes f(e′_{1}, ..., e′_{n}) and is defined as e′′. Since e′′ is obtained by replacing some subcomputations of f(e′_{1}, ..., e′_{n}) depending on x by computations depending on the current cache parameter, those parameters of f′ on which the replaced computations depend may become dead.

Dead code elimination is a traditional optimization [1, 24]. We assume a subroutine Elim is given so that Elim[[f′(v_{1}, ..., v_{k})]]D′′, where f′(v_{1}, .., v_{k}) is defined as e′′ in D′′, returns the pair ⟨f′(v_{i_{1}}, ..., v_{i_{j}}), D′′′⟩, where 1 ≤ i_{1} < ... < i_{j} ≤ k and f′(v_{i_{1}}, ..., v_{i_{j}}) is defined as some e′′′ in D′′′ after dead parameter elimination, and f′(v_{i_{1}}, ..., v_{i_{j}}) returns a value if and only if f′(v_{1}, ..., v_{k}) returns the same value.

Example. Consider our running example. For the application row(car(C), insert(i, a, R)) in the false branch of (6), we introduce a new function row′ as in (17). To obtain a definition of row′, we first unfold row(c, insert(i, a, R)) to get

if null(insert(i, a, R)) then nil

else cons(c ∗ car(insert(i, a, R)), row(c, cdr(insert(i, a, R)))) (20)

Then, we incrementalize (20) using row(c, R) = r_{1} as given by the cache set in (17). The incrementalization is sketched as follows. It is easy to see that insert(i, a, R) in the condition can be unfolded and the condition simplified to true, and thus (20) is reduced to

cons(c ∗ car(insert(i, a, R)), row(c, cdr(insert(i, a, R))))  (21)

The first occurrence of insert(i, a, R) in (21) can be unfolded, conditions in the unfolded application lifted, and car of cons applications simplified. Thus, (21) becomes

if i ≤ 1 then cons(c ∗ a, row(c, cdr(insert(i, a, R))))
else if null(R) then cons(c ∗ a, row(c, cdr(insert(i, a, R))))
else cons(c ∗ car(R), row(c, cdr(insert(i, a, R))))

(22)

The three occurrences of insert(i, a, R) in (22) can be specialized under their corresponding contexts, unfolded, and then cdr of cons applications simplified. Thus, (22) becomes

if i ≤ 1 then cons(c ∗ a, row(c, R))
else if null(R) then cons(c ∗ a, row(c, nil))
else cons(c ∗ car(R), row(c, insert(i−1, a, cdr(R))))

(23)

In the first branch of (23), row(c, R) can be directly replaced by r_{1}. In the second branch, row(c, nil) can be specialized and unfolded to nil. For the third branch, we have null(R) ↔ F; thus row(c, R) is specialized to cons(c ∗ car(R), row(c, cdr(R))) and the cache set is extended so that

c ∗ car(R) = car(r_{1}) and row(c, cdr(R)) = cdr(r_{1}).

Thus, c∗car(R) can be replaced by car(r_{1}), and the application row(c, insert(i−1, a, cdr(R))) can be replaced by row′(c, i−1, a, cdr(R), cdr(r_{1})). Additionally, in a situation similar to (9), null(R) can be replaced by null(r_{1}). Thus, (23) is reduced to

if i ≤ 1 then cons(c ∗ a, r_{1})
else if null(r_{1}) then cons(c ∗ a, nil)
else cons(car(r_{1}), row′(c, i−1, a, cdr(R), cdr(r_{1})))

(24)

Finally, for row′(c, i, a, R, r_{1}) defined as (24), it is clear that the parameter R is dead and can be eliminated. We obtain the final definition of row′ as given in Figure 2. The application row(car(C), insert(i, a, R)) can be replaced by row′(car(C), i, a, car(r)), since the latter is asymptotically at least as fast as the former.

To complete our example, for the initial application out(C, insert(i, a, R)), we introduce a new function out′ as in (14). In incrementalizing the unfolded application of out as in (6), the Boolean expression null(C) can be replaced by null(r) due to (9), the application of row can be replaced by row′(car(C), i, a, car(r)) as just given above, and the recursive application of out can be replaced by out′(cdr(C), i, a, R, cdr(r)) as followed from (19). Therefore, the unfolded application (6) is reduced to

if null(r) then nil

else cons(row′(car(C), i, a, car(r)), out′(cdr(C), i, a, R, cdr(r))) (25)

For out′(C, i, a, R, r) defined as (25), it is clear that the parameter R is dead and can be eliminated. We obtain the final definition of out′ as given in Figure 2. Finally, the application out(C, insert(i, a, R)) can be replaced by out′(C, i, a, r), i.e., given out(C, R) = r, out′(C, i, a, r) computes out(C, insert(i, a, R)) and is at least as fast.

6 Summarizing the Derivation Procedure

The derivation procedure can be summarized as follows. The function IncApply maintains the global set D, introduces new functions to compute function applications incrementally, and replaces these applications by appropriate applications of introduced functions. IncApply calls the function Inc, which maintains a cache set C, discovers subcomputations whose values can be retrieved from cached results, and incrementalizes the computation of an unfolded function by simplification and replacement using retrievals. Inc recursively calls IncApply if a subcomputation is a function application. The derivation procedure starts with

IncApply[[f_{0}(x ⊕ y)]] ∅ {⟨f_{0}(x), r, ∅⟩} ∅  (26)

and, if it terminates, returns ⟨f′_{0}(x, y, r), D⟩, where D is the set of functions introduced during the derivation. We can eliminate dead functions in F, the set of functions in the original program, and D that are not reachable from f′_{0} in the call-graph.

The derivation procedure preserves the semantics of programs and achieves at least as fast computations, i.e., if f_{0}(x) = r, then (a) whenever f_{0}(x ⊕ y) returns a value, f′_{0}(x, y, r) returns the same value; and (b) f′_{0}(x, y, r) is asymptotically at least as fast as f_{0}(x ⊕ y). To see this, notice that semantics are preserved and fast computations are achieved by all of the transformations in the derivation procedure — simplification by Simp, computation of cache sets and replacement by Repl, lifting of conditions and bindings by Subl, and function replacement and introduction with generalization by IncApply. Note that unfolding may result in computations that terminate more often than the original computations.

6.1 Transformation and Analysis Techniques Used

The derivation procedure combines a number of program analysis and transformation techniques to achieve the ambitious goal of deriving incremental programs. It is a deterministic transformational procedure.

The transformation starts with f_{0}(x ⊕ y), so that f′_{0} is computable, and aims to improve the efficiency by replacing subcomputations whose values can be retrieved from cached result r of f_{0}(x) by corresponding retrievals. This starting point is similar to that of partial evaluation, which starts with a trivial specialized program given by Kleene’s s-m-n theorem and attempts improvements by symbolic reductions or similar techniques.

Transformation Techniques. We summarize the major transformation techniques used and emphasize how they are combined to achieve our goal.

First, context information is collected for each subcomputation and used to simplify the computation, which mimics the main techniques of generalized partial evaluation [14], where program states are represented symbolically and programs are specialized with the help of a theorem prover. In addition to simplification, context information has another important role in our work, i.e., it serves as keys to cached results and introduced functions for valid replacement to happen.

Second, a cache set is maintained for each unfolded application and used to incrementalize it, i.e., to replace certain subcomputations, under certain context information, by retrievals from a cached result of a previous computation. A cache set is augmented, finitely and in a disciplined way, with the help of an auxiliary specializer so that the cached result is utilized effectively under valid context information. The use of a cached result often suggests memoization [22, 4]. However, the real power of our approach comes from the effective exploitation of a memoized value under valid context information. The approach to be proposed in Section 6.3 for increasing incrementality by caching intermediate results can be regarded as a form of smart memoization.

Third, in consistence with the strict semantics of our language, we apply simplification and replacement on subcomputations in applicative order, and moreover, we lift conditions and bindings out of subcomputations. This lifting technique is similar in spirit to the driving transformation by supercompilation [43]. It causes relatively drastic reorganization of program structures that helps expose incrementality that is otherwise hidden.

Fourth, a global definition set is maintained and used to replace function applications, with corresponding relevant cache elements and valid context information, by applications of introduced functions. Function introduction with generalization and function replacement use the unfold/define/fold scheme [6] in a regulated manner so that the transformations are deterministic and the derived programs do not lose termination. Moreover, relevant cache elements with valid context information are chosen to be passed into introduced functions, so that they can be effectively used to incrementalize the computation of corresponding function applications.

Last, after the replacements described above, we apply dead code elimination, a traditional optimization technique [1, 24]. It is particularly useful here, since replacement changes dependencies between computations, and computations on which no other computations depend are then dead and can be eliminated.

Analysis Techniques. To implement the above transformations, several program analysis techniques are needed and summarized here.

First, time analysis [46, 36] is used when replacing subcomputations by retrievals or replacing function applications by applications of introduced functions.^{3} It is a must if we want to guarantee the efficiency of the derived programs.

Then, a number of analyses [19] are used to assist transforming function applications. Dependence analysis enables us to recognize subcomputations that are possibly computed incrementally, i.e., subcomputations depending on x, and thus avoid introducing functions for function applications that depend only on y, which then helps the derivation procedure terminate. Call-graph analysis tells us whether a function is recursively defined and also whether an introduced function is fully defined. Occurrence counting analysis helps us decide whether an unfolding duplicates computations.

3The minor use of time analysis in assisting some simplifications can be easily avoided.

Finally, dead code analysis recognizes dead code to be eliminated. In particular, dead parameters of functions can be recognized with the help of dependence analysis, and dead functions can be identified with the help of call-graph analysis.

Additionally, other analysis techniques, although not mentioned in our transformations so far, would also benefit the derivation procedure. For example, type analysis would be helpful for simplifying overloaded functions. Also, static analysis could provide annotations that guide the derivation and help it terminate, mimicking binding time analysis in partial evaluation, as discussed below.

Last but not least, we should note that the quality of a derived incremental program depends on the corresponding non-incremental program. We should not expect “genuine creativity” without discoveries and proofs of some “substantial” theorems. On another hand, with the power of our combined techniques, a very simple theorem prover can already help us derive efficient incremental programs. Illustrative examples can be found in Section 7.

6.2 Improving the Derivation Procedure

A number of optimizations can be made to the derivation procedure. An implementer would naturally realize most of them. As an example, assume our replacement guarantees

if Repl[[e]]IC = ⟨e′, C′⟩, then Repl[[e′]]IC′ = ⟨e′, C′⟩,

then we can make the optimization:

Inc[[if e_{1} then e_{2} else e_{3}]]ICD = Inc[[e_{3}]]IC′D′, if Inc[[e_{1}]]ICD = ⟨F, C′, D′⟩.  (27)

A relatively important improvement is with the function introduction for a function application f(e_{1}, ..., e_{n}), as in the second case in Figure 6. While we incrementalize the unfolded application, its cache set is extended from C′ to C′′, but C′′ is discarded after this, even if C′′θ might be used in incrementalizing the rest of the unfolded application that contains f(e_{1}, ..., e_{n}). To make use of C′′ for this purpose, we can let IncApply also return the set C′′θ and merge it with the cache set of the unfolded application that contains f(e_{1}, ..., e_{n}).

Termination. The derivation procedure follows function applications and introduces new functions to compute these applications incrementally. Therefore, if functions are recursively defined, the derivation procedure may not terminate due to introducing infinitely many functions following infinite unfolding. Nontermination is a traditional problem in a transformational approach, and it is well-know that there is a trade-off between termination of the transformation and efficiency of the transformed programs.

In our derivation, we only introduce new functions for function applications that depend on x, which may affect the efficiency of other function applications, but makes the derivation terminate more often without impeding the discovery of incrementality. It is also clear that function replacement and the notion of generalization for function introduction help the derivation terminate in a natural way. However, our heuristic of one cache element per introduced function might impede achieving incrementality, since this element may not be sufficient, i.e., it may not enable all of the simplifications and replacements that are possible when using more cache elements. We could overcome this by using as many cache elements as possible when introducing a function and eliminating useless ones later. But this may cause a too complicated treatment of recursive functions and may make the derivation terminate less often. On the other hand, this is a place where separate passes of static analysis could help, imitating binding time analysis in partial evaluation. This suggests a direction for future work.

Although in general, any attempt to limit function introductions could affect achieving incrementality for certain programs, it does not hurt to try a few good heuristics with more reasonable termination behavior. For example, we may introduce a new function at a function application only if we can effectively decide that, in incrementalizing the unfolded application, some subcomputations can be simplified. Thus, assuming we have a complete equality reasoning mechanism and a sufficient cache element when introducing a function, if the derivation procedure does not terminate, there must be simplification possible along an infinite path, and thus there must an execution of the original program that does not terminate. In other words, if the original program terminates on all inputs, then the derivation procedure terminates, and the derived program terminates on all inputs at least as fast with the right values. Note, however, that the complexity of the derivation procedure may not be bounded by the size of a given program, since it may loop on ground values. The rationale is that computations done at transformation time need not be done in the transformed programs.

Other Concerns. Two other weaknesses result from unfolding as done by the derivation procedure. First, only partial correctness is preserved, i.e., a derived program may terminate more often than the original program. Second, subcomputations may be duplicated in a derived program.

Both drawbacks can be overcome by inserting let bindings to compute the arguments when unfolding function applications, i.e., instead of unfolding a function application to e_{f}[e_{1}/v_{1}, ..., e_{n}/v_{n}], we unfold it to

let v_{1}=e_{1} in ... let v_{n}=e_{n} in e_{f} end ... end

Then we modify the condition of unfolding let expressions in Simp, namely, let v = e_{1} in e_{2} end can be unfolded only if e_{2}[e_{1}/v] neither duplicates non-trivial computations nor discards non-terminating computations, where the latter means either e_{1} can be effectively decided to terminate or v occurs at least once on every (syntactic) execution path in e_{2}. As occurrence counting analysis helps decide whether an unfolding duplicates computations, it can also help decide whether an unfolding discards computations.

Similar solutions are proposed in partial evaluation [23, 5]. Note that, even without this technique, the efficiency of our derived programs are guaranteed with the help of time analysis. But in partial evaluation where no time analysis is employed, a transformed program could take exponential time while the original program takes only polynomial time [23]. As a matter of fact, even with this technique, time analysis is still needed in our derivation, since we replace subcomputations by retrievals from a cache result only when we can save time by doing so. This is inherent in incremental computation and is a complication over partial evaluation.

6.3 Caching Intermediate Results and Auxiliary Information

In the derivation approach presented above, the derived function f′ only uses the cached result r of f(x) to compute f(x ⊕ y) incrementally.^{4} Adding extra information about x for f′ to use could lead to greater incrementality, i.e., f′ might be able to compute f(x ⊕ y) even faster by making use of the additional information. We must augment the values returned by f to include this additional information.

Let f̂ denote the function obtained by extending f to return the augmented values, and assume that when f(x) is needed, it is projected out of f̂(x). Suppose f̂(x) returns the augmented value r̂. Then

using our derivation procedure presented above, we can obtain an incremental version f̂′ of f̂ such that f̂′(x, y, r̂) = f̂(x ⊕ y). Note that the domain of f̂′ is augmented from that of f′ to include the additional

information as input. At the same time, the range of f̂′ is also augmented from that of f′ to include the corresponding additional information about x ⊕ y. Therefore, we are prepared for incremental computation after further input changes, which is a natural requirement for normal applications.

We can regard the extension of f to f̂ as a separate step before the derivation procedure. In principle, given a function f and an input change operation ⊕, there is no general way of obtaining f̂ to enable greater incrementality in computing the value of f(x ⊕ y). We propose to approach the problem in two stages.

First, there may be subcomputations performed in f(x) whose results are not embedded in return value r but are crucial for achieving greater incrementality in computing f(x⊕y). We can expand f(x) and f(x⊕y) to identify such computations in f(x) and then extend f(x) to embed these intermediate results in the final return value.

4From this section on, for notational convenience, we use f to denote f_{0}.

Second, there may be information about x that is not computed by the original function f(x) at all but is crucial for obtaining greater incrementality in computing f(x ⊕ y). We expect to discover such auxiliary information in the computations in f(x ⊕ y) that only depend on x but are not in f(x). We can expand f(x⊕y) and f(x) to identify such computations in f(x⊕y) and then extend f(x) to compute them efficiently as well.

To illustrate the two points above, we present a simple example. Let x = ⟨x_{1}, x_{2}⟩, where x_{1} and x_{2} are two lists, and function f(x_{1}, x_{2}) return the product of the lengths of the two lists:

f(x_{1}, x_{2}) = len(x_{1}) ∗ len(x_{2}), len(x) = if null(x) then 0 else 1+ len(cdr(x))

Let y = ⟨y_{1}, y_{2}⟩ and let the new input to f, x ⊕ y, be ⟨cons(y_{1}, x_{1}), cons(y_{2}, x_{2})⟩. Suppose r is the cached result of f(x_{1}, x_{2}) and we use it in computing f(x ⊕ y) incrementally. Following the derivation procedure, we introduce f′(y_{1}, x_{1}, y_{2}, x_{2}, r) to compute f(cons(y_{1}, x_{1}), cons(y_{2}, x_{2})) incrementally. After unfolding the application of f and reducing subexpressions, we get (len(x_{1})+1) ∗ (len(x_{2})+1). Then, using properties of the primitive function ‘∗’, we get len(x_{1}) ∗ len(x_{2}) + len(x_{1}) + len(x_{2}) + 1, where len(x_{1}) ∗ len(x_{2}) can be replaced by r. Thus, we obtain an incremental version f′(x, r) that computes f(x ⊕ y):

f′(x_{1}, x_{2}, r) = r+len(x_{1})+len(x_{2})+1

Although f′ saves computing a ‘∗’ operation, it is of dubious value if we must recompute len(x_{1}) and len(x_{2}).

Using the idea of the first point above, we see that len(x_{1}) and len(x_{2}) are subcomputations performed in f(x_{1}, x_{2}) whose values could be used to compute f(x⊕y) even faster than f′(x, r) but can not be retrieved from the cached result r. Thus, we extend f to f̂_{1} such that f̂_{1} embeds the intermediate results len(x_{1}) and len(x_{2}) in the return value r̂_{1}:

f̂_{1}(x_{1}, x_{2}) = let l_{1} =len(x_{1}) in let l_{2} =len(x_{2}) in triple(l_{1}∗l_{2}, l_{1}, l_{2}) end end

where triple is a constructor with corresponding selectors 1st, 2nd, and 3rd. It is easy to see that using our derivation procedure, we can obtain an incremental version f̂′_{1}(r̂_{1}) that computes f̂_{1}(x ⊕ y):

f̂′_{1}(r̂_{1}) = triple(1st(r̂_{1})+2nd(r̂_{1})+3rd(r̂_{1})+1, 2nd(r̂_{1})+1, 3rd(r̂_{1})+1)

Compared to f′(x_{1}, x_{2}, r), f̂′_{1}(r̂_{1}) saves computing len(x_{1}) and len(x_{2}). Note that a cache of size three is required, whereas f′ requires only a cache of size one.

Using the idea of the second point above, we see that the computation len(x_{1}) + len(x_{2}) depends completely on x and its value would enable even faster computation of f(x⊕y) than f̂′_{1}(r̂_{1}) but the ‘+’ operation is not contained in the computation f(x) at all. Moreover, caching this auxiliary information would obviate the need to to cache the values of len(x_{1}) and len(x_{2}) separately. Thus, we extend f to f̂_{2} such that f̂_{2} returns r̂_{2} containing both the product and the sum of the two lengths:

f̂_{2}(x_{1}, x_{2}) = let l_{1} =len(x_{1}) in let l_{2} =len(x_{2}) in pair(l_{1}∗l_{2}, l_{1}+l_{2}) end end

where pair is a constructor with corresponding selectors fst and snd. It is easy to see that using our derivation procedure, we can obtain an incremental version f̂′_{2}(r̂_{2}) that computes f̂_{2}(x ⊕ y):

f̂′_{2}(r̂_{2}) = pair(fst(r̂_{2})+snd(r̂_{2})+1, snd(r̂_{2})+2)

Compared to f̂′_{1}(r̂_{1}), f̂′_{2}(r̂_{2}) does slightly less arithmetic and uses a smaller cache.

These two techniques above are currently being studied. In a forthcoming paper, we present a complete method for caching intermediate results that enhance incrementality.^{5} The degree to which it is possible to generate the auxiliary information automatically is an open question.

Corresponding to finding auxiliary information, many dynamic algorithms use specially designed data structures to answer queries quickly. Although there is no universally applicable data structure, some apply to a broad class of problems [11]. Accommodating such general data structures in our model for deriving incremental programs might help in deciding whether a data structure is applicable to a certain problem. How this might be done is another question open for study.

6.4 Mechanization

With the oracle of a theorem prover, time analysis techniques, and heuristics for function introductions, the derivation can be fully automated. In practice, the derivation can be made semi-automatic when some of these oracles are only semi-automatically provided.

Although we see the derivation as certainly no more automatable than partial evaluation, it is desirable to at least use the computer as a sophisticated editor, suggesting and carrying out detailed transformations. It is also nice that the derived programs are in the same language as the original programs, and therefore they are executable and one can check solutions and try out alternatives.

We have implemented a prototype system called CACHET for deriving incremental programs based on our approach. The implementation uses the Synthesizer Generator [34], a system for generating languagebased editors, and consists of about 14,000 lines of code written in SSL, the Synthesizer Generator language for specifying editors. Source-to-source transformations are operations built in to our editor.

Currently, the transformation rules are invoked manually mainly for two reasons. First, the Synthesizer Generator does not currently have a rewrite engine for us to do an applicative order reduction easily as is required by the derivation procedure. Second, we want an interactive environment to study the applicability of various transformations, thus manual invocation is suitable most of the time. Also, at present, we are only using a very simple equality reasoning engine, not a full-blown theorem prover.

CACHET has been used to derive numerous incremental programs. It is also helpful in studying transformations for caching intermediate results and auxiliary information. We plan to add rewrite mechanism into the Synthesizer Generator to further automate derivations by CACHET. We also plan to interface CACHET to a substantial theorem prover.

7 Examples

To see the power and some interesting behavior of the derivation procedure, we consider incrementalizing several different sorting programs. Let sort be a function that takes a list of numbers x and returns the sorted list sort(x). Let the change to the input of sort be that an extra number is added at the beginning of the list, i.e., x′ = cons(y, x).

7.1 Insertion Sort

Suppose the program is an insertion sort that inserts the first element of the list into the recursively sorted list of the rest.

sort(x) = if null(x) then nil else insert(car(x), sort(cdr(x)))

insert(i, x) = if null(x) then cons(i, nil) else if i ≤ car(x) then cons(i, x) else cons(car(x), insert(i, cdr(x))) (28)

5Y. A. Liu and T. Teitelbaum, Caching intermediate results for program improvement, to appear in Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’95), La Jolla, CA, June 1995.

To compute sort(cons(y, x)) incrementally using sort(x) = r, all we need to do is a function introduction, followed by an unfolding, a few simplifications, a replacement, and a dead parameter elimination, and finally a use of the introduced function, as sketched below:

sort′(y_{1}, x_{1}, r_{1}) = sort(cons(y_{1}, x_{1})), with sort(x_{1}) = r_{1}  function introduction

= if null(cons(y_{1}, x_{1})) then nil else insert(car(cons(y_{1}, x_{1})), sort(cdr(cons(y_{1}, x_{1})))) unfolding

= insert(y_{1}, sort(x_{1}))  simplifications
= insert(y_{1}, r_{1})  replacement
sort′(y_{1}, r_{1}) = insert(y_{1}, r_{1})  dead parameter elimination
sort(cons(y, x)) = sort′(y, r), for sort(x) = r  use of the introduced function

The derived incremental program simply uses insert to insert the newly added number into the previously sorted list.

A more formal derivation following the derivation procedure is given below. We start with

IncApply[[sort(cons(y, x))]] ∅ {⟨sort(x), r, ∅⟩} ∅  (29)

where we introduce sort′ as in the tuple d_{1}:

⟨sort(cons(y_{1}, x_{1})), sort′(y_{1}, x_{1}, r_{1}), C_{1}⟩, where C_{1} = {⟨sort(x_{1}), r_{1}, ∅⟩}

and we obtain a definition of sort′ as follows:

1. We unfold sort(cons(y_{1}, x_{1})) and get an expression e_{1}:

if null(cons(y_{1}, x_{1})) then nil
else insert(car(cons(y_{1}, x_{1})), sort(cdr(cons(y_{1}, x_{1}))))

2. We incrementalize e_{1}:

Inc[[e_{1}]] ∅ C_{1}D_{1}, where D_{1} = {d_{1}}

which first calls Subl to reduce subexpressions:

Subl[[e_{1}]] ∅ C_{1}D_{1}
− − by (if_{1}), Inc[[null(cons(y_{1}, x_{1}))]] ∅ C_{1}D_{1} = ⟨F, C_{1}, D_{1}⟩

= Subl[[if F then nil else e_{13}]] ∅ C_{1}D_{1}, where e_{13} denotes the false branch of e_{1}

− − by (if_{n}), Inc[[e_{13}]] {F ↔ F } C_{1}D_{1} = ⟨insert(y_{1}, r_{1}), C_{1}, D_{1}⟩ since car(cons(y_{1}, x_{1})) = y_{1}, cdr(cons(y_{1}, x_{1})) = x_{1}, and sort(x_{1}) = r_{1}, IncApply does not transform insert(y_{1}, r_{1}) since it does not depend on x

= ⟨if F then nil else insert(y_{1}, r_{1}), C_{1}, D_{1}⟩

and then applies Simp and Repl to the resulting expression:

Repl[[Simp[[if F then nil else insert(y_{1}, r_{1})]] ∅^{C_{1}}]] ∅^{C_{1}} C_{1}
= Repl[[insert(y_{1}, r_{1})]] ∅^{C_{1}} C_{1}
= insert(y_{1}, r_{1})

3. We eliminate dead parameters of sort′, defined by sort′(y_{1}, x_{1}, r_{1}) = insert(y_{1}, r_{1}). Clearly, x_{1} is dead. We obtain a final definition of sort′:

sort′(y_{1}, r_{1}) = insert(y_{1}, r_{1})  (30)

It is clear that sort′(y_{1}, r_{1}) computes asymptotically at least as fast as sort(cons(y_{1}, x_{1})) because each transformation step above guarantees this relation. Therefore, t(sort′(y, r))≤t(sort(cons(y, x))). Thus, (29) returns

⟨sort′(y, r), {⟨sort(cons(y_{1}, x_{1})), sort′(y_{1}, r_{1}), {⟨sort(x_{1}), r_{1}, ∅⟩}⟩}⟩

where sort′ is defined as in (30) and insert is defined as in the original program (28).

7.2 Selection Sort

Suppose the program is a selection sort that selects the least number in the list as the first number in the sorted list and sorts the rest recursively.

sort(x) = if null(x) then nil else let k = least(x) in cons(k, sort(rest(x, k))) end

least(x) = if null(cdr(x)) then car(x) else let s = least(cdr(x)) in if car(x) ≤ s then car(x) else s end

rest(x, k) = if k = car(x) then cdr(x) else cons(car(x), rest(cdr(x), k))

(31)

Again, we start by introducing sort′(y_{1}, x_{1}, r_{1}) to compute sort(cons(y_{1}, x_{1})) incrementally. But while we incrementalize the unfolded sort(cons(y_{1}, x_{1})) to get a definition of sort′, the application least(cons(y_{1}, x_{1})) is transformed recursively, which results in the lifting of some conditions and bindings, and then applications of rest are transformed under these conditions and bindings. As the result of these transformations, sort′ compares y_{1} with the first number in r_{1} to decide whether y_{1} should stay before r_{1}, and, if not, recursively considers y_{1} with the rest of r_{1}. But this is exactly the process of inserting y_{1} into r_{1} at the right place. Thus, to a certain degree, the derivation procedure discovered the insertion process from the selection sort via a series of transformations.

As the derivation procedure is more complicated, an informal but complete derivation is given below. As just mentioned, to compute sort(cons(y, x)) incrementally using sort(x) = r, we start by introducing sort′(y_{1}, x_{1}, r_{1}) for sort(cons(y_{1}, x_{1})) with sort(x_{1}) = r_{1}.

1. Unfold sort(cons(y_{1}, x_{1})):

if null(cons(y_{1}, x_{1})) then nil

else let k = least(cons(y_{1}, x_{1})) in cons(k, sort(rest(cons(y_{1}, x_{1}), k))) end (32)

2. Simplify the condition null(cons(y_{1}, x_{1})) to false, and thus (32) is to be simplified to the false branch:

let k = least(cons(y_{1}, x_{1})) in cons(k, sort(rest(cons(y_{1}, x_{1}), k))) end  (33)

3. Consider least(cons(y_{1}, x_{1})), and introduce least′(y_{2}, x_{2}, r_{2}) for least(cons(y_{2}, x_{2})) with sort(x_{2}) = r_{2}.

3.1. Unfold least(cons(y_{2}, x_{2})):

if null(cdr(cons(y_{2}, x_{2}))) then car(cons(y_{2}, x_{2}))
else let s = least(cdr(cons(y_{2}, x_{2})))
in if car(cons(y_{2}, x_{2})) ≤ s then car(cons(y_{2}, x_{2})) else s end

(34)

3.2. Simplify the condition null(cdr(cons(y_{2}, x_{2}))) to null(x_{2}), and replace null(x_{2}) by null(r_{2}) since

null(sort(x_{2})) is specialized to true (false) when null(x_{2}) is true (false).

In the true branch, simplify car(cons(y_{2}, x_{2})) to y_{2}. In the false branch, simplify least(cdr(cons(y_{2}, x_{2}))) to least(x_{2}), and replace least(x_{2}) by car(r_{2}) since when null(r_{2}) is false

sort(x_{2}) is specialized to let k_{2} = least(x_{2}) in cons(k_{2}, sort(rest(x_{2}, k_{2}))) end,

and then, in the body of the let expression, simplify car(cons(y_{2}, x_{2})) to y_{2}. Thus, (34) becomes

if null(r_{2}) then y_{2} else let s = car(r_{2}) in if y_{2} ≤ s then y_{2} else s end  (35)

3.3. For least′ defined by least′(y_{2}, x_{2}, r_{2}) = (35), eliminate dead parameter x_{2}. Replace least(cons(y_{1}, x_{1})) by least′(y_{1}, r_{1}), and unfold least′(y_{1}, r_{1}) since least′ is not recursively defined and unfolding does not duplicate non-trivial computations. Thus, (33) becomes

let k = (if null(r_{1}) then y_{1} else let s = car(r_{1}) in if y_{1} ≤ s then y_{1} else s end)

in cons(k, sort(rest(cons(y_{1}, x_{1}), k))) end (36)

4. Lift the first condition null(r_{1}) out of the top-level let. Thus, (36) becomes if null(r_{1}) then let k = y_{1} in cons(k, sort(rest(cons(y_{1}, x_{1}), k))) end

else let k = (let s = car(r_{1}) in if y_{1} ≤ s then y_{1} else s end)
in cons(k, sort(rest(cons(y_{1}, x_{1}), k))) end

(37)

5. In the true branch of (37), simplify x_{1} to nil. No functions are introduced for the applications of rest

and sort since they do not depend on x. Then unfold the let:

cons(y_{1}, sort(rest(cons(y_{1}, nil), y_{1})))  (38)

In the false branch of (37), lift the binding s = car(r_{1}) out of the first let:

let s = car(r_{1}) in let k = (if y_{1} ≤ s then y_{1} else s) in cons(k, sort(rest(cons(y_{1}, x_{1}), k))) end end

and then lift the condition y_{1} ≤ s out of the second let:

let s = car(r_{1}) in if y_{1} ≤ s then let k = y_{1} in cons(k, sort(rest(cons(y_{1}, x_{1}), k))) end else let k = s in cons(k, sort(rest(cons(y_{1}, x_{1}), k))) end end  (39)

6. In the true branch of (39), first consider rest(cons(y_{1}, x_{1}), k), and introduce rest′(y_{3}, x_{3}, k_{3}, r_{3}) for rest(cons(y_{3}, x_{3}), k_{3}) with sort(x_{3}) = r_{3} and also k_{3} ↔ y_{3}, etc. 6.1 Unfold rest(cons(y_{3}, x_{3}), k_{3}):

if k_{3} = car(cons(y_{3}, x_{3})) then cdr(cons(y_{3}, x_{3}))

else cons(car(cons(y_{3}, x_{3})), rest(cdr(cons(y_{3}, x_{3})), k_{3})) (40)

6.2 Simplify the condition k_{3} = car(cons(y_{3}, x_{3})) to k_{3} = y_{3}, and further simplify it to true, and thus

(40) is to be simplified to the true branch cdr(cons(y_{3}, x_{3})), which is then simplified to x_{3}. 6.3 For rest′ defined by rest′(y_{3}, x_{3}, k_{3}, r_{3}) = x_{3}, eliminate dead parameters y_{3}, k_{3}, and r_{3}. Replace rest(cons(y_{1}, x_{1}), k) by rest′(x_{1}), and unfold rest′(x_{1}) to x_{1}. Then, replace sort(x_{1}) by r_{1}. Finally, unfold the let. Thus, the true branch of (39) becomes

cons(y_{1}, r_{1})  (41)

7. In the false branch of (39), first consider rest(cons(y_{1}, x_{1}), k), and introduce rest′_{1}(y_{4}, x_{4}, k_{4}, r_{4}) for rest(cons(y_{4}, x_{4}), k_{4}) with sort(x_{4}) = r_{4} and also y_{4} ≤s ↔ F, k_{4} ↔ s, etc. 7.1 Unfold rest(cons(y_{4}, x_{4}), k_{4}):

if k_{4} = car(cons(y_{4}, x_{4})) then cdr(cons(y_{4}, x_{4}))

else cons(car(cons(y_{4}, x_{4})), rest(cdr(cons(y_{4}, x_{4})), k_{4})) (42)

7.2 Simplify the condition k_{4} = car(cons(y_{4}, x_{4})) to k_{4} = y_{4}, and further simplify it to false, and thus

(42) is to be simplified to the false branch, which is then simplified to cons(y_{4}, rest(x_{4}, k_{4})). 7.3 For rest′_{1} defined by rest′_{1}(y_{4}, x_{4}, k_{4}, r_{4}) = cons(y_{4}, rest(x_{4}, k_{4})), eliminate dead parameter r_{4}.

Replace rest(cons(y_{1}, x_{1}), k) by rest′_{1}(y_{1}, x_{1}, k), and unfold rest′_{1}(y_{1}, x_{1}, k) to cons(y_{1}, rest(x_{1}, k)). Then, replace sort(cons(y_{1}, rest(x_{1}, k))) by sort′(y_{1}, rest(x_{1}, k), cdr(r_{1})), since when null(r_{1}) is false

sort(x_{1}) is specialized to let k_{1} = least(x_{1}) in cons(k_{1}, sort(rest(x_{1}, k_{1}))) end,

which implies sort(rest(x_{1}, k)) = cdr(r_{1}) for k = s = car(r_{1}) = k_{1}. Finally, unfold the let. Thus, the false branch of (39) becomes

cons(s, sort′(y_{1}, rest(x_{1}, s), cdr(r_{1})))  (43)

8. Putting (37) (38) (39) (41) (43) together, sort′ is defined by

sort′(y_{1}, x_{1}, r_{1}) = if null(r_{1}) then cons(y_{1}, sort(rest(cons(y_{1}, nil), y_{1}))) else let s = car(r_{1}) in if y_{1} ≤ s then cons(y, r_{1}) else cons(s, sort′(y_{1}, rest(x_{1}, s), cdr(r_{1}))) end

Eliminating dead parameter x_{1}, we obtain a final definition of sort′:

sort′(y_{1}, r_{1}) = if null(r_{1}) then cons(y_{1}, sort(rest(cons(y_{1}, nil), y_{1}))) else let s = car(r_{1}) in if y_{1} ≤ s then cons(y_{1}, r_{1}) else cons(s, sort′(y_{1}, cdr(r_{1}))) end  (44)

It is easy to see that, in the true branch, sort(rest(cons(y_{1}, nil), y_{1})) returns nil in constant time given any number y_{1}; in the false branch, the let expression could be unfolded. Thus, sort′ exactly performs an insertion as the insert in (28).

At the end, we have sort(cons(y, x)) = sort′(y, r) for sort(x) = r, where sort′ is defined as in (44).

7.3 Merge Sort

Suppose the program is a merge sort that divides the list into two sublists, recursively sorts the two sublists, and then merges the two sorted sublists.

sort(x) = if null(x) then nil else if null(cdr(x)) then cons(car(x), nil) else merge(sort(odd(x)), sort(even(x)))

odd(x) = if null(x) then nil else cons(car(x), even(cdr(x)))

even(x) = if null(x) then nil else odd(cdr(x))

merge(x, y) = if null(x) then y else if null(y) then x else if car(x) ≤ car(y) then cons(car(x), merge(cdr(x), y)) else cons(car(y), merge(x, cdr(y)))

An insertion can be easily obtained if we are given the property that sorting the new list equals merging the new number into the previously sorted list.

sort′(y_{1}, x_{1}, r_{1}) = sort(cons(y_{1}, x_{1})), with sort(x_{1}) = r_{1} function introduction
= merge(cons(y_{1}, nil), sort(x_{1}))  property relating merge and sort
= merge(cons(y_{1}, nil), r_{1})  replacement
sort′(y_{1}, r_{1}) = merge(cons(y_{1}, nil), r_{1})  dead parameter elimination
sort(cons(y, x)) = sort′(y, r), for sort(x) = r  use of the introduced function

The derived program sort′ basically performs an insertion with a constant factor overhead over the insert in (28). The required property that relates merge and sort can be proved by a straightforward induction based on the associativity and commutativity of merge. However, if the above property is not given, then no incremental program can be derived using the derivation procedure. But what is interesting is the following.

Suppose we cache intermediate results during merge sort, i.e., we recursively cache sorted sublists. Then following the derivation procedure, we can easily obtain an incremental merge sort that incrementally sorts the new list by recursively merging the new number with the appropriate intermediate results.

An informal derivation with a few major transformation steps is given below. Let ŝort be a function that extends sort with cached intermediate results.

ŝort(x) = if null(x) then con(nil, aux_{0}) else if null(cdr(x)) then con(cons(car(x), nil), aux_{1}) else let so = ŝort(odd(x)) in let se = ŝort(even(x)) in con(merge(con_{r}(so), con_{r}(se)), aux(so, se)) end end

sort(x) = con_{r}(ŝort(x))

ŝort(x) returns a con constructor application, where the first element is the value of sort(x) and can be selected using con_{r}, and the second element contains the intermediate results corresponding to x and can be selected using con_{a}. In particular, the second element is a constant aux_{0} if x is nil, a constant aux_{1} if x is a single-element list, and an aux construction of ŝort(odd(x)) and ŝort(even(x)) otherwise, where the first element can be selected using aux_{o} and second aux_{e}.

We start by introducing ŝort′(y_{1}, x_{1}, r̂_{1}) to compute ŝort(cons(y_{1}, x_{1})) incrementally using ŝort(x_{1}) = r̂_{1}.

1. Unfold ŝort(cons(y_{1}, x_{1})):

if null(cons(y_{1}, x_{1})) then con(nil, aux_{0})
else if null(cdr(cons(y_{1}, x_{1}))) then con(cons(car(cons(y_{1}, x_{1})), nil), aux_{1})
else let so = ŝort(odd(cons(y_{1}, x_{1}))) in
let se = ŝort(even(cons(y_{1}, x_{1}))) in
con(merge(con_{r}(so), con_{r}(se)), aux(so, se)) end end

(45)

2. Simplify the first condition null(cons(y_{1}, x_{1})) to false, and thus the first branch is to be eliminated. Simplify the second condition null(cdr(cons(y_{1}, x_{1}))) to null(x_{1}), and in the second branch simplify car(cons(y_{1}, x_{1})) to y_{1}. In the third branch, simplify odd(cons(y_{1}, x_{1})) to cons(y_{1}, even(x_{1})), and even(cons(y_{1}, x_{1})) to odd(x_{1}). We get

if null(x_{1}) then con(cons(y_{1}, nil), aux_{1})
else let so = ŝort(cons(y_{1}, even(x_{1}))) in
let se = ŝort(odd(x_{1})) in
con(merge(con_{r}(so), con_{r}(se)), aux(so, se)) end end

(46)

3. When null(x_{1}) is false, ŝort(x_{1}) is specialized to a conditional expression with condition null(cdr(x_{1})). Thus, the false branch of (46) is to be separated into two corresponding cases.

4. null(x_{1}) is replaced by null(con_{r}(r̂_{1})) since

null(con_{r}(ŝort(x_{1}))) is specialized to true (false) when null(x_{1}) is true (false).

null(cdr(x_{1})) is replaced by null(cdr(con_{r}(r̂_{1}))) since

null(cdr(con_{r}(ŝort(x_{1})))) is specialized to true (false) when null(cdr(x_{1})) is true (false).

In the branch where null(cdr(x_{1})) is true, even(x_{1}) becomes nil, then ŝort(cons(y_{1}, nil)) becomes con(cons(y_{1}, nil), aux_{1}); odd(x_{1}) becomes cons(car(x_{1}), nil), then ŝort(cons(car(x_{1}), nil)) becomes con(cons(car(x_{1}), nil), aux_{1}), which is then replaced by r̂_{1} since

ŝort(x_{1}) is specialized to con(cons(car(x_{1}), nil), aux_{1}) when null(cdr(x_{1})) is true.

In the other branch where null(cdr(x_{1})) is false,

ŝort(x_{1}) is specialized to con(..., aux(ŝort(odd(x_{1})), ŝort(even(x_{1})))),

which implies ŝort(odd(x_{1})) = aux_{o}(con_{a}(r̂_{1})) and ŝort(even(x_{1})) = aux_{e}(con_{a}(r̂_{1})); thus ŝort(cons(y_{1}, even(x_{1}))) is replaced by ŝort′(y_{1}, even(x_{1}), aux_{e}(con_{a}(r̂_{1}))), and ŝort(odd(x_{1})) is replaced by aux_{o}(con_{a}(r̂_{1})). We get

if null(con_{r}(r̂_{1})) then con(cons(y_{1}, nil), aux_{1})
else if null(cdr(con_{r}(r̂_{1}))) then
let so = con(cons(y_{1}, nil), aux_{1}) in
con(merge(con_{r}(so), con_{r}(r̂_{1})), aux(so, r̂_{1})) end
else let so = ŝort′(y_{1}, even(x_{1}), aux_{e}(con_{a}(r̂_{1}))) in
let se = aux_{o}(con_{a}(r̂_{1})) in
con(merge(con_{r}(so), con_{r}(se)), aux(so, se)) end end

(47)

5. Eliminate dead parameter of ŝort′, defined by ŝort′(y_{1}, x_{1}, r̂_{1}) = (47). Obviously, x_{1} is dead. We obtain a final definition of ŝort′:

ŝort′(y_{1}, r̂_{1}) = if null(con_{r}(r̂_{1})) then con(cons(y_{1}, nil), aux_{1}) else if null(cdr(con_{r}(r̂_{1}))) then let so = con(cons(y_{1}, nil), aux_{1}) in con(merge(con_{r}(so), con_{r}(r̂_{1})), aux(so, r̂_{1})) end else let so = ŝort′(y_{1}, aux_{e}(con_{a}(r̂_{1}))) in let se = aux_{o}(con_{a}(r̂_{1})) in con(merge(con_{r}(so), con_{r}(se)), aux(so, se)) end end  (48)

At the end, we have ŝort(cons(y, x)) = ŝort′(y, r̂) for ŝort(x) = r̂, where ŝort′ is defined as in (48). ŝort′(y, r̂) incrementally sorts the new list and maintains the corresponding intermediate results.

Both insertion sort and selection sort take O(n^{2}) time, where n is the length of the input list, and merge sort takes O(n log n) time. Insertion takes only O(n) time; but it uses O(n) space to store the previously sorted list. Incremental merge sort also takes O(n) time; but it uses O(n log n) space to store intermediate results.

The derivation of the incremental merge sort suggests that our approach of exploiting cached values for incrementality is powerful: the power of caching obviates the reliance on a theorem prover for proving certain properties. We can also view it as trading space for theorem proving ability.

8 Related Work and Conclusion

Our approach to deriving incremental programs combines a number of program analysis and transformation techniques, which have been summarized in Section 6.1. Here, we take a closer look at related work in incremental computation, which is introduced in Section 1 and partitioned into three classes.

First of all, given particular problems with certain input changes, can our approach be used to derive as efficient incremental programs as those in the first class? The general answer is positive, but with three caveats. First, the particular problem needs to be coded naturally in the language for which our approach is presented. Second, the quality of a derived incremental program depends on the way the non-incremental program is coded, as seen in the sort examples in Section 7. Third, intermediate results and auxiliary information are needed for many incremental problems but may be difficult to determine. In this case, we can use the ideas in Section 6.3, at least use the derivation procedure on programs that are extended to compute manually determined intermediate results and auxiliary information, and derive programs that incrementally maintain these intermediate results and auxiliary information.

Since our transformational approach is related to partial evaluation in some aspects, it is worthwhile to specially compare it with the work by Sundaresh and Hudak [42, 41] in the second class. The common aspect is that both works aim at obtaining incremental computation by transforming non-incremental programs. However, the two approaches follow different lines. Their work mostly uses partial evaluation, with extra efforts on partitioning program inputs and combining residual programs. Our method combines a series of analysis and transformation techniques that “parallel” those used in (generalized) partial evaluation, but with the goal of incrementalization in addition to specialization, and therefore employs overall more extensive and more complicated techniques. We believe a major limitation of the Sundaresh-Hudak framework is that it can only handle input changes according to a pre-given input partition, which is partly implied as a work in the second class.

Our work is closest in spirit to the finite differencing techniques of the third class. The name “finite differencing” was originally given by Paige and Koenig [30]. Their work generalizes Cocke’s strength reduction [9] and provides a convenient framework for implementing a host of transformations including Earley’s “iterator inversion” [10]. They develop a set of rules for differentiating set-theoretic expressions and combine these rules using a chain rule to derive inexpensive programs with incremental loop bodies. Such techniques are indispensable as part of an optimizing compiler for languages like SETL or APL [29, 7]. The APTS program transformation system [28] has been developed for such purposes. Our technique differs from theirs 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, through which incrementalities can be discovered in existing programs written in standard languages.

Smith’s work in KIDS [38, 39] is closely related to ours. KIDS is a semi-automatic program development system that aims to derive efficient programs from high-level specifications [40], as is APTS. Its version of finite differencing was developed for the optimization of its derived functional programs and has two basic operations: abstraction and simplification. Abstraction of a function f adds an extra cache parameter to f. Simplification simplifies the definition of f given the added cache parameter. However, as to how the cache parameter should be used in the simplification to provide incrementality, KIDS provides only the observation that distributive laws can often be applied. The Munich CIP project [31] has a strategy for finite differencing that captures similar ideas. It first “defines by a suitable embedding a function f′”, and then “derives a recursive version of f′ using generalized unfold/fold strategy”, but provides no special techniques for discovering incrementality. We believe that both works provide only general strategies with no precise procedure to follow, and therefore are less automatable than ours.

We conclude with the contribution of our work to a general model of incremental computation, namely, a model M that takes a (non-incremental) program f written in some language L and an input change ⊕, which is also describable in L, and derives f′, an incremental version of f under ⊕. Such a model addresses all three classes of work in incremental computation, for the following reasons. The development of particular incremental algorithms in the first class is a special case of M, where f and ⊕ are fixed according to particular problems, and f′ is derived manually. An incremental execution framework in the second class is a kind of M that is general in that it automatically incrementalizes any application program f, but has poor specializability in that any change ⊕ to program f is handled in the way prescribed by the framework (and often no explicit f′ is derived). Work in the third class is not only general, but also specialized to any program f and change ⊕; however, so far effective methods focus on the class of M where the language L is limited to very high-level languages. What is needed is an effective approach for deriving incremental programs from non-incremental ones written in a standard language.

We have presented such a systematic approach for deriving incremental programs from non-incremental programs written in a standard functional programming language. It begins the study of a general model for incremental computation along unique lines distinct from all other approaches. Although this problem is, in general, very hard, we have shown that an effective approach can be developed to derive incremental programs by effectively combining particular program transformation and analysis techniques.

Although we presented our approach in terms of a first-order functional language with strict semantics, we have reason to believe that our basic principle applies to other standard languages as well, e.g., higher-order functional languages, functional languages with lazy semantics, and imperative languages. Of course, special program analysis and transformation techniques related to these language features must be exploited, and they may complicate the derivation issues in one way or another, just as when partial evaluation techniques are developed to cope with such language features. On the other hand, these other language features allow some algorithms to be coded more naturally and incremental versions derived to be more efficient, making a general model for incremental computation more complete.

By studying these general techniques, we aim to better understand the essence of incremental computation. We also aim to establish a general framework in which different ideas on incremental 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 in the literature [33].

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] B. Alpern, R. Hoover, B. Rosen, P. Sweeney, and K. Zadeck. Incremental evaluation of computational circuits. In Proceedings of the First Annual ACM-SIAM Symposium on Discrete Algorithms, pages 32–42, San Francisco, California, January 1990.

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

[4] R. S. Bird. Tabulation techniques for recursive programs. ACM Computing Surveys, 12(4):403–417, December 1980.

[5] A. Bondorf and O. Danvy. Automatic autoprojection of recursive equations with global variables and abstract data types. Science of Computer Programming, 16:151–195, 1991.

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

[7] J. Cai and R. Paige. Program derivation by fixed point computation. Science of Computer Programming, 11:197–261, September 1988/89.

[8] S. Ceri, M. A. W. Houtsma, A. M. Keller, and P. Samarati. Achieving incremental consistency among autonomous replicated databases. IFIP Transactions A [Computer Science and Technology], A-25:223–237, 1993.

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

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

[11] D. Eppstein, Z. Galil, G. F. Italiano, and A. Nissenzweig. Sparsification - a technique for speeding up dynamic graph algorithms. In Proceedings of the 33rd Annual IEEE Symposium on FOCS, Pittsburgh, Pennsylvania, October 1992.

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

[13] B. N. Freeman-Benson, J. Maloney, and A. Borning. An incremental constraint solver. Communications of the ACM, 33(1):54–63, January 1990.

[14] Y. Futamura and K. Nogi. Generalized partial evaluation. In Partial Evaluation and Mixed Computation, pages 133–151. North-Holland, Amsterdam, 1988.

[15] C. Ghezzi and D. Mandrioli. Incremental parsing. ACM Transactions on Programming Languages and Systems, 1(1):58–70, July 1979.

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

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

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

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

[20] E. Levy and A. Silberschatz. Incremental recovery in main memory database systems. IEEE Transactions on Knowledge and Data Engineering, 4(6):529–540, December 1992.

[21] R. Medina-Mora and P. Feiler. An incremental programming environment. IEEE Transactions on Software Engineering, SE-7(5):472–482, September 1981.

[22] D. Michie. “memo” functions and machine learning. Nature, 218:19–22, April 1968.

[23] T. Mogensen. Partially static structures in a self-applicable partial evaluator. In Partial Evaluation and Mixed Computation, pages 325–347. North-Holland, 1988.

[24] S. S. Muchnick and N. D. Jones, editors. Program Flow Analysis: Theory and Applications. Prentice-Hall, Englewood Cliffs, New Jersey, 1981.

[25] R. Paige. Formal Differentiation: A Program Synthesis Technique, volume 7 of Computer Science. Artificial Intelligence. UMI Research Press, Ann Arbor, Michigan, 1981. Revision of Ph.D. Thesis - New York University, 1979.

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

[27] R. Paige. Applications of finite differencing to database integrity control and query/transaction optimization. In H. Gallaire, J. Minker, and J.-M. Nicolas, editors, Advances in Database Theory, Vol. 2, pages 171–210. Plenum Press, New York, March 1984.

[28] R. Paige. Symbolic finite differencing - part I. In Proceedings of the 3rd ESOP, pages 36–56, Copenhagen, Denmark, May 1990. Springer-Verlag, Berlin. LNCS 432.

[29] 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–232, 1987.

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

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

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

[33] G. Ramalingam and T. Reps. A categorized bibliography on incremental computation. In Conference Record of the 20th Annual ACM Symposium on POPL, pages 502–510, Charleston, South Carolina, January 1993.

[34] T. Reps and T. Teitelbaum. The Synthesizer Generator: A System for Constructing Language-Based Editors. Springer-Verlag, New York, 1988.

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

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

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

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

[39] D. R. Smith. KIDS - a knowledge-based software development system. In M. R. Lowry and R. D. McCartney, editors, Automating Software Design, chapter 19, pages 483–514. AAAI Press/The MIT Press, 1991. Proceedings of the Workshop on Automating Software Design, AAAI ’88.

[40] D. R. Smith and M. R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14:305–321, 1990.

[41] R. S. Sundaresh. Building incremental programs using partial evaluation. In Proceedings of the Symposium on PEPM, pages 83–93, Yale University, June 1991. Published as SIGPLAN Notices, 26(9).

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

[43] V. F. Turchin. The concept of a supercompiler. ACM Transactions on Programming Languages and Systems, 8(3):292–325, July 1986.

[44] B. T. Vander Zanden. Incremental constraint satisfaction and its application to graphical interfaces. Ph.D. Thesis TR 88-941, Department of Computer Science, Cornell University, October 1988.

[45] A. Varma and S. Chalasani. An incremental algorithm for TDM switching assignments in satellite and terrestrial networks. IEEE Journal on Selected Areas in Communications, 10(2):364–377, February 1992.

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

[47] B. Wegbreit. Goal-directed program transformation. IEEE Transactions on Software Engineering, SE-2(2):69– 80, June 1976.

[48] D. Yeh and U. Kastens. Improvements on an incremental evaluation algorithm for ordered attribute grammars. SIGPLAN Notices, 23(12):45–50, 1988.

[49] D. M. Yellin. Speeding up dynamic transitive closure for bounded degree graphs. Acta Informatica, 30(4):369– 384, July 1993.

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