|
This article is cited in 1 scientific paper (total in 1 paper)
Mathematical logic, algebra and number theory
Kleene star, subexponentials without contraction, and infinite computations
S. L. Kuznetsov Steklov Mathematical Institute of RAS, 8, Gubkina str., Moscow GSP-1, 119991, Russia
Abstract:
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.
Received October 22, 2020, published September 1, 2021
Citation:
S. L. Kuznetsov, “Kleene star, subexponentials without contraction, and infinite computations”, Sib. Èlektron. Mat. Izv., 18:2 (2021), 905–922
Linking options:
https://www.mathnet.ru/eng/semr1410 https://www.mathnet.ru/eng/semr/v18/i2/p905
|
Statistics & downloads: |
Abstract page: | 112 | Full-text PDF : | 32 | References: | 21 |
|