量子 Hoare 规则与循环证明

本页承接量子 while 语法与执行，并与量子霍尔逻辑及最弱前置条件的记号一致。采用有限维寄存器、未归一化执行分支和只收集终止路径的指称语义。设 $E=\llbracket S\rrbracket$ ，断言是 effect $0\preceq P\preceq I$ ， $A\preceq B$ 表示 $B-A$ 半正定。

断言与两种正确性

完全正确性和部分正确性分别要求对所有部分密度算子 $\rho$ ：

\models_{tot}\{P\}S\{Q\}\Longleftrightarrow \operatorname{tr}(P\rho)\le\operatorname{tr}(QE(\rho)),

\models_{par}\{P\}S\{Q\}\Longleftrightarrow \operatorname{tr}(P\rho)\le\operatorname{tr}(QE(\rho)) +\operatorname{tr}(\rho)-\operatorname{tr}(E(\rho)).

完全正确性只在前置 effect 所承诺的范围内提出终止义务；任意 $P$ 的 total triple 不能推出程序对所有输入全局终止。 $P=I$ 才会在归一化输入上强制终止， $P=0$ 则是平凡三元组。下文 $t,p$ 分别表示 total、partial；同一推导必须固定一种语义。

基本公理

\{P\}\ \mathbf{skip}\ \{P\}_*,\qquad \{U^\dagger P U\}\ \bar q:=U[\bar q]\ \{P\}_*.

初始化由 $\mathcal R_q(\rho)=\sum_iA_i\rho A_i^\dagger$ 定义，其中 $A_i=|0\rangle\langle i|_q\otimes I$ ，规则为

\left\{\sum_i A_i^\dagger P A_i\right\}\ q:=0\ \{P\}_*.

因此不能把断言矩阵中的符号 $q$ 机械替换成 0；对单 qubit 的 $P=|0\rangle\langle0|$ ，该前置条件为 $I$ 。

顺序组合与后果规则

\frac{\{P\}S_1\{R\}_*\quad\{R\}S_2\{Q\}_*} {\{P\}S_1;S_2\{Q\}_*}.

\frac{P\preceq P'\quad\{P'\}S\{Q'\}_*\quad Q'\preceq Q} {\{P\}S\{Q\}_*}.

方向来自迹不等式：减小左端前置 effect 或增大右端后置 effect 保持有效；经典集合蕴涵不能直接替代 Löwner 序。

测量 case 规则

若每个结果 $m$ 都满足 $\{P_m\}S_m\{Q\}_*$ ，且 $\sum_mM_m^\dagger M_m=I$ ，则

\left\{\sum_mM_m^\dagger P_mM_m\right\} \mathbf{if}\ (\square_m M=m\to S_m)\ \mathbf{fi}\ \{Q\}_*.

这是一次测量的分支合并，不是依次测试独立布尔条件；测量扰动由两侧的 $M_m$ 表示。与未操作寄存器纠缠的输入仍需在共同 Hilbert 空间中解释。

qPD：部分正确性的循环规则

令 $W=\mathbf{while}\ M=1\ \mathbf{do}\ S\ \mathbf{od}$ ，测量为 $\{M_0,M_1\}$ 。取 body 开始时的继续分支断言 $P$ 与退出后的后置断言 $Q$ ，令

R=M_0^\dagger QM_0+M_1^\dagger PM_1.

则 qPD 的循环规则为

\frac{\{P\}S\{R\}_p}{\{R\}W\{Q\}_p}.

$R$ 是测量前的断言， $P$ 只约束继续分支进入 body 的状态， $Q$ 约束退出状态；三者一般不同。该规则允许 body 或循环不终止，剩余质量由部分正确性的补偿项处理。它等价于主页量子霍尔逻辑中的 (R.LP)。

qPD 还包括 skip、初始化、unitary、顺序、case 和 Löwner 后果规则。教材 Theorem 6.1（印刷页117）证明 qPD 可靠；Theorem 6.2（印刷页120）证明相对完备，前提是复数域上的序事实和断言语言能够表达所需 wlp。相对完备不等于工具自动生成不变式。

qTD：完全正确性和 ranking function

不能仅把 qPD 循环规则的下标 $p$ 换成 $t$ ：永不终止的循环也可能满足 body 保持性。教材 Definition 6.10（印刷页121）规定，对 effect $A$ 和 $\epsilon>0$ ，函数

