Document Open Access Logo

Comparing Infinitary Systems for Linear Logic with Fixed Points

Authors Anupam Das, Abhishek De, Alexis Saurin

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2023.40.pdf
  • Filesize: 0.85 MB
  • 17 pages

Document Identifiers

Author Details

Anupam Das
  • School of Computer Science, University of Birmingham, UK
Abhishek De
  • School of Computer Science, University of Birmingham, UK
Alexis Saurin
  • IRIF, CNRS, Université Paris Cité, France
  • INRIA $π^3$, Paris, France

Funding

The first and second authors are supported by a UKRI Future Leaders Fellowship, Structure vs. Invariants in Proofs, project reference MR/S035540/1. The third author is partially funded by the ANR project RECIPROG, project reference ANR-21-CE48-019-01.

Cite AsGet BibTex

Anupam Das, Abhishek De, and Alexis Saurin. Comparing Infinitary Systems for Linear Logic with Fixed Points. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 40:1-40:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSTTCS.2023.40

Abstract

Extensions of Girard’s linear logic by least and greatest fixed point operators (μMALL) have been an active field of research for almost two decades. Various proof systems are known viz. finitary and non-wellfounded, based on explicit and implicit (co)induction respectively. In this paper, we compare the relative expressivity, at the level of provability, of two complementary infinitary proof systems: finitely branching non-wellfounded proofs (μMALL^∞) vs. infinitely branching well-founded proofs (μMALL_{ω,∞}). Our main result is that μMALL^∞ is strictly contained in μMALL_{ω,∞}. For inclusion, we devise a novel technique involving infinitary rewriting of non-wellfounded proofs that yields a wellfounded proof in the limit. For strictness of the inclusion, we improve previously known lower bounds on μMALL^∞ provability from Π⁰₁-hard to Σ¹₁-hard, by encoding a sort of Büchi condition for Minsky machines.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Proof theory
Keywords
  • linear logic
  • fixed points
  • non-wellfounded proofs
  • omega-branching proofs
  • analytical hierarchy

Metrics

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

