Document Open Access Logo

Deriving an Abstract Machine for Strong Call by Need

Authors Małgorzata Biernacka, Witold Charatonik

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.8.pdf
  • Filesize: 0.53 MB
  • 20 pages

Document Identifiers

Author Details

Małgorzata Biernacka
  • Institute of Computer Science, University of Wrocław, Poland
Witold Charatonik
  • Institute of Computer Science, University of Wrocław, Poland

Funding

This research is supported by the National Science Centre of Poland, under grant number 2014/15/B/ST6/00619.

Cite AsGet BibTex

Małgorzata Biernacka and Witold Charatonik. Deriving an Abstract Machine for Strong Call by Need. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.8

Abstract

Strong call by need is a reduction strategy for computing strong normal forms in the lambda calculus, where terms are fully normalized inside the bodies of lambda abstractions and open terms are allowed. As typical for a call-by-need strategy, the arguments of a function call are evaluated at most once, only when they are needed. This strategy has been introduced recently by Balabonski et al., who proved it complete with respect to full beta-reduction and conservative over weak call by need. We show a novel reduction semantics and the first abstract machine for the strong call-by-need strategy. The reduction semantics incorporates syntactic distinction between strict and non-strict let constructs and is geared towards an efficient implementation. It has been defined within the framework of generalized refocusing, i.e., a generic method that allows to go from a reduction semantics instrumented with context kinds to the corresponding abstract machine; the machine is thus correct by construction. The format of the semantics that we use makes it explicit that strong call by need is an example of a hybrid strategy with an infinite number of substrategies.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Operational semantics
Keywords
  • abstract machines
  • reduction semantics

Metrics

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

