Skip to main content


eCommons@Cornell

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: Nov-1991
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR91-1243
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 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.
URI: http://hdl.handle.net/1813/7083
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
91-1243.pdf21.09 MBAdobe PDFView/Open
91-1243.ps4.04 MBPostscriptView/Open

Refworks Export

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

 

© 2014 Cornell University Library Contact Us