Grover 搜索的 Hoare 证明

已逐图核验教材 §6.6 书页 127–130（PDF 37–40 页），包括图 6.6–6.7 和公式 6.35–6.38。本页区分一般成功概率与教材为演示推理而采用的精确成功特例。

寄存器、规格与角度

搜索空间大小 $N=2^n$ ，有 $1\leq L\leq N/2$ 个解。令 $|\beta\rangle$ 、 $|\alpha\rangle$ 分别是解与非解的均匀叠加，定义 $\sin(\theta/2)=\sqrt{L/N}$ 。初态为

|u\rangle=\cos(\theta/2)|\alpha\rangle+\sin(\theta/2)|\beta\rangle.

每次 Grover 迭代在此二维空间旋转角 $\theta$ ，经过 $k$ 次后成功概率为

p_{\mathrm{succ}}=\sin^2((2k+1)\theta/2).

取最接近 $\pi/(2\theta)-1/2$ 的整数 $k$ ，则 $p_{\mathrm{succ}}\geq1-L/N$ 。教材书页 127 的角度定义印为 $\cos(\theta/2)=\sqrt{(N-L)/2}$ ，一般会超过 1；本页采用由归一化直接推得的分母 $N$ ，明确不照抄这个疑似排印错误。

成功断言 $P_{\mathrm{sol}}=\sum_{x\text{ 是解}}|x\rangle\langle x|$ 对辅助寄存器取恒等扩展。目标为 $\{p_{\mathrm{succ}}I\}\,\mathrm{Grover}\,\{P_{\mathrm{sol}}\}_t$ ，不是声称一般参数下成功概率为 1。

程序及循环体

循环 guard 为 $M_1=\sum_{l<k}|l\rangle\langle l|$ 、 $M_0=\sum_{l\geq k}|l\rangle\langle l|$ 。body $D$ 实现 oracle、扩散变换 $H^{\otimes n}(2|0\rangle\langle0|-I)H^{\otimes n}$ 以及 $r:=r+1$ 。在整数空间上，加一是双边移位酉算子。循环退出后在计算基测量搜索寄存器。

不变式与循环体证明

令 $|u_l\rangle=G^l|u\rangle$ ， $G$ 为 Grover 迭代，定义

P'=|u_k\rangle\langle u_k|\otimes|-\rangle\langle-|\otimes|k\rangle\langle k|, \quad Q=\sum_{l<k}|u_l\rangle\langle u_l|\otimes|-\rangle\langle-|\otimes|l\rangle\langle l|.

不同计数块正交，因此 $Q$ 是有界 effect。设 $R=M_0^\dagger P'M_0+M_1^\dagger QM_1$ ，由 $G|u_l\rangle=|u_{l+1}\rangle$ 和计数器移位得到 $D^\dagger RD=Q$ 。酉规则与顺序规则给出 $\{Q\}D\{R\}_t$ 。初始化后的态位于 $R$ 的值 1 子空间。

终止与一般排名函数

对实际初始化后的执行，计数器从 0 开始，每轮加一，恰好 $k$ 轮退出。若要应用对所有输入定义的 (R.LT)，不能把这一可达态事实直接代替全空间排名前提。

下面给出符合排名定义的构造，避免对无限计数支持直接取最大步数。令 $T=\llbracket D\rrbracket\circ\mathcal E_1$ 、 $A=M_1^\dagger QM_1$ 。对每个 $\epsilon>0$ 定义

t_\epsilon(\rho)=\min\{j\in\mathbb N:\ \mathrm{tr}(A T^m(\rho))<\epsilon\text{ 对所有 }m\geq j\}.

有限迹输入在整数基负无穷尾部的质量趋零，且每轮向右移动，故继续分支质量趋零，上述集合非空。移除第一步使排名不增；若当前质量至少为 $\epsilon$ ，则排名严格下降。结合 body 的完全正确性前提，可用 (R.LT) 推出 $\{R\}W\{P'\}_t$ 。这给出概率 1 终止，不声称所有任意输入有统一步数界。

成功概率和最终测量

最终计算基测量保持对角成功断言： $\sum_x M_x^\dagger P_{\mathrm{sol}}M_x=P_{\mathrm{sol}}$ 。初始化擦除原输入后，循环产生固定末态，其成功权重为 $p_{\mathrm{succ}}$ ；由迹语义和 wp 对偶，整体程序的 $\mathrm{wp}(P_{\mathrm{sol}})=p_{\mathrm{succ}}I$ ，得到目标三元组。

教材为了展示 qTD 推导，另外假定 $L=1$ 且 $k=\pi/(2\theta)-1/2$ 恰是整数，此时 $|u_k\rangle$ 是唯一解态， $P'\preceq P_{\mathrm{sol}}$ ，用后果规则即可完成概率 1 证明。这一附加整数条件不能推广成一般的精确成功定理。

来源和范围

Chapter 6 DOI，§6.6。本文使用正式 Hoare 规则组织证明；一般阈值排名构造替代原文计数支持表达式的边界问题，明确区分原文特例与一般概率结论。这里只证明理想 oracle 与门模型，未包括噪声、近似门或错误的 oracle 实现。