References

  1. Bahareh Afshari, Sebastian Enqvist, and Graham E Leigh. Cyclic proofs for the first-order µ-calculus. Logic Journal of the IGPL, page jzac053, August 2022. URL: https://doi.org/10.1093/jigpal/jzac053.
  2. Bahareh Afshari and Graham E. Leigh. Cut-free completeness for modal mu-calculus. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005088.
  3. R. Alur and T.A. Henzinger. A really temporal logic. In 30th Annual Symposium on Foundations of Computer Science, pages 164-169, 1989. URL: https://doi.org/10.1109/SFCS.1989.63473.
  4. David Baelde. Least and greatest fixed points in linear logic. ACM Trans. Comput. Logic, 13(1), January 2012. URL: https://doi.org/10.1145/2071368.2071370.
  5. David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for circular and non-wellfounded proofs: Towards compositionality with circular proofs. In LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3533375.
  6. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In 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 fuer 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, pages 92-106, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  8. James Brotherston and Alex Simpson. Complete sequent calculi for induction and infinite descent. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 51-62. IEEE, 2007. Google Scholar
  9. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, 2011. Google Scholar
  10. Rudolf Carnap. Logical Syntax of Language. Kegan Paul, Trench and Truber, 1937. Google Scholar
  11. Gianluca Curzi and Anupam Das. Non-uniform complexity via non-wellfounded proofs. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, 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. Anupam Das. On the logical complexity of cyclic arithmetic. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:1)2020.
  13. Anupam Das, Abhishek De, and Alexis Saurin. Decision problems for linear logic with least and greatest fixed points. In FSCD, volume 228 of LIPIcs, pages 20:1-20:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.20.
  14. Anuj Dawar and Yuri Gurevich. Fixed Point Logics. Bulletin of Symbolic Logic, 8(1):65-88, 2002. URL: https://doi.org/10.2178/bsl/1182353853.
  15. Abhishek De. Linear logic with the least and greatest fixed points: truth semantics, complexity, and a parallel syntax. PhD thesis, Université Paris Cité, 2022. URL: https://www.irif.fr/_media/users/ade/main.pdf.
  16. Abhishek De, Farzad Jafarrahmani, and Alexis Saurin. Phase semantics for linear logic with least and greatest fixed points. In Anuj Dawar and Venkatesan Guruswami, editors, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India, volume 250 of LIPIcs, pages 35:1-35:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2022.35.
  17. Amina Doumane. On the infinitary proof theory of logics with fixed points. (Théorie de la démonstration infinitaire pour les logiques à points fixes). PhD thesis, Paris Diderot University, France, 2017. URL: https://tel.archives-ouvertes.fr/tel-01676953.
  18. Walter Felscher. Dialogues, strategies, and intuitionistic provability. Annals of Pure and Applied Logic, 28(3):217-254, 1985. URL: https://doi.org/10.1016/0168-0072(85)90016-8.
  19. Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 248-262. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.248.
  20. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  21. Leo Harrington. Analytic determinacy and 0^#. The Journal of Symbolic Logic, 43(4):685-693, 1978. URL: https://doi.org/10.2307/2273508.
  22. Gerhard Jäger. Fixed points in peano arithmetic with ordinals. Annals of Pure and Applied Logic, 60(2):119-132, 1993. URL: https://doi.org/10.1016/0168-0072(93)90039-G.
  23. Dexter Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333-354, 1983. Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  24. Dexter Kozen. A finite model theorem for the propositional μ-calculus. Studia Logica, 47(3):233-241, September 1988. URL: https://doi.org/10.1007/BF00370554.
  25. G Kreisel. P. lorenzen. ein dialogisches konstruktwitätskriterium. infinitistic methods, proceedings of the symposium on foundations of mathematics, warsaw, 2-9 september 1959, panstwowe wydawnictwo naukowe, warsaw, and pergamon press, oxford-london-new york-paris, 1961, pp. 193-200. The Journal of Symbolic Logic, 32(4):516-516, 1968. Google Scholar
  26. 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.
  27. Stepan Kuznetsov. Complexity of commutative infinitary action logic. In Manuel A. Martins and Igor Sedlár, editors, Dynamic Logic. New Trends and Applications, pages 155-169, Cham, 2020. Springer International Publishing. Google Scholar
  28. Patrick Lincoln, John C. Mitchell, Andre Scedrov, and Natarajan Shankar. Decision problems for propositional linear logic. Ann. Pure Appl. Log., 56(1-3):239-311, 1992. URL: https://doi.org/10.1016/0168-0072(92)90075-B.
  29. R. Mansfield and G. Weitkamp. Recursive Aspects of Descriptive Set Theory. Oxford logic guides. Oxford University Press, 1985. URL: https://books.google.co.uk/books?id=jPzuAAAAMAAJ.
  30. Grigori Mints. Finite investigations of transfinite derivations. Journal of Soviet Mathematics, 10:548-596, 1978. Google Scholar
  31. Michael Möllerfeld. Generalized inductive definitions: the μ-calculus and Π¹₂-comprehension. PhD thesis, Westfälische Universität Münster, 2002. Google Scholar
  32. Yiannis N Moschovakis. Elementary Induction on Abstract Structures (Studies in Logic and the Foundations of Mathematics). American Elsevier Pub. Co, 1974. Google Scholar
  33. Damian Niwinski and Igor Walukiewicz. Games for the mu-calculus. Theor. Comput. Sci., 163(1&2):99-116, 1996. URL: https://doi.org/10.1016/0304-3975(95)00136-0.
  34. Ewa Palka. An infinitary sequent system for the equational theory of *-continuous action lattices. Fundam. Inf., 78(2):295-309, April 2007. Google Scholar
  35. Gerald E. Sacks. Higher Recursion Theory. Perspectives in Logic. Cambridge University Press, 2017. URL: https://doi.org/10.1017/9781316717301.
  36. Luigi Santocanale. A calculus of circular proofs and its categorical semantics. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, volume 2303 of Lecture Notes in Computer Science, pages 357-371. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_25.
  37. Thomas Studer. On the proof theory of the modal μ-calculus. Stud Logica, 89(3):343-363, 2008. URL: https://doi.org/10.1007/s11225-008-9133-6.
  38. M. Y. Vardi. A temporal fixpoint calculus. In POPL '88, pages 250-259, New York, NY, USA, 1988. Association for Computing Machinery. URL: https://doi.org/10.1145/73560.73582.
  39. Igor Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. In LICS 95, San Diego, California, USA, June 26-29, 1995, pages 14-24, 1995. 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