返回学习路线

U16 单元验收：输出、终止、时间与证据分别算 ​

任务 ​

程序先令 $x:=0$，随后在 $x=0$ 时反复执行 $x:=\mathrm{Bernoulli}(1/2)$，退出后返回 $x$。写出有限展开和极限输出次分布，计算后奖励 $f(x)=3x+1$ 的 wp，以及赋值/采样和每次守卫各成本一时的完整 ERT。再给一个 AST 却期望时间无穷的程序。最后对两个盒子的 observe 程序算后验，并解释零证据为什么不能归一化。

完整解答 ​

1. 输出次分布只累计已经终止的质量 ​

最多允许 $n$ 次采样、超过则视为尚未返回时，输出次分布为

$${\nu }_n=(1-2^{-n}){\delta }_1.$$

缺失质量 $2^{-n}$ 是仍未采到一的概率。令 $n\to \mathrm{\infty }$，极限为 ${\delta }_1$，总质量一，因此程序 AST。仍有“永远采到零”的无限运行，但其概率为零。

2. wp 积分输出奖励，不计算耗时 ​

因为返回时 $x=1$，所以 $f(1)=4$。有限展开奖励为 $4(1-2^{-n})$，极限 wp 为四。取后奖励一则 wp 为一，表示终止概率；取后奖励零则 wp 为零，不表示运行成本零。

一般成功概率 $p>0$ 时，循环奖励满足 $w=p\cdot 4+(1-p)w$，最小解为四。$p=0$ 时特征函数变成恒等映射，最小解为零；不能把 $p>0$ 的答案无条件延伸到零。

3. 成本必须算到最后一次失败守卫 ​

令 $R_1=1$，因为从 $x=1$ 开始仍要检查一次守卫才能退出。令 $R_0$ 为从零开始的循环成本，则

$$R_0=1+1+\frac{1}{2}{R}_1+\frac{1}{2}{R}_0,R_0=5.$$

再加初始化赋值成本一，完整 ERT 为六。按期望次数复核：两次采样、三次守卫、一次初始化。若以“掷币次数”为唯一成本，答案才是二；两种答案没有矛盾，成本合同不同。

4. 概率一结束仍可能平均工作无穷 ​

先令 $K$ 为首次公平币正面前的反面数，再实际执行 $2^K$ 次单位操作。每个有限 $K$ 都导致有限运行，而 $K$ 几乎必定有限，所以程序 AST。

然而 $\text{Pr}(K=k)=2^{-k-1}$，因此

$$\mathbb{E}T\ge \sum _{k\ge 0}{2}^{-k-1}{2}^k=\mathrm{\infty }.$$

若只用一条单位成本赋值计算 $2^K$ 而不执行这些操作，便不是同一个运行时间反例。必须明确何种操作被计时。

5. observe 留下的是未归一化质量 ​

以 $2/5$ 选盒 $A$、$3/5$ 选盒 $B$，红球概率分别为 $3/4$、$1/6$。执行 observe 红球后返回盒子，未归一化质量为 $\nu (A)=3/10$、$\nu (B)=1/10$，所以 $Z=2/5$；归一化后 $A,B$ 概率分别为 $3/4,1/4$。

如果两个盒子都没有红球，则 $Z=0$，归一化未定义。不能把 $0/0$ 填成零后称为概率分布，也不能任意返回原先的选盒概率。模型没有指定怎样处理不可能证据，需要改变观测假设或明确另一个语义。

连续变量恰等于某点也可能是零概率事件，不能因为该值“看上去合法”就使用这个简单 observe 筛选；需要似然密度或适当条件分布模型。

验收标准 ​

必须同时交代有限展开的缺失质量、极限的 AST、wp 的奖励含义、ERT 的成本清单、无穷期望的发散级数以及 $0<Z<\mathrm{\infty }$ 的归一化条件。把所有量都归一成一、漏算退出守卫、把 AST 当作有限均值、或对零证据强行归一化，均属于关键错误。

依据 ​

Kaminski–Katoen–Matheja–Olmedo《Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs》§§2–5；Jansen 等《Conditioning in Probabilistic Programming》；McIver 等《A New Proof Rule for Almost-Sure Termination》。