次概率程序语义

普通输出分布会默认程序总能给出结果。概率程序可能有一部分执行永远不返回，此时把剩余结果强行归一化，会悄悄改成“已知终止”的条件分布，抹掉程序失败返回的风险。

次概率语义保留这个缺口，而且缺口会穿过顺序组合：第一段未返回的质量，根本没有机会进入第二段。

返回一半，另一半永远循环 ​

程序先掷公平币：正面令 $x:=7$ 并结束，反面执行永不退出的循环。终止输出测度为

输出不是概率一的 ${\delta }_7$。后者是条件于终止后的分布，只有在另行声明条件化时才可使用。两程序可能在终止时总输出同一个数，却有不同终止概率，因此次概率语义会区分它们。

顺序组合把丢失质量继续传下去 ​

设 $C$ 以 $1/2$ 返回状态 $a$、以 $1/4$ 返回 $b$、其余不终止。$D$ 从 $a$ 以 $1/3$ 返回 ok，其余不终止；从 $b$ 必然返回 ok。则

一般公式为

总质量 $5/12$ 已计入两段可能不终止，不能先把 $C$ 的 $3/4$ 归一化后再组合；那会得到 $5/9$，改变问题。

循环由有限展开逼近 ​

重复独立掷币，首次正面时返回；每次正面概率 $p>0$。截断为最多允许 $n$ 次掷币、超限视为不返回，终止质量为

这些有限展开的次分布单调增加，极限质量为一。若 $p=0$，每个展开质量都为零，极限也为零。这就是循环语义选择最小不动点的来源：只累计确有有限终止见证的质量。

最弱前期望公理库最弱前期望Weakest preexpectation · Quantitative weakest precondition把输出奖励反向传过概率程序，推导赋值、概率分支和循环规则，并计算终止概率与未归一化期望。是该核对输出奖励的积分；取奖励恒为一，就读出终止概率。对任意可测事件 $A$，取指示函数便读出终止且满足 $A$ 的概率。

可以添加一个显式状态 $\mathrm{\perp }$，把缺失质量放到 $\mathrm{\perp }$，从而恢复总质量一的表示。但 $\mathrm{\perp }$ 必须有独立的组合规则，不能当成普通成功输出。两种表示可等价表达同一语义，关键是不要丢失不终止信息。

条件化与评分公理库概率程序中的条件化与评分Conditioning in probabilistic programs · Score semantics把 observe 看成筛选、score 看成加权，计算归一化常数并分别处理零证据、连续观测和不终止。引入后，质量还可能因拒绝证据而减少，或因评分而超过一。那时单靠“缺失质量等于不终止”已不够，必须扩展语义解释。