量子 while 程序：语法与执行规则

本页采用有限维量子寄存器上的顺序语言，约定测量结果用于经典控制，不额外返回经典存储。它是 Chapter 5 所讨论语言的一个有限维表述；无限维整数变量需要另外说明算子与收敛条件。语法、初始化和一步规则对应定义 5.1–5.4、图 5.1；循环展开对应命题 5.2。

状态、寄存器与程序语法

寄存器 $q$ 对应 Hilbert 空间 $\mathcal H_q$ ；多个寄存器的空间取张量积。输入用部分密度算子表示： $\rho\succeq0$ 、 $\mathrm{tr}(\rho)\leq1$ 。迹记录该执行分支的概率质量，不在每次测量后重新归一化。一个有限维核心语言是

S ::= \mathbf{skip}\mid q:=0\mid \bar q:=U[\bar q]\mid S_1;S_2 \mid \mathbf{if}\ (\square_m\ M[\bar q]=m\to S_m)\ \mathbf{fi} \mid \mathbf{while}\ M[\bar q]=1\ \mathbf{do}\ S\ \mathbf{od}.

$U$ 是作用在列出的寄存器上的酉算子。case 使用一次测量 $\{M_m\}$ ，满足 $\sum_mM_m^\dagger M_m=I$ ；它不是逐个求值的一组布尔 guard，也不要求这些算子是互相正交的投影。while 使用二结果测量 $\{M_0,M_1\}$ ，0 表示退出，1 表示继续。所有局部算子隐含对其他寄存器的恒等扩展。

初始化并不是把任意量子态复制成零

$q:=0$ 丢弃寄存器 $q$ 原有信息并准备 $\lvert0\rangle$ 。在 $q$ 的正交基 $\{\lvert i\rangle\}$ 下定义 $A_i=\lvert0\rangle\langle i\rvert\otimes I_{\mathrm{rest}}$ ，则

\mathcal R_q(\rho)=\sum_i A_i\rho A_i^\dagger =\lvert0\rangle\langle0\rvert_q\otimes\mathrm{tr}_q(\rho).

最后一种写法采用 $q$ 在前的张量次序。初始化可能破坏原有纠缠，但保持其他寄存器的约化态；它是保持迹的完全正映射，通常不是酉操作。

一步操作语义

配置写为 $\langle S,\rho\rangle$ ，终止标记为 $\downarrow$ 。以下关系的每条测量分支都携带未归一化状态；分支权重已经包含在迹中，不再额外乘一次概率。

\langle\mathbf{skip},\rho\rangle\to\langle\downarrow,\rho\rangle, \qquad \langle q:=0,\rho\rangle\to\langle\downarrow,\mathcal R_q(\rho)\rangle.

\langle\bar q:=U[\bar q],\rho\rangle\to\langle\downarrow,U\rho U^\dagger\rangle.

顺序组合的两条提升规则是

\frac{\langle S_1,\rho\rangle\to\langle S_1',\rho'\rangle} {\langle S_1;S_2,\rho\rangle\to\langle S_1';S_2,\rho'\rangle},\qquad \frac{\langle S_1,\rho\rangle\to\langle\downarrow,\rho'\rangle} {\langle S_1;S_2,\rho\rangle\to\langle S_2,\rho'\rangle}.

第一条的 $S_1'$ 是剩余命令而非终止标记；这并不意味着该命令会发散。case 对每个结果 $m$ 有

\langle\mathbf{if}\ (\square_m M=m\to S_m)\ \mathbf{fi},\rho\rangle \to\langle S_m,M_m\rho M_m^\dagger\rangle.

令 $W$ 表示循环，则退出和继续规则分别为

\langle W,\rho\rangle\to\langle\downarrow,M_0\rho M_0^\dagger\rangle, \qquad \langle W,\rho\rangle\to\langle S;W,M_1\rho M_1^\dagger\rangle.

若不同路径到达相同终止配置，汇总时仍须按路径计重，不能用集合去重而丢失概率。

从执行树到指称映射

