Is the Optimal Implementation Inefficient? Elementarily Not

Authors Stefano Guerrini, Marco Solieri

Thumbnail PDF


  • Filesize: 0.77 MB
  • 16 pages

Document Identifiers

Author Details

Stefano Guerrini
Marco Solieri

Cite AsGet BibTex

Stefano Guerrini and Marco Solieri. Is the Optimal Implementation Inefficient? Elementarily Not. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Sharing graphs are a local and asynchronous implementation of lambda-calculus beta-reduction (or linear logic proof-net cut-elimination) that avoids useless duplications. Empirical benchmarks suggest that they are one of the most efficient machineries, when one wants to fully exploit the higher-order features of lambda-calculus. However, we still lack confirming grounds with theoretical solidity to dispel uncertainties about the adoption of sharing graphs. Aiming at analysing in detail the worst-case overhead cost of sharing operators, we restrict to the case of elementary and light linear logic, two subsystems with bounded computational complexity of multiplicative exponential linear logic. In these two cases, the bookkeeping component is unnecessary, and sharing graphs are simplified to the so-called "abstract algorithm". By a modular cost comparison over a syntactical simulation, we prove that the overhead of shared reductions is quadratically bounded to cost of the naive implementation, i.e. proof-net reduction. This result generalises and strengthens a previous complexity result, and implies that the price of sharing is negligible, if compared to the obtainable benefits on reductions requiring a large amount of duplication.
  • optimality
  • sharing graphs
  • lambda-calculus
  • complexity
  • linear logic
  • proof nets


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Andrea Asperti. About the efficient reduction of lambda terms. arXiv, January 2017. 1701.04240. URL:
  2. Andrea Asperti, Paolo Coppola, and Simone Martini. (Optimal) duplication is not elementary recursive. Inform. and Comput., 193(1):21-56, 2004. URL:
  3. Andrea Asperti, Cecilia Giovannetti, and Andrea Naletto. The Bologna optimal higher-order machine. Journal of Functional Programming, 6(6):763-810, November 1996. URL:
  4. Andrea Asperti and Stefano Guerrini. The Optimal Implementation of Functional Programming Languages, volume 45 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998. Google Scholar
  5. Andrea Asperti and Harry G. Mairson. Parallel Beta Reduction Is Not Elementary Recursive. Inf. Comput., 170(1):49-80, 2001. URL:
  6. Andrea Asperti and Luca Roversi. Intuitionistic light affine logic. ACM Trans. Comput. Logic, 3:137-175, January 2002. URL:
  7. Patrick Baillot, Paolo Coppola, and Ugo Dal Lago. Light logics and optimal reduction: Completeness and complexity. Information and Computation, 209(2):118-142, February 2011. URL:
  8. Ugo Dal Lago. Context semantics, linear logic, and computational complexity. ACM Transactions on Computational Logic (TOCL), 10(4):25:1-25:32, August 2009. URL:
  9. Ugo Dal Lago and Beniamino Accattoli. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Logical Methods in Computer Science, 12, 2016. URL:
  10. Ugo Dal Lago and Simone Martini. On Constructor Rewrite Systems and the Lambda-Calculus. In Automata, Languages and Programming, pages 163-174. Springer, July 2009. URL:
  11. J.-Y. Girard. Geometry of interaction I. Interpretation of system F. In R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo, editors, Logic colloquium 1988, volume 127 of Studies in Logic and The Foundations of Mathematics, pages 221-260. North-Holland, 1989. URL:
  12. Jean-Yves Girard. Light linear logic. Information and Computation, 143(2):175-204, 1998. URL:
  13. Georges Gonthier, Martín Abadi, and Jean-Jacques Lévy. The geometry of optimal lambda reduction. In Conference record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'92), pages 15-26, Albequerque, New Mexico, January 1992. Google Scholar
  14. Stefano Guerrini, Thomas Leventis, and Marco Solieri. Deep into optimality – complexity and correctness of sharing implementation of bounded logics. Third International Workshop on Developments in Implicit Complexity, 2012. Google Scholar
  15. Stefano Guerrini, Simone Martini, and Andrea Masini. Modal Logic, Linear Logic, Optimal Lambda-Reduction. In Logic and Foundations of Mathematics, number 280 in Synthese Library, pages 271-282. Springer, 1999. URL:
  16. Stefano Guerrini, Simone Martini, and Andrea Masini. Coherence for sharing proof-nets. Theoretical Computer Science, 294(3):379-409, February 2003. URL:
  17. Pavol Hell and Jaroslav Nesetril. Graphs and homomorphisms. Oxford Univ. Press, 2004. Google Scholar
  18. Yves Lafont. Interaction nets. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL'90, pages 95-108, New York, NY, USA, 1990. ACM. URL:
  19. John Lamping. An algorithm for optimal lambda calculus reduction. In Proc. of Seventeenth Annual ACM Symposyum on Principles of Programming Languages, pages 16-30, San Francisco, California, January 1990. URL:
  20. Jean-Jacques Lévy. Optimal reductions in the lambda-calculus. In Jonathan P. Seldin and J. Roger Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 159-191. Academic Press, 1980. Google Scholar
  21. Simon L. Peyton Jones. Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine. Journal of Functional Programming, 2(2):127-202, April 1992. URL:
  22. Richard Statman. The typed λ-calculus is not elementary recursive. Theoretical Computer Science, 9(1):73-81, 1979. URL:
  23. Peter van Emde Boas. Machine models and simulations, Handbook of theoretical computer science (vol. A): algorithms and complexity. MIT Press, Cambridge, MA, 1991. Google Scholar
  24. C. P. Wadsworth. Semantics and pragmatics of the lambda-calculus. PhD thesis, University of Oxford, 1971. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail