终止性与良基关系

形式陈述 ​

二元关系公理库关系Relation · Binary relation带源集与目标集的二元关系，其底层关系图是 A×B 的子集。 $\prec$ 在集合 $W$ 上称为良基的，若不存在无限下降链

$$w_0\succ w_1\succ w_2\succ \cdots .$$

等价地，每个非空子集 $A\subseteq W$ 都含有一个 $\prec$-极小元。

设转移系统的状态集合为 $\mathrm{\Sigma }$、一步关系为 $\to$。它从初始集合 $I\subseteq \mathrm{\Sigma }$ 终止，表示不存在

$${\sigma }_0\to {\sigma }_1\to {\sigma }_2\to \cdots ({\sigma }_0\in I)$$

这样的无限执行。若存在映射 $\rho :\mathrm{\Sigma }\to W$，使 $(W,\prec )$ 良基且每一步都满足

$$\sigma \to {\sigma }^{\prime }⟹\rho ({\sigma }^{\prime })\prec \rho (\sigma ),$$

则 $\rho$ 称为排名函数，并证明系统终止。

自然数上的 $<$ 是最常用的良基关系。字典序、有限多重集合扩张和序数可组合多个阶段的下降，但必须单独证明所用复合关系仍良基。

直觉 ​

循环不变量说明执行“始终没有走错”，排名函数说明执行“不能永远走下去”。前者约束状态所在区域，后者给每一步分配不可无限减少的预算。

只证明变量非负不够；还要证明每一步严格下降。只证明偶尔下降也不够，除非能排除两次下降之间的无限停滞。终止性是对所有允许执行的量化，存在一条结束路径不能证明非确定程序必终止。

例子与边界 ​

欧几里得算法对正整数状态 $(a,b)$、$b>0$ 执行

$$(a,b)\to (b,amodb).$$

取排名 $\rho (a,b)=b$，下一步余数严格小于 $b$ 且非负，所以算法终止。

二分查找可取候选区间长度 $r-l$ 为排名。错误更新 l = mid 可能保持长度不变，因而部分正确性论证无法补上终止义务。

随机过程几乎必然终止，不等于每条样本路径都终止；期望终止时间有限又是更强的定量条件。并发系统的公平性也会影响活性：某线程一直不被调度造成的无限执行，可能在公平语义下被排除、在无公平假设下被允许。

推论与应用 ​

非终止可表示为无限下降序列公理库序列Sequence以自然数为定义域的函数。 x0 ≻ x1 ≻ x2 ≻⋯；良基性排除这种序列，因此给排名函数或良基关系就能把每一步严格下降转成终止证明。

完全正确性公理库算法正确性Algorithm correctness · Partial and total correctness所有合法执行都符合规格，并在完全正确时保证终止。等于部分正确性加终止性。循环、递归和重写系统可分别用变体、结构递归与简化序证明终止。强归纳公理库强归纳法Strong induction · Complete induction归纳步可假设所有较小自然数情形成立。是自然数良基归纳的常见实例；序数排名则能处理嵌套阶段和更复杂的下降模式。

自动终止分析尝试合成线性、词典序或分段排名函数；失败只表示该模板没有找到证书，不自动说明程序发散。停机问题排除了适用于所有程序的完备自动判定器。

参考资料

• Nachum Dershowitz and Zohar Manna, “Proving Termination with Multiset Orderings,” Communications of the ACM 22(8), 1979.
• Amir Pnueli, “The Temporal Logic of Programs,” FOCS, 1977.
• Jean-Pierre Jouannaud and Albert Rubio, “The Higher-Order Recursive Path Ordering,” LICS, 1999.