Kleene star, subexponentials without contraction, and infinite computations

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.