概率编程中的终止性分析与pGSL

# 概率编程中的终止性分析与pGSL ## 1. 抽象硬币翻转程序与证明义务调整 先来看一个抽象硬币翻转程序： ```plaintext xx, yy := heads, heads; while xx = yy do xx := heads ⊕ xx := tails; yy := heads ⊕ yy := tails end ``` 这里的二元运算符 `⊕` 是一种“抽象”的概率选择。只要实际使用的概率既不是 0 也不是 1，这个循环几乎肯定会终止，从而选出一个新的领导者。 在对 `while` 循环的证明义务进行调整时，有以下两个方面： - **调整终止参数**：变体必须有上下界。 - **解释 `⊕` 运算符**：在证明变体严格减少时，以“天使般”的方式解释 `⊕`，即只要求循环体有可能减少变体，而不是必须减少。对于其他用途，如证明不变式的保留，以“恶魔般”的方式解释 `⊕`。 ## 2. pGSL 中的全概率推理 ### 2.1 pGSL 简介 pGSL（概率广义替换语言）使用实值表达式而非布尔值表达式来描述程序行为，这些数字代表“期望值”。给定状态空间 `S`，设 `S` 上的谓词为 `PS`，期望为 `ES`。 考虑一个简单程序： ```plaintext xx := -yy 1/3 ⊕ xx := +yy ``` 对于最终状态上的任何谓词 `post` 和标准 GSL 替换 `prog`，谓词 `[prog]post` 作用于初始状态。如果 `prog` 是概率性的，`[prog]post` 在某个初始状态成立的概率可以通过 `[prog]⟨post⟩` 计算，其中 `⟨·⟩` 用于将谓词转换为期望，其值限制在单位区间内，`⟨false⟩` 为 0，`⟨true⟩` 为 1。 我们对 `[prog]` 进行推广，使用 `[[prog]]` 表示对期望的替换。有以下两个定义： - `[[xx := E]]exp ≡ “exp 中所有 xx 被 E 替换”` - `[[prog1 p⊕ prog2]]exp ≡ p × [[prog1]]exp + (1 - p) × [[prog2]]exp` 计算谓词“最终状态满足 `xx ≥ 0`”在给定初始状态成立的概率： ```plaintext [[xx := -yy 1/3 ⊕ xx := +yy]]⟨xx ≥ 0⟩ ≡ (1/3) × [[xx := -yy]]⟨xx ≥ 0⟩ + (2/3) × [[xx := +yy]]⟨xx ≥ 0⟩ ≡ (1/3)⟨-yy ≥ 0⟩ + (2/3)⟨+yy ≥ 0⟩ ≡ (1/3)⟨yy ≤ 0⟩ + (2/3)⟨yy ≥ 0⟩ ``` 根据 `yy` 的初始值不同，概率分别为： | `yy` 初始值 | 概率 | | ---- | ---- | | 负数 | 1/3 | | 零 | 1 | | 正数 | 2/3 | ### 2.2 pGSL 简明总结 pGSL 作用于“期望”而非谓词，期望取值在 `[0, 1] ∪ {∞}`。以下是 pGSL 中各种替换的定义： | 替换形式 | 定义 | | ---- | ---- | | `[[xx := E]]exp` | 将 `exp` 中所有自由出现的 `xx` 替换为 `E`，必要时重命名 `exp` 中的约束变量以避免捕获 `E` 中的自由变量。 | | `[[pre | prog]]exp` | `⟨pre⟩ × [[prog]]exp`，其中 `0 × ∞ ≡ 0`。 | | `[[prog1 2 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` | | `[[@xx · pred ==> prog]]exp` | `(min xx | pred · [[prog]]exp)`，其中 `xx` 不在 `exp` 中自由出现。 | | `prog1 ⊑ prog2` | `[[prog1]]exp ⇛ [[prog2]]exp` 对于所有 `exp` | ### 2.3 pGSL 习语 实际中对程序 `prog` 的分析通常会得出以下形式的结论： `p ≡ [[prog]]⟨post⟩` 可以有两种等价解释： 1. 最终状态的期望价值 `⟨post⟩` 在初始状态至少为 `p` 的值。 2. `prog` 建立 `post` 的概率至少为 `p`。 来看一个根竞争协议一轮的例子，计算硬币面不同的概率： ```plaintext [[ ```