Geodesic
Kleene star, subexponentials without contraction, and infinite computations
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 18 (2021) no. 2, pp. 905-922.

Voir la notice de l'article provenant de la source Math-Net.Ru

We present an extension of intuitionistic non-commutative linear logic with Kleene star and subexponentials which allow permutation and/or weakening, but not contraction. Subexponentials which allow contraction are useful for specifying correct terminating of computing systems (e.g., Turing machines). Dually, we show that Kleene star axiomatized by an omega-rule allows modelling infinite (never terminating) behaviour. Our system belongs to the $\Pi_1^0$ complexity class. Actually, it is $\Pi_1^0$-complete due to Buszkowski (2007). We show $\Pi_1^0$-hardness of the unidirectional fragment of this logic with two subexponentials and Kleene star (this result does not follow from Buszkowski’s construction). The omega-rule axiomatization can be equivalently reformulated as calculus with non-well-founded proofs (Das Pous, 2018). We also consider the fragment of this calculus with circular proofs. This fragment is capable of modelling looping of a Turing machine, but, interestingly enough, some non-cyclic computations can also be captured by this circular fragment.
Keywords: linear logic, Kleene star, infinite computations, complexity. 
@article{SEMR_2021_18_2_a4,
     author = {S. L. Kuznetsov},
     title = {Kleene star, subexponentials without contraction, and infinite computations},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {905--922},
     publisher = {mathdoc},
     volume = {18},
     number = {2},
     year = {2021},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2021_18_2_a4/}
}
TY  - JOUR
AU  - S. L. Kuznetsov
TI  - Kleene star, subexponentials without contraction, and infinite computations
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2021
SP  - 905
EP  - 922
VL  - 18
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SEMR_2021_18_2_a4/
LA  - en
ID  - SEMR_2021_18_2_a4
ER  - 
%0 Journal Article
%A S. L. Kuznetsov
%T Kleene star, subexponentials without contraction, and infinite computations
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2021
%P 905-922
%V 18
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SEMR_2021_18_2_a4/
%G en
%F SEMR_2021_18_2_a4
S. L. Kuznetsov. Kleene star, subexponentials without contraction, and infinite computations. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 18 (2021) no. 2, pp. 905-922. http://geodesic.mathdoc.fr/item/SEMR_2021_18_2_a4/

[1] D. Baelde, D. Miller, “Least and greatest fixed points in linear logic”, LPAR 2007: Logic for Programming, Artificial Intelligence, and Reasoning, Lect. Notes Comput. Sci., 4790, eds. N. Dershowitz, A. Voronkov, 2007, 92–106 | DOI | Zbl

[2] W. Buszkowski, “On action logic: equational theories of action algebras”, J. Log. Comput., 17:1 (2007), 199–217 | DOI | Zbl

[3] W. Buszkowski, E. Palka, “Infinitary action logic: complexity, models and grammars”, Stud. Log., 89:1 (2008), 1–18 | DOI | Zbl

[4] A. Das, D. Pous, “Non-wellfounded proof theory for (Kleene+action) (algebras+lattices)”, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), Leibniz Internat. Proc. Inform., 119, eds. D. Ghica, A. Jung, 2018, 19:1–19:18

[5] G. De Giacomo, E. Ternovska, R. Reiter, “Non-terminating processes in the situation calculus”, Ann. Math. Artif. Intell., 88:5–6 (2020), 623–640 | DOI | Zbl

[6] J.-Y. Girard, “Linear logic”, Theor. Comput. Sci., 50:1 (1987), 1–102 | DOI | Zbl

[7] W. Guttmann, “Algebras for iteration and infinite computations”, Acta Inf., 49:5 (2012), 343–359 | DOI | Zbl

[8] M. Kanazawa, “The Lambek calculus enriched with additional connectives”, J. Logic Lang. Inf., 1:2 (1992), 141–171 | DOI | Zbl

[9] M. Kanovich, S. Kuznetsov, V. Nigam, A. Scedrov, “A logical framework with commutative and non-commutative subexponentials”, IJCAR 2018: Automated Reasoning, Lect. Notes Comput. Sci., 10900, eds. D. Galmiche, S. Schulz, R. Sebastiani, 2018, 228–245 | DOI | Zbl

[10] M. Kanovich, S. Kuznetsov, V. Nigam, A. Scedrov, “Subexponentials in non-commutative linear logic”, Math. Struct. Comput. Sci., 29:8 (2019), 1217–1249 | DOI | Zbl

[11] D. Kőnig, “Über eine Schlusselweise aus dem Endlichen ins Unendliche”, Acta Szeged, 3:2–3 (1927), 121–130 | Zbl

