期望运行时间变换器

wp 把未终止路径的输出奖励记为零，ert 却必须记录它已经花掉、还会继续花掉的时间。仅把后期望设为一，得到的是终止概率，不是运行时间。

后续成本可能依赖前段生成的随机状态，因此顺序组合不能只把两个脱离输入的平均数相加。必须将后一段的成本函数传回前段积分。

抛到成功到底要付几次判断 ​

程序先执行 $x:=0$，然后 while x=0 do x:=Bernoulli(p)，其中 $p>0$ 为采到一的概率。一次采样赋值成本一，守卫成本一。

令 $R_0,R_1$ 为循环从 $x=0,1$ 出发的期望成本。已经成功时只需最后一次判断，故 $R_1=1$。未成功时支付判断和采样各一，再进入后继状态：

算上初始化，整程序成本为 $2/p+2$。公平币 $p=1/2$ 时为 $6$。也可逐项核对：平均采样两次、守卫三次、初始化一次，总和六。若只说“平均两次抛币所以运行时间二”，就是换了成本模型。

当 $p=0$，方程没有有限解，最小扩展非负解为无穷；不能在 $2/p+2$ 中把零分母忽略。

点态有限的后段仍可能有无穷平均 ​

前段几乎必然产生 $K$，且 $\text{Pr}(K=k)=2^{-k-1}$；后段执行 $2^K$ 次单位工作。对每个有限输入 $k$，后段成本都有限，但前段对该成本函数的期望为

因此“前段有限期望、后段每个输入有限时间”不足以推出组合有限期望。需要控制后段成本在前段输出分布下的可积性。[1, Introduction]

若找到 $I$ 使 ${\mathrm{\Psi }}_0(I)\le I$，最小不动点归纳给出 $\mathrm{ert}[W](0)\le I$。这和概率循环上界不变式公理库概率循环不变式与期望界Probabilistic loop invariant · Expectation invariant以循环特征函数的不等式证明输出期望界，展示上界归纳、下界反例，以及几乎必停和有界性怎样消除尾项。结构相同，但特征函数多了真正的执行成本。

成本模型可以改为指令数、查询数或能耗，但必须逐项重新说明。若允许零成本无限循环，累计成本可能有限而程序不终止；本页通过正成本守卫排除了这一情况，不能把有限成本结论无条件推广到任意自定义奖励。