References

  1. Beniamino Accattoli. The Useful MAM, a Reasonable Implementation of the Strong λ-Calculus. In 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: http://dx.doi.org/10.1007/978-3-662-52921-8_1.
  2. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. A Strong Distillery. In Proceedings of APLAS, volume 9458 of Lecture Notes in Computer Science, pages 231-250. Springer, 2015. Google Scholar
  3. 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 (PPDP'17), Namur, Belgium, October 09 - 11, 2017, pages 4-16. ACM, 2017. URL: http://dx.doi.org/10.1145/3131851.3131855.
  4. 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: http://dx.doi.org/10.1109/LICS.2015.23.
  5. Beniamino Accattoli and Giulio Guerrieri. Implementing Open Call-by-Value. In Mehdi Dastani and Marjan Sirjani, editors, Fundamentals of Software Engineering - 7th International Conference, FSEN 2017, Tehran, Iran, April 26-28, 2017, Revised Selected Papers, volume 10522 of Lecture Notes in Computer Science, pages 1-19. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-68972-2_1.
  6. Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Evaluators and Abstract Machines. In Dale Miller, editor, Proceedings of the Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'03), pages 8-19, Uppsala, Sweden, August 2003. ACM Press. Google Scholar
  7. Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Call-by-Need Evaluators and Lazy Abstract Machines. Inf. Process. Lett., 90(5):223-232, 2004. Extended version available as the research report BRICS RS-04-3. Google Scholar
  8. Zena M. Ariola and Matthias Felleisen. The Call-By-Need lambda Calculus. Journal of Functional Programming, 7(3):265-301, 1997. Google Scholar
  9. Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. The Call-by-Need Lambda Calculus. In Peter Lee, editor, Proceedings of the Twenty-Second Annual ACM Symposium on Principles of Programming Languages, pages 233-246, San Francisco, California, January 1995. ACM Press. Google Scholar
  10. Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner. Foundations of strong call by need. PACMPL, 1(ICFP):20:1-20:29, 2017. URL: http://dx.doi.org/10.1145/3110264.
  11. Pablo Barenbaum, Eduardo Bonelli, and Kareem Mohamed. Pattern Matching and Fixed Points: Resource Types and Strong Call-By-Need: Extended Abstract. In PPDP, pages 6:1-6:12. ACM, 2018. Google Scholar
  12. 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 fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2017.10.
  13. Małgorzata Biernacka and Olivier Danvy. A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines. Theor. Comput. Sci., 375(1-3):76-108, 2007. Google Scholar
  14. Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. Full Reduction at Full Throttle. In Proceedings of the First International Conference on Certified Programs and Proofs, CPP'11, pages 362-377, Berlin, Heidelberg, 2011. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-642-25379-9_26.
  15. Pierre Crégut. An abstract machine for lambda-terms normalization. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 333-340, Nice, France, June 1990. ACM Press. Google Scholar
  16. Pierre Crégut. Strongly Reducing Variants of the Krivine Abstract Machine. Higher-Order and Symbolic Computation, 20(3):209-230, 2007. A preliminary version was presented at the 1990 ACM Conference on Lisp and Functional Programming. Google Scholar
  17. Olivier Danvy, Kevin Millikin, Johan Munk, and Ian Zerny. Defunctionalized Interpreters for Call-by-Need Evaluation. In Matthias Blume and German Vidal, editors, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, number 6009 in Lecture Notes in Computer Science, pages 240-256, Sendai, Japan, April 2010. Springer. Google Scholar
  18. 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
  19. Olivier Danvy and Ian Zerny. A Synthetic Operational Account of Call-by-need Evaluation. In Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP '13, pages 97-108, New York, NY, USA, 2013. ACM. URL: http://dx.doi.org/10.1145/2505879.2505898.
  20. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics Engineering with PLT Redex. The MIT Press, 1st edition, 2009. Google Scholar
  21. Ronald Garcia, Andrew Lumsdaine, and Amr Sabry. Lazy evaluation and delimited control. In Benjamin C. Pierce, editor, Proceedings of the Thirty-Fifth Annual ACM Symposium on Principles of Programming Languages, pages 153-164. ACM Press, January 2009. Google Scholar
  22. A García-Pérez and Pablo Nogueira. On the syntactic and functional correspondence between hybrid (or layered) normalisers and abstract machines. Science of Computer Programming, 95:176-199, 2014. Google Scholar
  23. Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In Simon Peyton Jones, editor, Proceedings of the 2002 ACM SIGPLAN International Conference on Functional Programming (ICFP'02), SIGPLAN Notices, Vol. 37, No. 9, pages 235-246, Pittsburgh, Pennsylvania, September 2002. ACM Press. Google Scholar
  24. John Launchbury. A Natural Semantics for Lazy Evaluation. In Susan L. Graham, editor, Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 144-154, Charleston, South Carolina, January 1993. ACM Press. Google Scholar
  25. John Maraist, Martin Odersky, and Philip Wadler. The Call-by-Need Lambda Calculus. Journal of Functional Programming, 8(3):275-317, 1998. Google Scholar
  26. Simon L. Peyton Jones. Implementing Lazy Functional Languages on Stock Hardware: The Spineless Tagless G-Machine. Journal of Functional Programming, 2(2):127-202, 1992. Google Scholar
  27. Maciej Piróg and Dariusz Biernacki. A systematic derivation of the STG machine verified in Coq. In Jeremy Gibbons, editor, Proceedings of the 2010 ACM SIGPLAN Haskell Symposium (Haskell'10), pages 25-36, Baltimore, MD, September 2010. ACM Press. Google Scholar
  28. Peter Sestoft. Deriving a Lazy Abstract Machine. Journal of Functional Programming, 7(3):231-264, May 1997. Google Scholar
  29. Filip Sieczkowski, Małgorzata Biernacka, and Dariusz Biernacki. Automating derivations of abstract machines from reduction semantics: a generic formalization of refocusing in Coq. In Juriaan Hage and Marco T. Morazán, editors, The 22nd International Conference on Implementation and Application of Functional Languages (IFL 2010), number 6647 in Lecture Notes in Computer Science, pages 72-88, Alphen aan den Rijn, The Netherlands, September 2010. Springer-Verlag. Google Scholar
  30. The Coq Development Team. The Coq Proof Assistant, V. 8.7, 2018. URL: https://github.com/coq/coq.
  31. David A. Turner. A New Implementation Technique for Applicative Languages. Software - Practice and Experience, 9(1):31-49, 1979. Google Scholar
  32. C.P. Wadsworth. Semantics and Pragmatics of the Lambda-calculus. University of Oxford, 1971. URL: https://books.google.pl/books?id=kl1QIQAACAAJ.
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