[12] D. Kozen, “On action algebras”, Logic and Information Flow, eds. J. van Eijck, A. Visser, MIT Press, Cambridge, 1994, 78–88

[13] D. Kozen, “On the complexity of reasoning in Kleene algebra”, Inf. Comput., 179:2 (2002), 152–162 | DOI | Zbl

[14] S. Kuznetsov, “Complexity of infinitary Lambek calculus with Kleene star”, Rev. Symb. Logic, 2020, 1–28 | DOI

[15] S. Kuznetsov, “A $\Pi^0_1$-bounded fragment of infinitary action logic with exponential”, Logic, Language, and Security, Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday, Lect. Notes Comput. Sci., 12300, eds. V. Nigam et al., 2020, 3–16 | DOI | Zbl

[16] S. Kuznetsov, “Complexity of commutative infinitary action logic”, DaLí 2020: Dynamic Logic. New Trends and Applications, Lect. Notes Comput. Sci., 12569, eds. M.A. Martins, I. Sedlár, 2020, 155–169 | DOI | Zbl

[17] S.L. Kuznetsov, S.O. Speranski, Infinitary action logic with exponentiation, 2020, arXiv: 2001.06863

[18] P. Lincoln, J. Mitchell, A. Scedrov, N. Shankar, “Decision problems for propositional linear logic”, Ann. Pure Appl. Logic, 56:1–3 (1992), 239–311 | DOI | Zbl

[19] V. Nigam, D. Miller, “Algorithmic specifications in linear logic with subexponentials”, PPDP '09: Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, ACM, 2009, 129–140

[20] V. Nigam, C. Olarte, E. Pimentel, “A general proof system for modalities in concurrent constraint programming”, CONCUR 2013 — Concurrency Theory, Lect. Notes Comput. Sci., 8052, eds. P.R. D'Argenio, H. Melgratti, 2013, 410–424 | DOI | Zbl

[21] R. Nollet, A. Saurin, C. Tasson, “Local validity for circular proofs in linear logic with fixed points”, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), Leibniz Internat. Proc. Inform., 119, eds. D. Ghica, A. Jung, 2018, 35:1–35:23

[22] C. Olarte, E. Pimentel, V. Nigam, “Subexponential concurrent constraint programming”, Theor. Comput. Sci., 606 (2015), 98–120 | DOI | Zbl

[23] E. Palka, “An infinitary sequent system for the equational theory of *-continuous action lattices”, Fundam. Inform., 78:2 (2007), 295–309 | Zbl

[24] M. Pentus, “Lambek grammars are context-free”, 8th Annual IEEE Symposium on Logic in Computer Science (LICS 1993), IEEE Computer Society Press, 1993, 429–433

[25] M. Pentus, “Product-free Lambek calculus and context-free grammars”, J. Symb. Log., 62:2 (1997), 648–660 | DOI | Zbl

[26] M. Pentus, “Lambek calculus is NP-complete”, Theor. Comput. Sci., 357:1–3 (2006), 186–201 | DOI | Zbl

[27] F. Pfenning, R.J. Simmons, “Substructural operational semantics as ordered logic programming”, 24th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2009), IEEE, 2009, 101–110 | DOI

[28] J. Polakow, “Linear logic programming with an ordered context”, PPDP 2000: Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, ACM, 2000, 68–79

[29] V. Pratt, “Action logic and pure induction”, JELIA 1990: Logics in AI, Lect. Notes Comput. Sci., 478, ed. J. van Eijck, 1991, 97–120 | DOI | Zbl

[30] Yu. Savateev, “Unidirectional Lambek grammars in polynomial time”, Theor. Comput. Syst., 46:4 (2010), 662–672 | DOI | Zbl

[31] Yu. Savateev, “Product-free Lambek calculus is NP-complete”, Ann. Pure Appl. Logic, 163:7 (2012), 775–788 | DOI | Zbl

[32] W. Thomas, H. Lescow, “Logical specifications for infinite computations”, REX 1993: A Decade of Concurrency Reflections and Perspectives, Lect. Notes Comput. Sci., 803, eds. J.W. de Bakker, W.P. de Roever, G. Rozenberg, 1994, 583–621 | DOI

[33] K. Watkins, I. Cervesato, F. Pfenning, D. Walker, “A concurrent logical framework: the propositional fragment”, TYPES 2003: Types for Proofs and Programs, Lect. Notes Comput. Sci., 3085, eds. S. Berardi, M. Coppo, F. Damiani, 2003, 355–377 | DOI