Algorithmic complexity for theories of Commutative Kleene algebras
- Authors: Kuznetsov S.L.1
-
Affiliations:
- Steklov Mathematical Institute of Russian Academy of Sciences
- Issue: Vol 88, No 2 (2024)
- Pages: 44-79
- Section: Articles
- URL: https://journals.rcsi.science/1607-0046/article/view/254263
- DOI: https://doi.org/10.4213/im9480
- ID: 254263
Cite item
Open Access
Access granted
Subscription Access
Abstract
Kleene algebras are structures with addition, multiplication and constants $0$and $1$, which form an idempotent semiring, and the Kleene iterationoperation. In the particular case of $*$-continuous Kleene algebras,Kleene iteration is defined, in an infinitary way, as the supremum of powersof an element. We obtain results on algorithmic complexityfor Horn theories (semantic entailment from finite sets of hypotheses)of commutative $*$-continuous Kleene algebras. Namely,$\Pi_1^1$-completeness for the Horn theory and $\Pi^0_2$-completenessfor its fragment, where iteration cannot be used in hypotheses, is proved.These results are commutative counterparts of the corresponding theoremsof D. Kozen (2002) for the general (non-commutative) case.Several accompanying results are also obtained.
About the authors
Stepan Lvovich Kuznetsov
Steklov Mathematical Institute of Russian Academy of Sciences
ORCID iD: 0000-0003-0025-0133
Scopus Author ID: 54914981600
ResearcherId: P-2607-2016
Candidate of physico-mathematical sciences, no status
References
- С. К. Клини, “Представление событий в нервных сетях и конечных автоматах”, Автоматы, Сб. ст., ИЛ, М., 1956, 15–67
- D. Kozen, “On Kleene algebras and closed semirings”, Mathematical foundations of computer science (Banska Bystrica, 1990), Lecture Notes in Comput. Sci., 452, Springer-Verlag, Berlin, 1990, 26–47
- V. Pratt, “Action logic and pure induction”, Logics in AI (Amsterdam, 1990), Lecture Notes in Comput. Sci., 478, Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, 1991, 97–120
- В. Н. Редько, “Об алгебре коммутативных событий”, Укр. матем. журн., 16:2 (1964), 185–195
- R. J. Parikh, “On context-free languages”, J. Assoc. Comput. Mach., 13:4 (1966), 570–581
- D. Kozen, “On the complexity of reasoning in Kleene algebra”, Inform. and Comput., 179:2 (2002), 152–162
- S. L. Kuznetsov, “On the complexity of reasoning in Kleene algebra with commutativity conditions”, Theoretical aspects of computing – ICTAC 2023 (Lima, 2023), Lecture Notes in Comput. Sci., 14446, Springer, Cham, 2023, 83–99
- S. L. Kuznetsov, “Reasoning in commutative Kleene algebras from $*$-free hypotheses”, The Logica yearbook 2021, College Publications, London, 2022, 99–113
- E. Palka, “An infinitary sequent system for the equational theory of $*$-continuous action lattices”, Fund. Inform., 78:2 (2007), 295–309
- W. Buszkowski, E. Palka, “Infinitary action logic: complexity, models and grammars”, Studia Logica, 89:1 (2008), 1–18
- J.-Y. Girard, “Linear logic”, Theoret. Comput. Sci., 50:1 (1987), 1–101
- S. L. Kuznetsov, S. O. Speranski, “Infinitary action logic with exponentiation”, Ann. Pure Appl. Logic, 173:2 (2022), 103057, 29 pp.
- S. L. Kuznetsov, S. O. Speranski, “Infinitary action logic with multiplexing”, Studia Logica, 111:2 (2023), 251–280
- P. Lincoln, J. Mitchell, A. Scedrov, N. Shankar, “Decision problems for propositional linear logic”, Ann. Pure Appl. Logic, 56:1-3 (1992), 239–311
- S. L. Kuznetsov, “Kleene star, subexponentials without contraction, and infinite computations”, Сиб. электрон. матем. изв., 18:2 (2021), 905–922
- V. Danos, J.-B. Joinet, H. Schellinx, “The structure of exponentials: uncovering the dynamics of linear logic proofs”, Computational logic and proof theory (Brno, 1993), Lecture Notes in Comput. Sci., 713, Springer-Verlag, Berlin, 1993, 159–171
- M. L. Minsky, “Recursive unsolvability of Post's problem of “tag” and other topics in theory of Turing machines”, Ann. of Math. (2), 74:3 (1961), 437–455
- S. L. Kuznetsov, “Commutative action logic”, J. Logic Comput., 33:6 (2023), 1437–1462
- L. Strassburger, “On the decision problem for MELL”, Theor. Comput. Sci., 768 (2019), 91–98
- R. Schroeppel, A two counter machine cannot calculate $2^N$, Report no. AIM-257, MIT, Cambrigde, MA, 1972, 32 pp.
- E. Börger, Computability, complexity, logic, Stud. Logic Found. Math., 128, North-Holland Publishing Co., Amsterdam, 1989, xx+592 pp.
- S. C. Kleene, “Arithmetical predicates and function quantifiers”, Trans. Amer. Math. Soc., 79 (1955), 312–340
- C. Spector, “Recursive well-orderings”, J. Symb. Log., 20:2 (1955), 151–163
- P. Odifreddi, Classical recursion theory. The theory of functions and sets of natural numbers, Stud. Logic Found. Math., 125, North-Holland Publishing Co., Amsterdam, 1989, xviii+668 pp.
Supplementary files
