概率编程中的循环终止性与概率不变量

### 概率编程中的循环终止性与概率不变量 在概率编程领域，循环的终止性和概率不变量是两个重要的概念。下面我们将深入探讨这两个方面的内容。 #### 循环终止性中的确定性需求 在概率编程里，循环的终止情况并非总是确定的。以 `BadLoop` 为例： ```plaintext BadLoop ≜ kk := 1; while kk ≠ 0 do kk := 0 1/2kk ⊕ kk := kk + 1 end ``` 这个循环不能以概率 $\sum_{kk = 1}^{\infty}(1 - 1/2^kk)$（约为 0.29）终止。也就是说，它“很可能”终止（概率为 0.71），但并非几乎肯定会终止。其循环体包含一个不恰当的概率选择 `1/2kk ⊕`，对于任何 $\epsilon > 0$，都存在一种可能的执行情况，即当 `kk` 非常大时，`1/2^kk < ε`。因此，循环体不是确定的。考虑后置条件 `kk = 0`，循环体可以以任意小但非零的概率来满足这个条件。 `BadLoop` 满足除了循环体必须确定这一条件之外的所有定理 1 的前提条件。特别是，变体 `⟨kk ≠ 0⟩` 在每次迭代中都以非零（但不断减小）的概率减小。如果没有循环体必须确定这一限制，我们可能会错误地得出 `BadLoop` 几乎肯定会终止的结论。 即使使用恰当的选择，如果使用嵌套循环，也可能出现类似的情况。例如 `CountHeads` 程序： ```plaintext CountHeads ≜ xx := heads; nn := 0; while xx = heads do xx := heads 1/2⊕ xx := tails; nn := nn + 1 end ``` 它只包含恰当的选择（抛硬币的 `1/2⊕` 选择），但它不是确定的。我们有 `[[CountHeads]]⟨nn > N⟩ ≡ 1/2^N`，对于足够大的 `N`，这个值小于任何 $\Delta > 0$。 如果将 `CountHeads` 用于 `WorseLoop` 中： ```plaintext WorseLoop ≜ CountHeads; kk := 1; while nn ≤ kk do CountHeads; kk := kk + 1 end ``` 我们会看到与之前相同的效果：终止概率为 0.71，并且除了确定性之外，它满足定理 1 的所有前提条件。 要在 `WorseLoop` 的循环体中使用 `CountHeads`，根据 B 语言的规则，我们必须使用一个规范，最严格的规范可能类似于 `(@nn′ · nn′ ∈ N+ ⇒ nn := nn′)`。这个规范是确定的，但不满足条件 (B)：变体不能保证以非零概率减小，从而保证了正确性。 #### 概率广义替换语言（pGSL）基础 ##### 概率理论基础概念 在深入了解 pGSL 之前，我们先回顾一些基本的概率理论概念： - **实验**：任何观察或测量的过程。 - **结果**：实验得到的结果。 - **样本空间**：实验所有可能结果的集合。 - **事件**：样本空间的一个子集。 - **概率分布（离散）**：从样本空间到 `[0, 1]` 的归一化函数，给出每个结果的概率。 - **随机变量**：从样本空间到实数的任何函数。 - **特征函数**：事件的特征函数是一个随机变量，对于事件中的结果取值为 1，否则取值为 0。给定一个事件 `pre`（写成谓词形式），表达式 `⟨pre⟩` 就是该事件的特征函数。 - **期望值（离散）**：如果 `f` 是一个有界随机变量，`µ` 是一个离散分布，两者都基于样本空间 `S`，那么 `f` 相对于 `µ` 的期望值定义为 $\sum_{s \in S} f(s) * \mu(s)$。 从这些定义可以得出，特征函数在分布上的期望值等于该分布赋予其基础集合的概率。 ##### pGSL 简介 pGSL 是一种用于推理程序的逻辑，这些程序在一个计算模型中运行，该模型将初始状态转换为最终状态的分布（对于恶魔程序，则转换为最终分布的集合）。 pGSL 的一些替换规则总结如下表： | 替换形式 | 含义 | | --- | --- | | `[x := E ]exp` | 在 `exp` 中用 `E` 替换所有自由出现的 `x`，必要时重命名 `exp` 中的约束变量以避免捕获 `E` 中的自由变量 | | `[y, x := F, E ]exp` | 在 `exp` 中分别用 `F` 和 `E` 替换所有自由出现的 `y` 和 `x`，必要时重命名 `exp` 中的约束变量以避免捕获 `F` 和 `E` 中的自由变量 | | `[pre | prog ]exp` | `⟨pre⟩ × [prog ]exp`，其中 `0 × ∞ ≜ 0` | | `[prog1 [] prog2]exp` | `[prog1]exp min [prog2]exp` | | `[pre ⇒ prog ]exp` | `1 / ⟨pre⟩ × [prog ]exp`，其中 `∞ × 0 ≜ ∞` | | `[skip]exp` | `exp` | | `[prog1 p⊕ prog2]exp` | `p × [prog1]exp + (1 - p) × [prog2]exp` | | `[@y · pred ⇒ prog ]exp` | `(min y | pred · [prog ]exp)`，其中 `y` 不在 `exp` 中自由出现 | | `prog1 ⊑ prog2` | `[prog1]exp ⇛ [prog2]exp` 对于所有 `exp` | ##### pGSL 对标准 GSL 的扩展 在标准 GSL 中，我们通常处理的结论形式为 `pre ⇒ [prog ]post`，这意味着如果初始状态满足 `pre`，则最终状态保证满足 `post`。而在 pGSL 中，结论形式为 `preE ⇛ [prog ]postE`，表示最终状态下 `postE` 的期望值至少是初始状态下 `preE` 的期望值。 假设我们的前置和后置期望值是“标准的”，即它们的形式为 `⟨pre⟩` 和 `⟨post⟩`。那么，pGSL 的解释就变成了“最终状态下 `⟨post⟩` 的期望值至少是初始状态下 `⟨pre⟩` 的期望值”。根据基本概率理论，谓词的特征函数的期望值就是该谓词成立的概率，所以我们实际上是说“最终状态下 `post` 成立的概率至少是初始状态下 `pre` 成立的概率”。 对于标准程序，谓词要么成立（概率为 1），要么不成立（概率为 0）。对于 `x, y ∈ {0, 1}`，`x ≤ y` 意味着“如果 `x` 为 1，则 `y` 为 1”。因此，对于标准程序，pGSL 的解释与标准 GSL 的解释是一致的。 ##### pGSL 的一些