概率程序终止性分析：B方法中的关键技术与应用

# 概率程序终止性分析：B 方法中的关键技术与应用 ## 1. 恶魔收缩与零一律 ### 1.1 恶魔收缩的定义 在概率程序的分析中，恶魔收缩是一个重要概念。对于概率程序 `prog`，`[[prog ]]⟨post ⟩` 表示执行 `prog` 后建立后置条件 `post` 的最大保证概率。若 `prog` 是某个标准程序 `progd` 的细化，那么有 `[[progd ]]⟨post ⟩ ⇛ [[prog ]]⟨post ⟩`。由于标准程序应用于标准后置条件时，其结果取值仅在 `{0, 1}` 中，所以该式等价于 `[[progd ]]⟨post ⟩ ⇛ ⌊[[prog ]]⟨post ⟩⌋`，其中 `⌊·⌋` 是数学上的向下取整函数。 我们定义恶魔收缩 `⌊⌊prog ⌋⌋post` 为 `([[prog ]]⟨post ⟩ = 1)`，这里程序 `prog` 可以是概率程序，但 `⌊⌊prog ⌋⌋post` 是布尔值，因此是一个谓词。这样，若从满足前置条件 `pre` 的任何初始状态执行 `prog` 几乎肯定能建立 `post`，则可表示为 `pre ⇛ ⌊⌊prog ⌋⌋post`。 ### 1.2 零一律 恶魔收缩为零一律的表述提供了便利。零一律指出，如果一个循环终止的概率有下界且大于零，那么实际上这个概率就是 1。 设 `while G do prog end` 是一个循环，`I` 是其不变式，`δ` 严格大于零。若 `I ∧ G ⇛ ⌊⌊prog ⌋⌋I` 和 `δ × ⟨I⟩ ⇛ [[while G do prog end]]⟨true⟩` 都成立，那么 `I ⇛ ⌊⌊while G do prog end⌋⌋(I ∧ ¬G)`。这意味着如果 `I` 几乎肯定是不变式，且在 `I` 中任何地方循环终止的概率至少为某个正常数 `δ`，那么从满足不变式的任何初始状态开始，循环几乎肯定能同时建立不变式和否定后的循环条件。 ### 1.3 恶魔收缩的分配性 恶魔收缩具有与标准替换 `[·]` 相似的分配性。若 `0 < p < 1`，则 `⌊⌊prog1 p⊕ prog2⌋⌋post ≡ ⌊⌊prog1⌋⌋post ∧ ⌊⌊prog2⌋⌋post`。需要注意的是，对于 `while` 循环，没有关于 `⌊⌊·⌋⌋` 的分配规则。 ## 2. 几乎肯定终止的概率变体规则 ### 2.1 天使收缩与确定性 天使收缩是恶魔收缩的对偶概念，它表示“并非几乎肯定不成功”。对于概率程序 `prog`，若从满足前置条件 `pre` 的任何初始状态执行 `prog` 有“一定机会”建立后置条件 `post`，则 `⟨pre⟩ ⇛ ⌈[[prog ]]⟨post ⟩⌉`，其中 `⌈·⌉` 是数学上的向上取整函数。我们定义天使收缩 `⌈⌈prog ⌉⌉post` 为 `([[prog ]]⟨post ⟩ ≠ 0)`，这样可将上述条件简化为 `pre ⇛ ⌈⌈prog ⌉⌉post`。 此外，我们还需要更强形式的“一定机会”，即确定性。若存在正常数 `∆`，使得对于所有后置条件 `post`，当 `prog` 以非零概率建立 `post` 时，实际上建立 `post` 的概率至少为 `∆`，则称概率程序 `prog` 是“确定的”。若一个程序族中的所有程序都相对于同一个 `∆` 是确定的，则称该程序族是一致确定的。 ### 2.2 概率变体规则 为了建立零一律中的第二个前提条件，我们提出概率变体规则。对于循环 `while G do prog end`，若存在状态空间上的整数值表达式 `V` 满足以下条件： - `V` 有上下界：存在整数常量 `L` 和 `H`，使得 `I ∧ G ⇛ L ≤ V ≤ H`。 - `V` 有减小的机会：对于所有 `N`，`I ∧ G ∧ (V = N) ⇛ ⌈⌈prog ⌉⌉(V < N)`。 并且循环体 `prog` 是确定的，那么存在一个正数 `δ`，使得从满足 `I` 的任何状态开始，循环至少以该概率终止，即 `δ × ⟨I⟩ ⇛ [[while G do prog end]]⟨true⟩`。 ### 2.3 天使收缩的分配性 天使收缩的分配性与恶魔收缩类似，但有额外限制。若 `0 < p < 1`，则 `⌈⌈prog1 p⊕ prog2⌉⌉post ≡ ⌈⌈prog1⌉⌉post ∨ ⌈⌈prog2⌉⌉post`。若由满足谓词 `pred` 的 `xx` 值确定的程序族 `prog` 是一致确定的，则 `⌈⌈@xx · (pred =⇒ prog )⌉⌉post ≡ (∀xx · pred ⇒ ⌈⌈prog ⌉⌉post )`。同样，对于 `while` 循环，没有分配规则。 ## 3. 循环证明规则的重新组装 ### 3.1 循环几乎肯定正确性的证明规则 为了证明一个 `while` 循环（其循环体是确定的）的几乎肯定正确性，我们需要找到一个不变式和一个变体，并按以下步骤进行： - 确保变体有上界（以及下界）。 - 在证明“安全性”属性（如不变式的保持）时，使用 `⌊⌊·⌋⌋` 以恶魔方式解释概率选择。 - 在证明“活性”属性（如变体的减小）时，使用 `⌈⌈·⌉⌉` 以天使方式解释概率选择。 具体来说，对于循环 `while G do prog