Document Open Access Logo

The Zoo of Lambda-Calculus Reduction Strategies, And Coq

Authors Małgorzata Biernacka , Witold Charatonik , Tomasz Drab

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2022.7.pdf
  • Filesize: 0.83 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Operational semantics
  • Theory of computation → Automated reasoning
Keywords
  • Lambda calculus
  • Reduction strategies
  • Coq

Metrics

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

Abstract

We present a generic framework for the specification and reasoning about reduction strategies in the lambda calculus, representable as sets of term decompositions. It is provided as a Coq formalization that features a novel format of phased strategies. It facilitates concise description and algebraic reasoning about properties of reduction strategies. The formalization accommodates many well-known strategies, both weak and strong, such as call by name, call by value, head reduction, normal order, full β-reduction, etc. We illustrate the use of the framework as a tool to inspect and categorize the "zoo" of existing strategies, as well as to discover and study new ones with particular properties.

Cite As Get BibTex

Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab. The Zoo of Lambda-Calculus Reduction Strategies, And Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ITP.2022.7

Author Details

Małgorzata Biernacka
  • University of Wrocław, Faculty of Mathematics and Computer Science, Poland
Witold Charatonik
  • University of Wrocław, Faculty of Mathematics and Computer Science, Poland
Tomasz Drab
  • University of Wrocław, Faculty of Mathematics and Computer Science, Poland

Funding

This research is supported by the National Science Centre of Poland, under grant number 2019/33/B/ST6/00289.

Acknowledgements

We thank the anonymous reviewers for their comments and references to the literature. The last author thanks his wife, Monika, for taking care of everything around during proof completion.

Supplementary Materials

References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  6. Hendrik Pieter Barendregt, Richard Kennaway, Jan Willem Klop, and M. Ronan Sleep. Needed reduction and spine strategies for the lambda calculus. Inf. Comput., 75(3):191-231, 1987. URL: https://doi.org/10.1016/0890-5401(87)90001-0.
  7. 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, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings, 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.
  8. Malgorzata Biernacka, Witold Charatonik, and Klara Zielinska. Generalized refocusing: From hybrid strategies to abstract machines. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, volume 84 of LIPIcs, pages 10:1-10:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.10.
  9. Arthur Charguéraud. Pretty-big-step semantics. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7792 of Lecture Notes in Computer Science, pages 41-60. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_3.
  10. Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics, 2004. Google Scholar
  11. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. MIT Press, 2009. URL: http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11885.
  12. Matthias Felleisen and Robert Hieb. The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci., 103(2):235-271, 1992. URL: https://doi.org/10.1016/0304-3975(92)90014-7.
  13. 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.
  14. Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke. A mechanised proof of the time invariance thesis for the weak call-by-value λ-calculus. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pages 19:1-19:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.19.
  15. Yannick Forster and Gert Smolka. Call-by-value lambda calculus as a model of computation in coq. J. Autom. Reason., 63(2):393-413, 2019. URL: https://doi.org/10.1007/s10817-018-9484-2.
  16. Álvaro García-Pérez and Pablo Nogueira. On the syntactic and functional correspondence between hybrid (or layered) normalisers and abstract machines. Sci. Comput. Program., 95:176-199, 2014. URL: https://doi.org/10.1016/j.scico.2014.05.011.
  17. Gérard P. Huet. Residual theory in lambda-calculus: A formal development. J. Funct. Program., 4(3):371-394, 1994. URL: https://doi.org/10.1017/S0956796800001106.
  18. Gilles Kahn. Natural semantics. In Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing, editors, STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings, volume 247 of Lecture Notes in Computer Science, pages 22-39. Springer, 1987. URL: https://doi.org/10.1007/BFb0039592.
  19. Ugo Dal Lago and Beniamino Accattoli. Encoding turing machines into the deterministic lambda-calculus. CoRR, abs/1711.10078, 2017. URL: http://arxiv.org/abs/1711.10078.
  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 160-191. Academic Press, 1980. Google Scholar
  21. Conor McBride. The derivative of a regular type is its type of one-hole contexts (extended abstract), 2001. Google Scholar
  22. James McKinna and Robert Pollack. Some lambda calculus and type theory formalized. J. Autom. Reason., 23(3-4):373-409, 1999. URL: https://doi.org/10.1023/A:1006294005493.
  23. Michael Norrish. Mechanising lambda-calculus using a classical first order theory of terms with permutations. High. Order Symb. Comput., 19(2-3):169-195, 2006. URL: https://doi.org/10.1007/s10990-006-8745-7.
  24. Lawrence C. Paulson. ML for the working programmer (2. ed.). Cambridge University Press, 1996. Google Scholar
  25. Frank Pfenning. A proof of the church-rosser theorem and its representation in a logical framework, 1992. URL: https://www.cs.cmu.edu/~fp/papers/cr92.pdf.
  26. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. Programming Language Foundations. Software Foundations series, volume 2. Electronic textbook, May 2018. Version 5.5. Google Scholar
  27. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. URL: https://doi.org/10.1016/0304-3975(75)90017-1.
  28. Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebraic Methods Program., 60-61:17-139, 2004. Google Scholar
  29. Casper Bach Poulsen and Peter D. Mosses. Deriving pretty-big-step semantics from small-step semantics. In Zhong Shao, editor, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8410 of Lecture Notes in Computer Science, pages 270-289. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54833-8_15.
  30. John C. Reynolds. Definitional interpreters for higher-order programming languages. High. Order Symb. Comput., 11(4):363-397, 1998. URL: https://doi.org/10.1023/A:1010027404223.
  31. Peter Sestoft. Demonstrating lambda calculus reduction. 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 420-435. Springer, 2002. URL: https://doi.org/10.1007/3-540-36377-7_19.
  32. Natarajan Shankar. A mechanical proof of the church-rosser theorem. J. ACM, 35(3):475-522, 1988. URL: https://doi.org/10.1145/44483.44484.
  33. The Coq Development Team. The Coq proof assistant, January 2021. URL: https://doi.org/10.5281/zenodo.4501022.
  34. Eelco Visser. Stratego: A language for program transformation based on rewriting strategies. In Aart Middeldorp, editor, Rewriting Techniques and Applications, 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001, Proceedings, volume 2051 of Lecture Notes in Computer Science, pages 357-362. Springer, 2001. URL: https://doi.org/10.1007/3-540-45127-7_27.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact