Document Open Access Logo

Infinitary Cut-Elimination via Finite Approximations

Authors Matteo Acclavio , Gianluca Curzi , Giulio Guerrieri

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.8.pdf
  • Filesize: 0.91 MB
  • 19 pages

Document Identifiers

Author Details

Matteo Acclavio
  • University of Southern Denmark, Odense, Denmark
  • University of Sussex, Department of Informatics, Brighton, UK
Gianluca Curzi
  • University of Birmingham, UK
  • University of Gothenburg, Sweden
Giulio Guerrieri
  • University of Sussex, Department of Informatics, Brighton, UK

Funding

  • Acclavio, Matteo: Supported by Villum Fonden, grant no. 50079

Acknowledgements

We would like to thank Anupam Das, Abhishek De, Farzad Jafar-Rahmani, Alexis Saurin, Tito (Lê Thành Dung Nguyên), Damiano Mazza and the anonymous reviewers for their useful comments and suggestions.

Cite AsGet BibTex

Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri. Infinitary Cut-Elimination via Finite Approximations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.8

Abstract

We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressing criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Proof theory
Keywords
  • cut-elimination
  • non-wellfounded proofs
  • parsimonious logic
  • linear logic
  • proof theory
  • approximation
  • sequent calculus
  • non-uniform proofs

Metrics

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

Related Versions

References

  1. Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri. Non-uniform polynomial time via non-wellfounded parsimonious proofs. Unpublished. URL: http://gianlucacurzi.com/Non-uniform-polynomial-time-via-non-wellfounded-parsimonious-proofs.pdf.
  2. Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri. Infinitary cut-elimination via finite approximations (extended version). CoRR, abs/2308.07789, 2023. URL: https://doi.org/10.48550/ARXIV.2308.07789.
  3. Matteo Acclavio and Giulio Guerrieri. A deep inference system for differential linear logic. In Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity&TLLA@IJCAR-FSCD 2020, volume 353 of EPTCS, pages 26-49, 2020. URL: https://doi.org/10.4204/EPTCS.353.2.
  4. Roberto M. Amadio and Pierre-Louis Curien. Domains and lambda-calculi, volume 46 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1998. Google Scholar
  5. Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, 2009. URL: https://doi.org/10.1017/CBO9780511804090.
  6. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 42:1-42:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.42.
  7. David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In Nachum Dershowitz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, volume 4790 of Lecture Notes in Computer Science, pages 92-106. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-75560-9_9.
  8. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, 2011. Google Scholar
  9. Bruno Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25(2):95-169, 1983. URL: https://doi.org/10.1016/0304-3975(83)90059-2.
  10. Gianluca Curzi and Anupam Das. Cyclic implicit complexity. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3533340.
  11. Gianluca Curzi and Anupam Das. Non-uniform complexity via non-wellfounded proofs. In 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, volume 252 of LIPIcs, pages 16:1-16:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.16.
  12. Vincent Danos and Jean-Baptiste Joinet. Linear logic and elementary time. Inf. Comput., 183(1):123-137, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00010-5.
  13. Anupam Das. On the logical strength of confluence and normalisation for cyclic proofs. In 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, volume 195 of LIPIcs, pages 29:1-29:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.29.
  14. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In International Conference on Foundations of Software Technology and Theoretical Computer Science, pages 273-284. Springer, 2006. Google Scholar
  15. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Math. Struct. Comput. Sci., 28(7):995-1060, 2018. URL: https://doi.org/10.1017/S0960129516000372.
  16. Thomas Ehrhard and Farzad Jafar-Rahmani. On the denotational semantics of linear logic with least and greatest fixed points of formulas. CoRR, abs/1906.05593, 2019. URL: https://arxiv.org/abs/1906.05593.
  17. Thomas Ehrhard, Farzad Jafar-Rahmani, and Alexis Saurin. On relation between totality semantic and syntactic validity. In 5th International Workshop on Trends in Linear Logic and Applications (TLLA 2021), June 2021. URL: https://hal-lirmm.ccsd.cnrs.fr/lirmm-03271408.
  18. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Theor. Comput. Sci., 364(2):166-195, 2006. URL: https://doi.org/10.1016/J.TCS.2006.08.003.
  19. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347-372, 2008. URL: https://doi.org/10.1016/J.TCS.2008.06.001.
  20. Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Computer Science Logic 2013, CSL 2013, volume 23 of LIPIcs, pages 248-262. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.248.
  21. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  22. Jean-Yves Girard. Light linear logic. Information and Computation, 143(2):175-204, 1998. URL: https://doi.org/10.1006/inco.1998.2700.
  23. Denis Kuperberg, Laureline Pinault, and Damien Pous. Cyclic proofs, system T, and the power of contraction. Proc. ACM Program. Lang., 5(POPL):1-28, 2021. URL: https://doi.org/10.1145/3434282.
  24. Yves Lafont. Soft linear logic and polynomial time. Theoretical Computer Science, 318(1):163-180, 2004. Implicit Computational Complexity. URL: https://doi.org/10.1016/j.tcs.2003.10.018.
  25. Damiano Mazza. Non-uniform polytime computation in the infinitary affine lambda-calculus. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, volume 8573 of Lecture Notes in Computer Science, pages 305-317. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_26.
  26. Damiano Mazza. Simple parsimonious types and logarithmic space. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, volume 41 of LIPIcs, pages 24-40. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.24.
  27. Damiano Mazza and Kazushige Terui. Parsimonious types and non-uniform computation. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 350-361. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_28.
  28. Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In António Porto and Francisco Javier López-Fraguas, editors, Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 129-140. ACM, 2009. URL: https://doi.org/10.1145/1599410.1599427.
  29. Damian Niwiński and Igor Walukiewicz. Games for the μ-calculus. Theoretical Computer Science, 163(1-2):99-116, 1996. URL: https://doi.org/10.1016/0304-3975(95)00136-0.
  30. Michele Pagani and Lorenzo Tortora de Falco. Strong normalization property for second order linear logic. Theor. Comput. Sci., 411(2):410-444, January 2010. URL: https://doi.org/10.1016/j.tcs.2009.07.053.
  31. Myriam Quatrini. Sémantique cohérente des exponentielles: de la logique linéaire à la logique classique. PhD thesis, Aix-Marseille 2, 1995. Google Scholar
  32. Luca Roversi and Luca Vercelli. Safe recursion on notation into a light logic by levels. In Patrick Baillot, editor, Proceedings International Workshop on Developments in Implicit Computational complExity, DICE 2010, Paphos, Cyprus, 27-28th March 2010, volume 23 of EPTCS, pages 63-77, 2010. URL: https://doi.org/10.4204/EPTCS.23.5.
  33. Alexis Saurin. A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points (extended version). working paper or preprint, 2023. URL: https://hal.science/hal-04169137.
  34. Alex Simpson. Cyclic arithmetic is equivalent to peano arithmetic. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 283-300, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_17.
  35. Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc., USA, 2006. Google Scholar
  36. Terese. Term rewriting systems, volume 55 of Cambridge tracts in theoretical computer science. Cambridge University Press, 2003. Google Scholar
  37. A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2 edition, 2000. URL: https://doi.org/10.1017/CBO9781139168717.
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