The geometry of optimal lambda reduction

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

The geometry of optimal lambda reduction

Full text

Pdf (1.06 MB)

Source

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

Albuquerque, New Mexico, United States

Pages: 15 - 26

Year of Publication: 1992

ISBN:0-89791-453-8

Authors

Georges Gonthier
Martín Abadi
Jean-Jacques Lévy

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): 5, Downloads (12 Months): 35, Citation Count: 38

Additional Information:

abstract references cited by index terms collaborative colleagues

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/143165.143172 What is a DOI?

ABSTRACT

Lamping discovered an optimal graph-reduction implementation of the &lgr;-calculus. Simultaneously, Girard invented the geometry of interaction, a mathematical foundation for operational semantics. In this paper, we connect and explain the geometry of interaction and Lamping's graphs. The geometry of interaction provides a suitable semantic basis for explaining and improving Lamping's system. On the other hand, graphs similar to Lamping's provide a concrete representation of the geometry of interaction. Together, they offer a new understanding of computation, as well as ideas for efficient and correct implementations.

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.

	Fie90	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]
	Gira	Jean-Yves Girard. Geometry of interaction II: Deadlock-free algorithms.
	Girb	Jean-Yves Girard. Linear logic and parallelism.
	Gir87	Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
	Gir89	Jean-Yves Girard. Geometry of interaction I: interpretation of system F. In Ferro, Bonotto, Valentini, and Zanardo, editors, Logic Colloquium '88, pages 221-260. Elsevier Science Publishers B.V. (North Holland), 1989.
	Gir91	Jean-Yves Girard. A new constructive logic: Classical logic. Technical report, June 1991. INRIA Report 1443.
	Kat90	Vinod Kathail. Optimal interpreters for lambda-calculus based functional languages. PhD thesis, MIT, May 1990.
	Laf90	Yves Lafont, Interaction nets, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.95-108, December 1989, San Francisco, California, United States [doi>10.1145/96709.96718]
	Lam90	John Lamping, An algorithm for optimal lambda calculus reduction, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.16-30, December 1989, San Francisco, California, United States [doi>10.1145/96709.96711]
	Lév80	Jean-Jacques L~vy. Optimal reductions in the lambda-calculus. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pages 159-191. Academic Press, 1980.
	Wad71	Christopher P. Wadsworth. Semantics and pragmatics of the lambda calculus. PhD thesis, Oxford, 1971.

CITED BY 38

	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
	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
	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
	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
	Ian Mackie, YALE: yet another lambda evaluator based on interaction nets, ACM SIGPLAN Notices, v.34 n.1, p.117-128, Jan. 1999
	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
	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
	Ian Mackie, The geometry of interaction machine, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.198-208, January 23-25, 1995, San Francisco, California, United States
	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
	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
	Stefano Guerrini , Simone Martini , Andrea Masini, Coherence for sharing proof-nets, Theoretical Computer Science, v.294 n.3, p.379-409, 18 February 2003
	Maribel Fernández , Ian Mackie, Operational equivalence for interaction nets, Theoretical Computer Science, v.297 n.1-3, p.157-181, 17 March 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
	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
	Maribel Fernández , Lionel Khalil, Interaction nets with McCarthy's amb: properties and applications, Nordic Journal of Computing, v.10 n.2, p.134-162, Summer 2003
	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 Aspetri , Harry G. Mairson, Parallel beta reduction is not elementary recursive, Information and Computation, v.170 n.1, p.49-80, October 10, 2001
	Damiano Mazza, A denotational semantics for the symmetric interaction combinators, Mathematical Structures in Computer Science, v.17 n.3, p.527-562, June 2007
	Samson Abramsky , Esfandiar Haghverdi , Philip Scott, Geometry of Interaction and linear combinatory algebras, Mathematical Structures in Computer Science, v.12 n.5, p.625-665, October 2002
	Alberto Pravato , Simona Ronchi Della Rocca , Luca Roversi, The call-by-value λ-calculus: a semantic investigation, Mathematical Structures in Computer Science, v.9 n.5, p.617-650, October 1999
	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
	Sylvain Lippi, The graphical Krivine machine, Higher-Order and Symbolic Computation, v.20 n.3, p.295-318, September 2007
	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
	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
	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
	Esfandiar Haghverdi, Unique decomposition categories, Geometry of Interaction and combinatory logic, Mathematical Structures in Computer Science, v.10 n.2, p.205-230, April 2000
	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
	Horatiu Cirstea , Germain Faure , Maribel Fernández , Ian Mackie , François-Régis Sinot, From Functional Programs to Interaction Nets via the Rewriting Calculus, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.10, p.39-56, July, 2007
	José Bacelar Almeida , Jorge Sousa Pinto , Miguel Vilaça, A Local Graph-rewriting System for Deciding Equality in Sum-product Theories, Electronic Notes in Theoretical Computer Science (ENTCS), v.176 n.1, p.139-163, May, 2007
	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
	F.-R. Sinot, Call-by-need in token-passing nets, Mathematical Structures in Computer Science, v.16 n.4, p.639-666, August 2006
	Maribel Fernández, Type assignment and termination of interaction nets, Mathematical Structures in Computer Science, v.8 n.6, p.593-636, December 1998
	Zena M. Ariola , Matthias Felleisen, The call-by-need lambda calculus, Journal of Functional Programming, v.7 n.3, p.265-301, May 1997
	Denis Béchet , Sylvain Lippi, Universal Boolean Systems, Electronic Notes in Theoretical Computer Science (ENTCS), v.203 n.1, p.19-30, March, 2008
	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
	Esfandiar Haghverdi , Philip J. Scott, Proofs as Polynomials, Electronic Notes in Theoretical Computer Science (ENTCS), 218, p.53-72, October, 2008
	Ugo Dal Lago, The geometry of linear higher-order recursion, ACM Transactions on Computational Logic (TOCL), v.10 n.2, p.1-38, February 2009
	Ugo Dal Lago, Context semantics, linear logic, and computational complexity, ACM Transactions on Computational Logic (TOCL), v.10 n.4, p.1-32, August 2009