|
Эта публикация цитируется в 1 научной статье (всего в 1 статье)
Математическая логика, алгебра и теория чисел
Kleene star, subexponentials without contraction, and infinite computations
S. L. Kuznetsov Steklov Mathematical Institute of RAS, 8, Gubkina str., Moscow GSP-1, 119991, Russia
Аннотация:
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.
Ключевые слова:
linear logic, Kleene star, infinite computations, complexity.
Поступила 22 октября 2020 г., опубликована 1 сентября 2021 г.
Образец цитирования:
S. L. Kuznetsov, “Kleene star, subexponentials without contraction, and infinite computations”, Сиб. электрон. матем. изв., 18:2 (2021), 905–922
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/semr1410 https://www.mathnet.ru/rus/semr/v18/i2/p905
|
Статистика просмотров: |
Страница аннотации: | 97 | PDF полного текста: | 28 | Список литературы: | 20 |
|