Complexity of the Infinitary Lambek Calculus with Kleene Star

DOI10.1017/S1755020320000209arXiv2005.00404MaRDI QIDQ6339828

Stepan Kuznetsov

Publication date: 1 May 2020

Abstract: We consider the Lambek calculus, or non-commutative multiplicative intuitionistic linear logic, extended with iteration, or Kleene star, axiomatised by means of an $omega$-rule, and prove that the derivability problem in this calculus is $P{i}_1^0$-hard. This solves a problem left open by Buszkowski (2007), who obtained the same complexity bound for infinitary action logic, which additionally includes additive conjunction and disjunction. As a by-product, we prove that any context-free language without the empty word can be generated by a Lambek grammar with unique type assignment, without Lambek's non-emptiness restriction imposed (cf. Safiullin 2007).

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

This page was built for publication: Complexity of the Infinitary Lambek Calculus with Kleene Star

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6339828)