John Field
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 λ-calculus and describe an incremental reduction algorithm, Λinc. We show that Λ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 λ-reduction strategy that may prove useful in a non-incremental setting as well.
Incremental λ-reduction can be used to advantage in any setting where an algorithm is specified in a functional or applicative manner.
- ACCL90.M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Levy. Explicit substitutions. In Proc. Seventeenth A CM Symposium on Principles o.f Progrumming Languages, San Francisco, 1990. Google Scholar
Digital Library
- 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.Google Scholar
- Bar84.H.P. Barendregt. The ~ambda Calculus, volume 103 of Studies in Logic and the Founda. tions of Mathematics. lXIorth-Holland, Amsterdam, 1984.Google Scholar
- Ben82.S.A. Bengelloun. Aspects of Incremental Computing. PhD thesis, Yale University, 1982. Google ScholarDigital Library
- BKKS87.H.P. Barendregt, J.R. Kennaway, J.W. Klop, and M.R. Sleep. Needed reduction and spine strategies for the lambda calculus. Information and Computation, 75:191-231, 1987. Google ScholarDigital Library
- 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.Google Scholar
- BvEG+87.H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway, M.J. Plasmeijer, and M.R. Sleep. Term graph rewriting. In Proc. PARLE Conference, Vol. H: Parallel Languages, pages 141-158, Eindhoven, The Netherlands, 1987. Springer-Verlag. Lecture Notes in Computer Science 259. Google ScholarDigital Library
- CCM87.G. Cousineau, P.-L. Curien, and M. Mauny. The categorical abstract machine. Science of Computer Programming, 8:173-202, 1987. Google ScholarDigital Library
- Cur86a.P.-L. Curien. Categorical combinators. Information and Control, 69:188-254, 1986. Google ScholarDigital Library
- Cur86b.P.-L. Curien. Categorical Combinators, Sequential Algorithms, and Functional Programming. Research Notes in Theoretical Computer Science. Pitman, London, 1986. Google ScholarDigital Library
- 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.Google Scholar
- DRT81.A. Demers, T. Reps, and T. Teitelbaum. Incremental evaluation for attribute grammars with application to syntax-directed editors. Proc. Eighth A CM Syrup. on Principles of C Programruing Languages, pages 105-116, 1981. Google ScholarDigital Library
- Ear76.J. Earley. High level iterators and a method for automatically designing data structure representation. Journal o/ Computer Languages, 1:321-342, 1976.Google ScholarDigital Library
- Fie90a.John Field. Incremental Reduction and its Applications. PhD thesis, Cornell University, 1990. (Forthcoming).Google Scholar
- Fie90b.John Field. On laziness and optimality in lambda interpreters: Tools for specification and analysis. In Proc. Seventeenth A CM Symposium on Principles of Programming Languages, San Francisco, January 1990. Google ScholarDigital Library
- FW87.Jon FairbaJrn and Stuart Wray. Tim: A simpie, lazy abstract machine to execute supercombinators. In Proc. Conference on Functional Programming Languages and Computer Architecture, pages 34-45, Portland, 1987. Springer- Verlag. Lecture Notes in Computer Science 274. Google ScholarDigital Library
- HM76.P. Henderson and J.H. Morris. A lazy evalutor. In Proc. Third A CM Symposium on Principles of Programming Languages, pages 95-103, 1976. Google ScholarDigital Library
- 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.Google Scholar
- Klo80.J.W. Klop. Coml~inator!l Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematical Centre, Kruislaan 413, Amsterdam 1098SJ, The Netherlands, 1980.Google Scholar
- 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).Google Scholar
- 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.Google Scholar
- O’D77.Michael J. O'Donnell. Computing in Systems Described by Equations. Springer-Verlag, 1977. Lecture Notes in Computer Science 58. Google ScholarDigital Library
- Pey87.S.L. Peyton Jones. The Implementation o! Functional Programming Languages. Prentice Hall International, Englewood Cliffs, New Jersey, 1987. Google ScholarDigital Library
- PK82.R. Paige and S. Koenig. Finite differencing of computable expressions. Transactions on Programming Languages and Systems, 4(3):402- 454, July 1982. Google ScholarDigital Library
- PT89.W. Pugh and T. Teitelbaum. Incremental computation by function caching. In Proc. Sixteenth A CM Sgtmp. on Principles of Programming Languages, 1989. Google ScholarDigital Library
- Rep82.T. Reps. Optimal-time incremental semantic analysis for syntax-directed editors. Proc. Ninth A CM Syrup. on Principles o! Programming Languages, pages 169-176, 1982. Google ScholarDigital Library
- Sun90.R.S. Sundaresh. Technical report. Yale University, 1990.Google Scholar
- Wad71.C.P. Wadsworth. Semantics and Pragmatics of the ~ambda-Calculus. PhD thesis, Oxford University, 1971.Google Scholar
- 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.Google Scholar
Index Terms
- Incremental reduction in the lambda calculus
Recommendations
Nested proof search as reduction in the Lambda-calculus
PPDP '11: Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programmingWe present a system for propositional implicative intuitionistic logic in the calculus of structures, which is a generalisation of the sequent calculus to the deep inference methodology. We show that it is sound and complete with respect to the usual ...
Comments