二元长度归约循环重写的合流性不可判定性
Undecidability of Confluence for Binary Length-Reducing Cycle Rewriting
浏览论文内容
中文总结 AI 辅助
该研究证明固定字母表{0,1}上二元长度归约循环重写系统的合流性不可判定，通过编译确定性验证器为加权循环系统再转成二元长度归约系统完成证明，区分了循环与字符串重写。
中文摘要 AI 辅助
合流性保证发散的重写选择总能重新汇合。对于有限终止的字符串重写系统和项重写系统，可通过临界对分析判定合流性，且对于长度归约的字符串，判定过程可在多项式时间内完成。相比之下，对于有限终止的超图变换系统，合流性是不可判定的。我们证明，这种不可判定性已出现在圆上的字中，即模旋转的字符串。在固定字母表{0,1}上，有限循环重写系统的合流性是不可判定的，实际上是Π⁰₁完全的，即使每条规则都有非空右部且严格归约长度。在该限制下，终止性在语法上是显然的，且从非空长度为n的循环出发的推导步数少于n步。对于每个至少包含两个字母的固定字母表，情况相同，而单字母的情况是可判定的。仅旋转就将循环重写与字符串重写区分开来。该证明将确定性验证器编译为具有一个受控分支的加权循环系统，然后通过游程编码将其编译为二元长度归约系统，其清理规则将每个可归约的畸形循环发送到一个错误范式。
英文摘要
Confluence guarantees that diverging rewrite choices can always be rejoined. For finite terminating string- and term-rewriting systems, confluence is decidable by critical-pair analysis, and in polynomial time for length-reducing strings. For finite terminating (hyper)graph transformation systems, in contrast, confluence is undecidable. We show that undecidability already appears for words on a circle, that is, strings up to rotation. Confluence of finite cycle-rewriting systems over the fixed alphabet $\{0,1\}$ is undecidable, indeed $Π^0_1$-complete, even when every rule has a nonempty right-hand side and strictly reduces length. Under this restriction termination is syntactically evident, and derivations from a nonempty length-$n$ cycle have fewer than $n$ steps. The same holds over every fixed alphabet with at least two letters, while the one-letter case is decidable. Rotation alone separates cyclic from string rewriting. The proof compiles a deterministic verifier into a weighted cycle system with one controlled branch, then into a binary length-reducing system via a run-length code whose cleanup rules send every reducible malformed cycle to one error normal form.
