Document Open Access Logo

Tower-Complete Problems in Contraction-Free Substructural Logics

Author Hiromi Tanaka

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.34.pdf
  • Filesize: 0.98 MB
  • 19 pages

Document Identifiers

Author Details

Hiromi Tanaka
  • Keio University, Tokyo, Japan

Funding

This work was partially supported by JST, CREST Grant Number JPMJCR2114, Japan.

Acknowledgements

I would like to thank Koji Mineshima for helpful comments on the introduction section. I am also grateful to the anonymous reviewers for useful suggestions, which improve some proofs and deepen the discussion in Section 7.

Cite AsGet BibTex

Hiromi Tanaka. Tower-Complete Problems in Contraction-Free Substructural Logics. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 34:1-34:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.34

Abstract

We investigate the non-elementary computational complexity of a family of substructural logics without contraction. With the aid of the technique pioneered by Lazić and Schmitz (2015), we show that the deducibility problem for full Lambek calculus with exchange and weakening (FL_{ew}) is not in Elementary (i.e., the class of decision problems that can be decided in time bounded by an elementary recursive function), but is in PR (i.e., the class of decision problems that can be decided in time bounded by a primitive recursive function). More precisely, we show that this problem is complete for Tower, which is a non-elementary complexity class forming a part of the fast-growing complexity hierarchy introduced by Schmitz (2016). The same complexity result holds even for deducibility in BCK-logic, i.e., the implicational fragment of FL_{ew}. We furthermore show the Tower-completeness of the provability problem for elementary affine logic, which was proved to be decidable by Dal Lago and Martini (2004).

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Proof theory
Keywords
  • substructural logic
  • linear logic
  • full Lambek calculus
  • BCK-logic
  • computational complexity
  • provability
  • deducibility

Metrics

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

Related Versions

