Document Open Access Logo

A Strong Call-By-Need Calculus

Authors Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.9.pdf
  • Filesize: 0.77 MB
  • 22 pages

Document Identifiers

Author Details

Thibaut Balabonski
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Gif-sur-Yvette, 91190, France
Antoine Lanco
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, LMF, Gif-sur-Yvette, 91190, France
Guillaume Melquiond
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, LMF, Gif-sur-Yvette, 91190, France

Cite AsGet BibTex

Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A Strong Call-By-Need Calculus. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.9

Abstract

We present a call-by-need λ-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a λ-term t admits a normal form n in the λ-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
Keywords
  • strong reduction
  • call-by-need
  • evaluation strategy
  • normalization

Metrics

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

Related Versions

References

  1. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. A strong distillery. In Xinyu Feng and Sungwoo Park, editors, Programming Languages and Systems, volume 9458 of Lecture Notes in Computer Science, pages 231-250, 2015. URL: https://doi.org/10.1007/978-3-319-26529-2_13.
  2. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, page 659–670, 2014. URL: https://doi.org/10.1145/2535838.2535886.
  3. Beniamino Accattoli, Andrea Condoluci, and Claudio Sacerdoti Coen. Strong call-by-value is reasonable, implosively, 2021. URL: http://arxiv.org/abs/2102.06928.
  4. Beniamino Accattoli and Delia Kesner. The structural λ-calculus. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, pages 381-395, 2010. URL: https://doi.org/10.5555/1887459.1887491.
  5. Zena M. Ariola, John Maraist, Martin Odersky, Matthias Felleisen, and Philip Wadler. A call-by-need lambda calculus. In 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '95, pages 233-246, 1995. URL: https://doi.org/10.1145/199448.199507.
  6. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. Journal of Formalized Reasoning, 7(2):1-89, 2014. URL: https://doi.org/10.6092/issn.1972-5787/4650.
  7. Thibaut Balabonski. A unified approach to fully lazy sharing. In John Field and Michael Hicks, editors, 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pages 469-480, 2012. URL: https://doi.org/10.1145/2103656.2103713.
  8. 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, pages 263-274, September 2013. URL: https://doi.org/10.1145/2500365.2500606.
  9. Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner. Foundations of strong call by need. Proc. ACM Program. Lang., 1(ICFP), 2017. URL: https://doi.org/10.1145/3110264.
  10. Malgorzata Biernacka, Dariusz Biernacki, Witold Charatonik, and Tomasz Drab. An abstract machine for strong call by value. In Bruno C. d. S. Oliveira, editor, Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, volume 12470 of Lecture Notes in Computer Science, pages 147-166. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-64437-6_8.
  11. Malgorzata Biernacka and Witold Charatonik. Deriving an Abstract Machine for Strong Call by Need. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1-8:20, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.8.
  12. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the Lambda-Calculus. Logic Journal of the IGPL, 25(4):431-464, July 2017. URL: https://doi.org/10.1093/jigpal/jzx018.
  13. Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, 49(3):363-408, 2012. URL: https://doi.org/10.1007/s10817-011-9225-2.
  14. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In 13th ACM SIGPLAN International Conference on Functional Programming, ICFP, pages 143-156, 2008. URL: https://doi.org/10.1145/1411204.1411226.
  15. M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, 1980. URL: https://doi.org/10.1305/ndjfl/1093883253.
  16. Pierre Crégut. An abstract machine for lambda-terms normalization. In ACM Conference on LISP and Functional Programming, LFP '90, page 333–340, 1990. URL: https://doi.org/10.1145/91556.91681.
  17. Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. PhD thesis, Université Aix-Marseille II, 2007. Google Scholar
  18. Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, pages 555-574, 1994. Google Scholar
  19. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In 7th ACM SIGPLAN International Conference on Functional Programming, ICFP '02, page 235–246, 2002. URL: https://doi.org/10.1145/581478.581501.
  20. Carsten Kehler Holst and Darsten Krogh Gomard. Partial evaluation is fuller laziness. In ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM '91, page 223–233, 1991. URL: https://doi.org/10.1145/115865.115890.
  21. Delia Kesner. A theory of explicit substitutions with safe and full composition. Logical Methods in Computer Science, 5(3), 2009. URL: https://doi.org/10.2168/LMCS-5(3:1)2009.
  22. 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, pages 424-441, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_25.
  23. Delia Kesner and Daniel Ventura. Quantitative types for the linear substitution calculus. In Josep Diaz, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science, volume 8705 of Lecture Notes in Computer Science, pages 296-310, 2014. URL: https://doi.org/10.1007/978-3-662-44602-7_23.
  24. John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. J. Funct. Program., 8(3):275–317, May 1998. URL: https://doi.org/10.1017/S0956796898003037.
  25. Robin Milner. Local bigraphs and confluence: Two conjectures. Electron. Notes Theor. Comput. Sci., 175(3):65–73, 2007. URL: https://doi.org/10.1016/j.entcs.2006.07.035.
  26. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  27. Gordon D. Plotkin. A structural approach to operational semantics. Technical report, DAIMI FN-19, Computer Science Department, Aarhus University, 1981. Google Scholar
  28. Christopher P. Wadsworth. Semantics and Pragmatics of the Lambda Calculus. PhD thesis, Oxford, 1971. Google Scholar
  29. Nobuko Yoshida. Optimal reduction in weak-lambda-calculus with shared environments. In Conference on Functional Programming Languages and Computer Architecture, FPCA '93, page 243–252, 1993. URL: https://doi.org/10.1145/165180.165217.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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