终止性与良基关系

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

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

欧几里得算法在整数状态 $a>0,b\ge 0$ 上，当 $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归纳步可假设所有较小自然数情形成立。是自然数良基归纳的常见实例；序数排名则能处理嵌套阶段和更复杂的下降模式。

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

自然数多重集序理路自然数多重集终止序Multiset termination order · Dershowitz–Manna order on naturals允许一个大任务换成任意有限个更小任务，用取消公共出现的证书判定自然数bag严格下降，并在任务数增长时证明所有调度终止。把一份大任务替换为任意有限份更小任务，返回取消公共出现的下降证书；任务数与大小总和都可能增长。大小变化分析理路大小变化终止分析Size-change termination · SCT从可靠的跨调用弱/严格下降图计算非空路径闭包，以幂等图的严格自环证书排除无限下降线程，并区分抽象失败与具体非终止。则合成跨调用的弱/严格参数关系，检查全部幂等图能否接出严格自环。后者分析失败时，应区分摘要遗漏真实下降与确有可执行无限循环。

良拟序理路良拟序Well quasi order · WQO用每条无限序列中的顺向可比对定义良拟序，证明向上闭集有限基和增长链终止，并辨别良基与良拟序。用于验证搜索的终止时，除下降链之外还排除无限反链，从而让向上闭摘要的增长过程稳定。它保证的是搜索摘要最终不再变新，不一定是被验证系统的每条运行都停止。

随机程序还需区分几乎必然终止理路概率程序的几乎必然终止Almost-sure termination区分所有运行终止、几乎必然终止和有限期望时间，用几何等待与指数工作量构造可核算的边界。与有限期望时间。排序上鞅理路排序上鞅Ranking supermartingale用非负势函数的统一条件期望下降证明概率程序终止与时间上界，并用对称随机游走说明严格下降的必要性。把逐步下降改成统一条件期望下降，在非负性和可积性等条件下给出终止及时间界；任意非负上鞅本身并不是终止证书。