Document Open Access Logo

Decision Problems for Linear Logic with Least and Greatest Fixed Points

Authors Anupam Das, Abhishek De, Alexis Saurin

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.20.pdf
  • Filesize: 0.86 MB
  • 20 pages

Document Identifiers

Author Details

Anupam Das
  • University of Birmingham, UK
Abhishek De
  • IRIF, CNRS, Université Paris Cité & INRIA, France
Alexis Saurin
  • IRIF, CNRS, Université Paris Cité & INRIA, France

Funding

  • Das, Anupam: This author is supported by a UKRI Future Leaders Fellowship, Structure vs. Invariants in Proofs, project reference MR/S035540/1.
  • De, Abhishek: This author has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 754362.
  • Saurin, Alexis: This author has been partially supported by ANR project RECIPROG, project reference ANR-21-CE48-019-01.

Acknowledgements

We would like to thank anonymous reviewers for their valuable comments that enhanced the clarity and presentation of this paper. We also thank Sylvain Schmitz for his insights on alternating vector addition systems.

Cite AsGet BibTex

Anupam Das, Abhishek De, and Alexis Saurin. Decision Problems for Linear Logic with Least and Greatest Fixed Points. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 20:1-20:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.20

Abstract

Linear logic is an important logic for modelling resources and decomposing computational interpretations of proofs. Decision problems for fragments of linear logic exhibiting "infinitary" behaviour (such as exponentials) are notoriously complicated. In this work, we address the decision problems for variations of linear logic with fixed points (μMALL), in particular, recent systems based on "circular" and "non-wellfounded" reasoning. In this paper, we show that μMALL is undecidable. More explicitly, we show that the general non-wellfounded system is Π⁰₁-hard via a reduction to the non-halting of Minsky machines, and thus is strictly stronger than its circular counterpart (which is in Σ⁰₁). Moreover, we show that the restriction of these systems to theorems with only the least fixed points is already Σ⁰₁-complete via a reduction to the reachability problem of alternating vector addition systems with states. This implies that both the circular system and the finitary system (with explicit (co)induction) are Σ⁰₁-complete.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Proof theory
  • Theory of computation → Complexity theory and logic
Keywords
  • Linear logic
  • fixed points
  • decidability
  • vector addition systems

Metrics

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

Related Versions

References

  1. Bahareh Afshari, Gerhard Jäger, and Graham E. Leigh. An infinitary treatment of full μ-calculus. In Rosalie Iemhoff, Michael Moortgat, and Ruy de Queiroz, editors, Logic, Language, Information, and Computation, pages 17-34, Berlin, Heidelberg, 2019. Springer Berlin Heidelberg. Google Scholar
  2. David Baelde. On the proof theory of regular fixed points. In Martin Giese and Arild Waaler, editors, Automated Reasoning with Analytic Tableaux and Related Methods, 18th International Conference, TABLEAUX 2009, Oslo, Norway, July 6-10, 2009. Proceedings, volume 5607 of Lecture Notes in Computer Science, pages 93-107. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02716-1_8.
  3. David Baelde, Amina Doumane, Denis Kuperberg, and Alexis Saurin. Bouncing threads for infinitary and circular proofs. In LICS, New York, NY, USA, 2022. Association for Computing Machinery. (to appear). Google Scholar
  4. 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: http://www.dagstuhl.de/dagpub/978-3-95977-022-4.
  5. 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.
  6. Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors. Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning. North-Holland, 2007. URL: https://www.sciencedirect.com/bookseries/studies-in-logic-and-practical-reasoning/vol/3/suppl/C.
  7. James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Bernhard Beckert, editor, Automated Reasoning with Analytic Tableaux and Related Methods, pages 78-92, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  8. James Brotherston and Alex Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, October 2010. URL: https://doi.org/10.1093/logcom/exq052.
  9. Paul Brunet. A complete axiomatisation of a fragment of language algebra. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 11:1-11:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.11.
  10. J. Richard Buchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. URL: http://www.jstor.org/stable/1994916.
  11. S. Buss. Chapter 1: An introduction to proof theory. In Samuel R. Buss, editor, Handbook of Proof Theory. Elsevier, 1998. Google Scholar
  12. Wojciech Buszkowski. On action logic: Equational theories of action algebras. Journal of Logic and Computation, 17(1):199-217, October 2006. URL: https://doi.org/10.1093/logcom/exl036.
  13. 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.
  14. Anupam Das, Abhishek De, and Alexis Saurin. Decision problems for linear logic with least and greatest fixed points (Extended version). working paper or preprint, April 2022. URL: https://hal.archives-ouvertes.fr/hal-03655651.
  15. Anupam Das, Amina Doumane, and Damien Pous. Left-handed completeness for Kleene algebra, via cyclic proofs. In LPAR, volume 57 of EPiC Series in Computing, pages 271-289. EasyChair, 2018. Google Scholar
  16. Anupam Das and Damien Pous. A cut-free cyclic proof system for Kleene algebra. In Renate A. Schmidt and Cláudia Nalon, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 261-277, Cham, 2017. Springer International Publishing. Google Scholar
  17. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In FSTTCS, volume 4337 of Lecture Notes in Computer Science, pages 273-284. Springer, 2006. Google Scholar
  18. Christian Dax, Martin Hofmann, and Martin Lange. A proof system for the linear time μ-calculus. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 273-284. Springer, 2006. URL: https://doi.org/10.1007/11944836_26.
  19. Abhishek De, Luc Pellissier, and Alexis Saurin. Canonical proof-objects for coinductive programming: Infinets with infinitely many cuts. In 23rd International Symposium on Principles and Practice of Declarative Programming, PPDP 2021, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3479394.3479402.
  20. P. de Groote, B. Guillaume, and S. Salvati. Vector addition tree automata. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pages 64-73, 2004. URL: https://doi.org/10.1109/LICS.2004.1319601.
  21. 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.
  22. Amina Doumane and Damien Pous. Completeness for identity-free kleene lattices. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 18:1-18:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.18.
  23. Uffe Engberg and Glynn Winskel. Petri nets as models of linear logic. In A. Arnold, editor, CAAP '90, pages 147-161, Berlin, Heidelberg, 1990. Springer Berlin Heidelberg. Google Scholar
  24. Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979. URL: https://doi.org/10.1016/0022-0000(79)90046-1.
  25. Jérôme Fortier and Luigi Santocanale. Cuts for circular proofs: semantics and cut-elimination. In CSL, 2013. Google Scholar
  26. Silvio Ghilardi, Maria João Gouveia, and Luigi Santocanale. Fixed-point elimination in the intuitionistic propositional calculus. ACM Trans. Comput. Logic, 21(1), September 2019. URL: https://doi.org/10.1145/3359669.
  27. Silvio Ghilardi, Maria João Gouveia, and Luigi Santocanale. Fixed-point elimination in the intuitionistic propositional calculus. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures, pages 126-141, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. Google Scholar
  28. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  29. Jean-Yves Girard. Linear logic: Its syntax and semantics. In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, Advances in Linear Logic, pages 222-1. Cambridge University Press, 1995. Google Scholar
  30. Gary A. Kildall. A unified approach to global program optimization. In Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’73, pages 194-206, New York, NY, USA, 1973. Association for Computing Machinery. URL: https://doi.org/10.1145/512927.512945.
  31. Alexei Kopylov. Decidability of linear affine logic. Inf. Comput., 164:173-198, January 2001. URL: https://doi.org/10.1006/inco.1999.2834.
  32. D. Kozen. A completeness theorem for kleene algebras and the algebra of regular events. In [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pages 214-225, 1991. URL: https://doi.org/10.1109/LICS.1991.151646.
  33. 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.
  34. Saul Aaron Kripke. The problem of entailment” (abstract). The Journal of Symbolic Logic, 24(4):312-326, 1959. URL: http://www.jstor.org/stable/2963903.
  35. Daniel Krob. Complete systems of b-rational identities. Theoretical Computer Science, 89(2):207-343, 1991. URL: https://doi.org/10.1016/0304-3975(91)90395-I.
  36. Stepan Kuznetsov. *-continuity vs. induction: Divide and conquer. In Guram Bezhanishvili, Giovanna D'Agostino, George Metcalfe, and Thomas Studer, editors, Advances in Modal Logic 12, proceedings of the 12th conference on "Advances in Modal Logic," held in Bern, Switzerland, August 27-31, 2018, pages 493-510. College Publications, 2018. URL: http://www.aiml.net/volumes/volume12/Kuznetsov.pdf.
  37. 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
  38. Yves Lafont. The finite model property for various fragments of linear logic. Journal of Symbolic Logic, 62(4):1202-1208, 1997. URL: https://doi.org/10.2307/2275637.
  39. Ranko Lazić and Sylvain Schmitz. Non-elementary complexities for branching vass, mell, and extensions. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2603088.2603129.
  40. Ranko Lazić and Sylvain Schmitz. Nonelementary complexities for branching vass, mell, and extensions. ACM Trans. Comput. Logic, 16(3), June 2015. URL: https://doi.org/10.1145/2733375.
  41. Patrick Lincoln. Computational Aspects of Linear Logic. PhD thesis, Standford University, 1992. Google Scholar
  42. Patrick Lincoln. Deciding provability of linear logic formulas. In Proceedings of the Workshop on Advances in Linear Logic, pages 109-122, USA, 1995. Cambridge University Press. Google Scholar
  43. Patrick Lincoln, John Mitchell, Scedrov Andre, and Natarajan Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56(1):239-311, 1992. URL: https://doi.org/10.1016/0168-0072(92)90075-B.
  44. José Meseguer and Ugo Montanari. Petri nets are monoids. Information and Computation, 88(2):105-155, 1990. URL: https://doi.org/10.1016/0890-5401(90)90013-8.
  45. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., USA, 1967. Google Scholar
  46. J. F. Nash. Equilibrium points in N-person games. Proceedings of the National Academy of Sciences of the United States of America, 36(48-49), 1950. Google Scholar
  47. Damian Niwiński. Fixed point characterization of infinite behavior of finite-state systems. Theor. Comput. Sci., 189(1–2):1-69, December 1997. URL: https://doi.org/10.1016/S0304-3975(97)00039-X.
  48. Damian Niwinski and Igor Walukiewicz. Games for the μ-calculus. Theor. Comput. Sci., 163(1&2):99-116, 1996. URL: https://doi.org/10.1016/0304-3975(95)00136-0.
  49. Ewa Palka. An infinitary sequent system for the equational theory of *-continuous action lattices. Fundam. Inf., 78(2):295-309, April 2007. Google Scholar
  50. Michael Oser Rabin. Automata on Infinite Objects and Church’s Problem. American Mathematical Society, USA, 1972. Google Scholar
  51. 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, pages 357-371, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. Google Scholar
  52. HAROLD SCHELLINX. Some Syntactical Observations on Linear Logic. Journal of Logic and Computation, 1(4):537-559, September 1991. URL: https://doi.org/10.1093/logcom/1.4.537.
  53. Dana Scott. Outline of a mathematical theory of computation. Technical Report PRG02, OUCL, November 1970. Google Scholar
  54. 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, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 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.
  55. Lutz Straßburger. On the decision problem for MELL. Theoretical Computer Science, 768:91-98, 2019. URL: https://doi.org/10.1016/j.tcs.2019.02.022.
  56. Thomas Studer. On the proof theory of the modal mu-calculus. Studia Logica: An International Journal for Symbolic Logic, 89(3):343-363, 2008. URL: http://www.jstor.org/stable/40268983.
  57. Alasdair Urquhart. The complexity of decision procedures in relevance logic ii. The Journal of Symbolic Logic, 64(4):1774-1802, 1999. URL: http://www.jstor.org/stable/2586811.
  58. Igor Walukiewicz. A complete deductive system for the μ-calculus. PhD thesis, Warsaw University, 1994. Google Scholar
  59. 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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact