结果族 129：Exponential state costs for two-way automata · 学科：Theoretical computer science · 验证状态：主结果已 Lean 形式化
自动机是一台只带”有限格记忆”的读带小机器:每读一个字符,就按当前心情(状态)决定下一步。双向机器更灵活,读头能左右来回走,还允许”猜”出一条走得通的路。论文证明:让这种机器改做相反判决(原来接受的现在一律拒绝),它的心情清单必须暴增——不存在一劳永逸的省心压缩。
关键词卡片
看个具体例子
论文对每个 @@M@@n\ge4@@ 造出一台恰有 @@M@@n@@ 个状态的 2NFA,而识别其补语言的任何 2NFA 状态数有指数下界。
公式卡 补机至少需要 @@M@@\tfrac12 2^{\lfloor(n-4)/127\rfloor}-1@@ 个状态:@@M@@n=1000\Rightarrow\ge\tfrac12\cdot2^{7}-1=63@@ 个;@@M@@n=10000\Rightarrow\ge\tfrac12\cdot2^{78}-1\approx1.5\times10^{23}@@ 个。
状态需求随 @@M@@n@@ 指数增长,任何多项式 @@M@@p(n)=n^C@@ 都追不上——”与字母表无关的多项式补”就此被否定;即使补机继续保留”猜”的能力,也逃不掉这道指数墙。
为什么值得关心
这个问题从 Sakoda–Sipser 1978 年的经典工作一路传下来,2026 年的综述仍把它列为公开问题;本文给出否定答案,顺带也排除了与字母表无关的多项式确定化界。
已 Lean 形式化
第一级台阶
导读里那台”只带有限格记忆的读带小机器”翻译过来：对象是一条两端有标记的输入带和一台只有有限个状态（心情）的机器；操作是读头沿带左右移动，遇到岔路可以”猜”一条走得通的路，猜中一条即接受。补运算要求机器对同样的输入做出完全相反的判决——原来接受的现在一律拒绝。论文问：把判决反过来，心情清单必须膨胀多少？答案是指数级。
第二级台阶
用本科术语精确化。双向非确定有限自动机（2NFA）的状态数衡量机器大小；某台机器接受的语言之补，指全部输入中它不接受的那部分。要害在”与字母表无关的多项式界”：是否存在一个多项式 p，使得任何 n 状态的 2NFA，其补语言都能被 p(n) 状态的 2NFA 识别——p 不许依赖字母表有多大。下界的试金石是活性语言：字母表取全体二元关系，一个字被接受当且仅当这些关系的乘积非空。
第三级台阶
定理在这样的语境下陈述：对每个 n≥4，存在恰好 n 个状态的 2NFA 识别上述活性语言，而任何识别其补语言的 2NFA——读头可任意双向移动、且仍可继续”猜”——至少需要 ½·2^⌊(n−4)/127⌋−1 个状态。假设的分工：字母表随 n 增长（大小为 2 的 (n−2)² 次方），这正是”字母表一致”命题的本意，界限必须顶住任意大的字母表；补机保持非确定性，使结论覆盖最强的对手。用这些术语说结论：不存在与字母表无关的多项式补状态界，这道从 Sakoda–Sipser（1978）传下、2026 年综述仍列为公开问题的悬案得到否定回答。
论文证明双向非确定有限自动机（2NFA）的补运算不存在与字母表无关的多项式状态界：对每个 @@M@@n\ge4@@ 构造 @@M@@n@@ 状态的 2NFA，识别其补语言的任何 2NFA 至少需要 @@M@@\tfrac12 2^{\lfloor(n-4)/127\rfloor}-1@@ 个状态，从而给出指数下界。
双向非确定有限自动机（two-way nondeterministic finite automaton, 2NFA）的读头可在带端标记的输入上左右移动，接受当且仅当某条有限计算到达接受态。补运算问的是：是否存在一个与字母表无关的多项式 @@M@@p@@，使每个 @@M@@n@@ 状态 2NFA 的补语言都能被 @@M@@p(n)@@ 状态的 2NFA 识别？这条线索始于 Sakoda 与 Sipser 1978 年关于非确定性与双向自动机的经典工作；Vardi 1989 年给出指数级的一向非确定补机构造，Kapoutsis 2006 年证明了”单向活性”（one-way liveness）语言的补在所有扫掠式（sweeping）2NFA 中需指数状态，但读头只能在端标记处折返。对允许任意双向移动的补机，Guillon、Prigioniero 与 Taheri 在 2026 年的综述中仍将多项式补列为公开问题（他们只对可重写带格的 1-limited 自动机给出多项式补）。本文否定性地解决了这个字母表一致的多项式补问题。
对每个 @@M@@n\ge4@@，取 @@M@@H=\{1,\ldots,n-2\}@@，字母表 @@M@@\Sigma_n@@ 取为 @@M@@H@@ 上全部二元关系（@@M@@|\Sigma_n|=2^{(n-2)^2}@@，随 @@M@@n@@ 增长），考虑关系乘积活性语言 @@M@@L_H=\{w:r(w)\ne\varnothing\}@@，即 Sakoda–Sipser 的语言族 @@M@@B_h@@、Kapoutsis 所称的 one-way liveness。主定理：存在恰好 @@M@@n@@ 状态的 2NFA @@M@@A_n@@ 识别 @@M@@L_H@@，而任何识别补语言 @@M@@\Sigma_n^*\setminus L(A_n)@@ 的 2NFA 至少需要 @@M@@\tfrac12 2^{\lfloor(n-4)/127\rfloor}-1@@ 个状态。由于右端随 @@M@@n@@ 指数增长，不存在与有限字母表无关的多项式补状态界。附带推论：借助 2DFA 可线性补的已知结果（Geffert–Mereghetti–Pighizzini），同一语言族也排除与字母表无关的多项式确定化界。
证明把计算表示与有限代数下界分开。源机器极简：@@M@@h+2=n@@ 个状态单向”猜路径”——初始态在左端标记处任选 @@M@@p\in H@@ 进入，读到关系 @@M@@R@@ 时若 @@M@@(p,q)\in R@@ 则右移到 @@M@@q@@，抵达右端标记即接受；接受恰好当关系乘积非空。难点全在补机一侧。
先建立表示层。任何 @@M@@s@@ 状态 2NFA 的有限计算被编码为”路径图”（path diagram）：一段计算由四个关系 @@M@@F,B@@（贯穿）与 @@M@@L,R@@（返回）记录其两个边界上的进出口，标签集是 @@M@@m=s+1@@ 个带方向的机器状态副本。路径图按路径序合成，恰为 Martin–Mazorchuk 的分块二元关系幺半群（monoid of partitioned binary relations）@@M@@\mathcal T_m@@。加边只会增加接受路径，故 @@M@@\tau(u)\sqsubseteq\tau(v)@@ 蕴含任意上下文中 @@M@@u@@ 被 @@M@@v@@ 替换后仍接受。而补机恰好接受乘积为空的字，用单点关系字母 @@M@@I_{\{p\}},I_{\{q\}}@@ 做上下文即可逐对”测出”乘积内容，从而得到从 @@M@@\mathcal T_{s+1}@@ 的子幺半群到 @@M@@\mathcal R_H@@ 的满射同态 @@M@@\phi@@，且 @@M@@\phi@@ 反转包含序：@@M@@z\sqsubseteq w\Rightarrow\phi(w)\subseteq\phi(z)@@。
再证代数下界 @@M@@2m\ge2^{\lfloor(h-2)/127\rfloor}@@。对幂等图 @@M@@e@@（@@M@@e^2=e@@），边界标签按”递归类”（recurrent classes）分组，至多 @@M@@2m@@ 类；在角幺半群 @@M@@e\mathcal T_me@@ 中，元素 @@M@@z@@ 可能摧毁某些类的贯穿回路，记录为缺失集 @@M@@\mathcal M_e(z)@@。两个结构事实控制损失：其一（传输引理），经固定语境搬运时缺失界只放大两倍且落到单一公共集合上；其二（链界），沿嵌套幂等链逐级损失之和不超过初始预算的两倍——关键是一个二分法：每个新递归类要么包含一个未损失的旧类，要么包含两个旧类，用赋权 @@M@@1/2@@ 的计数即可汇总。
最后是放大步骤。取 @@M@@t=64@@，归纳证明在像中添加一个非对角对（@@M@@\phi(a)=I_H\cup\{(x,y)\}@@）必须付出 @@M@@|\mathcal M_e(a)|\ge D(h)=2^{\lfloor(h-2)/127\rfloor}@@ 的代价：先用置换的单位原像共轭出 @@M@@2t@@ 个分别添加 @@M@@(u_i,z)@@、@@M@@(z,v_j)@@ 的生成元，传输引理给它们公共预算 @@M@@\le8tc@@；相乘得 @@M@@t^2@@ 个各添加一对 @@M@@(u_i,v_j)@@ 的元素，沿长度 @@M@@t^2@@ 的嵌套幂等链逐个加入，链界给出总代价 @@M@@\le16tc@@；而每一步限制到保留 @@M@@h-127@@ 个点的小实例后由归纳假设至少花 @@M@@D(h-127)/2@@。两相比较得 @@M@@c\ge(t/32)D(h-127)=D(h)@@。代入 @@M@@m=s+1@@、@@M@@h=n-2@@ 整理即得定理。
主结果已在 Lean 中形式化证明（结果族 129 的官方文档）。同族姊妹篇用独立的”匹配图”秩损失论证对同一语言证明更强的确定性下界（指数率 @@M@@h/62@@，对比本文经线性补推出的 @@M@@h/127@@），两文方法独立而结论互相印证；本文的障碍甚至适用于非确定的补机，覆盖范围更广。作者为 OpenAI，按其官方声明，未经形式化的结果可能有问题，而本文主要结果已形式化，可信度高。
问 1：证明中最关键、也最脆弱的一步在哪里？
| 答：放大步骤。归纳地证明往同态像中添加一个非对角对必须付出 | M_e(a) | ≥D(h)=2^⌊(h−2)/127⌋ 的缺失代价：先用置换的单位原像共轭出 2t 个生成元（t=64），传输引理给它们公共预算 ≤8tc；相乘得 t² 个各添一对的元素，沿长度 t² 的嵌套幂等链逐个加入，链界给出总代价 ≤16tc；而每一步限制到保留 h−127 个点的小实例后由归纳假设至少花 D(h−127)/2。两相比较得 c≥(t/32)D(h−127)=D(h)。常数 127 正是 t 与”新递归类二分法、赋权 1/2”层层折算的产物——这条链上任何一处预算翻倍系数算错，指数率立即塌掉。 |
问 2：字母表随 n 指数膨胀，是不是下界的弱点？
答：是题中之义而非弱点：命题是”与字母表无关”的多项式补不存在，故构造可以动用大小为 2^{(n−2)²} 的字母表。真正的开放点是反向：若字母表固定，多项式补是否可能——论文未讨论固定字母表情形，综述中也只对可重写带格的受限模型有多项式结果。
问 3：相对 Vardi、Kapoutsis 等已有工作，真正新意是什么？
答：Vardi（1989）给的是一向非确定补机的指数上界构造；Kapoutsis（2006）的指数下界只对扫掠式补机（读头仅在端标记处折返）成立；Guillon–Prigioniero–Taheri 2026 年综述明确把任意双向补机的多项式补列为公开问题。本文的障碍对任意双向移动、且补机本身仍可非确定的对手成立，正面关上这扇门。
问 4：AI 生成证明最可能在哪里出错？
答：表示层的对应细节：有限计算编码为路径图、按路径序合成恰为分块二元关系幺半群 T_m、满射同态 φ 反转包含序——这些代数桥若在带端标记行为或接受条件的边角定义上有微差，整个框架悄然错位。好消息是主结果已 Lean 形式化，此类风险已被机器核验兜住。
问 5：为什么源机器能小到 n 个状态，补机却炸成指数？
答：源机器是单向”猜路径”：初始态在左端标记任选 p∈H，读到关系 R 时若 R 中含 (p,q) 便右移到 q，抵达右端即接受——接受恰当关系乘积非空。补语言要求”证明不存在任何通路”，这是对存在性的全称否定；非确定猜路对前者天然合适，对后者无处着力，指数代价由此而来。
问 6：谁会用这个结果？
答：描述复杂度与自动机理论社区：它否定了字母表一致的多项式补，并经 2DFA 可线性补的已知结果顺带排除与字母表无关的多项式确定化。同族姊妹篇用独立的匹配图秩损失论证对同一语言证得更强指数率 h/62（确定性方向），两法互证；与 Sakoda–Sipser 型电路下界问题的联系是后续自然方向，论文未展开。
总评
近五十年的字母表一致多项式补问题被干脆利落地否定，且主定理有形式化背书、有姊妹篇独立印证，是本批结果中可信度最高的一类；残留的不确定性只在固定字母表情形等外延问题的开放状态。