论文标题
无限兰贝克微积分与克莱恩之星的复杂性
Complexity of the Infinitary Lambek Calculus with Kleene Star
论文作者
论文摘要
我们考虑Lambek演算或非交通性的乘法直觉线性逻辑，以迭代延伸，或通过$ω$ rule的式构想，并证明该校算中的衍生性问题为$π_1^0 $ -HARD。这解决了Buszkowski（2007）留下的问题，后者获得了与无限行动逻辑相同的复杂性，该逻辑还包括加性结合和脱节。作为副产品，我们证明，任何没有空白的语言的语言都可以由具有独特类型分配的Lambek语法生成，而没有Lambek的非空置限制（参见Safiullin 2007）。
We consider the Lambek calculus, or non-commutative multiplicative intuitionistic linear logic, extended with iteration, or Kleene star, axiomatised by means of an $ω$-rule, and prove that the derivability problem in this calculus is $Π_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).
