Non-commutative linear logic fragments with sub-context-free complexity
Yusaku Nishimiya, Masaya Taniguchi
我们提出了新的描述性复杂性表征类REG(普通语言),LCFL(线性上下文自由语言)和CFL(无上下文语言)作为推理规则的限制,公式的大小和允许的连接在兰贝克演算; 零直觉的非交换线性逻辑的片段与方向敏感的暗示连接。 我们对具有证明复杂性REG和LCFL的兰贝克微积分碎片的鉴定是同类的第一个结果。 我们进一步展示了逻辑中严格“最弱”的可能变体之一的CFL复杂性,只承认一个单一的推理规则。 此外,其证明是基于对可证明的琉挛的语法和形式语法的直接翻译以及可证明的隐身的结构归纳;一种比先前作品中使用的更简单,更直观的方法。 因此,我们建立了切消除定理的明确概念效用,用于比较形式语法和连续演算,并确定兰贝克语法中Greibach正常形式的精确模拟。 我们认为,本文介绍的结果构成了计算与逻辑之间相互作用的更广泛和更丰富的表征的第一步,以及各种连续演算的细粒度复杂性分离。
We present new descriptive complexity characterisations of classes REG (regular languages), LCFL (linear context-free languages) and CFL (context-free languages) as restrictions on inference rules, size of formulae and permitted connectives in the Lambek calculus; fragments of the intuitionistic non-commutative linear logic with direction-sensitive implication connectives. Our identification of the Lambek calculus fragments with proof complexity REG and LCFL is the first result of its kind. We f...