概率机器中的概率不变式：原理、应用与挑战

### 概率机器中的概率不变式：原理、应用与挑战 #### 1. 概率不变式的保证 为了理解概率不变式的保证，我们先回顾标准不变式。假设一台机器有初始化操作 `Init` 以及两个操作 `OpX` 和 `OpY`。若对于某个不变式 `I` 满足以下标准证明义务： - `true ⇒[Init]I` - `I ⇒[OpX]I` - `I ⇒[OpY]I` 那么对于从 `{OpX, OpY}` 中选取的任意（有限）操作序列 `Op?`，都有 `true ⇒[Init; Op?; Op?; ...; Op?]I` 成立。而且，操作序列是提前选择还是根据机器状态和已执行操作的输出“即时”选择并不影响结果。这体现了标准不变式技术的可靠性。 对于概率不变式技术，也有类似情况。若满足以下条件： - `E ⇛[Init]I` - `I ⇛[OpX]I` - `I ⇛[OpY]I` 则对于任意有限操作序列 `Op?; Op?; ...; Op?`，无论何时或如何选择，都有 `E ⇛[Init; Op?; Op?; ...; Op?]I` 成立。这里的 `E` 是某个“初始”表达式，可能依赖于机器的参数。 下面通过 `Counter` 机器来说明在概率情况下，操作选择的“时间/方式”至关重要。 ```plaintext MACHINE Counter SEES Int TYPE , Real TYPE VARIABLES count INVARIANT count ∈INT INITIALISATION count := 0 OPERATIONS cc ←−OpX
= PCHOICE frac ( 1 , 2 ) OF count := count + 1 ∥ cc := count OR count := count −1 ∥ cc := count END ; OpY
= count := 0 END ``` 对于提前选择的任意有限操作序列，`0 ⇛[Init; Op?; Op?; ...; Op?](count)` 显然成立，但该机器不满足概率证明义务，因为无法证明 `count ⇛[OpY](count)`。例如，对于程序片段： ```plaintext Prog = Init; c ←−OpX; IF c = 1 THEN OpY ELSE OpX END. ``` 执行该程序片段后，`count` 的期望值为 -0.5，不满足 `0 ⇛[Prog](count)`。所以，概率不变式在满足相应条件时能保证 `E ⇛[Init; Op?; Op?; ...; Op?]I` 成立。 #### 2. 图书馆系统的概率不变式 在图书馆系统中，由于新的 `EndLoan` 操作引入了概率选择替换，我们希望找到一个概率不变式来估计丢失书籍数量的上限。通过“非正式”推理，我们认为 `pp ∗loansEnded` 是实际丢失书籍数量的期望值，进而得出 `pp∗loansEnded−booksLost` 的期望值至少为 0。因此，我们定义 `V = pp ∗loansEnded −booksLost` 为概率图书馆机器的期望值不变式，其初始值为 0。 当我们声称 `V` 是该机器的期望值不变式时，意味着在图书馆操作运行期间多次检查 `V` 的值，其观测平均值至少为 0。由此可得出，对于该概率图书馆机器，丢失书籍的期望值（`booksLost` 的值）上限为 `pp∗loansEnded`。 #### 3. 证明义务 非概率机器的证明义务如下： | 编号 | 内容 | | ---- | ---- | | N1 | 初始化需要在机器上下文（集合和常量信息）下建立不变式：`[Init]I` | | N2 | 操作需要维护不变式：`I ⇒[Op]I` | 对于概率机器，同样的思想适用，但不变式现在可能取实数值而非布尔值。为证明实值不变式有下界，需要证明以下内容： | 编号 | 内容 | | ---- | ---- | | P1 | 初始化需要在机器上下文下建立概率不变式的下界：`e ⇛[Init]V` | | P2 | 操作不降低概率不变式的期望值，即操作后不变式的期望值至少等于操作前的期望值：`V ⇛[Op]V` | 对于每个实值不变式都要进行上述证明。标准（布尔）不变式的处理方式与之前相同（概率选择替换视为恶魔式），因此概率（期望）和布尔不变式的证明义务可以分别生成和证明。 #### 4. 证明义务的验证 这里我们仅讨论概率不变式 `V = pp ∗loansEnded −booksLost` 的维护证明。 对于初始化的证明义务（P1），我们要证明 `0 ⇛[Initialisation]V`。计算如下： ```plaintext [Initialisation]V ≡  booksInLibrary, loansStarted, loansEnded, booksLost := totalBooks, 0, 0, 0  V ≡  booksInLibrary, loansStarted, loansEnded, booksLost := totalBooks, 0, 0, 0   pp ∗loansEnded −booksLost  ≡ pp ∗0 −0 substitution ≡ 0 arithmetic ``` 这表明初始化建立了概率不变式的初始下界。 对于 `StartLoan` 操作，由于该操作确定性地增加 `loansStarted` 并减少 `booksInLibrary`，且期望值不变式不包含 `loansStarted` 和 `booksInLibrary`，所以可以轻松证明该操作维护了不变式。 对于 `EndLoan` 操作，要证明 `V ⇛[EndLoan]V`（证明义务 P2），计算过程如下： ```plaintext [EndLoan]V ≡     (booksLost := booksLost + 1 pp⊕ booksInLibrary := booksInLibrary + 1)   || loansEnded := loansEnded + 1   V ≡ parallel substitution with pp⊕     (booksLost := booksLost + 1 || loansEnded := loansEnded + 1)   pp⊕  (booksInLibrary := booksInLibrary + 1 || loansEnded := loansEnded + 1)      pp ∗loansEnded −booksLost  ≡ pp⊕ pp ∗   booksLost := booksLost + 1 || loansE ```