Optimality and inefficiency: what isn't a cost model of the lambda calculus?

ABSTRACT

We investigate the computational efficiency of the sharing graphs of Lamping [Lam90], Gonthier, Abadi, and Lévy [GAL92], and Asperti [Asp94], designed to effect so-called optimal evaluation, with the goal of reconciling optimality, efficiency, and the clarification of reasonable cost models for the λ-calculus. Do these graphs suggest reasonable cost models for the λ-calculus? If they are optimal, are they efficient?We present a brief survey of these optimal evaluators, identifying their common characteristics, as well as their shared failures. We give a lower bound on the efficiency of sharing graphs by identifying a class of λ-terms that are normalizable in Θ(n) time, and require Θ(n) "fan interactions," but require Ω(2ⁿ) bookkeeping steps. For [GAL92], we analyze this anomaly in terms of the dynamic maintenance of deBruijn indices for intermediate terms. We give another lower bound showing that sharing graphs can do Ω(2ⁿ) work (via fan interactions) on graphs that have no β-redexes. Finally, we criticize a proposed cost model for λ-calculus given by Frandsen and Sturtivant [FS91], showing by example that the model does not take account of the size of intermediate forms. Our example is a term requiring Θ(2ⁿ) steps while having proposed cost Θ(n). We propose some cost models that both reflect this parameter, and simultaneously reconcile key concepts from optimal reduction.

REFERENCES

• Asp94: Andrea Asperti. Linear logic, comonads, and optimal reductions. Unpublished manuscript.
• Asp95: Andrea Asperti, deltao!Epsilon = 1 - Optimizing Optimal lambda-Calculus Implementations, Proceedings of the 6th International Conference on Rewriting Techniques and Applications, p.102-116, April 05-07, 1995
• Asp96: 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 [doi>10.1145/237721.237742]
• Bar84: Hendrik Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984.
• vEB90: Peter van Erode Boas. Machi'~e models and simulation. Handbook of Theoretical Computer Science, volume A, pp. 1-66. North Holland, 1990.
• Chu41: Alonzo Church. The Cah:uli of Lambdaconversion. Princeton University Press, 1941.
• 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]
• FS91: Gudmund S. Frandsen , Carl Sturtivant, What is an efficient implementation of the &lgr;-calculus?, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.289-312, June 1991, Cambridge, Massachusetts, United States
• Gir88: Jean-Yves Girard. Geometry of interaction i: interpretation of System F. Logic Colloquim 1988, pp. 221-260. Elsevier (North Holland), 1989.
• GAL92: 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]
• Gue95: Stefano Guerrini. Sharing-graphs, sharingmorphisms, and (optimal))~-graph reductions (draft). Unpublished manuscript. June 16, 1995.
• Hug82: R. J. M. Hughes, Super-combinators a new implementation method for applicative languages, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.1-10, August 15-18, 1982, Pittsburgh, Pennsylvania, United States [doi>10.1145/800068.802129]
• Kat90: Vinod Kathail. Optimal interpreters for Iambdacalculus based functional languages. Ph.D. Thesis, MIT, May 1990.
• 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évy78: Jean-Jacques L~vy. Rdductio~s correcies et optimales dans le lambda-caIcuI. Th~se d'Etat, Universit~ Paris 7, 1978.
• Lévy80: Jean-Jacques L~vy. Optimal reductions in the lambda-calcuIus. To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, (Jonathan P. Seldin and J. Roger Hindley, editors), pp. 159-191. Academic Press, 1980.
• HM94: Harry G. Mairson and Fritz Henglein. The complexity of type inference for higher-order typed lambda calculi. Journal of Functional Programming 4:4 (October 1994), pp. 435-478.
• Mac95: 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]
• PJ87: Simon Peyton-Jones. The Implementation of Functional Programming Languages. Prentice-HaU~ 1987.
• Tur79: David A. Turner. New implementation techniques for applicative languages. Software Practice and Experience 9 (1979), pp. 31-49.

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

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY

General Terms:
Design, Languages, Theory, Verification