Document Open Access Logo

IMELL Cut Elimination with Linear Overhead

Authors Beniamino Accattoli , Claudio Sacerdoti Coen

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2024.24.pdf
  • Filesize: 0.93 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

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

Metrics

Abstract

Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination. He also introduced a new cut elimination strategy, dubbed the good strategy, and showed that its number of steps is a time cost model with polynomial overhead for ESC/IMELL, and the first such one.
Here, we refine Accattoli’s result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead.

Cite As Get BibTex

Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.FSCD.2024.24

Author Details

Beniamino Accattoli
  • Inria & LIX, École Poytechnique, UMR 7161, Palaiseau, France
Claudio Sacerdoti Coen
  • Alma Mater Studiorum - Università di Bologna, Italy

Funding

  • Sacerdoti Coen, Claudio: Supported by the INdAM-GNCS project "Modelli Composizionali per l'Analisi di Sistemi Reversibili Distribuiti" and by the Cost Action CA2011 EuroProofNet.

Supplementary Materials

References

  1. Samson Abramsky. Computational interpretations of linear logic. Theor. Comput. Sci., 111(1&2):3-57, 1993. URL: https://doi.org/10.1016/0304-3975(93)90181-R.
  2. Beniamino Accattoli. An abstract factorization theorem for explicit substitutions. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, volume 15 of LIPIcs, pages 6-21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPICS.RTA.2012.6.
  3. 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, pages 1-21, 2016. URL: https://doi.org/10.1007/978-3-662-52921-8_1.
  4. Beniamino Accattoli. Exponentials as substitutions and the cost of cut elimination in linear logic. Log. Methods Comput. Sci., 19(4), 2023. URL: https://doi.org/10.46298/LMCS-19(4:23)2023.
  5. Beniamino Accattoli and Pablo Barenbaum. A diamond machine for strong evaluation. In Chung-Kil Hur, editor, Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Taipei, Taiwan, November 26-29, 2023, Proceedings, volume 14405 of Lecture Notes in Computer Science, pages 69-90. Springer, 2023. URL: https://doi.org/10.1007/978-981-99-8311-7_4.
  6. 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.
  7. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. A strong distillery. CoRR, abs/1509.00996, 2015. URL: https://arxiv.org/abs/1509.00996.
  8. 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.
  9. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 659-670. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535886.
  10. 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.
  11. Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead, 2024. URL: https://arxiv.org/abs/2405.03669.
  12. 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.
  13. Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. Crumbling abstract machines. In 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.
  14. Beniamino Accattoli and Ugo Dal Lago. On the Invariance of the Unitary Cost Model for Head Reduction. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, pages 22-37. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.22.
  15. Beniamino Accattoli and Ugo Dal Lago. (Leftmost-outermost) Beta reduction is invariant, indeed. Logical Methods in Computer Science, 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:4)2016.
  16. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The (in)efficiency of interaction. Proc. ACM Program. Lang., 5(POPL):1-33, 2021. URL: https://doi.org/10.1145/3434332.
  17. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. The space of interaction. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470726.
  18. 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.
  19. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. Reasonable space for the λ-calculus, logarithmically. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 47:1-47:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533362.
  20. Beniamino Accattoli and Maico Leberle. Useful open call-by-need. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 4:1-4:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.CSL.2022.4.
  21. Francisco Alberti and Eike Ritter. An efficient linear abstract machine with single-pointer property, 1998. ESSLLI. Google Scholar
  22. Malgorzata 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.
  23. Malgorzata 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.
  24. Guy E. Blelloch and John Greiner. Parallelism in sequential functional languages. In Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995, pages 226-237, 1995. URL: https://doi.org/10.1145/224164.224210.
  25. Eduardo Bonelli. The linear logical abstract machine. In Stephen D. Brookes and Michael W. Mislove, editors, Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 2006, Genova, Italy, May 23-27, 2006, volume 158 of Electronic Notes in Theoretical Computer Science, pages 99-121. Elsevier, 2006. URL: https://doi.org/10.1016/J.ENTCS.2006.04.007.
  26. 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.
  27. Ugo Dal Lago and Simone Martini. An invariant cost model for the lambda calculus. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006, Proceedings, volume 3988 of Lecture Notes in Computer Science, pages 105-114. Springer, 2006. URL: https://doi.org/10.1007/11780342_11.
  28. Ugo Dal Lago and Simone Martini. Derivational complexity is an invariant cost model. In Marko C. J. D. van Eekelen and Olha Shkaravska, editors, Foundational and Practical Aspects of Resource Analysis - First International Workshop, FOPARA 2009, Eindhoven, The Netherlands, November 6, 2009, Revised Selected Papers, volume 6324 of Lecture Notes in Computer Science, pages 100-113. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-15331-0_7.
  29. Ugo Dal Lago and Simone Martini. On constructor rewrite systems and the lambda-calculus. In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E. Nikoletseas, and Wolfgang Thomas, editors, Automata, Languages and Programming, 36th Internatilonal Colloquium, ICALP 2009, Rhodes, Greece, July 5-12, 2009, Proceedings, Part II, volume 5556 of Lecture Notes in Computer Science, pages 163-174. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02930-1_14.
  30. Vincent Danos and Laurent Regnier. Reversible, irreversible and optimal lambda-machines. In Jean-Yves Girard, Mitsuhiro Okada, and Andre Scedrov, editors, Linear Logic Tokyo Meeting 1996, Keio University, Mita Campus, Tokyo, Japan, March 29 - April 2, 1996, volume 3 of Electronic Notes in Theoretical Computer Science, pages 40-60. Elsevier, 1996. URL: https://doi.org/10.1016/S1571-0661(05)80402-5.
  31. Hugo Herbelin. A lambda-calculus structure isomorphic to gentzen-style sequent calculus structure. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 61-75. Springer, 1994. URL: https://doi.org/10.1007/BFB0022247.
  32. Delia Kesner and Shane Ó Conchúir. Milner’s lambda-calculus with partial substitutions. CoRR, abs/2312.13270, 2023. https://arxiv.org/abs/2312.13270, URL: https://doi.org/10.48550/arXiv.2312.13270.
  33. Yves Lafont. The linear abstract machine. Theor. Comput. Sci., 59:157-180, 1988. URL: https://doi.org/10.1016/0304-3975(88)90100-4.
  34. Ugo Dal Lago and Simone Martini. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci., 398(1-3):32-50, 2008. URL: https://doi.org/10.1016/J.TCS.2008.01.044.
  35. Ian Mackie. The geometry of interaction machine. In Ron K. Cytron and Peter Lee, editors, Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 198-208. ACM Press, 1995. URL: https://doi.org/10.1145/199448.199483.
  36. Ian Mackie. Interaction nets for linear logic. Theor. Comput. Sci., 247(1-2):83-140, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00198-5.
  37. Ian Mackie and Jorge Sousa Pinto. Encoding linear logic with interaction combinators. Inf. Comput., 176(2):153-186, 2002. URL: https://doi.org/10.1006/INCO.2002.3163.
  38. Ian Mackie and Shinya Sato. A calculus for interaction nets based on the linear chemical abstract machine. In Vincent Danos and Mariangiola Dezani, editors, Proceedings of the Third International Workshop on Developments in Computational Models, DCM@ICALP 2007, Wroclaw, Poland, July 15, 2007, volume 192 of Electronic Notes in Theoretical Computer Science, pages 59-70. Elsevier, 2007. URL: https://doi.org/10.1016/J.ENTCS.2008.10.027.
  39. Seikoh Mikami and Yohji Akama. A study of abramsky’s linear chemical abstract machine. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 243-257. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_18.
  40. Robin Milner. Local bigraphs and confluence: Two conjectures (extended abstract). In Roberto M. Amadio and Iain Phillips, editors, Proceedings of the 13th International Workshop on Expressiveness in Concurrency, EXPRESS 2006, Bonn, Germany, August 26, 2006, volume 175 of Electronic Notes in Theoretical Computer Science, pages 65-73. Elsevier, 2006. URL: https://doi.org/10.1016/J.ENTCS.2006.07.035.
  41. Claudio Sacerdoti Coen. sesame. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:93776e14435d0dd5cde6deee3d9cf8f515f18fac;origin=https://github.com/sacerdot/sesame/;visit=swh:1:snp:74121b1dcd8f080d2a02e4be91e979c54d140288;anchor=swh:1:rev:adbc17089f06623e5b24c5b9836a4f6d45f45cae (visited on 2024-06-19). URL: https://github.com/sacerdot/sesame/.
  42. David Sands, Jörgen Gustavsson, and Andrew Moran. Lambda calculi and linear speedups. 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 60-84. Springer, 2002. URL: https://doi.org/10.1007/3-540-36377-7_4.
  43. Shinya Sato, Toru Sugimoto, and Shinichi Yamada. An implementation model of the typed lambda-calculus based on linear chemical abstract machine. In Michael Hanus, editor, International Workshop on Functional and (Constraint) Logic Programming, WFLP 2001, Kiel, Germany, September 13-15, 2001, Selected Papers, volume 64 of Electronic Notes in Theoretical Computer Science, pages 292-307. Elsevier, 2001. URL: https://doi.org/10.1016/S1571-0661(04)80356-6.
  44. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  45. David N. Turner and Philip Wadler. Operational interpretations of linear logic. Theor. Comput. Sci., 227(1-2):231-248, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00054-7.
  46. Gabriele Vanoni. On Reasonable Space and Time Cost Models for the λ-Calculus. (Sur les modèles de coût raisonnable en espace et en temps pour le λ-calcul). PhD thesis, University of Bologna, Italy, 2022. URL: https://tel.archives-ouvertes.fr/tel-03923206.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact