终止性与良基关系

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

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

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

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

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

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

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

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

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