Document Open Access Logo

Useful Open Call-By-Need

Authors Beniamino Accattoli , Maico Leberle

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.4.pdf
  • Filesize: 0.82 MB
  • 21 pages

Document Identifiers

Author Details

Beniamino Accattoli
  • Inria & École Polytechnique, Palaiseau, France
Maico Leberle
  • Inria & École Polytechnique, Palaiseau, France

Cite As Get BibTex

Beniamino Accattoli and Maico Leberle. Useful Open Call-By-Need. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.4

Abstract

This paper studies useful sharing, which is a sophisticated optimization for λ-calculi, in the context of call-by-need evaluation in presence of open terms. Useful sharing turns out to be harder in call-by-need than in call-by-name or call-by-value, because call-by-need evaluates inside environments, making it harder to specify when a substitution step is useful. We isolate the key involved concepts and prove the correctness and the completeness of useful sharing in this setting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Operational semantics
Keywords
  • lambda calculus
  • call-by-need
  • operational semantics
  • sharing
  • cost models

Metrics

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

Related Versions

References

  1. Samson Abramsky and C.-H. Luke Ong. Full abstraction in the lazy lambda calculus. Inf. Comput., 105(2):159-267, 1993. Google Scholar
  2. Beniamino Accattoli. The complexity of abstract machines. In WPTE@FSCD 2016, pages 1-15, 2016. URL: https://doi.org/10.4204/EPTCS.235.1.
  3. Beniamino Accattoli. The Useful MAM, a Reasonable Implementation of the Strong λ-Calculus. In WoLLIC 2016, pages 1-21, 2016. URL: https://doi.org/10.1007/978-3-662-52921-8_1.
  4. 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.
  5. Beniamino Accattoli. A fresh look at the lambda-calculus (invited talk). In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 1:1-1:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.1.
  6. 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.
  7. Beniamino Accattoli and Bruno Barras. Environments and the complexity of abstract machines. In PPDP 2017, pages 4-16, 2017. URL: https://doi.org/10.1145/3131851.3131855.
  8. Beniamino Accattoli and Bruno Barras. The negligible and yet subtle cost of pattern matching. In Bor-Yuh Evan Chang, editor, Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings, volume 10695 of Lecture Notes in Computer Science, pages 426-447. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-71237-6_21.
  9. Beniamino Accattoli and Claudio Sacerdoti Coen. On the relative usefulness of fireballs. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 141-155. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.23.
  10. 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.
  11. Beniamino Accattoli, Andrea Condoluci, and Claudio Sacerdoti Coen. Strong call-by-value is reasonable, implosively. In LICS, pages 1-14. IEEE, 2021. Google Scholar
  12. 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.
  13. Beniamino Accattoli and Ugo Dal Lago. On the invariance of the unitary cost model for head reduction. In RTA, volume 15 of LIPIcs, pages 22-37. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. Google Scholar
  14. Beniamino Accattoli and Ugo Dal Lago. (Leftmost-Outermost) Beta-Reduction is Invariant, Indeed. Logical Methods in Computer Science, 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:4)2016.
  15. Beniamino Accattoli and Giulio Guerrieri. Open call-by-value. In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 206-226, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_12.
  16. 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.
  17. 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.
  18. Beniamino Accattoli and Maico Leberle. Useful open call-by-need. CoRR, abs/2107.06591, 2021. URL: https://arxiv.org/abs/2107.06591, URL: http://arxiv.org/abs/2107.06591.
  19. Zena M. Ariola and Matthias Felleisen. The call-by-need lambda calculus. J. Funct. Program., 7(3):265-301, 1997. URL: http://journals.cambridge.org/action/displayAbstract?aid=44089.
  20. Zena M. Ariola, Hugo Herbelin, and Alexis Saurin. Classical call-by-need and duality. In C.-H. Luke Ong, editor, Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, volume 6690 of Lecture Notes in Computer Science, pages 27-44. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21691-6_6.
  21. Andrea Asperti and Harry G. Mairson. Parallel beta reduction is not elementary recursive. Inf. Comput., 170(1):49-80, 2001. URL: https://doi.org/10.1006/inco.2001.2869.
  22. Thibaut Balabonski. Weak optimality, and the meaning of sharing. In ICFP, pages 263-274. ACM, 2013. Google Scholar
  23. 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.
  24. Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A strong call-by-need calculus. In FSCD, volume 195 of LIPIcs, pages 9:1-9:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  25. 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.
  26. Hendrik Pieter Barendregt. The Lambda Calculus - Its Syntax and Semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1984. Google Scholar
  27. Bruno Barras. Auto-validation d'un système de preuves avec familles inductives. PhD thesis, Université Paris 7, 1999. Google Scholar
  28. 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, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 8:1-8:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.8.
  29. Tomasz Blanc, Jean-Jacques Lévy, and Luc Maranget. Sharing in the weak lambda-calculus. In Processes, Terms and Cycles, volume 3838 of Lecture Notes in Computer Science, pages 70-87. Springer, 2005. Google Scholar
  30. 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.
  31. Stephen Chang and Matthias Felleisen. The call-by-need lambda calculus, revisited. In Helmut Seidl, editor, Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7211 of Lecture Notes in Computer Science, pages 128-147. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_7.
  32. Arthur Charguéraud and François Pottier. Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In ITP 2015, pages 137-153, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_9.
  33. Ugo Dal Lago and Simone Martini. Derivational complexity is an invariant cost model. In Marko C. J. D. van Eekelen and Olha Shkaravska, editors, Foundational and Practical Aspects of Resource Analysis - First International Workshop, FOPARA 2009, Eindhoven, The Netherlands, November 6, 2009, Revised Selected Papers, volume 6324 of Lecture Notes in Computer Science, pages 100-113. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-15331-0_7.
  34. Ugo Dal Lago and Simone Martini. On constructor rewrite systems and the lambda calculus. Logical Methods in Computer Science, 8(3), 2012. URL: https://doi.org/10.2168/LMCS-8(3:12)2012.
  35. Olivier Danvy and Ian Zerny. A synthetic operational account of call-by-need evaluation. In Ricardo Peña and Tom Schrijvers, editors, 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, Madrid, Spain, September 16-18, 2013, pages 97-108. ACM, 2013. URL: https://doi.org/10.1145/2505879.2505898.
  36. Paul Downen, Luke Maurer, Zena M. Ariola, and Daniele Varacca. Continuations, processes, and sharing. In Olaf Chitil, Andy King, and Olivier Danvy, editors, Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014, pages 69-80. ACM, 2014. URL: https://doi.org/10.1145/2643135.2643155.
  37. Ronald Garcia, Andrew Lumsdaine, and Amr Sabry. Lazy evaluation and delimited control. Log. Methods Comput. Sci., 6(3), 2010. URL: http://arxiv.org/abs/1003.5197.
  38. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Mitchell Wand and Simon L. Peyton Jones, editors, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002, pages 235-246. ACM, 2002. URL: https://doi.org/10.1145/581478.581501.
  39. Jennifer Hackett and Graham Hutton. Call-by-need is clairvoyant call-by-value. Proc. ACM Program. Lang., 3(ICFP):114:1-114:23, 2019. URL: https://doi.org/10.1145/3341718.
  40. Hugo Herbelin and Étienne Miquey. A calculus of expandable stores: Continuation-and-environment-passing style translations. In LICS, pages 564-577. ACM, 2020. Google Scholar
  41. 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.
  42. Delia Kesner, Loïc Peyrot, and Daniel Ventura. The spirit of node replication. In FoSSaCS, volume 12650 of Lecture Notes in Computer Science, pages 344-364. Springer, 2021. Google Scholar
  43. Delia Kesner, Alejandro Ríos, and Andrés Viso. Call-by-need, neededness and all that. In FoSSaCS, volume 10803 of Lecture Notes in Computer Science, pages 241-257. Springer, 2018. Google Scholar
  44. 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, Maryland, USA, September 27-29, 1998, pages 324-335. ACM, 1998. URL: https://doi.org/10.1145/289423.289462.
  45. 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.
  46. Maico Leberle. Dissecting call-by-need by customizing multi type systems. Theses, Institut Polytechnique de Paris, May 2021. URL: https://tel.archives-ouvertes.fr/tel-03284370.
  47. Jean-Jacques Lévy. Réductions correctes et optimales dans le lambda-calcul. Thése d'Etat, Univ. Paris VII, France, 1978. Google Scholar
  48. John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. J. Funct. Program., 8(3):275-317, 1998. URL: http://journals.cambridge.org/action/displayAbstract?aid=44169.
  49. Masayuki Mizuno and Eijiro Sumii. Formal verifications of call-by-need and call-by-name evaluations with mutual recursion. In APLAS, volume 11893 of Lecture Notes in Computer Science, pages 181-201. Springer, 2019. Google Scholar
  50. Pierre-Marie Pédrot and Alexis Saurin. Classical by-need. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 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 9632 of Lecture Notes in Computer Science, pages 616-643. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_24.
  51. 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.
  52. Peter Sestoft. Deriving a lazy abstract machine. J. Funct. Program., 7(3):231-264, 1997. URL: http://journals.cambridge.org/action/displayAbstract?aid=44087.
  53. Christopher P. Wadsworth. Semantics and pragmatics of the lambda-calculus. PhD Thesis, Oxford, 1971. Google Scholar
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 About DROPS Imprint Privacy Contact