An algorithm for optimal lambda calculus reduction

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An algorithm for optimal lambda calculus reduction

Full text

Pdf (1.56 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

San Francisco, California, United States

Pages: 16 - 30

Year of Publication: 1989

ISBN:0-89791-343-4

Author

John Lamping

Xerox PARC

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 53, Citation Count: 42

Additional Information:

abstract references cited by index terms collaborative colleagues peer to peer

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/96709.96711 What is a DOI?

ABSTRACT

We present an algorithm for lambda expression reduction that avoids any copying that could later cause duplication of work. It is optimal in the sense defined by Lévy. The basis of the algorithm is a graphical representation of the kinds of commonality that can arise from substitutions; the idea can be adapted to represent other kinds of expressions besides lambda expressions. The algorithm is also well suited to parallel implementations, consisting of a fixed set of local graph rewrite rules.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	H. P. Barendregt. The Lambda Calculus its Syntax: and Semantics, volume 103 of Studies in logic and the foundations of mathemalies. North-Holland, 1981.
	2	ti. P. Barendregt et al. LEAN, an intermediate language based on graph rewriting. Parallel Compulin9, 9:163-177, 1989.
	3	Vinod Kathail. private communication, 1989.
	4	jean-Jacques L~vy. R~ductions correctes et optimales dans le lambda-calcul. PhD thesis, Universit6 de Paris, 1978.
	5	Jean-Jacques Ldvy. Optimal reductions in the lambda-calculus. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinalory Logic, Lambda Calculus and Formalism, pages 159- 191. Academic Press, 1980.
	6	John Staples. Efficient evaluation of lambda expressions: a new strategy. Technical Report 23, University of Queensland, Department of Computer Science, St. Lucia, Queensland, 4067, Australia, 1980.
	7	John Staples, Two-level expression representation for faster evaluation, Proceedings of the 2nd International Workshop on Graph-Grammars and Their Application to Computer Science, p.392-404, October 04-08, 1982
	8	D. A. Turner. A new implementation technique for applicative languages. Software Practice and Experience, 9(1), 1979.
	9	C. P. Wadsworth. Semantics and Pragmatics of the )~-calculus. PhD thesis, Oxford University , 1971.

CITED BY 42

	Nobuko Yoshida, Optimal reduction in weak-&lgr;-calculus with shared environments, Proceedings of the conference on Functional programming languages and computer architecture, p.243-252, June 09-11, 1993, Copenhagen, Denmark
	Jens Peter Secher , Morten Heine Sørensen, From checking to inference via driving and dag grammars, ACM SIGPLAN Notices, v.37 n.3, p.41-51, March 2002
	Abubakar Hassan , Shinya Sato, Interaction Nets With Nested Pattern Matching, Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.1, p.79-92, March, 2008
	Sylvain Lippi, Encoding left reduction in the λ-calculus with interaction nets, Mathematical Structures in Computer Science, v.12 n.6, p.797-822, December 2002
	Harry G. Mairson, From Hilbert space to Dilbert space: context semantics as a language for games and flow analysis, ACM SIGPLAN Notices, v.38 n.9, p.125-125, September 2003
	Manuel Bodirsky , Katrin Erk , Joachim Niehren , Alexander Koller, Underspecified beta reduction, Proceedings of the 39th Annual Meeting on Association for Computational Linguistics, p.74-81, July 06-11, 2001, Toulouse, France
	Denis Béchet , Sylvain Lippi, Universal Boolean Systems, Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.1, p.19-30, March, 2008
	Georges Gonthier , Martín Abadi , Jean-Jacques Lévy, The geometry of optimal lambda reduction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.15-26, January 19-22, 1992, Albuquerque, New Mexico, United States
	Marco Pedicini , Francesco Quaglia, A parallel implementation for optimal lambda-calculus reduction, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.3-14, September 20-23, 2000, Montreal, Quebec, Canada
	Ugo Dal Lago , Simone Martini, The weak lambda calculus as a reasonable machine, Theoretical Computer Science, v.398 n.1-3, p.32-50, May, 2008
	Sylvain Lippi, The graphical Krivine machine, Higher-Order and Symbolic Computation, v.20 n.3, p.295-318, September 2007
	Ian Mackie , Jorge Sousa Pinto, Encoding linear logic with interaction combinators, Information and Computation, v.176 n.2, p.153-186, 01 August 2002
	Andrea Asperti, On the complexity of beta-reduction, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-118, January 21-24, 1996, St. Petersburg Beach, Florida, United States
	Julia L. Lawall , Harry G. Mairson, On global dynamics of optimal graph reduction, ACM SIGPLAN Notices, v.32 n.8, p.188-195, Aug. 1997
	Andrea Asperti , Paolo Coppola , Simone Martini, (Optimal) duplication is not elementary recursive, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.96-107, January 19-21, 2000, Boston, MA, USA
	Paolo Coppola , Simona Ronchi della Rocca, Principal Typing for Lambda Calculus in Elementary Affine Logic, Fundamenta Informaticae, v.65 n.1-2, p.87-112, January 2005
	Luc Maranget, Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.255-269, January 21-23, 1991, Orlando, Florida, United States
	F.-R. Sinot, Call-by-need in token-passing nets, Mathematical Structures in Computer Science, v.16 n.4, p.639-666, August 2006
	Paolo Coppola , Simone Martini, Optimizing optimal reduction: A type inference algorithm for elementary affine logic, ACM Transactions on Computational Logic (TOCL), v.7 n.2, p.219-260, April 2006
	Julia L. Lawall , Harry G. Mairson, Optimality and inefficiency: what isn't a cost model of the lambda calculus?, ACM SIGPLAN Notices, v.31 n.6, p.92-101, June 15, 1996
	Giorgio Busatto , Markus Lohrey , Sebastian Maneth, Efficient memory representation of XML document trees, Information Systems, v.33 n.4-5, p.456-474, June, 2008
	Stefano Guerrini , Simone Martini , Andrea Masini, Coherence for sharing proof-nets, Theoretical Computer Science, v.294 n.3, p.379-409, 18 February 2003
	Andrea Asperti , Paolo Coppola , Simone Martini, (Optimal) duplication is not elementary recursive, Information and Computation, v.193 n.1, p.21-56, 25 August 2004
	Marco Pedicini , Francesco Quaglia, PELCR: Parallel environment for optimal lambda-calculus reduction, ACM Transactions on Computational Logic (TOCL), v.8 n.3, p.14-es, July 2007
	Ian Mackie, YALE: yet another lambda evaluator based on interaction nets, ACM SIGPLAN Notices, v.34 n.1, p.117-128, Jan. 1999
	Hai Liu , Paul Hudak, Plugging a Space Leak with an Arrow, Electronic Notes in Theoretical Computer Science (ENTCS), 193, p.29-45, November, 2007
	Sandra Alves , Mário Florido , Ian Mackie , François-Régis Sinot, Minimality in a Linear Calculus with Iteration, Electronic Notes in Theoretical Computer Science (ENTCS), 204, p.163-179, April, 2008
	Zena M. Ariola , John Maraist , Martin Odersky , Matthias Felleisen , Philip Wadler, A call-by-need lambda calculus, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.233-246, January 23-25, 1995, San Francisco, California, United States
	François-Régis Sinot, Complete Laziness: a Natural Semantics, Electronic Notes in Theoretical Computer Science (ENTCS), 204, p.129-145, April, 2008
	Andrea Asperti , Harry G. Mairson, Parallel beta reduction is not elementary recursive, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-315, January 19-21, 1998, San Diego, California, United States
	Roberto Di Cosmo , Delia Kesner , Emmanuel Polonovski, Proof nets and explicit substitutions, Mathematical Structures in Computer Science, v.13 n.3, p.409-450, June 2003
	Pierre Crégut, Strongly reducing variants of the Krivine abstract machine, Higher-Order and Symbolic Computation, v.20 n.3, p.209-230, September 2007
	John Maraist , Martin Odersky , Philip Wadler, The call-by-need lambda calculus, Journal of Functional Programming, v.8 n.3, p.275-317, May 1998
	Zurab Khasidashvili , John Glauert, Relating conflict-free stable transition and event models via redex families, Theoretical Computer Science, v.286 n.1, p.65-95, 6 September 2002
	Zena M. Ariola , Matthias Felleisen, The call-by-need lambda calculus, Journal of Functional Programming, v.7 n.3, p.265-301, May 1997
	Andrea Aspetri , Harry G. Mairson, Parallel beta reduction is not elementary recursive, Information and Computation, v.170 n.1, p.49-80, October 10, 2001
	Zurab Khasidashvili , John Glauert, The conflict-free reduction geometry, Theoretical Computer Science, v.347 n.3, p.465-497, 1 December 2005
	Peter Møller Neergaard , Harry G. Mairson, Types, potency, and idempotency: why nonlinearity and amnesia make a type system work, ACM SIGPLAN Notices, v.39 n.9, September 2004
	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
	Pierre-Louis Curien , Thérèse Hardin , Jean-Jacques Lévy, Confluence properties of weak and strong calculi of explicit substitutions, Journal of the ACM (JACM), v.43 n.2, p.362-397, March 1996
	Healfdene Goguen , Jean Goubault-Larrecq, Sequent combinators: a Hilbert system for the lambda calculus, Mathematical Structures in Computer Science, v.10 n.1, p.1-79, February 2000
	Kohei Honda, Elementary structures in process theory (1): Sets with renaming, Mathematical Structures in Computer Science, v.10 n.5, p.617-663, October 2000