经典控制的量子递归程序

语法、声明与适用范围

本页依据教材第 5.5 节（书页 82–90）。这里的递归由测量结果控制，是经典控制的递归量子程序，不是第 12 章的量子相干控制递归。先备知识见指称语义与量子编程语言。

定义 5.14–5.16 在 while 语言中加入过程标识符 $X$ 。程序模式可含调用；声明 $D=\{X_i\Leftarrow S_i\}_{i=1}^n$ 给出互不相同的过程名与过程体，每个过程体都可调用这些过程。完整程序由主语句 $S$ 和声明 $D$ 组成，允许直接递归与相互递归。本节正式处理无参数过程；经典参数和量子参数是后续扩展问题，不能默认为已经覆盖。

调用的操作语义

配置 $\langle S,\rho\rangle$ 中的 $\rho$ 是部分密度算子。图 5.6（p. 84）的 REC 规则为

\frac{X_i\Leftarrow S_i\in D}{\langle X_i,\rho\rangle\longrightarrow_D\langle S_i,\rho\rangle}.

调用一步展开为过程体，量子状态不变。“复制规则”复制的是程序语法，不是未知量子态。其余 while 规则继续使用，只把转移关系换成相对于声明的关系。

定义 5.19 将所有有限终止执行的输出相加得到 $\llbracket S\mid D\rrbracket(\rho)$ 。相同输出若来自不同执行路径，仍须按路径重数计入；无限执行没有终止输出。对归一化输入，输出的迹为终止概率，不能事先把各分支归一化。

while 循环作为递归

书页 85 将 while M[q]=1 do B od 表为声明

X\Leftarrow\mathbf{if}\ M[q]=0\to\mathbf{skip}\;\square\;1\to B;X\ \mathbf{fi}.

主语句取 $X$ ，其指称与原循环相同。测量的 0 分支终止，1 分支执行循环体后再次调用。这个例子说明递归包含循环，但一般相互递归不限于单个循环构造。

顺序执行仍满足 $\llbracket T_1;T_2\mid D\rrbracket=\llbracket T_2\mid D\rrbracket\circ\llbracket T_1\mid D\rrbracket$ ，不能颠倒复合顺序。

有限展开与上确界

定义 5.20、式 (5.16)（p. 85）对任意程序模式统一定义

S_D^{(0)}\equiv\mathbf{abort},\qquad S_D^{(k+1)}\equiv S[S_{1D}^{(k)}/X_1,\ldots,S_{nD}^{(k)}/X_n].

替换是同时替换；初始近似为不产生终止输出的 abort，而不是 skip。每个近似都不含过程调用，但可以保留原有 while 构造，所以“有限展开”不等于“每次运行必终止”。

命题 5.8（p. 86）给出

\llbracket S\mid D\rrbracket=\bigsqcup_{k\geq0}\llbracket S_D^{(k)}\rrbracket.

这里是递增语义链的上确界，不是把所有近似相加；相加会重复计算已经出现的终止路径。证明通过两向对应建立：每条有限终止执行出现在某个有限展开中，而有限展开的终止执行也对应原程序的执行。

最小不动点

令 $F_S$ 表示把过程名解释为量子操作后的程序模式语义，声明诱导

F_D(\mathcal E_1,\ldots,\mathcal E_n)= (F_{S_1}(\mathcal E_1,\ldots,\mathcal E_n),\ldots,F_{S_n}(\mathcal E_1,\ldots,\mathcal E_n)).

第 5.5.4 节使用量子操作域及逐分量的序；连续性保证从全零量子操作元组迭代得到最小不动点。定理 5.2（p. 88）为

\mu F_D=\bigsqcup_{k\geq0}F_D^k(\mathbf0),\qquad \llbracket S\mid D\rrbracket=F_S(\mu F_D).

最小性排除没有有限终止执行支持的额外输出。例如 $X\Leftarrow X$ 的方程形式上允许很多解，但从零开始的最小解始终为零，准确表示永不终止。最小不动点的存在不意味着程序几乎必然终止。

核验来源

教材第 5 章 §5.5：定义 5.14–5.21、图 5.6、命题 5.8、定理 5.2。已对照书页 84、85、86、88 的 PDF 图像核验 REC、同时替换、上确界与不动点公式；其余范围依据分页全文。本文是语义导览，不声称完整复现全章证明。