eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/7083
Title:  Incremental Reduction in the Lambda Calculus and Related Reduction Systems 
Authors:  Field, John H. 
Keywords:  computer science technical report 
Issue Date:  Nov1991 
Publisher:  Cornell University 
Citation:  http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR911243 
Abstract:  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 latticetheoretic 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 nonincremental 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 metatheory. 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. 
URI:  http://hdl.handle.net/1813/7083 
Appears in Collections:  Computer Science Technical Reports

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
