论文标题
具有次指数和括号方式的乘添加式lambek演算
The Multiplicative-Additive Lambek Calculus with Subexponential and Bracket Modalities
论文作者
论文摘要
我们为Morrill引入的系统提供了证明理论和算法的复杂性分析，以作为Catlog类别语法解析器的核心。我们考虑了Morrill的计算的两个最新版本，并专注于它们的片段，包括乘法（Lambek）连接，添加剂的连接和脱节，括号和括号模态以及！亚指数模态。对于这两个系统，我们解决与剪切规则相关的问题并提供必要的修改，之后我们证明了削减的可接受性（削减消除定理）。我们还证明了两种计算的算法不可证明性，并表明基于它们的类别语法可以产生任意递归枚举的语言。
We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill's calculi, and focus on their fragments including multiplicative (Lambek) connectives, additive conjunction and disjunction, brackets and bracket modalities, and the ! subexponential modality. For both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut (cut elimination theorem). We also prove algorithmic undecidability for both calculi, and show that categorial grammars based on them can generate arbitrary recursively enumerable languages.
