Document Open Access Logo

The Cost of Skeletal Call-By-Need, Smoothly

Authors Beniamino Accattoli , Francesco Magliocca , Loïc Peyrot , Claudio Sacerdoti Coen

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.5.pdf
  • Filesize: 1.01 MB
  • 22 pages
HTML5 Logo HTML (experimental)
LIPIcs.FSCD.2025.5.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • λ-calculus
  • abstract machines
  • call-by-need
  • cost models

Metrics

Abstract

Skeletal call-by-need is an optimization of call-by-need evaluation also known as "fully lazy sharing": when the duplication of a value has to take place, it is first split into "skeleton", which is then duplicated, and "flesh" which is instead kept shared.
Here, we provide two cost analyses of skeletal call-by-need. Firstly, we provide a family of terms showing that skeletal call-by-need can be asymptotically exponentially faster than call-by-need in both time and space; it is the first such evidence, to our knowledge.
Secondly, we prove that skeletal call-by-need can be implemented efficiently, that is, with bi-linear overhead. This result is obtained by providing a new smooth presentation of ideas by Shivers and Wand for the reconstruction of skeletons, which is then smoothly plugged into the study of an abstract machine following the distillation technique by Accattoli et al.

Cite As Get BibTex

Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, and Claudio Sacerdoti Coen. The Cost of Skeletal Call-By-Need, Smoothly. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.5

Author Details

Beniamino Accattoli
  • Inria & LIX, École Polytechnique, Palaiseau, France
Francesco Magliocca
  • Università degli Studi di Napoli Federico II, Italy
Loïc Peyrot
  • IMDEA Software Institute, Madrid, Spain
Claudio Sacerdoti Coen
  • Alma Mater Studiorum - Università di Bologna, Italy

Funding

  • Sacerdoti Coen, Claudio: Supported by the INdAM-GNCS project "Modelli Composizionali per l'Analisi di Sistemi Reversibili Distribuiti" and by the Cost Action CA2011 EuroProofNet.

Supplementary Materials

