2025-11-20T10:49:14.996806

Complexity of Nonassociative Lambek Calculus with classical logic

PÅaczek

The Nonassociative Lambek Calculus (NL) represents a logic devoid of the structural rules of exchange, weakening, and contraction, and it does not presume the associativity of its connectives. Its finitary consequence relation is decidable in polynomial time. However, the addition of classical connectives conjunction and disjunction (FNL) makes the consequence relation undecidable. Interestingly, if these connectives are distributive, the consequence relation is decidable in exponential time. This paper provides the proof that we can merge classical logic and NL (i.e. BFNL), and still the consequence relation is decidable in exponential time.

academic

Complexity of Nonassociative Lambek Calculus with classical logic

基本信息

论文ID: 2501.00493
标题: Complexity of Nonassociative Lambek Calculus with classical logic
作者: Paweł Płaczek (WSB Merito University in Poznan, Poland)
分类: cs.LO (Logic in Computer Science), cs.CC (Computational Complexity)
发表会议: Non-Classical Logics Theory and Applications (NCL'24), EPTCS 415, 2024
论文链接: https://arxiv.org/abs/2501.00493

Lambek演算的发展历程：Lambek在1958年引入了句法演算(后称为Lambek演算L)，随后在1961年引入了非结合性版本(NL)。这些逻辑系统在形式语言学和计算语言学中有重要应用。
复杂性问题的重要性：
- 纯NL的有穷后承关系在多项式时间内可判定
- 纯L是NP完全的，但其有穷后承关系不可判定
- 添加经典连接词后的复杂性变化是一个核心问题
现有研究的局限：
- FNL(带加法连接词的完全非结合性Lambek演算)的后承关系不可判定
- DFNL(分配性FNL)在指数时间内可判定
- BFNL(布尔FNL)和HFNL(海廷FNL)的复杂性上界尚未确定

研究动机

本文的核心动机是确定BFNL(结合了非结合性Lambek演算和布尔逻辑的系统)的计算复杂性上界，这对理解逻辑系统的表达能力与计算复杂性之间的权衡具有重要意义。

核心贡献

主要理论结果：证明了BFNL的有穷后承关系在指数时间(EXPTIME)内可判定
技术方法创新：扩展了Shkatov和Van Alten在DFNL上的方法，适用于包含否定的布尔情况
完整性证明：提供了带常元1的BFNL版本的完整证明
理论框架：建立了部分剩余布尔代数的理论框架，为复杂性分析提供了数学基础

变量：可数个命题变量
二元连接词：⊗(乘积), , /(剩余), ∨(析取), ∧(合取)
一元连接词：¬(否定)
常元：1, ⊤, ⊥

2. 序列演算系统

使用束(bunches)而非传统序列，束是自由双幺半群的元素：

逗号表示⊗操作
分号表示∧操作
ε是逗号的单位元，δ是分号的单位元

关键推理规则包括：

(⊗⇒) Γ[(A,B)]⇒C / Γ[A⊗B]⇒C
(⇒⊗) Γ⇒A  Δ⇒B / Γ,Δ⇒A⊗B
(¬⇒) A∧¬A ⇒⊥
(⇒¬) ⊤⇒ A∨¬A

3. 语义模型

BFNL的模型是剩余布尔代数，满足：

**(G,⊗,,/,1,≤)**是单位剩余群胚
**(G,∨,∧,¬,⊥,⊤,≤)**是布尔代数
剩余性质：a⊗b ≤ c ⟺ b ≤ a\c ⟺ a ≤ c/b

核心技术方法

1. 部分结构理论

定义：部分剩余布尔代数是可嵌入到完全剩余布尔代数中的部分结构。

关键定理3.19：给出了识别部分剩余布尔代数的充要条件，包括：

(S) 分离性条件
(M⊗), (M), (M/) 乘法和剩余的模态条件
(M1) 单位元条件

2. 滤子理论

利用素滤子刻画代数结构：

素滤子：满足F1-F3和FB条件的滤子
剩余框架：(F(B), I_B, R_B)，其中F(B)是素滤子集合
复布尔代数构造：从剩余框架构造复代数

3. 复杂性分析算法

算法4.1：验证部分剩余布尔代数

步骤1-3：多项式时间检查基本性质
步骤4：构造素滤子族，检查模态条件
- 时间复杂度：O(2^(5|B|))
步骤5：检查分离性条件
- 时间复杂度：O(|B|2^(2|B|))

主定理4.3：BFNL后承关系的EXPTIME可判定性

构造大小不超过n = 2(总公式大小) + 4的所有部分剩余布尔代数
对每个代数检查所有可能赋值
总时间复杂度：O(2^((L+1)n³+5n))

实验设置

本文是纯理论研究，不涉及实验验证。主要通过数学证明建立复杂性结果。

理论验证方法

构造性证明：通过显式算法证明可判定性
复杂性分析：详细分析算法各步骤的时间复杂度
完备性论证：证明算法的正确性和完整性

实验结果

主要理论结果

EXPTIME上界：BFNL的有穷后承关系在指数时间内可判定
与相关系统的比较：
- NL：PTIME可判定
- FNL：不可判定
- DFNL：EXPTIME完全(无常元1)，EXPTIME内(有常元1)
- BFNL：EXPTIME内(本文结果)
复杂性层次：
- 无常元1的BFNL：EXPTIME完全(因为是DFNL的强保守扩张)
- 有常元1的BFNL：EXPTIME内，下界仍为开放问题