Document Open Access Logo

Optimality and the Linear Substitution Calculus

Authors Pablo Barenbaum, Eduardo Bonelli

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2017.9.pdf
  • Filesize: 0.64 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • Rewriting
  • Lambda Calculus
  • Explicit Substitutions
  • Optimal Reduction

Metrics

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

Abstract

We lift the theory of optimal reduction to a decomposition of the lambda calculus known as the Linear Substitution Calculus (LSC). LSC decomposes beta-reduction into finer steps that manipulate substitutions in two distinctive ways: it uses context rules that allow substitutions to act "at a distance" and rewrites modulo a set of equations that allow substitutions to "float" in a term. We propose a notion of redex family obtained by adapting Lévy labels to support these two distinctive features. This is followed by a proof of the finite family developments theorem (FFD). We then apply FFD to prove an optimal reduction theorem for LSC. We also apply FFD to deduce additional novel properties of LSC, namely an algorithm for standardisation by selection and normalisation of a linear call-by-need reduction strategy. All results are proved in the axiomatic setting of Glauert and Khashidashvili's Deterministic Residual Structures.

Cite As Get BibTex

Pablo Barenbaum and Eduardo Bonelli. Optimality and the Linear Substitution Calculus. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.9

Author Details

Pablo Barenbaum
Eduardo Bonelli

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: http://dx.doi.org/10.1017/S0956796800000186.
  2. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. Distilling abstract machines. In J. Jeuring and M. Chakravarty, editors, Proceedings of ICFP, pages 363-376. ACM, 2014. Google Scholar
  3. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. A strong distillery. In Xinyu Feng and Sungwoo Park, editors, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings, volume 9458 of LNCS, pages 231-250. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-26529-2_13.
  4. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In Suresh Jagannathan and Peter Sewell, editors, POPL'14, San Diego, CA, USA, January 20-21, 2014, pages 659-670. ACM, 2014. URL: http://dx.doi.org/10.1145/2535838.2535886.
  5. Beniamino Accattoli and Claudio Sacerdoti Coen. On the relative usefulness of fireballs. In 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.
  6. Beniamino Accattoli and Delia Kesner. The structural lambda-calculus. In Anuj Dawar and Helmut Veith, editors, CSL 2010, volume 6247 of LNCS, pages 381-395. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15205-4_30.
  7. Beniamino Accattoli and Ugo Dal Lago. Beta reduction is invariant, indeed. In Thomas A. Henzinger and Dale Miller, editors, CSL-LICS'14, Vienna, Austria, July 14-18, 2014, pages 8:1-8:10. ACM, 2014. URL: http://dx.doi.org/10.1145/2603088.2603105.
  8. Beniamino Accattoli and Ugo Dal Lago. (leftmost-outermost) beta reduction is invariant, indeed. Logical Methods in Computer Science, 12(1), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(1:4)2016.
  9. Beniamino Accattoli and Luca Paolini. Call-by-value solvability, revisited. In Tom Schrijvers and Peter Thiemann, editors, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings, volume 7294 of LNCS, pages 4-16. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-29822-6_4.
  10. Andrea Asperti and Stefano Guerrini. The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science. CUP, 1999. Google Scholar
  11. Thibaut Balabonski. Weak optimality, and the meaning of sharing. In Greg Morrisett and Tarmo Uustalu, editors, ICFP'13, Boston, MA, USA - September 25-27, 2013, pages 263-274. ACM, 2013. URL: http://dx.doi.org/10.1145/2500365.2500606.
  12. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103. Elsevier, 1984. Google Scholar
  13. Zine-El-Abidine Benaissa, Pierre Lescanne, and Kristoffer Høgsbro Rose. Modeling sharing and recursion for weak reduction strategies using explicit substitution. In Herbert Kuchen and S. Doaitse Swierstra, editors, PLILP'96, Aachen, Germany, September 24-27, 1996, Proceedings, volume 1140 of LNCS, pages 393-407. Springer, 1996. URL: http://dx.doi.org/10.1007/3-540-61756-6_99.
  14. Gérard Boudol. Computational semantics of term rewriting systems. In M. Nivat and J.C. Reynolds, editors, Algebraic Methods in Semantics, page 169–236. CUP, 1985. Google Scholar
  15. John R. W. Glauert and Zurab Khasidashvili. Relative normalization in deterministic residual structures. In Hélène Kirchner, editor, CAAP'96, Linköping, Sweden, April, 22-24, 1996, Proceedings, volume 1059 of LNCS, pages 180-195. Springer, 1996. URL: http://dx.doi.org/10.1007/3-540-61064-2_37.
  16. Georges Gonthier, Martín Abadi, and Jean-Jacques Lévy. The geometry of optimal lambda reduction. In Ravi Sethi, editor, POPL'92, Albuquerque, New Mexico, USA, January 19-22, 1992, pages 15-26. ACM Press, 1992. URL: http://dx.doi.org/10.1145/143165.143172.
  17. Delia Kesner. Reasoning about call-by-need by means of types. In FoSSaCS 2016, pages 424-441. Springer-Verlag, 2016. Google Scholar
  18. Jean-Jacques Lévy. Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Université de Paris 7, 1978. Google Scholar
  19. Jean-Jacques Lévy. Generalized finite developments. In Essays in Honour of Gilles Kahn. CUP, 2007. Google Scholar
  20. Luc Maranget. Optimal derivations in weak lambda-calculi and in orthogonal terms rewriting systems. In David S. Wise, editor, POPL'91, Orlando, Florida, USA, January 21-23, 1991, pages 255-269. ACM Press, 1991. URL: http://dx.doi.org/10.1145/99583.99618.
  21. Paul-André Melliès. Description Abstraite des Systèmes de Réécriture. PhD thesis, Université Paris 7, december 1996. Google Scholar
  22. Paul-André Melliès. Axiomatic rewriting theory II: the λσ-calculus enjoys finite normalisation cones. J. Log. Comput., 10(3):461-487, 2000. URL: http://dx.doi.org/10.1093/logcom/10.3.461.
  23. Paul-André Melliès. Axiomatic rewriting theory VI residual theory revisited. In Sophie Tison, editor, RTA 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedings, volume 2378 of LNCS, pages 24-50. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-45610-4_4.
  24. Robin Milner. Local bigraphs and confluence: Two conjectures: (extended abstract). Electr. Notes Theor. Comput. Sci., 175(3):65-73, 2007. URL: http://dx.doi.org/10.1016/j.entcs.2006.07.035.
  25. Michael J. O'Donnell. Computing in Systems Described by Equations, volume 58 of LNCS. Springer, 1977. URL: http://dx.doi.org/10.1007/3-540-08531-9.
  26. H. J. Sander Bruggink. A proof of finite family developments for higher-order rewriting using a prefix property. In Frank Pfenning, editor, RTA 2006, volume 4098 of LNCS, pages 372-386. Springer, 2006. URL: http://dx.doi.org/10.1007/11805618_28.
  27. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. CUP, 2003. Google Scholar
  28. Vincent van Oostrom. Finite family developments. In Hubert Comon, editor, RTA-97, Sitges, Spain, June 2-5, 1997, Proceedings, volume 1232 of LNCS, pages 308-322. Springer, 1997. URL: http://dx.doi.org/10.1007/3-540-62950-5_80.
  29. Vincent van Oostrom, Kees-Jan van de Looij, and Marijn Zwitserlood. ] (lambdascope). Workshop on Algebra and Logic on Programming Systems (ALPS), April 2004. 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