记 $\mathcal E_m(\rho)=M_m\rho M_m^\dagger$ 、 $\mathcal B=\llbracket S\rrbracket$ 。基本指称满足

\llbracket S_1;S_2\rrbracket=\llbracket S_2\rrbracket\circ\llbracket S_1\rrbracket, \qquad \llbracket\mathbf{if}\rrbracket=\sum_m\llbracket S_m\rrbracket\circ\mathcal E_m.

循环恰好完成 $n$ 次 body 后退出的贡献为 $\mathcal E_0\circ(\mathcal B\circ\mathcal E_1)^n$ ，故

\llbracket W\rrbracket(\rho)=\sum_{n=0}^{\infty} \mathcal E_0\big((\mathcal B\circ\mathcal E_1)^n(\rho)\big).

其有限部分和单调递增且迹不超过输入迹，因此在有限维中收敛。令 $F_0=0$ 、 $F_{k+1}=\mathcal E_0+F_k\circ\mathcal B\circ\mathcal E_1$ ，极限是方程 $F=\mathcal E_0+F\circ\mathcal B\circ\mathcal E_1$ 的最小解。零映射是永不终止程序的语义，不是“立即正常返回”。

对归一化输入， $\mathrm{tr}(\llbracket S\rrbracket(\rho))$ 是最终终止概率；缺失质量是发散概率，包括 body 自身可能发散的情形。概率 1 终止不意味着存在统一的有限步数上界。

例子：测量后翻转并再次检测

取计算基测量 $M_i=\lvert i\rangle\langle i\rvert$ ，body 为 $X$ 。结果 0 立即退出，结果 1 经 $X$ 变为零态，下一轮必退出。因此

\llbracket W\rrbracket(\rho)=M_0\rho M_0+M_0XM_1\rho M_1X^\dagger M_0 =\mathrm{tr}(\rho)\lvert0\rangle\langle0\rvert.

它对所有输入概率 1 终止。若把 body 改为 skip，输入 $\lvert1\rangle$ 永远不退出；其指称是零，而输入 $\lvert0\rangle$ 会立即退出。

教材中的无限维整数变量

类型定义见书页 64，初始化与操作规则见书页 67 的图 5.1。教材同时允许 Boolean 类型 $\mathcal H_2$ 和 integer 类型 $\mathcal H_\infty$ ；后者以 $\{\lvert n\rangle:n\in\mathbb Z\}$ 为计算基，可写为 $\ell^2(\mathbb Z)$ 。量子寄存器是有限个不同变量组成的序列，因此有限个寄存器也可能具有无限维状态空间。

整数变量初始化的原文规则是

\mathcal R_q(\rho)=\sum_{n=-\infty}^{\infty} (\lvert0\rangle_q\langle n\rvert\otimes I)\rho (\lvert n\rangle_q\langle0\rvert\otimes I).

这里输入是正的迹类算子。有限部分和是正算子且迹有界，可按迹范数解释其收敛；不能当作任意无界矩阵的形式级数。对偶断言是有界 effect，局部酉算子与测量算子也应在对应 Hilbert 空间中合法定义；无界位置或动量算子不能直接作为 effect 使用。有限维矩阵枚举与数值求特征值的方法不因此自动推广到无限维。

图 5.1 把配置定义为程序与部分密度算子的二元组，没有另设一般经典存储。本页使用同一约定。原文书页 68 的图 5.2 另给纯态概率转移：先归一化条件态，再在箭头标注概率；这与本页把概率吸收到部分密度算子中的表示不同，不能同时重复计权。初始化可能将全局纯纠缠态变为混合态，因此图 5.2 没有一般纯态初始化规则。

继续阅读与来源

指称语义介绍组合性；最弱前置条件把这些映射反向作用到断言；量子霍尔逻辑用于证明程序性质。

Mingsheng Ying，Foundations of Quantum Programming, 2nd edition，Chapter 5，2024。章节 DOI。相关公式见定义 5.1–5.6、图 5.1–5.2、命题 5.1–5.2（pp. 64–76）。经典递归、变量访问和局部块参见量子编程语言与指称语义。