量子 Hoare 逻辑的辅助规则

本页依据 Chapter 6 §6.7，已核验书页 131–133（PDF 41–43 页）的图 6.9、6.10 和引理 6.8。三元组含义见Hoare 规则。所有断言均为 $0\preceq A\preceq I$ 的 effect；下文出现的局部算子隐含恒等扩展。

局部性与不变断言

程序只使用变量 $\operatorname{var}(S)$。对不相交集合 $V$ 上的断言 $C$，圆柱扩展是 $C\otimes I_{\operatorname{var}(S)}$。公理 (Ax.Inv) 给出 $\{C\}S\{C\}_p$；它只保证部分正确性，因为程序仍可能发散。

(R.TI) 在 $V\cap W=\varnothing$、$\operatorname{var}(S)\subseteq V$ 下，从 $\{A\otimes I_W\}S\{B\otimes I_W\}$ 推出 $\{A\}S\{B\}$。它对部分和完全正确性均有效，是移除未使用辅助空间的规则，不是忽略输入纠缠的许可。

凸组合与独立不变式

若每个 $\{A_i\}S\{B_i\}_*$ 成立，$p_i\geq0$ 且 $\sum_i p_i\leq1$，则 (R.CC) 给出

这里 $*$ 可统一取部分或完全正确性。凸组合保持 effect 的上下界，不能直接以非交换矩阵乘积充当逻辑合取。

(R.Inv) 进一步允许在 $\{A\}S\{B\}_*$ 两端加入独立空间上的同一个断言 $C$：

必要的独立性条件是 $C$ 的变量集合与程序变量不相交。

伴随变换和缩放

(R.SO) 对作用在程序未使用变量上的量子操作 $\mathcal E$，允许从 $\{A\}S\{B\}$ 推出 $\{\mathcal E^*(A)\}S\{\mathcal E^*(B)\}$。完全正确性允许一般量子操作；部分正确性还要求 $\mathcal E$ 保持迹。不能将此规则任意用于与程序操作相同寄存器的噪声。

(R.Lin) 给出 $\{\lambda A\}S\{\lambda B\}$，其中 $\lambda\geq0$ 且两端仍是 effect。它对完全正确性有效；部分正确性还要求 $\lambda\leq1$，因为不终止补偿项不能任意放大。

弱算子极限

若 $A_n\to A$、$B_n\to B$ 为弱算子收敛，即对所有向量 $\psi,\phi$ 有 $\langle\psi|A_n|\phi\rangle\to\langle\psi|A|\phi\rangle$，且所有 $\{A_n\}S\{B_n\}_*$ 有效，(R.Lim) 推出 $\{A\}S\{B\}_*$。必须保留断言的统一有界性，不能把任意发散矩阵级数代入。

用不终止界加强组合规则

对归一化输入，定义 $d_S(\rho)=1-\mathrm{tr}(\llbracket S\rrbracket(\rho))$。教材的 $\operatorname{Term}(C)$ 表示 $d_S(\rho)\leq\mathrm{tr}(C\rho)$，即不终止概率的上界；$\operatorname{Abort}(C)$ 表示 $\mathrm{tr}(C\rho)\leq d_S(\rho)$，即下界。名称中的 Term 并不意味着程序无条件终止。

在部分正确性下，若已有 $\{A_i\}S\{B_i\}_p$，则：

• (R.CC1)：$p_i\geq0$、$s=\sum_i p_i\leq1$ 且 $\operatorname{Abort}(C)$ 时，可取前置 $\sum_i p_iA_i+(1-s)C$、后置 $\sum_i p_iB_i$。
• (R.CC2)：$\lambda_i\geq0$、$s=\sum_i\lambda_i\geq1$ 且 $\operatorname{Term}(C)$ 时，可取前置 $\sum_i\lambda_iA_i-(s-1)C$、后置 $\sum_i\lambda_iB_i$；两者必须仍满足 effect 条件。

例如永不终止的程序有 $d_S=1$，所以 $\operatorname{Abort}(I)$ 成立；不能从其部分正确性推断任何输出真正产生。

来源

Mingsheng Ying，Foundations of Quantum Programming, 2nd edition，§6.7，书页 131–133，图 6.9–6.10、引理 6.8–6.9。Chapter 6 DOI。本页核验的是辅助规则，不能据此推断两章其余内容已全部验收。