Incremental reduction in the lambda calculus

ABSTRACT

An incremental algorithm is one that takes advantage of the fact that the function it computes is to be evaluated repeatedly on inputs that differ only slightly from one another, avoiding unnecessary duplication of common computations. We define here a new notion of incrementality for reduction in the untyped &lgr;-calculus and describe an incremental reduction algorithm, &Lgr;inc. We show that &Lgr;inc has the desirable property of performing non-overlapping reductions on related terms, yet is simple enough to allow a practical implementation. The algorithm is based on a novel &lgr;-reduction strategy that may prove useful in a non-incremental setting as well. Incremental &lgr;-reduction can be used to advantage in any setting where an algorithm is specified in a functional or applicative manner.

REFERENCES

• ACCL90: M. Abadi , P. L. Curien , J. J. Levy, Explicit substitutions, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.31-46, December 1989, San Francisco, California, United States [doi>10.1145/96709.96712]
• ACR+87: B. Alpern, A. Carle, B. Rosen, P. Sweeney, and K. Zadeck. Incremental evaluation of attributed graphs. Technical Report RC 13205, IBM Thomas J. Watson Research Center, Yorktown Heights, New York 10598, October 1987.
• Bar84: H.P. Barendregt. The ~ambda Calculus, volume 103 of Studies in Logic and the Founda. tions of Mathematics. lXIorth-Holland, Amsterdam, 1984.
• Ben82: Safwan Abdelmajid Bengelloun, Aspects of incremental computing, 1982
• BKKS87: H. P. Barendregt , J. R. Kennaway , J. W. Klop , M. R. Sleep, Needed reduction and spine strategies for the lambda calculus, Information and Computation, v.75 n.3, p.191-231, Dec. 1987 [doi>10.1016/0890-5401(87)90001-0]
• BPR85: A.M. Berman, M. C. Paull, and B. G. Ryder. Proving relative lower bounds for incremental algorithms. Technical Report DCS-TR-154, Department of Computer Science, Rutgers University, New Brunswick, New Jersey 08903, 1985.
• BvEG+87: H P Barendregt , M C J D Eekelen , J R W Glauert , J R Kennaway , M J Plasmeijer , M R Sleep, Term graph rewriting, Volume II: Parallel Languages on PARLE: Parallel Architectures and Languages Europe, p.141-158, March 1987, Eindhoven, The Netherlands
• CCM87: G. Cousineau , P.-L. Curien, The categorical abstract machine, Science of Computer Programming, v.8 n.2, p.173-202, April 1, 1987 [doi>10.1016/0167-6423(87)90020-7]
• Cur86a: P-L Curien, Categorical combinators, Information and Control, v.69 n.1-3, p.188-254, April/May/June 1986 [doi>10.1016/S0019-9958(86)80047-X]
• Cur86b: Pierre-Louis Curien, Categorical combinators, sequential algorithms, and functional programming (2nd ed.), Birkhauser Boston Inc., Cambridge, MA, 1994
• dB72: N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Proc. of the Koninklijke 1Vederlandse Akademie van Wetenschappen, 75(5):381-392, 1972.
• DRT81: Alan Demers , Thomas Reps , Tim Teitelbaum, Incremental evaluation for attribute grammars with application to syntax-directed editors, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-116, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567544]
• Ear76: J. Earley. High level iterators and a method for automatically designing data structure representation. Journal o/ Computer Languages, 1:321-342, 1976.
• Fie90a: John Field. Incremental Reduction and its Applications. PhD thesis, Cornell University, 1990. (Forthcoming).
• Fie90b: John Field, On laziness and optimality in lambda interpreters: tools for specification and analysis, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-15, December 1989, San Francisco, California, United States [doi>10.1145/96709.96710]
• FW87: John Fairbairn , Stuart Wray, TIM: A simple, lazy abstract machine to execute supercombinators, Proc. of a conference on Functional programming languages and computer architecture, p.34-45, October 1987, Portland, Oregon, United States
• HM76: Peter Henderson , James H. Morris, Jr., A lazy evaluator, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.95-103, January 19-21, 1976, Atlanta, Georgia [doi>10.1145/800168.811543]
• JSS89: Neil D. Jones, Peter Sestoft, and Harald SZndergaard. Mix: A self-applicable partial evaluator for experiments in compiler generation. Lisp and Symbolic Computation, 2, 1989.
• Klo80: J.W. Klop. Coml~inator!l Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematical Centre, Kruislaan 413, Amsterdam 1098SJ, The Netherlands, 1980.
• Lév78: Jean-Jacques L~vy. Rdductions correctes et optimales dans le lambda-calcul. PhD thesis, Universit6 de Paris VII, 1978. (Thbse d'Et~t).
• Lév80: Jean-Jacques L6vy. Optimal reductions in the lambda-calculus. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combi. natory Logic, Lambda Calculus, and Formalism. Academic Press, London, 1980.
• O’D77: Michael J. O'Donnell, Computing in Systems Described by Equations, Springer-Verlag New York, Inc., Secaucus, NJ, 1977
• Pey87: Simon L. Peyton Jones, The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science), Prentice-Hall, Inc., Upper Saddle River, NJ, 1987
• PK82: Robert Paige , Shaye Koenig, Finite Differencing of Computable Expressions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.402-454, July 1982 [doi>10.1145/357172.357177]
• PT89: W. Pugh , T. Teitelbaum, Incremental computation via function caching, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.315-328, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75305]
• Rep82: Thomas Reps, Optimal-time incremental semantic analysis for syntax-directed editors, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.169-176, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582172]
• Sun90: R.S. Sundaresh. Technical report. Yale University, 1990.
• Wad71: C.P. Wadsworth. Semantics and Pragmatics of the ~ambda-Calculus. PhD thesis, Oxford University, 1971.
• YS87: D. Yellin and R. Strom. ~INC~: A language for incremental computations. Technical Report RC 13327, IBM Thomas J. Watson Research Center, Yorktown Heights, New York 1(}598, December 1987.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs

General Terms:
Algorithms, Languages, Theory