Document Open Access Logo

Optimizing a Non-Deterministic Abstract Machine with Environments

Authors Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.11.pdf
  • Filesize: 0.69 MB
  • 22 pages

Document Identifiers

Author Details

Małgorzata Biernacka
  • Institute of Computer Science, University of Wrocław, Poland
Dariusz Biernacki
  • Institute of Computer Science, University of Wrocław, Poland
Sergueï Lenglet
  • Université de Lorraine, Nancy, France
  • Université Sorbonne Paris Nord, France
Alan Schmitt
  • INRIA, France

Funding

This work is partially funded by the National Science Centre of Poland under grant no. 2019/33/B/ST6/00289, and PHC Polonium.

Acknowledgements

We thank the anonymous reviewers for their comments.

Cite AsGet BibTex

Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Optimizing a Non-Deterministic Abstract Machine with Environments. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.11

Abstract

Non-deterministic abstract machine (NDAM) is a recent implementation model for programming languages where one must choose among several redexes at each reduction step, like process calculi. These machines can be derived from a zipper semantics, a mix between structural operational semantics and context-based reduction semantics. Such a machine has been generated also for the λ-calculus without a fixed reduction strategy, i.e., with the full non-deterministic β-reduction. In that machine, substitution is an external operation that replaces all the occurrences of a variable at once. Implementing substitution with environments is more low-level and more efficient as variables are replaced only when needed. In this paper, we define a NDAM with environments for the λ-calculus without a fixed reduction strategy. We also introduce other optimizations, including a form of refocusing, and we show that we can restrict our optimized NDAM to recover some of the usual λ-calculus machines, e.g., the Krivine Abstract Machine. Most of the improvements we propose in this work could be applied to other NDAMs as well.

Subject Classification

ACM Subject Classification
  • Theory of computation → Abstract machines
Keywords
  • Abstract machine
  • Explicit substitutions
  • Refocusing

Metrics

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

