Article

Free access

Incremental reduction in the lambda calculus

Authors:

Tim TeitelbaumAuthors Info & Claims

LFP '90: Proceedings of the 1990 ACM conference on LISP and functional programming

Pages 307 - 322

https://doi.org/10.1145/91556.91679

Published: 01 May 1990 Publication History

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.

References

[1]

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.

Digital Library

[2]

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.

[3]

H.P. Barendregt. The ~ambda Calculus, volume 103 of Studies in Logic and the Founda. tions of Mathematics. lXIorth-Holland, Amsterdam, 1984.

[4]

S.A. Bengelloun. Aspects of Incremental Computing. PhD thesis, Yale University, 1982.

Digital Library

[5]

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.

Digital Library

[6]

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.

[7]

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.

Digital Library

[8]

G. Cousineau, P.-L. Curien, and M. Mauny. The categorical abstract machine. Science of Computer Programming, 8:173-202, 1987.

Digital Library

[9]

P.-L. Curien. Categorical combinators. Information and Control, 69:188-254, 1986.

Digital Library

[10]

P.-L. Curien. Categorical Combinators, Sequential Algorithms, and Functional Programming. Research Notes in Theoretical Computer Science. Pitman, London, 1986.

Digital Library

[11]

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.

[12]

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.

Digital Library

[13]

J. Earley. High level iterators and a method for automatically designing data structure representation. Journal o/ Computer Languages, 1:321-342, 1976.

Digital Library

[14]

John Field. Incremental Reduction and its Applications. PhD thesis, Cornell University, 1990. (Forthcoming).

[15]

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.

Digital Library

[16]

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.

Digital Library

[17]

P. Henderson and J.H. Morris. A lazy evalutor. In Proc. Third A CM Symposium on Principles of Programming Languages, pages 95-103, 1976.

Digital Library

[18]

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.

[19]

J.W. Klop. Coml~inator!l Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematical Centre, Kruislaan 413, Amsterdam 1098SJ, The Netherlands, 1980.

[20]

Jean-Jacques L~vy. Rdductions correctes et optimales dans le lambda-calcul. PhD thesis, Universit6 de Paris VII, 1978. (Thbse d'Et~t).

[21]

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.

[22]

Michael J. O'Donnell. Computing in Systems Described by Equations. Springer-Verlag, 1977. Lecture Notes in Computer Science 58.

Digital Library

[23]

S.L. Peyton Jones. The Implementation o! Functional Programming Languages. Prentice Hall International, Englewood Cliffs, New Jersey, 1987.

Digital Library

[24]

R. Paige and S. Koenig. Finite differencing of computable expressions. Transactions on Programming Languages and Systems, 4(3):402- 454, July 1982.

Digital Library

[25]

W. Pugh and T. Teitelbaum. Incremental computation by function caching. In Proc. Sixteenth A CM Sgtmp. on Principles of Programming Languages, 1989.

Digital Library

[26]

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.

Digital Library

[27]

R.S. Sundaresh. Technical report. Yale University, 1990.

[28]

C.P. Wadsworth. Semantics and Pragmatics of the ~ambda-Calculus. PhD thesis, Oxford University, 1971.

[29]

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.

Cited By

Stein BChang BSridharan MFreund SYahav E(2021)Demanded abstract interpretationProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454044(282-295)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454044
Lester MOng LSchäfer M(2016)Information flow analysis for a dynamically typed language with staged metaprogrammingJournal of Computer Security10.3233/JCS-16055724:5(541-582)Online publication date: 8-Nov-2016
https://doi.org/10.3233/JCS-160557
Çiçek EGarg DAcar U(2015)Refinement Types for Incremental Computational ComplexityProgramming Languages and Systems10.1007/978-3-662-46669-8_17(406-431)Online publication date: 2015
https://doi.org/10.1007/978-3-662-46669-8_17
Show More Cited By

Index Terms

Incremental reduction in the lambda calculus
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
      1. Lambda calculus
  2. Mathematical analysis
    1. Calculus
      1. Lambda calculus
2. Theory of computation
  1. Randomness, geometry and discrete structures
  2. Semantics and reasoning
    1. Program constructs
      1. Functional constructs

Recommendations

Incremental Reduction in the Lambda Calculus
Incremental reduction in the lambda calculus and related reduction systems
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 programming

We 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LFP '90: Proceedings of the 1990 ACM conference on LISP and functional programming

May 1990

348 pages

ISBN:089791368X

DOI:10.1145/91556

Chairman:
Gilles Kahn

Copyright © 1990 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGAI: ACM Special Interest Group on Artificial Intelligence
SIGPLAN: ACM Special Interest Group on Programming Languages
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGSAM: ACM Special Interest Group on Symbolic and Algebraic Manipulation
INRIA: Institut Natl de Recherche en Info et en Automatique

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 1990

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

LFP90

Sponsor:

LFP90: ACM Conference on Lisp and Functional Programming

June 27 - 29, 1990

Nice, France

Acceptance Rates

Overall Acceptance Rate 30 of 109 submissions, 28%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

46
Total Citations
View Citations
517
Total Downloads

Downloads (Last 12 months)71
Downloads (Last 6 weeks)10

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Stein BChang BSridharan MFreund SYahav E(2021)Demanded abstract interpretationProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454044(282-295)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454044
Lester MOng LSchäfer M(2016)Information flow analysis for a dynamically typed language with staged metaprogrammingJournal of Computer Security10.3233/JCS-16055724:5(541-582)Online publication date: 8-Nov-2016
https://doi.org/10.3233/JCS-160557
Çiçek EGarg DAcar U(2015)Refinement Types for Incremental Computational ComplexityProgramming Languages and Systems10.1007/978-3-662-46669-8_17(406-431)Online publication date: 2015
https://doi.org/10.1007/978-3-662-46669-8_17
Chen YAcar UTangwongsan K(2014)Functional programming for dynamic and large data with self-adjusting computationACM SIGPLAN Notices10.1145/2692915.262815049:9(227-240)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2628150
Hammer MPhang KHicks MFoster J(2014)AdaptonACM SIGPLAN Notices10.1145/2666356.259432449:6(156-166)Online publication date: 9-Jun-2014
https://dl.acm.org/doi/10.1145/2666356.2594324
Chen YAcar UTangwongsan KJeuring JChakravarty M(2014)Functional programming for dynamic and large data with self-adjusting computationProceedings of the 19th ACM SIGPLAN international conference on Functional programming10.1145/2628136.2628150(227-240)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2628136.2628150
Hammer MPhang KHicks MFoster JO'Boyle MPingali K(2014)AdaptonProceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2594291.2594324(156-166)Online publication date: 9-Jun-2014
https://dl.acm.org/doi/10.1145/2594291.2594324
ACAR UBLUME MDONHAM J(2013)A consistent semantics of self-adjusting computationJournal of Functional Programming10.1017/S095679681300009923:3(249-292)Online publication date: 22-Oct-2013
https://doi.org/10.1017/S0956796813000099
Hammer MNeis GChen YAcar U(2011)Self-adjusting stack machinesACM SIGPLAN Notices10.1145/2076021.204812446:10(753-772)Online publication date: 22-Oct-2011
https://dl.acm.org/doi/10.1145/2076021.2048124
Burckhardt SLeijen DSadowski CYi JBall T(2011)Two for the price of oneACM SIGPLAN Notices10.1145/2076021.204810146:10(427-444)Online publication date: 22-Oct-2011
https://dl.acm.org/doi/10.1145/2076021.2048101
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents