YALE: yet another lambda evaluator based on interaction nets

ABSTRACT

Interaction nets provide a graphical paradigm of computation based on net rewriting. They have proved most successful in understanding the dynamics of reduction in the λ-calculus, where the prime example is the implementation of optimal reduction for the λ-calculus (Lamping's algorithm), given by Gonthier, Abadi and Lévy. However, efficient implementations of optimal reduction have had to break away from the interaction net paradigm. In this paper we give a new efficient interaction net encoding of the λ-calculus which is not optimal, but overcomes the inefficiencies caused by the bookkeeping operations in the implementations of optimal reduction. We believe that this implementation of the λ-calculus could provide the basis for highly efficient implementations of functional languages.

REFERENCES

• 1: Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques L~vy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, October 1991.
• 2: Samson Abramsky, The lazy lambda calculus, Research topics in functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 3: Samson Abramsky, Computational interpretations of linear logic, Theoretical Computer Science, v.111 n.1-2, p.3-57, April 12, 1993 [doi>10.1016/0304-3975(93)90181-R]
• 4: Francisco Alberti. An abstract machine based on linear logic and explicit substitutions. Master's thesis, University of Birmingham, 1997.
• 5: Andrea Asperti, Cecilia Giovannetti, and Andrea Naletto. The bologna optimal higher-order machine. Journal of Functional Programming, 6(6):763- 810, November 1996.
• 6: Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, second, revised edition, 1984.
• 7: Vincent Danos and Laurent Regnier. Local and asynchronous beta-reduction (an analysis of Girard's execution formula). In Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science (LICS'93), pages 296-306. IEEE Computer Society Press, 1993.
• 8: Maribel Fernandez and Ian Mackie. A calculus for interaction nets, 1998. Available from http: //lix. pol yt e chnique, fr/~macki e.
• 9: 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]
• 10: Jean-Yves Girard. Geometry of interaction 1: Interpretation of System F. In R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo, editors, Logic Colloquium 88, Studies in Logic and the Foundations of Mathematics. North Holland Publishing Company, Amsterdam, August 1989.
• 11: 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 [doi>10.1145/143165.143172]
• 12: SSren Holmstr5m. Linear functional programming. In T. Johnsson, Simon L. Peyton Jones, and K. Karlsson, editors, Proceedings of the Workshop on Implementation of Lazy Functional Languages, pages 13-32, 1988.
• 13: Y. Lafont, The linear abstract machine, Theoretical Computer Science, v.59 n.1-2, p.157-180, July 1988 [doi>10.1016/0304-3975(88)90100-4]
• 14: 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]
• 15: Yves Lafont, Interaction combinators, Information and Computation, v.137 n.1, p.69-101, Aug. 25, 1997 [doi>10.1006/inco.1997.2643]
• 16: 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]
• 17: Ian Madde. The Geometry of Implementation. PhD thesis, Department of Computing, Imperial College of Science, Technology and Medicine, September 1994.
• 18: lan Mackie. Lilac: A functional programming language based on linear logic. Journal of Functional Programruing, 4(4):395-433, October 1994.
• 19: 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 [doi>10.1145/199448.199483]
• 20: I. Mackie, Linear Logic With Boxes, Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, p.309, June 21-24, 1998
• 21: Ian Mack"e and Jorge Sousa Pinto. Compiling the ),-calculus into interaction combinators, January 1998. Available from http:/.lli x. polyte chnique, fr/~mackie.
• 22: 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
• 23: Gmdon P'.otkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223-256, 1977.
• 24: Christopher P. Wadsworth. Semantics and Pragmatics .,~f ~he Lambda-Calculus. PhD thesis, Oxford University, 1972.
• 25: D'ax, id 'Wakeling. Linearity and Laziness. PhD thesis, Uni'~:m'sity of York, 1990.

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:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

General Terms:
Algorithms, Design, Experimentation, Languages, Measurement, Performance, Theory, Verification