Decidable fragments of the Lambek calculus with subexponentials

The extension of the Lambek calculus with the exponential modality (that is, non-commutative intuitionistic linear logic), is undecidable [Lincoln et al. 1992]. Moreover, the same happens for any subexponential modality, under which the non-local contraction rule is allowed [Kanovich et al. 2019]. However, if the subexponential modality is allowed to be applied only to variables, then the system becomes decidable [Kanovich et al. 2016] and belongs to the NP class, as the original Lambek calculus does. We prove decidability for broader fragments, in which we allow formulae of implication depth 1 under subexponential. (If one allows formulae of depth 2, the system is already undecidable.) We consider such fragments for two versions of subexponential: the exponential, which allows all structural rules, and the relevant modality, which allows contraction and permutation, but not weakening. The latter is motivated by linguistic applications.
Joint work with Boris Karlov and Evgenia Fofanova.