Document Open Access Logo

A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus

Author Thibaut Balabonski

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.9.pdf
  • Filesize: 0.84 MB
  • 26 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Complexity classes
Keywords
  • Lambda-calculus
  • Complexity
  • Space
  • Logspace
  • Weak reduction

Metrics

Abstract

We propose a simple space-cost measure for the λ-calculus, that extends the natural model measuring the size of the terms by also taking into consideration their origin. This new model is able to capture sublinear space complexity and we prove that, in the context of weak reduction, it is reasonable with respect to standard complexity theory. Precisely, the weak λ-calculus and Turing machines can simulate each other with a constant-factor space overhead, for any computation of logarithmic or higher space complexity. This means that the weak λ-calculus equipped with our cost model gives a proper characterization of the classical space complexity classes, including LOGSPACE and PSPACE.

Cite As Get BibTex

Thibaut Balabonski. A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 9:1-9:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.9

Author Details

Thibaut Balabonski
  • Université Paris-Saclay, CNRS, Laboratoire Méthodes Formelles, 91190 Gif-sur-Yvette, France

References

  1. Beniamino Accattoli. The complexity of abstract machines. In Horatiu Cirstea and Santiago Escobar, editors, Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE@FSCD 2016, Porto, Portugal, 23rd June 2016, volume 235 of EPTCS, pages 1-15, 2016. URL: https://doi.org/10.4204/EPTCS.235.1.
  2. Beniamino Accattoli and Ugo Dal Lago. (leftmost-outermost) beta reduction is invariant, indeed. Log. Methods Comput. Sci., 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:4)2016.
  3. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. Multi types and reasonable space. Proc. ACM Program. Lang., 6(ICFP), August 2022. URL: https://doi.org/10.1145/3547650.
  4. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. A log-sensitive encoding of turing machines in the λ-calculus. CoRR, abs/2301.12556, 2023. URL: https://doi.org/10.48550/arXiv.2301.12556.
  5. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. Reasonable space for the λ-calculus, logarithmically. Log. Methods Comput. Sci., 20(4), 2024. URL: https://doi.org/10.46298/LMCS-20(4:15)2024.
  6. Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. Google Scholar
  7. Thibaut Balabonski. Weak optimality, and the meaning of sharing. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013, pages 263-274. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500606.
  8. Thibaut Balabonski. A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus. working paper or preprint, October 2025. URL: https://hal.science/hal-05322360.
  9. Thibaut Balabonski. Inlining as a Space Optimization: A Simple Time- and Space-Invariant Implementation of the Weak Lambda-Calculus. Proc. ACM Program. Lang., Volume 10, Issue ICFP(307), August 2026. URL: https://doi.org/10.1145/3828705.
  10. Hendrik P. Barendregt. The Lambda Calculus – Its Syntax and Semantics. North-Holland Publishing Company, Amsterdam, revised edition, 1984. Google Scholar
  11. Guy E. Blelloch and John Greiner. Parallelism in sequential functional languages. In John Williams, editor, Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995, pages 226-237. ACM, 1995. URL: https://doi.org/10.1145/224164.224210.
  12. Alonzo Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2):345-363, 1936. URL: http://www.jstor.org/stable/2371045.
  13. Alan Cobham. The intrinsic computational difficulty of functions. In Yehoshua Bar-Hillel, editor, Logic, Methodology and Philosophy of Science: Proceedings of the 1964 International Congress (Studies in Logic and the Foundations of Mathematics), pages 24-30. North-Holland Publishing, 1965. Google Scholar
  14. Haskell B. Curry, Robert Feys, and William Craig. Combinatory logic, Volume I. Studies in logic and the foundations of mathematics. North-Holland, Amsterdam, 1958. Google Scholar
  15. Nicolaas G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  16. Yannick Forster, Fabian Kunze, and Marc Roth. The weak call-by-value λ-calculus is reasonable for both time and space. Proc. ACM Program. Lang., 4(POPL):27:1-27:23, 2020. URL: https://doi.org/10.1145/3371095.
  17. Gudmund S. Frandsen and Carl Sturtivant. What is an efficient implementation of the λ-calculus? In John Hughes, editor, Functional Programming Languages and Computer Architecture, pages 289-312, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg. Google Scholar
  18. John Glauert and Zurab Khasidashvili. Relative normalization in deterministic residual structures. In Hélène Kirchner, editor, Trees in Algebra and Programming - CAAP '96, pages 180-195, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-61064-2_37.
  19. Juris Hartmanis and Richard E. Stearns. On the computational complexity of algorithms. Transactions of The American Mathematical Society - TRANS AMER MATH SOC, 117:285-285, May 1965. URL: https://doi.org/10.2307/1994208.
  20. John E. Hopcroft and Jeffrey D. Ullman. Formal Languages and Their Relation to Automata. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1969. Google Scholar
  21. Gérard Huet. Residual theory in λ-calculus: a formal development. Journal of Functional Programming, 4(3):371-394, 1994. URL: https://doi.org/10.1017/S0956796800001106.
  22. Jean-Louis Krivine. A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, 20:199-207, 2007. URL: https://doi.org/10.1007/S10990-007-9018-9.
  23. Ugo Dal Lago and Beniamino Accattoli. Encoding turing machines into the deterministic lambda-calculus. CoRR, abs/1711.10078, 2017. URL: https://arxiv.org/abs/1711.10078.
  24. Ugo Dal Lago and Simone Martini. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci., 398(1-3):32-50, 2008. URL: https://doi.org/10.1016/J.TCS.2008.01.044.
  25. Peter J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308-320, January 1964. URL: https://doi.org/10.1093/comjnl/6.4.308.
  26. Julia L. Lawall and Harry G. Mairson. Optimality and inefficiency: What isn't a cost model of the lambda calculus? In Robert Harper and Richard L. Wexelblat, editors, Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, ICFP 1996, Philadelphia, Pennsylvania, USA, May 24-26, 1996, pages 92-101. ACM, 1996. URL: https://doi.org/10.1145/232627.232639.
  27. Jean-Jacques Lévy. Optimal reductions in the lambda calculus. To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, January 1980. Google Scholar
  28. Christos H. Papadimitriou. Computational Complexity. Addison-Wesley, Reading, MA, 1994. Google Scholar
  29. David Sands, Jörgen Gustavsson, and Andrew Moran. Lambda calculi and linear speedups. In Torben Æ. Mogensen, David A. Schmidt, and Ivan Hal Sudborough, editors, The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones [on occasion of his 60th birthday], volume 2566 of Lecture Notes in Computer Science, pages 60-84. Springer, 2002. URL: https://doi.org/10.1007/3-540-36377-7_4.
  30. Cees F. Slot and Peter van Emde Boas. On tape versus core; an application of space efficient perfect hash functions to the invariance of space. J. Inf. Process. Cybern., 21(4/5):246-253, 1985. Google Scholar
  31. Richard E. Stearns, Juris Hartmanis, and Philip M. Lewis. Hierarchies of memory limited computations. In Proceedings of the 6th Annual Symposium on Switching Circuit Theory and Logical Design (SWCT 1965), FOCS '65, pages 179-190, USA, 1965. IEEE Computer Society. URL: https://doi.org/10.1109/FOCS.1965.11.
  32. Terese. Term rewriting systems, volume 55 of Cambridge tracts in theoretical computer science. Cambridge University Press, 2003. Google Scholar
  33. Alan M. Turing. Computability and λ-definability. Journal of Symbolic Logic, 2(4):153-163, 1937. URL: https://doi.org/10.2307/2268280.
  34. Alan M. Turing. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society, s2-42(1):230-265, January 1937. URL: https://doi.org/10.1112/plms/s2-42.1.230.
  35. Jan van Leeuwen, editor. Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity. Elsevier and MIT Press, 1990. Google Scholar
  36. Jan van Leeuwen, editor. Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics. Elsevier and MIT Press, 1990. URL: https://www.sciencedirect.com/book/9780444880741/formal-models-and-semantics.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact