Document Open Access Logo

Renamingless Capture-Avoiding Substitution for Definitional Interpreters

Author Casper Bach Poulsen

PDF

File

Thumbnail PDF
PDF
OASIcs.EVCS.2023.2.pdf
  • Filesize: 0.55 MB
  • 10 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Semantics
Keywords
  • Capture-avoiding substitution
  • lambda calculus
  • definitional interpreter

Metrics

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

Abstract

Substitution is a common and popular approach to implementing name binding in definitional interpreters. A common pitfall of implementing substitution functions is variable capture. The traditional approach to avoiding variable capture is to rename variables. However, traditional renaming makes for an inefficient interpretation strategy. Furthermore, for applications where partially-interpreted terms are user facing it can be confusing if names in uninterpreted parts of the program have been changed. In this paper we explore two techniques for implementing capture avoiding substitution in definitional interpreters to avoid renaming.

Cite As Get BibTex

Casper Bach Poulsen. Renamingless Capture-Avoiding Substitution for Definitional Interpreters. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/OASIcs.EVCS.2023.2

Author Details

Casper Bach Poulsen
  • Delft University of Technology, The Netherlands

Acknowledgements

Thanks to Jan Friso Groote for feedback on a previous version of this paper, and to the anonymous reviewers who pointed out the work of Berkling and Fehr as an alternative solution to renamingless substitution.

Supplementary Materials

References

  1. Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. J. Funct. Program., 1(4):375-416, 1991. URL: https://doi.org/10.1017/S0956796800000186.
  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. Nada Amin and Tiark Rompf. Type soundness proofs with definitional interpreters. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 666-679. ACM, 2017. URL: https://doi.org/10.1145/3093333.3009866.
  4. Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser. Intrinsically-typed definitional interpreters for imperative languages. Proc. ACM Program. Lang., 2(POPL):16:1-16:34, 2018. URL: https://doi.org/10.1145/3158104.
  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. Henk Barendregt. The impact of the lambda calculus in logic and computer science. Bull. Symb. Log., 3(2):181-215, 1997. URL: https://doi.org/10.2307/421013.
  7. K. J. Berkling and Fehr E. A modification of the λ-calculus as a base for functional programming languages. In ICALP 1982. Springer Berlin Heidelberg, 1982. Google Scholar
  8. Felice Cardone and J. Roger Hindley. Logic from Russell to Church, volume 5 of Handbook of the History of Logic, chapter History of Lambda-calculus and Combinatory Logic. Elsevier, 2009. Google Scholar
  9. Arthur Charguéraud. The locally nameless representation. J. Autom. Reason., 49(3):363-408, 2012. URL: https://doi.org/10.1007/s10817-011-9225-2.
  10. Alonzo Church. A set of postulates for the foundation of logic. Annals of Mathematics, 33(2):346-366, 1932. Google Scholar
  11. Alonzo Church. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58(2):345-363, April 1936. URL: https://doi.org/10.2307/2371045.
  12. Haskell B. Curry and Robert Feys. Combinatory Logic. Combinatory Logic. North-Holland Publishing Company, 1958. Google Scholar
  13. Nils Anders Danielsson. Operational semantics using the partiality monad. In Peter Thiemann and Robby Bruce Findler, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pages 127-138. ACM, 2012. URL: https://doi.org/10.1145/2364527.2364546.
  14. N.G de Bruijn. Lambda calculus notation with nameless dummies. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  15. Shriram Krishnamurthi. Programming languages: Application and interpretation. https://www.plai.org/3/2/PLAI%20Version%203.2.0%20electronic.pdf, 2002. Accessed: 2022-12-01.
  16. P. J. Landin. The mechanical evaluation of expressions. Comput. J., 6(4):308-320, 1964. URL: https://doi.org/10.1093/comjnl/6.4.308.
  17. 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.
  18. Robin Milner, Mads Tofte, and Robert Harper. Definition of standard ML. MIT Press, 1990. Google Scholar
  19. Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. Functional big-step semantics. In 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 589-615, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-49498-1_23.
  20. Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Google Scholar
  21. 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.
  22. 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.
  23. Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. Intrinsically-typed definitional interpreters for linear, session-typed languages. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 284-298. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373818.
  24. Jeremy Siek. Essentials of Compilation. MIT Press, 2022. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact