On laziness and optimality in lambda interpreters: tools for specification and analysis

ABSTRACT

In this paper, I introduce a new formal system, ACCL, based on Curien's Categorical Combinators [Cur86a]. I show that ACCL has properties not possessed by Curien's original combinators that make it particularly appropriate as the basis for implementation and analysis of a wide range of reduction schemes using shared environments, closures, or &lgr;-terms. As an example of the practical utility of this formalism, I use it to specify a simple lazy interpreter for the &lgr;-calculus, whose correctness follows trivially from the properties of ACCL. I then describe a labeled variant of ACCL, ACCLL, which can be used as a tool to determine the degree of “laziness” possessed by various &lgr;-reduction schemes. In particular, ACCLL is applied to the problem of optimal reduction in the &lgr;-calculus. A reduction scheme for the &lgr;-calculus is optimal if the number of redex contractions that must be performed in the course of reducing any &lgr;-term to a normal form (if one exists) is guaranteed to be minimal. Results of Lévy [Lév78,Lév80] showed that for a natural class of reduction strategies allowing shared redexes, optimal reductions were, at least in principle, possible. He conjectured that an optimal reduction strategy might be realized in practice using shared closures and environments as well as shared &lgr;-terms. I show, however, using ACCLL, a practical optimal reduction scheme for arbitrary &lgr;-terms using only shared environments, closures, or terms is unlikely to exist.

REFERENCES

• ACCJL89: M. Abadi, L. CardeUi, P.-L. Curien, and J.J.- Levy. Explicit substitutions. In Proc. Seventeenth A CM Symposium on Principles o} Programming Languages, San Francisco, 1989.
• AKP84: Arvind, Vinod Kathail, and Keshav Pingali. Sharing of computation in functional language implementations, in Proc. international Work. shop on High-Level Computer Architecture, Los Angeles, 1984.
• AP81: Luigia Aiello and Gianfraneo Prini. An efficient interpreter for the lambda calculus. Journal of Computer and Sl/stem Sciences, 23:383-424, 1981.
• Aug84: Lennart Augustsson, A compiler for lazy ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.218-227, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802038]
• Bar84: H.P. Barendregt. The Lombda Calculus, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1984.
• BBKV76: H.P. Barendregt, J. Bergstra, J.W. Klop, and H. Volken. Degrees, reductions, and representability in the lambda calculus. Preprint 22, Department of Mathematics, University of Utrecht, The Netherlands, 1976.
• BKKS87: H. P. Barendregt , J. R. Kennaway , J. W. Klop , M. R. Sleep, Needed reduction and spine strategies for the lambda calculus, Information and Computation, v.75 n.3, p.191-231, Dec. 1987 [doi>10.1016/0890-5401(87)90001-0]
• CCM87: G. Cousineau , P.-L. Curien, The categorical abstract machine, Science of Computer Programming, v.8 n.2, p.173-202, April 1, 1987 [doi>10.1016/0167-6423(87)90020-7]
• Chu41: A. Church. The Calculi of Lambda Conversion. Princeton University Press, Princeton, NJ, 1941.
• Cur86a: P-L Curien, Categorical combinators, Information and Control, v.69 n.1-3, p.188-254, April/May/June 1986 [doi>10.1016/S0019-9958(86)80047-X]
• Cur86b: Pierre-Louis Curien, Categorical combinators, sequential algorithms, and functional programming (2nd ed.), Birkhauser Boston Inc., Cambridge, MA, 1994
• Cur86c: P.-L. Curien. De Is diificult~ d'impl~menter le partage optimal au sens de l~vy. Unpublished Note, Universit~ de Paris VII, 1986.
• dB72: N.G. de Bruijn. Larnbda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-tosser theorem. Proc. of the Koninkli. jke Nederlandse Akademie van Wetenschappen, 75(5):381-392, 1972.
• dB78: N.G. de Bruijn. Lambdn calculus with namefree formulas involving symbols that represent reference transforming mappings. Proc. of the Koninklijke Nederlandse Akademie van Wetenschappen, 81(3):348-356, 1978.
• Der87: Nachum Dershowitz, Termination of rewriting, Journal of Symbolic Computation, v.3 n.1-2, p.69-116, Feb./April 1987 [doi>10.1016/S0747-7171(87)80022-6]
• FH88: Anthony J. Field and Peter G. Harrison. Func. tional Programming. Addison-Wesley, Wakingham, England, 1988.
• FW87: John Fairbairn , Stuart Wray, TIM: A simple, lazy abstract machine to execute supercombinators, Proc. of a conference on Functional programming languages and computer architecture, p.34-45, October 1987, Portland, Oregon, United States
• Har87: Th~r~se Hardin. R~sultats de Confluence pour lea R~gles Fortes de la Logique Combinatoire Cat~gorique et Liens avec lea Lambda-Calctds. PhD thesis, Universit~ de Paris VII, 1987.
• Har89: Thérèse Hardin, Confluence results for the pure strong categorical logic CCL. &lgr;-calculi as subsystems of CCL, Theoretical Computer Science, v.65 n.3, p.291-342, July 1989 [doi>10.1016/0304-3975(89)90105-9]
• HL86: Th~r~se Hardin and AlaJn Laville. Proof of termination of the rewriting system SUBST on CUL. Rapports de Recherche 560, Institut National de Recherche en Informatique et en Autom~tique, Domxine de Voluceau, Rocquencourt, B.P. 105, 78153 Le Chesnay Cedex, France, August 1986.
• HM76: Peter Henderson , James H. Morris, Jr., A lazy evaluator, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.95-103, January 19-21, 1976, Atlanta, Georgia [doi>10.1145/800168.811543]
• HO80: G. Hunt a~d D.C. Oppen. Equations and rewrite rules: A survey. In R.V. Book, editor, Formal Language Theory, Perspectives, and Open Problems, pages 349-405. Academic Press, London, 1980.
• HS86: J. Roger Hindley , Jonathan P. Seldin, Introduction to combinators and &lgr;-calculus, Cambridge University Press, New York, NY, 1986
• Hue80: Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
• Hug84: R.J.M. Hughes. The Design and Implements. tion of Programming Languages. PhD thesis, Oxford University, September 1984. (PRG-40).
• Joh84: Thomas Johnsson, Efficient compilation of lazy evaluation, Proceedings of the 1984 SIGPLAN symposium on Compiler construction, p.58-69, June 17-22, 1984, Montreal, Canada
• Joh85: Thomas Johnsson, Lambda lifting: transforming programs to recursive equations, Proc. of a conference on Functional programming languages and computer architecture, p.190-203, January 1985, Nancy, France
• KL80: S. Kamin and J.-J. L~vy. Two generalizations of the recursive path orderings. Unpublished note, Department of Computer Science, Unlverity of Illinois, Urbana, IL, 1980.
• Klo80: J.W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematical Centre, Kruislaan 413, Amsterdam 1098SJ, The Netherlands, 1980.
• Lam89: 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]
• Lan64: P.J. Laadin. The mechanical evaluation of expressions. Computer Journal, 6:308-320, 1964.
• Les84: Pierre Lescanne. Uniform termination of term rewriting systems. In B. Courcelle, editor, Ninth Colloquium on Trees in Algebra and Pro. gramming, pages 181-191, Bordeaux, France, 1984. Cambridge University Press.
• Lév75: Jean-Jacques Lévy, An algebraic interpretation of the lambda beta - calculus and a labeled lambda - calculus, Proceedings of the Symposium on Lambda-Calculus and Computer Science Theory, p.147-165, March 25-27, 1975
• Lév78: Jeu-Jacques L~vy. R~duction8 correctes et op. timales dons le lambda-calcul. PhD thesis, Universit~ de Paris VII, 1978. (Th~se d'Etat).
• Lév80: Jeu-Jscques L~vy. Optimal reductions in the lsmbda-calculus. In J.P. Seldin and J.R. Hind- Icy, editors, To H.B. Curry: EsJays on Combi. natory Logic, Lambda Calculus, and Formalism. AceAemic Press, London, 1980.
• Lin87: R. D. Lins, On the efficiency of categorical combinators as a rewriting system, Software—Practice & Experience, v.17 n.8, p.547-559, Aug. 1987 [doi>10.1002/spe.4380170807]
• Pey87: 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
• Rus87: Michael Rusinowitch, Path of subterms ordering and recursive decomposition ordering revisited, Journal of Symbolic Computation, v.3 n.1-2, p.117-131, Feb./April 1987 [doi>10.1016/S0747-7171(87)80023-8]
• Sta80a: John Staples. Computation on graph-like expressions. Theoretical Computer Science, 10:171-185, 1980.
• Sta80b: John Staples. Optimal evaluations of graphlike expressions. Theoretical Computer Science, 10:297-316, 1980.
• Sta80c: John Staples. Speeding up subtree replacement systems. Theoretical Computer Science, 11:39- 4~, 1980.
• Sta81: John Staples. Efficient combinatory reduction. Zeitschr. !. math. Logik und Grundlagen d. Math., 27:391-402, 1981.
• Sta82: 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
• Tur79: D.A. Turner. A new imptementation technique for applicative lugusges. Software--Practice and Experience, 9:31-49, 1979.
• Wad71: C.P. Wadsworth. Semantics and Pragmatics of the Lambda.Calculus. PhD thesis, Oxford University, 1971.
• Yok89: Hirofumi Yokouchi, Church-Rosser theorem for a rewriting system on categorical combinators, Theoretical Computer Science, v.65 n.3, p.271-290, July 1989 [doi>10.1016/0304-3975(89)90104-7]

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.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Algorithms, Design, Languages