论文标题
无收缩下结构逻辑中的塔式完全问题
Tower-Complete Problems in Contraction-Free Substructural Logics
论文作者
论文摘要
我们研究了没有收缩的非元素逻辑家族的非元素计算复杂性。借助Lazić和Schmitz（2015）开创的技术，我们表明，全兰贝克微积分和交换和弱化的可推迟性问题（$ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ mathbf {\ mathbf {ew {ew}} $）在基本问题（即，iS element in pr a insuest）的范围（i.e.e.e.e. （即，可以按原始递归功能限制的决策类问题类别）。更确切地说，我们证明了塔是完整的，这是一个非优质复杂性类，构成了Schmitz（2016）引入的快速增长复杂性层次结构的一部分。在BCK-Logic（即$ \ Mathbf {fl} _ {\ Mathbf {ew}} $中的含义片段中，相同的复杂性结果甚至适用于bck-logic。我们此外，还显示了基本仿射逻辑的可证明性问题的塔式完整性，这被Dal Lago和Martini（2004）证明是可以决定的。
We investigate the non-elementary computational complexity of a family of substructural logics without contraction. With the aid of the technique pioneered by Lazić and Schmitz (2015), we show that the deducibility problem for full Lambek calculus with exchange and weakening ($\mathbf{FL}_{\mathbf{ew}}$) is not in Elementary (i.e., the class of decision problems that can be decided in time bounded by an elementary recursive function), but is in PR (i.e., the class of decision problems that can be decided in time bounded by a primitive recursive function). More precisely, we show that this problem is complete for Tower, which is a non-elementary complexity class forming a part of the fast-growing complexity hierarchy introduced by Schmitz (2016). The same complexity result holds even for deducibility in BCK-logic, i.e., the implicational fragment of $\mathbf{FL}_{\mathbf{ew}}$. We furthermore show the Tower-completeness of the provability problem for elementary affine logic, which was proved to be decidable by Dal Lago and Martini (2004).