References

  1. Andrea Asperti. Light affine logic. In Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, pages 300-308, 1998. URL: https://doi.org/10.1109/LICS.1998.705666.
  2. Patrick Baillot. On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy. Information and Computation, 241:3-31, 2015. URL: https://doi.org/10.1016/j.ic.2014.10.005.
  3. A.R. Balasubramanian, Timo Lang, and Revantha Ramanayake. Decidability and complexity in weakening and contraction hypersequent substructural logics. In Proceedings of the 36th Annual IEEE Symposium on Logic in Computer Science, pages 1-13, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470733.
  4. Willem J. Blok and Clint J. van Alten. The finite embeddability property for residuated lattices, pocrims and BCK-algebras. Algebra Universalis, 48:253-271, 2002. URL: https://doi.org/10.1007/s000120200000.
  5. Willem J. Blok and Clint J. van Alten. On the finite embeddability property for residuated ordered groupoids. Transactions of the American Mathematical Society, 357(10):4141-4157, 2005. URL: https://doi.org/10.1090/S0002-9947-04-03654-2.
  6. Wojciech Buszkowski. Some decision problems in the theory of syntactic categories. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 28(33-38):539-548, 1982. URL: https://doi.org/10.1002/malq.19820283308.
  7. Wojciech Buszkowski. On the complexity of some substructural logics. Reports on Mathematical Logic, 43:5-24, 2008. Google Scholar
  8. Paolo Coppola and Simone Martini. Optimizing optimal reduction: a type inference algorithm for elementary affine logic. ACM Transactions on Computational Logic, 7(2):219-260, 2006. URL: https://doi.org/10.1145/1131313.1131315.
  9. Wojciech Czerwiński and Łukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. In Proceedings of the 62nd Annual IEEE Symposium on Foundations of Computer Science, pages 1229-1240, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  10. Ugo Dal Lago and Simone Martini. Phase semantics and decidability of elementary affine logic. Theoretical Computer Science, 318(3):409-433, 2004. URL: https://doi.org/10.1016/j.tcs.2004.02.037.
  11. Vincent Danos and Jean-Baptiste Joinet. Linear logic and elementary time. Information and Computation, 183(1):123-137, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00010-5.
  12. Philippe de Groote, Bruno Guillaume, and Sylvain Salvati. Vector addition tree automata. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pages 64-73, 2004. URL: https://doi.org/10.1109/LICS.2004.1319601.
  13. Francesc Esteva and Lluís Godo. Monoidal t-norm based logic: towards a logic for left-continuous t-norms. Fuzzy Sets and Systems, 124(3):271-288, 2001. URL: https://doi.org/10.1016/S0165-0114(01)00098-7.
  14. Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono. Residuated Lattices: An Algebraic Glimpse at Substructural Logics, volume 151 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2007. Google Scholar
  15. Nikolaos Galatos and Hiroakira Ono. Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL. Studia Logica, 83:279-308, 2006. URL: https://doi.org/10.1007/s11225-006-8305-5.
  16. Jean-Yves Girard. Linear logic: its syntax and semantics. In Jean-Yves Girard, Yves Lafont, and Laurent Regnier, editors, Advances in Linear Logic, volume 222 of London Mathematical Society Lecture Note Series, pages 1-42. Cambridge University Press, 1995. URL: https://doi.org/10.1017/CBO9780511629150.002.
  17. Jean-Yves Girard. Light linear logic. Information and Computation, 143(2):175-204, 1998. URL: https://doi.org/10.1006/inco.1998.2700.
  18. Petr Hájek. Metamathematics of Fuzzy Logic, volume 4 of Trends in Logic. Springer, 1998. URL: https://doi.org/10.1007/978-94-011-5300-3.
  19. Zuzana Haniková. Computational complexity of propositional fuzzy logics. In Petr Cintula, Petr Hájek, and Carles Noguera, editors, Handbook of Mathematical Fuzzy Logic (Volume 2), volume 38 of Mathematical Logic and Foundations, pages 793-851. College Publications, 2011. Google Scholar
  20. Zuzana Haniková. Complexity of some language fragments of fuzzy logics. Soft Computing, 21:69-77, 2017. URL: https://doi.org/10.1007/s00500-016-2346-0.
  21. Rostislav Horčík and Kazushige Terui. Disjunction property and complexity of substructural logics. Theoretical Computer Science, 412(31):3992-4006, 2011. URL: https://doi.org/10.1016/j.tcs.2011.04.004.
  22. Kiyoshi Iséki and Shôtarô Tanaka. An introduction to theory of BCK-algebras. Mathematica Japonica, 23:1-26, 1978. Google Scholar
  23. Max I. Kanovich. The complexity of Horn fragments of linear logic. Annals of Pure and Applied Logic, 69(2-3):195-241, 1994. URL: https://doi.org/10.1016/0168-0072(94)90085-X.
  24. 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.
  25. Olivier Laurent. Around classical and intuitionistic linear logics. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 629-638, 2018. URL: https://doi.org/10.1145/3209108.3209132.
  26. Ranko Lazić and Sylvain Schmitz. Nonelementary complexities for branching VASS, MELL, and extensions. ACM Transactions on Computational Logic, 16(3):20:1-20:30, 2015. URL: https://doi.org/10.1145/2733375.
  27. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In Proceedings of the 62nd Annual IEEE Symposium on Foundations of Computer Science, pages 1241-1252, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  28. Patrick Lincoln, John Mitchell, Andre Scedrov, and Natarajan Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56(1-3):239-311, 1992. URL: https://doi.org/10.1016/0168-0072(92)90075-B.
  29. Mitsuhiro Okada. A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theoretical Computer Science, 281(1-2):471-498, 2002. URL: https://doi.org/10.1016/S0304-3975(02)00024-5.
  30. Mitsuhiro Okada and Kazushige Terui. The finite model property for various fragments of intuitionistic linear logic. Journal of Symbolic Logic, 64(2):790-802, 1999. URL: https://doi.org/10.2307/2586501.
  31. Hiroakira Ono. Substructural logics and residuated lattices - an introduction. In Vincent F. Hendricks and Jacek Malinowski, editors, Trends in Logic: 50 Years of Studia Logica, volume 21 of Trends in Logic, pages 193-228, 2003. URL: https://doi.org/10.1007/978-94-017-3598-8_8.
  32. Hiroakira Ono and Yuichi Komori. Logics without the contraction rule. Journal of Symbolic Logic, 50(1):169-201, 1985. URL: https://doi.org/10.2307/2273798.
  33. Mati Pentus. Lambek calculus is NP-complete. Theoreitcal Computer Science, 357(1-3):186-201, 2006. URL: https://doi.org/10.1016/j.tcs.2006.03.018.
  34. Greg Restall. An Introduction to Substructural Logics. Routledge, 2000. Google Scholar
  35. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory, 8(1):1-36, 2016. URL: https://doi.org/10.1145/2858784.
  36. Sylvain Schmitz. Implicational relevance logic is 2-EXPTIME-complete. Journal of Symbolic Logic, 81(2):641-661, 2016. URL: https://doi.org/10.1017/jsl.2015.7.
  37. Richard Statman. Intuitionistic propositional logic is polynomial-space complete. Theoreical Computer Science, 9(1):67-72, 1979. URL: https://doi.org/10.1016/0304-3975(79)90006-9.
  38. Kazushige Terui. Light Logic and Polynomial Time Computation. PhD thesis, Keio University, 2002. Google Scholar
  39. Kazushige Terui. Light affine set theory: a naive set theory of polynomial time. Studia Logica, 77:9-40, 2004. URL: https://doi.org/10.1023/B:STUD.0000034183.33333.6f.
  40. Anne Sjerp Troelstra. Lectures on Linear logic, volume 29 of CSLI Lecture Notes. Center for the Study of Language and Information, 1992. Google Scholar
  41. Alasdair Urquhart. The complexity of decision procedures in relevance logic II. Journal of Symbolic Logic, 64(4):1774-1802, 1999. URL: https://doi.org/10.2307/2586811.
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