Kleene Star, Subexponentials without Contraction, and Infinite Computations

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.