t_\epsilon:\mathcal D(\mathcal H_{all})\to\mathbb N

是 $(A,\epsilon)$ -ranking function，当且仅当对所有部分密度算子 $\rho$ 有

T(\rho)=\llbracket S\rrbracket(M_1\rho M_1^\dagger),\qquad t_\epsilon(T(\rho))\le t_\epsilon(\rho),

并且

\operatorname{tr}(A\rho)\ge\epsilon \Longrightarrow t_\epsilon(T(\rho))<t_\epsilon(\rho).

测量后的继续分支必须出现在 $T$ 中；不能直接用经典的 $t(\llbracket S\rrbracket(\rho))<t(\rho)$ 。自然数的良基性排除无限严格下降链。

沿用本页符号 $R=M_0^\dagger QM_0+M_1^\dagger PM_1$ ，教材的 (R.LT)（Figure 6.5，印刷页123）为

\frac{ \{P\}S\{R\}_t\quad \forall\epsilon>0,\ t_\epsilon\text{ 是 }(M_1^\dagger PM_1,\epsilon)\text{-ranking function} }{ \{R\}W\{Q\}_t}.

教材图使用 $P$ 表示循环最终断言、 $Q$ 表示 body 断言，恰好与本页字母交换，公式含义相同。ranking function 针对前置断言相关的质量，并不要求程序对所有输入全局终止；body 的 total triple 和每个正阈值 $\epsilon$ 的 ranking 义务都不能删去。

Lemma 6.6（印刷页122）给出等价的极限判据：对任意 ranking 相关 effect $A$ ，每个 $\epsilon>0$ 都存在 $(A,\epsilon)$ -ranking function 当且仅当

\lim_{n\to\infty}\operatorname{tr}\left(A(\llbracket S\rrbracket\circ E_1)^n(\rho)\right)=0, \qquad E_1(\rho)=M_1\rho M_1^\dagger,

对所有 $\rho$ 成立。应用于本页 (R.LT) 时实际代入 $A=M_1^\dagger PM_1$ ，其中 $P$ 是 body 前置断言。这里归零的是继续迭代中由 $A$ 看到的残余量，不是任意前置 effect 的全局“终止质量”。Theorem 6.3（印刷页124）和 Theorem 6.4（印刷页126）分别给出 qTD 可靠性与相对完备性。

最弱前置条件与不动点

令 $E^*$ 为迹伴随，则

\operatorname{wp}_S(Q)=E^*(Q),\qquad \operatorname{wlp}_S(Q)=E^*(Q)+I-E^*(I),

且 $P\preceq\operatorname{wp}_S(Q)$ 等价于 total triple， $P\preceq\operatorname{wlp}_S(Q)$ 等价于 partial triple。循环 wp 从零 effect 迭代

F_Q(X)=M_0^\dagger QM_0+M_1^\dagger\operatorname{wp}_S(X)M_1

得到 least fixed point；以 wlp 替换 body wp 并从 $I$ 向下逼近得到 greatest fixed point。详见最弱前置条件。

示例：测量循环复位 qubit

对计算基测量和 body $X$ ，取退出后置 $Q=|0\rangle\langle0|$ 、继续分支 body 前置 $P=|1\rangle\langle1|$ 。此时 $R=I$ ，且 $\{P\}X\{I\}_p$ 成立，所以 qPD 给出 $\{I\}W\{Q\}_p$ 。继续分支经 $X$ 后下一次测量必退出，循环几乎必然终止，故该具体三元组也满足 total correctness；这是实例的终止事实，不是 qPD 循环规则本身的结论。

参考与审计页码

本页规则与主量子霍尔逻辑页对齐，并核对 Foundations of Quantum Programming 第6章：qPD Figure 6.3 为 PDF页25/印刷页115；qPD soundness/completeness 为 PDF页27、30/印刷页117、120；ranking 定义6.10 为 PDF页31/印刷页121；极限 Lemma 6.6 为 PDF页32/印刷页122；qTD Figure 6.5 与 (R.LT) 为 PDF页33/印刷页123；qTD soundness/completeness 为 PDF页34、36/印刷页124、126。完整的 effect 定义、wp/wlp 结构式和辅助规则见主页。

Mingsheng Ying, Foundations of Quantum Programming, Chapter 6, 2024, DOI。
Mingsheng Ying, Floyd–Hoare Logic for Quantum Programs, 2011, DOI。