概率循环不变式与期望界

上界可以从零开始归纳：零不超过候选界，每次展开后仍不超过它，极限自然也不超过它。下界若从一个较大的候选开始，可能一直保留只在无限运行中存在的“虚假奖励”；要把这种残留消掉，需要终止和尾部条件。

因此概率不变式不是把布尔循环不变式的真、假换成数字就结束了。极限中的奖励是否还留在未终止路径上，是新的证明义务。

手算对称赌徒的胜率 ​

状态 $x\in \{0,1,2,3,4\}$，在 $1,2,3$ 时等概率走到 $x-1$ 或 $x+1$，到边界 $0,4$ 停止。后期望为 $f=[x=4]$，候选 $I(x)=x/4$。

在内部，${\mathrm{\Phi }}_f(I)(x)=\frac{1}{2}(x-1)/4+\frac{1}{2}(x+1)/4=x/4$；在边界，$I(0)=0$、$I(4)=1$ 与奖励相同。因此上界规则给胜率至多 $x/4$。

从任意内部状态，连续四次选同一方向的概率至少为 $1/16$，在此前必已碰到边界。故每四步仍未终止的概率至多乘 $15/16$，循环几乎必停。又有 $0\le I\le 1$，下界条件也成立，于是胜率恰为 $x/4$；从 $x=1$ 出发为 $1/4$。

下不动点本身为什么不够 ​

对 while true do skip，特征函数为 $\mathrm{\Phi }(X)=X$。取常数 $I=1$，有 $I\le \mathrm{\Phi }(I)$，但循环永不终止，所以最弱前期望是零，$1\le 0$ 显然错误。失败来自最小不动点的选择，而不是某次代数计算。

让尾项消失的具体计算 ​

记终止时刻为 $T$、运行状态为 $S_n$。将 $I\le {\mathrm{\Phi }}_f(I)$ 展开 $n$ 次，得到

若 $I\le M<\mathrm{\infty }$，第二项至多 $M{\text{Pr}}_s(T>n)$；几乎必停使它趋零。第一项由非负单调收敛定理公理库单调收敛定理Monotone convergence theorem非负可测函数单调递增时，积分极限等于极限函数积分。趋于真实终止奖励 $w(s)$，所以 $I(s)\le w(s)$。

如果 $I(S_n)$ 在越来越罕见的未终止路径上爆炸，概率趋零本身不能保证乘积期望趋零。这正是无界期望需要额外分析的地方。

本页的上界证明只需从零开始的可数迭代：由 $0\le I$、${\mathrm{\Phi }}_f(I)\le I$ 及单调性，归纳得到 ${\mathrm{\Phi }}_f^n(0)\le I$；再用单调收敛取极限。这个证明不要求全体可测函数构成完备格。

若状态空间可数且取离散 σ-代数，则所有非负扩展实值函数都可测，它们的逐点序确实构成完备格，这时也可直接用 Knaster–Tarski 不动点定理公理库Knaster–Tarski 不动点定理Knaster-Tarski fixed-point theorem · Tarski fixed-point theorem完备格上的单调自映射之全部不动点构成完备格，并具有规范的最小与最大不动点。。一般可测空间中，任意一族可测函数的逐点上确界未必可测，不能无条件调用其完备格版本。

若想证明有限期望运行时间，应对成本特征函数寻找上界，而非只对终止奖励一寻找上界。排序上鞅公理库排序上鞅Ranking supermartingale用非负势函数的统一条件期望下降证明概率程序终止与时间上界，并用对称随机游走说明严格下降的必要性。提供平均下降证书，运行时间变换器公理库期望运行时间变换器Expected runtime transformer · ERT calculus给概率程序逐项计费并反向组合期望成本，用几何循环算出守卫检查的额外开销，区分 ert 与 wp。则将每条语句的成本逐项组合。