概率分布单子

普通函数给一个答案，概率计算给一份答案分布。bind 做两件事：先从前段分布选一个中间值，再按这个值运行后段随机计算，最后把所有中间分支的质量加起来。

单子律允许改变括号、插入或删除无效果的确定返回，而不改变分布。它不允许把依赖前段结果的后段随意提前执行，也不意味着所有随机选择自动独立。

先选机器，再看输出 ​

先以 $1/4$ 选机器 $a$、以 $3/4$ 选机器 $b$。机器 $a$ 以 $1/2$ 输出一，机器 $b$ 以 $1/6$ 输出一。bind 后

若随后确定性地返回输出的平方，分布不变；若返回其补比特，则两项质量交换。后段可以依赖中间机器标签，不能只保留一个未经核对的“平均机器”。

结合律其实是同一份路径质量 ​

对最终输出 $z$，左侧结合给

右侧给 $\sum _x\mu (x)\sum _{y}f(x)(y)g(y)(z)$。有限求和交换说明二者相等；每条路径 $x\to y\to z$ 的权重始终是三项乘积。一般核版本先对事件指示函数验证“对复合测度积分”等于逐层核积分，再经非负简单函数及单调收敛定理公理库单调收敛定理Monotone convergence theorem非负可测函数单调递增时，积分极限等于极限函数积分。推广到非负可测函数。这里后一个核可随前一个输入变化，不能把它未经说明当作固定乘积测度；带符号积分还需额外可积性条件。

共享一次采样与重复采样不同 ​

掷一次公平币得 $b$，返回 $(b,b)$，只在 $(0,0),(1,1)$ 各放 $1/2$。掷两次独立公平币返回 $(b,c)$，四种结果各有 $1/4$。两者都能用 return 与 bind 写出，单子律不会把它们认成同一个计算；把随机值复制和把采样动作复制是两件事。

连续分布不能只用有限支撑 $D$。Giry 单子把可测空间 $X$ 送到其概率测度空间，后者取由评估映射 $\nu \mapsto \nu (A)$ 生成的 σ-代数；单位仍是 Dirac，乘法为

这套可测结构让混合分布与核组合成为合法映射，不能只说“所有分布组成一个集合”就略去可测性。[1]

允许不终止时，应换成次概率公理库次概率程序语义Subprobabilistic program semantics将概率程序解释为输入到终止输出的次概率核，用缺失质量记录不终止，并逐步计算顺序组合。版本，bind 继续传播缺失质量。条件化公理库概率程序中的条件化与评分Conditioning in probabilistic programs · Score semantics把 observe 看成筛选、score 看成加权，计算归一化常数并分别处理零证据、连续观测和不终止。中的归一化则不是总定义操作：零质量时无法执行，而且先局部归一化可能改变后续混合权重。因此“概率计算有单子结构”不等于“所有推断操作都可以随意交换”。