概率程序的几乎必然终止

AST 允许存在不终止运行，只要求它们总体概率为零。有限期望还限制罕见但极长的运行，不能让它们的概率与耗时相乘后累积成无穷。

因此“每次继续的概率都小于一”“每条有限路径以后都有机会结束”“平均时间有限”是不同说法。需要计算累计存活概率，而不是只看某一步的分支概率。

抛到正面：不终止路径存在，概率却为零 ​

每次独立抛公平币，正面结束，反面继续。按抛掷次数计时，有 $\text{Pr}(T>n)=2^{-n}$，因此

“永远反面”是一条合法无限运行，所以程序不是每条运行都终止；它仍 AST，甚至 PAST。零概率不是逻辑不可能。

AST 但期望工作量无穷 ​

先抛公平币，令 $K$ 为第一次正面前出现的反面次数；随后实际执行 $2^K$ 次单位操作，再结束。这里指数工作必须真的通过循环执行，不能用一个单位成本赋值假装已经做完。

$\text{Pr}(K=k)=2^{-k-1}$，$K$ 几乎必定有限，第二段对每个有限 $k$ 也终止，所以整程序 AST。但是

每一种规模出现得越来越少，却各自对期望贡献同样的 $1/2$，无限多个规模累加后发散。

每轮都可能结束，仍可有正概率永不结束 ​

第 $n\ge 1$ 轮条件终止概率取 $p_n=2^{-n-1}$，否则进入下一轮。到第 $N$ 轮后仍存活的概率为 $\prod _{n=1}^N(1-p_n)$。由于 $\sum _n{p}_n<\mathrm{\infty }$ 且各项远离一，这个无限乘积为正；例如用 $\log (1-x)\ge -2x$（$0\le x\le 1/2$）可给出正下界。

所以每轮“有机会退出”不够。若存在统一 $\epsilon >0$，保证每轮条件退出概率至少 $\epsilon$，才可用几何尾界推出有限期望轮数。

对非负整数时间，尾和公式 $\mathbb{E}T=\sum _{n\ge 0}\text{Pr}(T>n)$ 同时解释两个层级：AST 只要求尾概率趋零，有限期望要求整个尾和收敛。

排序上鞅公理库排序上鞅Ranking supermartingale用非负势函数的统一条件期望下降证明概率程序终止与时间上界，并用对称随机游走说明严格下降的必要性。若提供统一正幅度的平均下降，通常可证明 PAST；只有非负上鞅或没有统一下降幅度，则需要更精细的 AST 规则。期望运行时间变换器公理库期望运行时间变换器Expected runtime transformer · ERT calculus给概率程序逐项计费并反向组合期望成本，用几何循环算出守卫检查的额外开销，区分 ert 与 wp。可以直接表达无穷期望，而不会把“概率一结束”误当成有限数值答案。

本页没有调度非确定性。若程序还由调度者选择动作，必须说明是对每个调度者都 AST，还是存在一个调度者 AST；概率一不能替代这个额外量词。