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/