References

  1. Beniamino Accattoli. An abstract factorization theorem for explicit substitutions. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, volume 15 of LIPIcs, pages 6-21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPICS.RTA.2012.6.
  2. Beniamino Accattoli. Proof nets and the call-by-value λ-calculus. Theor. Comput. Sci., 606:2-24, 2015. URL: https://doi.org/10.1016/J.TCS.2015.08.006.
  3. Beniamino Accattoli. Proof nets and the linear substitution calculus. In Bernd Fischer and Tarmo Uustalu, editors, Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings, volume 11187 of Lecture Notes in Computer Science, pages 37-61. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02508-3_3.
  4. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. Distilling abstract machines. In Johan Jeuring and Manuel M. T. Chakravarty, editors, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, pages 363-376. ACM, 2014. URL: https://doi.org/10.1145/2628136.2628154.
  5. Beniamino Accattoli and Bruno Barras. Environments and the complexity of abstract machines. In Wim Vanhoof and Brigitte Pientka, editors, Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017, pages 4-16. ACM, 2017. URL: https://doi.org/10.1145/3131851.3131855.
  6. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 659-670. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535886.
  7. Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. Crumbling abstract machines. In Ekaterina Komendantskaya, editor, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019, pages 4:1-4:15. ACM, 2019. URL: https://doi.org/10.1145/3354166.3354169.
  8. Beniamino Accattoli, Andrea Condoluci, and Claudio Sacerdoti Coen. Strong call-by-value is reasonable, implosively. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470630.
  9. Beniamino Accattoli and Ugo Dal Lago. On the invariance of the unitary cost model for head reduction. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, volume 15 of LIPIcs, pages 22-37. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPICS.RTA.2012.22.
  10. 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.
  11. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The (in)efficiency of interaction. Proc. ACM Program. Lang., 5(POPL):1-33, 2021. URL: https://doi.org/10.1145/3434332.
  12. Beniamino Accattoli and Giulio Guerrieri. Abstract machines for open call-by-value. Sci. Comput. Program., 184, 2019. URL: https://doi.org/10.1016/J.SCICO.2019.03.002.
  13. Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Types by need. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 410-439. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_15.
  14. Beniamino Accattoli and Delia Kesner. The structural λ-calculus. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop , CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 381-395. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_30.
  15. 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.
  16. Beniamino Accattoli and Adrienne Lancelot. Mirroring call-by-need, or values acting silly. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, volume 299 of LIPIcs, pages 23:1-23:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.FSCD.2024.23.
  17. Beniamino Accattoli and Maico Leberle. Useful open call-by-need. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany, volume 216 of LIPIcs, pages 4:1-4:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.CSL.2022.4.
  18. Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, and Claudio Sacerdoti Coen. The cost of skeletal call-by-need, smoothly, 2025. URL: https://arxiv.org/abs/2505.09242.
  19. Beniamino Accattoli and Claudio Sacerdoti Coen. On the value of variables. Inf. Comput., 255:224-242, 2017. URL: https://doi.org/10.1016/J.IC.2017.01.003.
  20. Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL cut elimination with linear overhead. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, July 10-13, 2024, Tallinn, Estonia, volume 299 of LIPIcs, pages 24:1-24:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.FSCD.2024.24.
  21. Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. In Ron K. Cytron and Peter Lee, editors, Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 233-246. ACM Press, 1995. URL: https://doi.org/10.1145/199448.199507.
  22. Thibaut Balabonski. A unified approach to fully lazy sharing. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 469-480. ACM, 2012. URL: https://doi.org/10.1145/2103656.2103713.
  23. 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.
  24. Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner. Foundations of strong call by need. PACMPL, 1(ICFP):20:1-20:29, 2017. URL: https://doi.org/10.1145/3110264.
  25. Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A strong call-by-need calculus. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 9:1-9:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.FSCD.2021.9.
  26. Pablo Barenbaum, Eduardo Bonelli, and Kareem Mohamed. Pattern matching and fixed points: Resource types and strong call-by-need: Extended abstract. In David Sabel and Peter Thiemann, editors, Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pages 6:1-6:12. ACM, 2018. URL: https://doi.org/10.1145/3236950.3236972.
  27. Andrea Condoluci, Beniamino Accattoli, and Claudio Sacerdoti Coen. Sharing equality is linear. In Ekaterina Komendantskaya, editor, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019, pages 9:1-9:14. ACM, 2019. URL: https://doi.org/10.1145/3354166.3354174.
  28. 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.
  29. Tom Gundersen, Willem Heijltjes, and Michel Parigot. Atomic lambda calculus: A typed lambda-calculus with explicit sharing. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 311-320. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.37.
  30. John Hughes. The Design and Implementation of Programming Languages. PhD thesis, Programming Research Group, Oxford University, July 1983. Google Scholar
  31. Delia Kesner. Reasoning about call-by-need by means of types. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 424-441. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_25.
  32. Delia Kesner, Loïc Peyrot, and Daniel Ventura. Node replication: Theory and practice. Log. Methods Comput. Sci., 20(1), 2024. URL: https://doi.org/10.46298/LMCS-20(1:5)2024.
  33. Delia Kesner, Alejandro Ríos, and André s Viso. Call-by-need, neededness and all that. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Thessaloniki, Greece, April 14-20, 2018 , Proceedings, volume 10803 of Lecture Notes in Computer Science, pages 241-257. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_13.
  34. Arne Kutzner and Manfred Schmidt-Schauß. A non-deterministic call-by-need lambda calculus. In Matthias Felleisen, Paul Hudak, and Christian Queinnec, editors, Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), Baltimore, USA, September 27-29, 1998, pages 324-335. ACM, 1998. URL: https://doi.org/10.1145/289423.289462.
  35. John Launchbury. A natural semantics for lazy evaluation. In Mary S. Van Deusen and Bernard Lang, editors, Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993, pages 144-154. ACM Press, 1993. URL: https://doi.org/10.1145/158511.158618.
  36. Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987. Google Scholar
  37. 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.
  38. Peter Sestoft. Deriving a lazy abstract machine. J. Funct. Program., 7(3):231-264, 1997. URL: https://doi.org/10.1017/S0956796897002712.
  39. Olin Shivers and Mitchell Wand. Bottom-up beta-reduction: Uplinks and lambda-dags. Fundam. Informaticae, 103(1-4):247-287, 2010. URL: https://doi.org/10.3233/FI-2010-328.
  40. D. A. Turner. A new implementation technique for applicative languages. Softw. Pract. Exp., 9(1):31-49, 1979. URL: https://doi.org/10.1002/SPE.4380090105.
  41. Christopher P. Wadsworth. Semantics and pragmatics of the lambda-calculus. PhD Thesis, Oxford, 1971. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact