Incremental Reduction in the Lambda Calculus and Related Reduction Systems
An incremental algorithm is one that computes a function repeatedly on a series of inputs that differ only slightly from one another, yet avoids unnecessary duplication of computations from one input to the next. This thesis is a study of incremental computation in a general class of reduction systems, focusing particularly on the untyped lambda calculus and term rewriting systems. We also study implementation techniques used for such reduction systems and the question of the existence of optimal reduction strategies. Most of our results are based on a new class of reduction systems we define called regular replacement systems. These systems combine an abstract reduction relation with a notion of structure defined by a Brouwerian algebra. The reduction relation defines a computation system, while the algebra is used to define what constitutes an incremental change to some object. Numerous reduction systems, including many term and graph rewriting systems and a variant of the lambda calculus, constitute regular replacement systems. Among our results is a generalization of the lattice-theoretic reduction theory of Levy to regular replacement systems. This theory makes it possible to give a precise and intuitively appealing definition of what it means for both incremental and non-incremental computations to be optimal. We then investigate a family of term rewriting systems centered around a system we call $\bf \Lambda${\bf CCL}. Each of these systems is capable of simulating a normalizing reduction strategy in the lambda calculus. However, unlike the lambda calculus, the notion of substitution is an explicit part of $\bf \Lambda${\bf CCL}'s semantics, rather than being relegated to the status of meta-theory. Our study culminates with the definition of a $\bf \Lambda${\bf CCL}-based incremental reduction algorithm. This algorithm is optimal, yet it is simple enough to allow a practical implementation. We believe that appropriate generalizations of the ideas embodied in the algorithm can be used in a variety of practical settings, particularly those in which an algorithm is expressed in a functional or applicative manner.