We prove that the problem of deciding the consequence relation of the full Lambek calculus with weakening is complete for the class HAck of hyper-Ackermannian problems (i.e., level F_{\omega}^{\omega} of the ordinal-indexed hierarchy of fast-growing complexity classes). Provability was already known to be PSPACE-complete. We prove that deducibility is HAck-complete even for the multiplicative fragment. Lower bounds are proved via a novel reduction from reachability in lossy channel systems and the upper bounds are obtained by combining structural proof theory (forward proof search over sequent calculi) and well-quasi-order theory (length theorems for Higman's Lemma).
翻译:我们证明了判定带弱化的全Lambek演算后承关系的问题对于超阿克曼问题类HAck(即快速增长复杂度类序数分层中的F_{\omega}^{\omega}层级)具有完全性。其可证性已知为PSPACE完全问题。我们证明了即使对于乘法片段,可推导性仍具有HAck完全性。下界证明通过从损耗信道系统的可达性问题进行新颖规约实现,上界证明则结合了结构证明理论(基于相继式演算的前向证明搜索)与良拟序理论(Higman引理的长度定理)。