Related Versions

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. Google Scholar
  2. Beniamino Accattoli. The Useful MAM, a reasonable implementation of the strong λ-calculus. In Jouko A. Väänänen, Åsa Hirvonen, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information, and Computation - 23rd International Workshop, WoLLIC 2016, Puebla, Mexico, August 16-19th, 2016. Proceedings, volume 9803 of Lecture Notes in Computer Science, pages 1-21. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-52921-8_1.
  3. Beniamino Accattoli and Pablo Barenbaum. A diamond machine for strong evaluation. CoRR, abs/2309.12515, 2023. URL: https://doi.org/10.48550/arXiv.2309.12515.
  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, Pablo Barenbaum, and Damiano Mazza. A strong distillery. In Xinyu Feng and Sungwoo Park, editors, Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings, volume 9458 of Lecture Notes in Computer Science, pages 231-250. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-26529-2_13.
  6. 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.
  7. 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.
  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, 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.
  10. 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.
  11. Beniamino Accattoli and Delia Kesner. The structural lambda-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.
  12. Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden, pages 8-19. ACM, 2003. Google Scholar
  13. Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Optimized abstract machine implementation. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:ba776d5226cde3b68cc6346fcd3a3495ad4d04e8;origin=https://gitlab.inria.fr/skeletons/lambda-am.git;visit=swh:1:snp:8f5867159d7cf9ce3bb93fed410bda2642b6f27a;anchor=swh:1:rev:3df61046f24f3c22170ab95c10be9a0fb67f5dd0 (visited on 06/06/2024). URL: https://gitlab.inria.fr/ skeletons/lambda-am.git.
  14. Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Non-deterministic abstract machines. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages 7:1-7:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  15. Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, and Alan Schmitt. Optimizing a non-deterministic abstract machine with environments. Available at https://inria.hal.science/hal-04568253, 2024.
  16. Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab. A derived reasonable abstract machine for strong call by value. In Niccolò Veltri, Nick Benton, and Silvia Ghilezan, editors, PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, Tallinn, Estonia, September 6-8, 2021, pages 6:1-6:14. ACM, 2021. URL: https://doi.org/10.1145/3479394.3479401.
  17. Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab. A simple and efficient implementation of strong call by need by an abstract machine. Proc. ACM Program. Lang., 6(ICFP):109-136, 2022. URL: https://doi.org/10.1145/3549822.
  18. Małgorzata Biernacka, Witold Charatonik, and Tomasz Drab. The zoo of lambda-calculus reduction strategies, and Coq. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237 of LIPIcs, pages 7:1-7:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.7.
  19. Małgorzata Biernacka and Olivier Danvy. A concrete framework for environment machines. ACM Trans. Comput. Log., 9(1):6, 2007. Google Scholar
  20. Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt. Skeletal semantics and their interpretations. PACMPL, 3(POPL):44:1-44:31, 2019. Google Scholar
  21. Luca Cardelli. Compiling a functional language. In Robert S. Boyer, Edward S. Schneider, and Guy L. Steele Jr., editors, Proceedings of the 1984 ACM Conference on LISP and Functional Programming, LFP 1984, Austin, Texas, USA, August 5-8, 1984, pages 208-217. ACM, 1984. URL: https://doi.org/10.1145/800055.802037.
  22. Guy Cousineau, Pierre-Louis Curien, and Michel Mauny. The Categorical Abstract Machine. Sci. Comput. Program., 8(2):173-202, 1987. URL: https://doi.org/10.1016/0167-6423(87)90020-7.
  23. Pierre Crégut. Strongly reducing variants of the Krivine abstract machine. High. Order Symb. Comput., 20(3):209-230, 2007. URL: https://doi.org/10.1007/s10990-007-9015-z.
  24. Pierre-Louis Curien. An abstract framework for environment machines. Theor. Comput. Sci., 82(2):389-402, 1991. URL: https://doi.org/10.1016/0304-3975(91)90230-Y.
  25. Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. Confluence properties of weak and strong calculi of explicit substitutions. J. ACM, 43(2):362-397, 1996. URL: https://doi.org/10.1145/226643.226675.
  26. Olivier Danvy. From reduction-based to reduction-free normalization. In Pieter W. M. Koopman, Rinus Plasmeijer, and S. Doaitse Swierstra, editors, Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures, volume 5832 of Lecture Notes in Computer Science, pages 66-164. Springer, 2008. Google Scholar
  27. Olivier Danvy and Lasse R. Nielsen. Syntactic theories in practice. Electron. Notes Theor. Comput. Sci., 59(4):358-374, 2001. Google Scholar
  28. Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics. Research Report BRICS RS-04-26, DAIMI, Department of Computer Science, Aarhus University, Aarhus, Denmark, November 2004. A preliminary version appeared in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science, Vol. 59.4. Google Scholar
  29. Nicholas G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34(5):381-392, 1972. Google Scholar
  30. Marc Feeley. An efficient and general implementation of futures on large scale shared-memory multiprocessors. PhD thesis, Department of Computer Science, Brandeis University, 1993. Google Scholar
  31. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. The MIT Press, 2009. Google Scholar
  32. Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD-machine, and the λ-calculus. In Martin Wirsing, editor, Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2/WG 2.2 Working Conference on Formal Description of Programming Concepts - III, Ebberup, Denmark, 25-28 August 1986, pages 193-222. North-Holland, 1987. Google Scholar
  33. Cormac Flanagan and Matthias Felleisen. The semantics of future and an application. J. Funct. Program., 9(1):1-31, 1999. URL: https://doi.org/10.1017/S0956796899003329.
  34. Álvaro García-Pérez and Pablo Nogueira. The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus. J. Funct. Program., 29:e7, 2019. URL: https://doi.org/10.1017/S0956796819000017.
  35. Álvaro García-Pérez, Pablo Nogueira, and Juan José Moreno-Navarro. Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order. 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 85-96. ACM, 2013. URL: https://doi.org/10.1145/2505879.2505887.
  36. Simon L. Peyton Jones. Implementing lazy functional languages on stock hardware: The Spineless Tagless G-machine. J. Funct. Program., 2(2):127-202, 1992. Google Scholar
  37. David A. Kranz, Robert H. Halstead Jr., and Eric Mohr. Mul-t: A high-performance parallel Lisp. In Richard L. Wexelblat, editor, Proceedings of the ACM SIGPLAN'89 Conference on Programming Language Design and Implementation (PLDI), Portland, Oregon, USA, June 21-23, 1989, pages 81-90. ACM, 1989. Google Scholar
  38. Jean-Louis Krivine. A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, 20(3):199-207, 2007. Google Scholar
  39. Peter J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308-320, 1964. Google Scholar
  40. Ivan Lanese, Jorge A. Pérez, Davide Sangiorgi, and Alan Schmitt. On the expressiveness and decidability of higher-order process calculi. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 145-155. IEEE Computer Society, 2008. Google Scholar
  41. Xavier Leroy. The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA, 1990. Google Scholar
  42. Joachim Niehren, Jan Schwinghammer, and Gert Smolka. A concurrent lambda calculus with futures. Theor. Comput. Sci., 364(3):338-356, 2006. URL: https://doi.org/10.1016/J.TCS.2006.08.016.
  43. Luca Paolini and Simona Ronchi Della Rocca. Call-by-value solvability. RAIRO Theor. Informatics Appl., 33(6):507-534, 1999. URL: https://doi.org/10.1051/ita:1999130.
  44. Gordon D. Plotkin. A structural approach to operational semantics. Technical Report FN-19, DAIMI, Department of Computer Science, Aarhus University, Aarhus, Denmark, September 1981. Google Scholar
  45. Kristoffer H. Rose. Explicit substitutions - tutorial & survey. BRICS Lecture Series LS-96-3, DAIMI, Aarhus, Denmark, September 1996. Google Scholar
  46. Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Inf. Comput., 239:340-355, 2014. Google Scholar
  47. Davide Sangiorgi. Bisimulation in higher-order process calculi. In Ernst-Rüdiger Olderog, editor, Programming Concepts, Methods and Calculi, Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi (PROCOMET '94) San Miniato, Italy, 6-10 June, 1994, volume A-56 of IFIP Transactions, pages 207-224. North-Holland, 1994. Google Scholar
  48. Peter Sestoft. Deriving a lazy abstract machine. J. Funct. Program., 7(3):231-264, 1997. URL: https://doi.org/10.1017/s0956796897002712.
  49. C.P. Wadsworth. Semantics and Pragmatics of the Lambda-Calculus. PhD thesis, University of 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 Imprint Privacy Contact