递减图对转移系统合流性是否完备？

完备性问题究竟在问什么

合流性又称 Church–Rosser 性质，指的是从同一状态出发的两条有限计算总能在某个公共归约结果处汇合。van Oostrom 的递减图技术把这一全局性质化归为局部性质：只要一步关系存在局部递减标号，即每个局部峰都能用一个各步在良基序上递减的图来汇合，系统就是合流的。

完备性问的是反方向：是否每个合流转移系统都存在这样的标号？van Oostrom 于 1993 年提出该问题，它成为 RTA 开放问题清单中的第 56 题。在本论文之前，肯定答案只对可数系统已知，后来推进到首个不可数基数 aleph 1。一般情形一直悬而未决。

三标签在任意基数下都够用

主定理指出，每个合流抽象重写系统在标签序 {0,1,2} 及通常的小于关系上都是递减 Church–Rosser 的。该结果不设基数限制，因此适用于可数系统、大小为 aleph 1 的系统，以及远大于连续统的系统。

证明按连通分支逐一处理。可数分支由一条两标签引理解决。不可数的几乎正则分支由扇形构造解决。剩下的奇异情形，即关系的共尾基数奇异，由双扇形构造解决，它产生一个共尾、连通、合流且局部几乎确定性的子系统。

为什么两个标签不够用

三标签这一界是最优的。即便在首个不可数基数上，两个标签也不够用，这一事实此前由 Ivanov 确立，本文将其作为匹配的下界引用。因此论文的贡献不只是存在某个有限标号，而是一般情形下所需的最少标签数恰好是三。

这一区分很重要，因为可数情形确实更容易：对可数系统而言，两个标签已经够用。二与三之间的差距只在引入不可数系统后才出现，而这正是论文要覆盖的范围。

几乎确定性子系统承担了核心工作

核心机制是：在任意高基数的每个合流抽象重写系统中，都存在一个共尾、连通、合流且局部几乎确定性的子系统。几乎确定性重写序列至多含一个非确定性步骤，因此至多做出一次真正的选择；这恰好是两标签递减图所能吸收的。

论文把该子系统描述为一种重写策略。证明构造出它，说明它在原系统中共尾，再用它构造重写步骤的局部递减标号。作者指出，这把 Klop 的共尾归约推广到了可数情形之外。

合流性如今与终止性平起平坐

论文把这一结果定位为让合流性与终止性处于同等地位。对终止性而言，原则上完备的判据早已存在：项重写系统终止当且仅当它与某个良基单调代数相容，依赖对框架也给出了完备刻画。而对合流性，此前没有可与之相比的完备方法。

最紧凑的推论是 Church–Rosser 性质与递减 Church–Rosser 性质等价。按作者的解读，递减图作为合流判据没有损失任何能力，因为每个合流系统都能由这一单一方法证明合流。同样的等价也适用于 de Bruijn 的弱菱形性质，它与递减图强度相同。

实数系统无需额外假设

由于完备性在每个基数上都成立，它特别地也适用于状态为实数的系统，而且是无条件成立的，与连续统假设无关。论文将其列为单独推论，因为实数是实际意义最大的基数。

这对此前的最先进结果很重要。Ivanov 的界只在连续统假设下才达到连续统；若不假设它，实数的基数可能位于 aleph 层级中任意高的位置。因此论文的无条件处理覆盖了先前界在缺少集合论假设时无法触及的实值系统。

该证明没有提供什么

证明是非构造性的，依赖选择公理。作者明确表示，对其产生的标号不主张任何有效内容，并把递减标号的可计算性与构造性存在列为开放方向。对左线性项重写系统等受限类，递减标号已经可以通过规则标号和相对终止自动构造，但那是另一条工作线。

该结果也不延伸到交换性。van Oostrom 把递减图推广到交换性的版本对证明交换性并不完备，论文把寻找交换性的完备推广列为未来工作。这里的完备性主张专门针对合流性。

实际挑战变成寻找一个好的标号

论文自身对实际后果的解读是：难点所在的位置发生了转移。既然局部递减标号总是存在，核心的实际挑战就变成找到一个好的标号，而不是判定它是否存在。作者提出发展启发式方法，把递减图和弱菱形性质应用于真实程序，扩展参与者程序的合流分析与项重写系统的规则标号技术。

该结果在 Isabelle/HOL 和 Lean 中分别独立机器验证，两份形式化都存档于 Zenodo。作者指出，根据 Isabelle/HOL 的证明论保守性，把定义展开后的定理已经可在 Pitts 的标准 HOL 中证明，因此完备性结果在 ZFC 中成立；仅有 Lean 证明则做不到这一点，因为 Lean 的类型论要在 ZFC 中解释需要不可达基数。形式化工作是在作者指导与审阅下，借助 Anthropic 的 Claude 完成的。

本文引用的文献