概率程序的预期运行时间分析

### 概率程序的预期运行时间分析 #### 1. 引言 随机化算法在计算领域有着重要地位。1976 年，Michael Rabin 提出解决计算几何中最近点对问题的随机化算法，相比朴素的确定性暴力算法的二次时间复杂度，该算法的预期时间复杂度为线性。1977 年，Robert Solovay 和 Volker Strassen 提出随机素性测试算法，证明素性测试属于复杂度类 coRP。1992 年，Leonard Adleman 和 Ming - Deh Huang 进一步将素性测试的复杂度降低到 ZPP。将低效的确定性算法转化为预期更高效的随机化算法，是引入随机化计算的主要动机，像 Freivalds 的矩阵乘法验证和 Hoare 的随机选择枢轴的快速排序变体都是典型例子。 概率程序不仅局限于随机化算法，还是描述图形模型（如贝叶斯网络或马尔可夫随机场）的强大建模形式，推动了概率编程作为概率建模新范式的出现。概率编程语言的关键特性是将单个模型与分析算法（如贝叶斯推理技术）分离。在这种背景下，分析概率程序的预期运行时间，对于加速推理算法至关重要。 为了对概率程序的预期运行时间进行推理，我们引入了预期运行时间演算。它是一种类似于 Dijkstra 的最弱前置条件风格的演算，核心是预期运行时间变换器 ert。ert[c](t)(σ) 表示程序 c 从初始状态 σ 开始执行的预期运行时间，其中 t 是后运行时间，即在程序 c 终止后到达的最终状态中评估的预期运行时间。 #### 2. 概率程序 我们考虑用概率扩展的 Dijkstra 受保护命令语言（pGCL）编写的概率程序。pGCL 的语法规则如下： ```plaintext C −→ empty | x :≈μ | C; C | if (ϕ) {C} else {C} | {c1} □{c2} | while (ϕ) {C} ``` - **随机赋值**：pGCL 的关键特性是能够从离散概率分布 μ 中采样值并赋给变量 x，形式为 `x :≈μ`。例如，`heads :≈1/3 · ⟨true⟩+ 2/3 · ⟨false⟩` 模拟了一个有偏的硬币翻转。在我们的运行时模型中，每个随机赋值消耗一个时间单位。 - **控制流**： - **顺序组合**：`c1; c2` 先执行 `c1` 再执行 `c2`，组合操作本身不消耗时间。 - **条件选择**：`if (ϕ) {c1} else {c2}` 根据布尔表达式 `ϕ` 的值执行 `c1` 或 `c2`，条件评估消耗一个时间单位。 - **循环**：`while (ϕ) {c}` 只要 `ϕ` 为真就执行循环体 `c`，每次循环条件评估消耗一个时间单位。 - **非确定性**：`{c1} □{c2}` 表示在 `c1` 和 `c2` 之间进行非确定性选择，在我们的运行时模型中，非确定性选择本身不消耗额外时间。当推理 pGCL 程序的预期运行时间时，我们使用恶魔调度器来解决非确定性，即选择预期运行时间最长的执行路径。 以下是一个概率程序示例： ```plaintext h :≈0; t :≈30; while (h ≤t) { c :≈1/2 ·⟨true⟩+ 1/2 ·⟨false⟩; if (c = true) { h :≈h + uniform[0 . . . 10] } else {empty}; t :≈t + 1 } ``` 这个程序模拟了乌龟和兔子的赛跑，初始赋值需要两个时间单位，每次循环迭代消耗四到五个时间单位。 #### 3. 语义复杂性 在推理概率程序的预期运行时间时，会遇到一些微妙的现象。 - **终止条件过强**：对于普通程序，只要有一个发散的运行就会导致运行时间为无穷大。但概率程序可能有任意长甚至无穷的运行，但预期运行时间仍然有限。例如，程序 ```plaintext cgeo : b :≈1; while(b = 1){ b :≈1/2 ·⟨0⟩+ 1/2 ·⟨1⟩ } ``` 虽然有无限运行的可能，但它的运行时间是几何分布的，预期运行时间是有限的，平均在两次循环迭代后终止。因此，普通程序的终止概念对于概率程序来说太强了。 - **几乎必然终止条件过弱**：对于普通程序，终止意味着运行时间有限。但对于概率程序，即使是几乎必然终止的程序，预期运行时间也可能是无限的。例如，程序 ```plaintext crw : x :≈10; while (x > 0){ x :≈1/2 · ⟨x−1⟩+ 1/2 · ⟨x+1⟩ } ``` 虽然几乎必然终止，但平均需要无限多个步骤才能终止，预期运行时间是无限的。 - **正几乎必然终止不具有组合性**：对于普通程序，两个终止的程序顺序执行仍然会终止。但对于概率程序，考虑以下两个程序： ```plaintext c1 : x :≈1; b :≈1; c2 : while(x > 0){ while(b = 1){ x :≈x −1 b :≈1/2 ·⟨0⟩+ 1/2 ·⟨1⟩; } x :≈2x } ``` 两个程序本身正几乎必然终止，但组合后的程序 `c1; c2` 预期运行时间是无限的，尽管它几乎必然终止。 #### 4. 预期运行时间演算 我们引入一个健全且完整的演算来对概率程序的预期运行时间进行严格推理。核心概念包括程序状态和运行时间。程序状态 `σ` 是程序变量的赋值，运行时间是一个将每个程序状态 `σ` 映射到非负实数或无穷大的函数。 我们使用运行时间变换器 `ert[ · ]: pGCL →(T →T)` 来表示程序的预期运行时间。`ert[c](t)(σ)` 表示程序 c 从初始状态 σ 开始执行的预期运行时间，假设 `t` 捕获了程序 c 之后的计算运行时间。 以下是 `ert` 对不同 pGCL 语句的定义： | 语句 `c` | `ert [c] (t)` | | --- | --- | | `empty` | `t` | | `x :≈μ` | `1 + λσ • ∑v∈Val Pr[μ](σ)(v) · t[x/v](σ)` | | `c1; c2` | `ert[c1](ert[c2](t))` | | `if (ϕ) {c1} else {c2}` | `1 + [ϕ] · ert[c1](t) + [¬ϕ] · ert[c2](t)` | | `{c1} □{c2}` | `max {ert[c1](t), ert[c2](t)}` | | `while (ϕ) {c′}` | `lfp Ft`，其中 `Ft(X) = 1 + [ϕ] · ert[c′](X) + [¬ϕ] · t` | 例如，对于顺序组合 `c1; c2`，我们先确定 `c2` 相对于 `t` 的预期运行时间 `ert[c2](t)`，然后确定 `c1` 相对于 `ert[c2](t)` 的预期运行时间，即 `ert[c1; c2](t) = ert[c1](ert[c2](t))`。 下面是一个无循环程序的例子： ```plaintext c1 : x :≈1/2 · ⟨true⟩+ 1/2 · ⟨false⟩; c2 : if(x = true){ c3 : x :≈1/ ```