第3章
量子程序的语法与语义
在2.3节中，我们使用底层的量子计算模型（即量子线路模型）来介绍量子算法。那么, 我们如何为量子计算机设计和实现高级量子编程语言呢？从本章起，我们将系统地介绍量子 编程的基础知识。
首先，让我们看看如何直接扩展经典的编程语言，使其能够为量子计算机编程。正如1.1 节和1.2节所述，该问题是量子编程早期研究中的主要关注点。本章对一类经典程序的简单 量子化扩展进行研究 —— 使用经典控制的量子程序，即程序处于数据叠加范式。121节 已经对这类量子程序的设计思路进行了简单介绍。本章将会对这类程序的控制流进行简要 讨论。
本章分为三部分：
- while语句是许多经典编程语言的“核心”。本章的第一部分介绍while语句的量子 化扩展，由3.1-3.3节构成。其中，3.1节定义量子while语句的语法，3.2节和3.3 节分别介绍它的操作语义和指称语义。
在这部分中，我们还简单地介绍了量子域理论，该理论是刻画量子while语句中循 环的指称语义所必需的。为了增强可读性，关于量子域的一些引理的冗长证明被推迟 到本章末尾的单独部分一3.6节。 - 第二部分是3.4节，这部分将通过增加（带经典控制的）递归量子程序来扩充量子 while语句。这部分还对递归量子程序的操作语义和指称语义进行了定义。此处同样 —需要使用量子域理论来处理指称语义。
- 第三部分是3.5节，这部分将通过一个例子来说明如何使用本章定义的编程语言来实现Grover量子搜索。
3.1 语法
本节中，我们将定义经典while语句的量子化扩展的语法。回想一下，经典的while程 序是由如下语法产生的：
其中S, Si, S2是程序，"是变量，t是表达式，b是一个布尔表达式。直观上而言，while程 序是按照如下顺序执行的：
- 语句skip除了使程序终止之外，并不完成其他任务。
- 赋值语句“u :=t”将表达式t的值赋给变量s
- 顺序组合“s1;s2”先执行S1，当s1终止之后再执行S2。
- 条件语句"if b then S1 else S2 fi"首先对布尔表达式b的值进行计算，当b为真时 执行s1,否则执行S2.我们可以将条件语句进一步扩展为case语句
或者简写为：
其中G1, G2,.... Gn是布尔表达式，通常称为卫式；s1, s2,…,Sn是程序。case语句 从计算卫式的值开始执行：如果卫式Gi为真，那么执行相应的子程序si。
- while循环“while b do S od”从计算循环卫式b的值开始执行：如果b为假，则循 环立刻终止；否则执行循环体S,当S终止之后会重复上述过程。
现在我们对while语句进行扩展，使其可应用于量子编程。我们首先确定量子while 语句的入门规范：
- qVar是量子变量的可数无限集。符号
,如,…将用作量子变量的元变量。 - 每个量子变量qc∈qVar都对应一个成类，这是一个希尔伯特空间，即由q表示的量子系统的态空间。为简单起见，我们只思考两种基本类型：
需要注意，经典计算中由Boolean和integer类型表示的集合恰好分别为珞和 徐的可计算基矢（参考例子2.1.1和2.1.2）O本章介绍的主要结论可以简单地扩展 到包含更多数据类型的情况。
量子寄存器是由不同量子变量组成的有限序列（量子寄存器的概念在2.2节已经介绍过了，这里只是简单地将其扩展，使它可以包含其他量子变量，而不仅是量子比特变量）。量子寄存器
,如的希尔伯特态空间是q中的量子变量的态空间的张量积：
在必要的时候，我们用
来表示
是量子变量qi的态，即
因此
表示qi的态|ψi和|ϕi的外积，且 
是Hq中的态，其中对于任意的1<=i<=n
都满足qi处于
态。
通过上述讨论，我们可以通过量子 while 语句来对程序进行定义：
定义 3.1.1 量子程序是通过如下语法产生的：
我们需要对这个定义进行详细解释：
- 与经典 while 语句类似，语句 skip 除了使程序终止之外，并不执行其他任务。
- 初始化语句“q := |0i”将量子变量 q 设为基态 |0i。对于任意的纯态 |ψi ∈ Hq，显然
存在一个属于 Hq 的幺正算子 U 使得 |ψi = U|0i 成立。所以，可以按照这种初始化
方式及幺正变换 q := [q] 来制备处于 |ψi 态的系统 q。
- 语句“q := U[q]”意味着在量子寄存器 q 上执行幺正变换 U，而不属于 q 的量子变量
的态保持不变。 - 顺序组合与它在经典编程语言中的副本的含义相同。
- 程序结构
是对经典 case 语句（式 (3.1)）的量子化扩展。回想一下，在执行语句 (3.1) 时，第一
步是检查哪个卫式 Gi 满足条件。但是根据量子力学第三基本假设（参考 2.1.4 节），
想要从量子系统获取信息就必须对其进行测量。所以在执行语句 (3.3) 时，将会对量
子寄存器 
执行量子测量：
接着会根据测量结果选择合适的子程序 Sm 执行。基于测量的 case 语句 (3.3) 和经
典 case 语句有一点重要的不同：前者程序变量的态在测量之后会发生变化，而后者
却不会变化。
- 语句
是经典循环“while b do S od”的量子化扩展。为了获取关于量子寄存器 q 的信息，
要对其执行测量 M。测量 M = {M0, M1} 是 yes-no 测量，它只有两种可能的测量结
果：0（no）和 1（yes）。如果观测到的测量结果为 0，那么程序终止；如果结果为 1，
那么会执行子程序 S 并继续。量子循环 (3.4) 和经典循环的唯一区别在于，经典循环
在检查循环卫式 b 时不会改变程序变量的状态，但在量子循环中却并非如此。
经典控制流
现在是时候解释为什么本章开始说通过量子 while 语句编写的程序的控制流是经典的。
回想一下，程序的控制流就是它执行的顺序。在量子 while 语句中只有两类语句（case 语
句 (3.3) 和循环 (3.4)），它们的执行是通过从两条或更多条路径中进行选择来决定的。case 语
句 (3.3) 根据测量 M 的结果选择其中一条命令去执行：如果测量结果是 mi，那么会执行相应的命令 Smi。既然量子测量的结果是经典信息，那么语句 (3.3) 中的控制流就是经典的。
可以通过相同的方式论证循环 (3.4) 的控制流也是经典的。
正如1.2.2 节所指出的那样，也可以定义带量子控制流的程序。程序的量子控制流很难
理解，它是第6章和第7章的主题。
量子变量
在本节结束之前，我们将介绍如下技术性定义，该定义在接下来的论述中会用到。
3.2 操作语义
上一节中定义了量子while程序的语义。这节将对量子 while 语句的操作语义进行定
义。我们先介绍几个符号：
- ρ是希尔伯特空间H中的正定算子，如果tr(ρ) <= 1，那么我们称它为局部密度算子。所以，如果密度算子ρ（参考定义 2.1.21）满足tr(ρ)=1，那么它是局部密度算子。我们将H中局部密度算子的集合记为 D(H )。在量子编程理论中，因为包含循环（或者更一般地，递归）的程序可能以确定的概率不会终止，并且其输出一定是局部密度算子而不一定是密度算子，所以局部密度算子是一个非常有用的概念。
- 我们将所有量子变量的希尔伯特态空间的张量积记为 Hall：
- 令
=q1, · · · , qn是一个量子寄存器。
的态空间H
中的算子A的柱面扩张为A⊗I∈Hall，其中I是不属于寄存器
中的量子变量的希尔伯特态空间
中的单位算子。下文中我们将其柱面扩张简记为 A，且它可以通过上下文进行分辨，不会有产生混淆的风险。
- 我们用符号 E 表示空程序，即终止。
与经典编程理论相似，可以从配置之间转换的角度对量子程序的执行进行合理的描述。
量子配置之间的转换
意味着态为ρ的量子程序S执行一步后，量子变量的态会变为 ρ'，S'是程序S的剩余部分并会继续执行。特别地，如果S' = E，那么程序S会在态ρ'终止。
我们应当将先前定义的操作语义（也就是关系 →）理解为满足图 3.1 中规则的量子配置之间的最小转换关系。显然，转换规则 (IN)、(UT)、(IF)、(L0) 和 (L1) 是由量子力学的基本假设决定的。正如第 2 章所述，概率性是由量子计算中的测量引起的。但应当注意到量子程序的操作语义是一类普通的转换关系 →，而不是概率性转换关系。以下备注可以帮助读者更好地理解这些转换规则：
- 规则 (UT) 的目标配置中的符号 U 实际代表 U 在 Hall 中的柱面扩张。适用于测量和循环的规则 (IF)、(L0) 和 (L1) 也都是如此。
- 在规则 (IF) 中，观测到结果为 m 的概率为:
并且在这种情况下，测量之后系统的态变为
所以，规则 (IF) 的一个本质的描述就是概率性转换：
但是，如果我们将概率 pm 和密度算子 ρm 编码为局部密度算子
那么就可以将这个规则表述为一种普通的（非概率性）转换。
- 同样，在规则 (L0) 和 (L1) 中测量得到 0 和 1 的概率分别为：
当测量结果为0时系统的态会从ρ变为M0ρM†0/p0，当测量结果为1时系统的态会从ρ变为M1ρM†1/p1。将概率和测量之后的态编码为局部密度算子，就可以用普通的转换来代替概率性转换对规则 (L0) 和 (L1) 进行描述。
从上述讨论中我们发现，概率和测量之后的态进行合并的惯例使得我们能够将操作语义 → 定义为非概率性转换关系。
纯态的转换规则
图 3.1 中的转换规则是通过密度算子的语言进行描述的。正如下一节所述，这类一般性的设置为我们提供了一种指称语义的优雅的形式化描述。但是在应用中使用纯态通常会更加方便。所以我们在图 3.2 中描述了这些转换规则的纯态变体。在纯态转换规则中，配置可以用二元组
表示，其中S是量子程序或者空程序E，|ψi是 Hall 中的纯态。正如上文所述，图 3.1 中的转换都是非概率性的。但是规则 (IF0)、(L00) 和 (L10) 中的转换则是概率性的，它们都具有如下形式：
当概率 p = 1 时，可以将这种转换缩写为
当然，图3.2中的规则是图3.1中所对应的规则的特殊情况。反过来说，通过密度算子和纯态的系综之间的等价性，图3.1中的规则可以从图3.2中对应的规则推导得到。
读者可能已经注意到图 3.2 中并没有初始化规则 (IN) 的纯态版本。实际上，规则 (IN)没有纯态版本是因为初始化操作可能会将纯态转换为混合态：虽然初始化操作 q := |0i 将局部变量 q 的状态变为纯态 |0i，但它对其他变量的副作用可能会导致所有变量 qVar 的总体态 |ψi ∈ Hall 变为混态。为了更清晰地理解规则 (IN)，我们以 type(q) =integer 的情况为例进行讨论。
例子 3.2.1
(1) 我们首先思考这类情况：ρ 是纯态，即存在
使得
成立。我们将 |ψ> 写成如下形式：
其中所有的 |ψk> 都是积态：
显然，虽然ρ是纯态，但ρq0却不一定是纯态。
(2) 总体来说，假设ρ是通过纯态的系综{(pi
, |ψii)} 产生的，也就是说
对于任意的i，我们记ρi = |ψiihψi|，并假设在初始化之后它会变为ρqi0。通过上述讨论，我们可以将ρqi0 写成如下形式：
程序的计算
现在可以从量子程序计算的转换的角度对它的概念进行自然而然的定义。
为了阐述这个定义，让我们看一个简单的例子：
例子 3.2.2
假设 type(q1) = Boolean，type(q2) = integer，思考如下程序：
其中：
那么从 ρ 开始的 S 的计算为：
其中：
所以S可以从ρ发散。注意S2也有转换
但当目标配置的局部密度算子是零算子时，我们通常舍弃这种转换。
不确定性
本节最后我们看看经典 while 程序和量子 while 程序的操作语义之间一个有趣的差异。经典的 while 程序是一类典型的确定性程序，它会在给定的态下开始精确的计算。（这里，如果不仅包含条件语句“if· · · then · · · else”，而且包含 case 语句 (3.1)，那么假设卫式G1, G2, · · · , Gn 不会同时成立。）但是，这个例子表明，因为语句if(¤m · M[q] = m → Sm)fi和 while M[q] = 1 do S od 中的测量会导致概率性的产生，所以量子 while 程序便不再具有确定性了。本质上而言，定义 3.2.2 中给出的量子程序的操作语义 → 是一种概率性转换关系。但是，在将概率性编码为局部密度算子之后，概率性体现为转换规则 (IF)(L0)和 (L2)中的不确定性。因此，我们应当将语义 → 理解为不确定性转换关系。
3.3 指称语义
我们在上一节中定义了量子程序的操作语义。指称语义可以基于操作语义进行定义，或者更确切地说，是基于定义 3.2.3 中的计算概念进行定义的。量子程序的指称语义是一类语义函数，它可以将局部密度算子映射到它本身。直观上而言，对于任意的量子程序 S，S 的语义函数对 S 的所有可终止性计算的计算结果进行求和。
如果可以从
通过n次转换关系 → 到达配置
意味着存在配置
,
满足
那么我们记
此外，将 → 的自反传递闭包记为 →∗，即
当且仅当存在某个n>=0 使得 
成立。
公式 (3.7) 中使用多重集而不是传统集合的原因在于通过不同的计算路径可能会得到相同的局部密度算子，这与我们在上一节的规则 (IF)、(L0) 和(L1) 中看到的类似。接下来这个简单的例子更确切地对这种情况进行了说明。
例子 3.3.1 假设 type(q) = Boolean。思考程序：
其中：
那么从态ρ开始的S的计算为：
所以，我们有：
3.3.1 语义函数的基本属性
与经典编程理论相似，操作语义可以方便地描述量子程序的执行。另一方面，指称语义适用于研究量子程序的数学属性。现在我们建立几条语义函数的基本属性，这对于推导量子程序非常有用。
首先，我们观察到任意量子程序的语义函数都是线性的。
证明：可以通过对 S 的结构使用归纳法来证明如下事实：
于是引理 3.3.1 成立。
其次，我们为量子程序（除了 while 循环）的语义函数提出一种结构化表示。量子循环的语义函数的这种表示需要一些格理论中的数学工具。所以，我们先在下一节中对必要的数学工具进行介绍，再在 3.3.3 节对其进行描述。
证明：(1)、(2) 和 (3) 显然成立。
(4) 通过引理 3.3.1 和规则 (SC)，我们得出:
(5) 可以从规则 (IF) 中得到。
3.3.2 量子域
在提出量子 while 循环的语义函数的表示之前，我们首先做一些铺垫。在这一小节中，
我们将对局部密度算子和量子操作的域进行考察。本小节介绍的概念和引理在3.4节和第7章中也会用到。
基本格理论
我们首先回顾一下格理论的基本概念。
当X是序列
时，通常将
记为
或者
。
在编程理论中，接下来的定理被广泛地应用于对循环和递归程序的语义进行描述。
练习 3.3.2 证明定理 3.3.1。
局部密度算子的域
我们现在思考在量子while循环的表示中所需的量子对象的格理论结构。事实上，我们需要对两种等级的量子对象进行处理。低等级的是局部密度算子。令 H 为任意的希尔伯特空间。定义2.1.13已经对局部密度算子的集合D(H)中的偏序进行了介绍。回想一下L¨owner序是这样定义的：对于任意的算子A,B∈L(H), 如果B−A是正定算子，那么A
B成立。接下来的引理对具有L¨owner序
的D(H)的格理论属性进行了说明：
量子操作的域
我们进一步思考量子操作（参考定义 2.1.25）的格理论结构。
引理3.3.2、3.3.3和3.3.4的证明过程非常复杂。为了便于阅读，我们将这些证明放在3.6节中。
3.3.3 循环的语义函数
现在我们已经准备好说明量子 while 循环的语义函数可以通过它的有限语法逼近的语义函数的极限来表示。为此，我们需要一个辅助的符号 ——abort表示量子程序，满足：
对于任意的ρ∈D(H)都成立。直观上而言，程序abort并不保证一定会终止。例如，可以选取
其中q是量子变量，
是态空间Hq中的平凡测量。我们将程序abort作为归纳定义量子循环的语法逼近时的归纳基。
可以将量子 while 循环的语义函数表示为：
证明： 对于i=0,1，我们引入辅助的算子
将其定义为对于所有的ρ∈D(H)，都有Ei(ρ)=MiρM†i 。
首先我们通过对k使用归纳法来证明：对于所有的k>=1，都有
上述等式中的符号◦表示量子操作的组合，即量子操作E和F的组合F◦E定义为对于任意的ρ∈D(H)都有(F◦E)(ρ)=F(E(ρ))。k=1的情况显然成立。那么通过命题 3.3.1的 (1)、(4) 和 (5) 以及 k−1 时的归纳假设，我们可以得到：
其次，我们有：
所以，可以证明对于任意的 k >= 1 都有
有了上述论述，通过对 k 使用归纳法不难证明这个等式成立。
可以从上述命题中推导出量子循环的语义函数的不动点特性描述。
证明： 从命题 3.3.2 和式 (3.9) 可以直接得出。
3.3.4 量子变量的改变与访问
理解程序行为的核心问题是观察程序变量的状态是如何改变的，以及在程序的执行过程中如何访问程序变量。作为刚刚研究的语义函数的第一个应用，我们现在来解决量子程序中的这个问题。
为了简化表述，我们引入一个缩写。令X⊆qVar是一个量子变量的集合。对于任意算子A∈L(Hall)，我们记：
其中tr⊗q∈X Hq 是系统Nq∈X Hq上的偏迹（参考定义 2.1.22）。那么我们有：
回想定义2.1.22，当所有量子变量的总体态是 ρ 时，trX(ρ) 描述了不属于 X 中的量子变量的态。所以，可以将上述命题直观地解释为：
- 命题 3.3.3(1) 表明不属于 qvar(S) 的量子变量的态在程序 S 执行之后与 S 执行之前是相同的。这意味着程序 S 只能改变属于 qvar(S) 的量子变量的态。
- 命题 3.3.3(2) 表明如果qvar(S)中的量子变量的两个输入态 ρ1 和 ρ2 是相同的，那么分别从 ρ1和ρ2开始的程序S的计算结果也相同。换言之，如果程序S以ρ1为输入和以ρ2为输入的输出结果不同，那么当我们只考虑 ρ1 和 ρ2 在 qvar(S) 中时，ρ1和 ρ2 就一定不相同。这意味着程序 S 至多只能访问 qvar(S) 中的量子变量。
练习 3.3.3 证明命题 3.3.3（提示：使用在命题 3.3.1 和 3.3.2 中介绍的语义函数表
80 示法）。
3.3.5 终止和发散的概率
程序行为的另一个核心问题是它的可终止性。关于量子程序的这个问题的第一个考虑
是基于如下命题的，该命题表明语义函数不会增加量子变量的局部密度算子的迹。
证明： 我们通过对 S 的结构使用归纳法来证明。
对于所有的n>0 都成立。这个证明可以通过对n使用归纳法来完成。n=0的情况显然成立。通过对n的递归假设和S’，我们有：
直观上而言，tr([[S]](ρ)) 是程序S从态 ρ 开始执行的终止概率。从上述命题的证明过程中，我们可以发现能够导致 tr([[S]](ρ)) 6 tr(ρ) 的程序结构只有程序S中的循环。因此，
是程序S从输入态ρ发散的概率。这条结论可以通过下面这个例子进一步说明。
例子 3.3.2 令 type(q) = integer，且令
那么M={M0, M1} 是希尔伯特态空间中的 yes-no测量（注意 M 不是投影测量）。思考程序：
那么经过一系列计算，我们有：
第 5 章会更为系统地对量子程序的终止进行研究。
3.3.6 作为量子操作的语义函数
本节的最后，我们将建立量子程序和量子操作（参考 2.1.7节）之间的关联。
可以将量子程序的语义函数定义为从Hall中的局部密度算子到它本身的一种映射关系。令V是qVar的一个子集。当Hall中的量子操作E是HV =Nq∈VHq中的量子操作F的柱面扩展时，即
其中I是HqVarV中的单位量子操作，我们通常将E和F视为等价的，并且可以将E视作HV中的量子操作。通过这些约定，我们有：
证明： 可以通过对S的结构使用归纳法来证明这个命题。对于S 不是循环的情况，可以通过定理2.1.1(3)和命题3.3.1来证明该命题。对于S是循环的情况，可以通过命题3.3.2和引理3.3.4来证明该命题。
反过来可能有人会问：所有的量子操作都可以通过量子程序来建模吗？为了回答这个问题，我们首先需要对局部量子变量的概念进行介绍。
块状命令 (3.10) 的直观含义是程序S在以q为局部变量且局部变量都在S中进行初始化的环境中执行。程序S执行之后，会舍弃由局部变量q表示的辅助系统。这就是块状命令的语义的定义式 (3.11) 中对 Hq 求迹的原因。注意式 (3.11) 是 Hqvar(S)q 中的一个局部密度算子。
可以将块状命令视为一个后续的量子程序。那么我们可以对前面提出的问题给予正面答复。接下来的命题本质上是从量子程序的角度对定理 2.1.1(2) 进行重述。
证明： 通过定理 2.1.1(2)，可以发现，存在：
这样很容易验证
。
3.4 量子编程中的经典递归
递归概念的出现使得我们在编程的过程中不需要做大量重复性工作。在前几节中，我们已经研究了while 语句的量子化扩展，它可以通过一类被称为量子while循环的程序结构去实现量子计算中的一类特殊递归 —— 迭代。经典编程中广泛使用了递归过程的一般形式。这是一个比递归更强有力的工具，通过使用递归，可以直接或间接地从函数本身的角度对函数进行定义。在本节中，我们将递归的一般性概念添加到量子 while 语句中，使得量子计算中的程序可以调用它本身。
因为本节中所思考的递归中的控制流是经典的（或者更精确地说，控制是由量子测量的结果决定的），所以应该将它合理地称为量子编程中的经典递归。带量子控制流的递归的概念将会在第 7 章中介绍。为了避免混淆，我们将包含带经典控制的递归的量子程序称为递归量子程序，而将包含带量子控制的递归的量子程序称为量子递归程序。利用 3.3.2 节介绍的数学工具，本节介绍的递归量子程序理论或多或少是对经典递归程序理论的直接扩展。然而，正如读者将在第 7 章看到的那样，对量子递归程序进行处理会更加困难，它需要的一些思想与本节所使用的截然不同。
3.4.1 语法
我们首先定义递归量子程序的语法。通过在量子while程序的入门规范中增加一个由X, X1, X2, · · · 组成的过程标识符的集合，就能够得到递归量子程序的入门规范。
我们将量子程序模式定义为可能包含过程标识符的一般性的量子 while 程序。形式化地，我们有：
语法 (3.2) 和语法 (3.12) 的唯一不同之处在于后者增加了过程标识符 X 的子句。如果一个程序模式 S 至多包含过程标识符 X1, · · · , Xn，那么我们记：
与经典编程相似，我们通常将量子程序模式中的过程标识符用作子程序，并称其为过程
调用。它们由按照如下方式定义的声明所指定：
3.4.2 操作语义
递归量子程序是量子程序模式加上其中的过程标识符的声明。所以，我们首先定义关于给定声明的量子程序模式的操作语义。为此，需要对 3.2 节定义的配置的概念进行扩展。
除了S不仅可以是程序还可以是程序模式以外，该定义与定义 3.2.1 是相同的。
现在可以将定义 3.2.2 中给出的量子程序的操作语义简单地扩展为量子程序模式的
情况。
当然，在这个定义中，会对图 3.1 中的规则按照如下方式进行扩展：允许程序模式出现在配置中，并将转换符号 → 替换为 →D。与经典编程相似，图 3.3 的规则（REC）也被称为拷贝规则，它表明在程序运行时，可以将对程序的调用过程视作将被调用的程序体插入调用产生的地方。
3.4.3 指称语义
基于上一小节描述的操作语义，通过定义3.2.3和3.3.1 的直接扩展很容易得到量子程序模式的指称语义。
假设递归量子程序由主语句 S 和声明 D 构成。那么可以将它的指称语义定义为 [[S|D]]。
显然，如果 S 是一个程序（即不包含任何过程标识符的程序模式），那么 [[S|D]] 并不依赖于D 且它与定义 3.3.1 是一致的，因此我们可以将 [[S|D]] 简单地记作 [[S]]。
在对一般性递归程序的各种特性进行研究之前，让我们看看如何将前面几小节中讨论的量子 while 循环视作一类特殊的递归量子程序。我们思考如下循环：
这里 S 是量子程序（不包含任何的过程标识符）。令 X 是通过 D 进行声明的过程标识符：
那么量子循环 while 实际上与以 X 作为它的主语句的递归量子程序是相同的。
练习 3.4.1 证明 [[while]] = [[X|D]]。
递归量子程序的语义函数的基本性质
我们现在建立一些递归量子程序的语义函数的基本性质。下面这条命题是在关于声明
的量子程序模式的情况下对命题 3.3.1 和 3.3.2 的推广。
证明： 与命题3.3.1和3.3.2的证明过程相似。
可以进一步扩展命题 3.4.1(5)，使得递归量子程序的指称语义可以从它的语法逼近的角度进行表示。
应当注意到上述定义是通过对 k 使用归纳法给定的，其中 S 是任意一个量子程序模式。因此，假设在 k 的归纳假设中已经对式 (3.14) 中的S(k)1D , · · · , S(k)nD 进行了定义。显然对于所有的 k > 0，S(k)D 是一个程序（不包含任何过程标识符）。下面这条引理阐明了用于定义程序语义的声明及其替换之间的关系。
证明：
(1) 可以通过对 S 的结构使用归纳法，再结合命题 3.4.1 来证明。
(2) 通过 (1) 可以得出
基于上述引理，我们可以通过递归程序的语法逼近得到其语义函数的表示。
我们能够证明对于任意的整数 r, k > 0，如下声明成立：
上述内容可以通过对 r 和 k 使用归纳法以及使用转换规则的推论的深度来证明。
练习 3.4.2 完成对命题 3.4.2 的证明。
3.4.4 不动点特性
命题 3.4.2 可以被视作通过命题 3.4.1(5) 对命题 3.3.2 进行的推广。3.3.3 节中将量子while 循环的不动点特性作为命题 3.3.2 的推论给出。在本节中，我们将给出递归量子程序的不动点特性，并因此得出推论 3.3.1 的一般形式。在经典编程理论中，递归方程是在函数的一个确定的域中进行求解的。这里，我们将在 3.3.2 节中定义的量子操作的域中求解递归量子方程。为此，我们首先介绍如下内容。
我们认为语义泛函 [[S]] 是定义明确的。从命题3.3.6可以推导出程序 Ti 总是存在。另一方面，如果
是另一个满足对于任意的程序0i都有[[T0i]] =Ei 成立的声明，那么我们可以证明：
现在我们定义一个域，希望在该域中找到通过过程标识符X1;...;Xn 的声明定义的语义泛函的不动点。让我们思考笛卡儿幂
中的序
可以自然而言地通过
中的序
推导得到：对于任意的
，
-
, 对于任意的1<=i<=n，都有
。
从引理3.3.4 可以得出(QO(Hall)n;v) 是CPO。此外，我们有：
证明： 对于任意的1<=i<=n，令
是
中的一个递增序列。我们需要证明的是：
假设：
是满足对于任意的1<=i<=n和任意的j，都有
成立的声明。那么足以证明
使用命题3.4.1，这个证明通过对S的结构使用归纳法来完成。
练习3.4.3 证明等式(3.15)。
令D是一个通过公式(3.13)给定的声明。那么D可以自然而然地推导出语义泛函：
对于任意的
都成立。从命题3.4.3可以得出
是连续的。那么通过Knaster-Tarski定理（定理3.3.1），我们断言[[D]]有一个不动点：
我们现在可以介绍递归量子程序的不动点特性：
证明：首先，我们要求对于任意的程序模式
和任意的程序T1;...; Tn，都有
实际上，我们思考声明
因为T1;...; Tn 都是程序（不包含过程标识符），所以通过定义3.4.8和引理3.4.1(1)，我们可以得到：
其次，我们将从
中最小的元素
开始的[[D]]的迭代定义为：
其中0是
中的零量子操作。那么它满足
对于任意的整数k>=0都成立。可以通过对k使用归纳法来对公式(3.17)进行证明。实际上，k=0的情况显然成立。通过k的归纳假设和公式(3.16)可以得出：
最后，利用公式(3.16)、命题3.4.3、Knaster-Tarski定理和命题3.4.1(3)，我们可以得到：
本节的最后，我们将给读者留下两个思考题。正如本节开头所述，本节中介绍的材料与经典递归程序理论相似，但我相信通过对这两个问题进行研究会发现递归量子程序和经典递归程序之间的一些有趣且微妙的不同之处。
问题3.4.1
(1) 量子程序中任意的一般性测量是否可以通过一个投影测量加上一个幺正变换来实现？如果这个程序不包含任何递归（和循环），那么命题2.1.1已经对这个问题进行了回答。
(2) 如何延迟执行量子程序中的测量？对于程序中不包含递归（和循环）的情况，2.2.6小节中的延迟测量原则已经对这个问题进行了回答。如果程序中包含递归或者循环，问题将变得很有趣。
问题3.4.2 本小节只考虑了不带参数的递归量子程序。我们如何定义带参数的递归量子程序呢？我们需要对两类不同的参数进行处理：
(1) 经典参数。
(2) 量子参数。
Bernstein-Varzirani递归傅里叶采样和Grover 不动点量子搜索是两个带参数的递归量子程序的例子。
3.5 例子：Grover 量子搜索
前几节对量子while语句及其带递归量子程序的扩展进行了研究。为了说明它的功能，我们现在使while语句编程实现Grover搜索算法。为了方便读者阅读，让我们首先简单地回忆一下2.3.3节介绍的算法。该算法会对一个由N=2n个元素构成的数据库进行搜索，这些元素的下标是数字0; 1;...;N-1。假设该搜索问题恰好有L个解且
。此外我们还拥有一个有能力识别该搜索问题的解的黑盒。我们将整数
和它的二进制表示法
视为等价的。那么该黑盒可以通过n + 1 个量子比特上的幺正操作O来表示：
对于任意的
都成立，其中
的定义为
这是解的特征方程。Grover算子G由以下几步构成：
- 应用黑盒O。
- 应用Hadamard变换
。 - 执行一个条件相移Ph:
即
。
- 再次应用Hadamard变换
2.3.3节详细地描述了算子G作为旋转的几何学知识。图3.4对使用Grover算子的搜索算法进行了描述，其中Grover 算子的迭代次数k是一个在区间
中的正整数，且θ是通过Grover算子旋转的角度，我们可以将它定义为等式：
现在我们使用量子while语句对Grover算法进行编程。我们将使用n+2个量子变量：
- 这些变量的类型为：
- 变量r用于统计Grover算子的迭代次数。为了达到这个目的，我们使用量子变量r来替代经典变量，出于方便的考虑，量子while语句中并不包含经典变量。
那么我们可以将Grover算法写成图3.5中的Grover程序。注意因为待搜索数据库的大小为N=2^n，所以应当将程序Grover中的n理解为元变量。在Grover中的一些内容需要详细说明：
循环卫式（第7行）中的测量
为：
其中k市区件
的正整数。
- 循环体D（第7 行）如图3.6 所示。
- 在
语句（第8行）中，N是在n个量子比特的可计算基矢上进行的测量，即
通过下一章中设计的程序逻辑，我们可以对该程序的正确性进行证明。
3.6 引理的证明
3.3.2节中介绍的一些关于量子操作和局部密度算子的域的引理并没有证明。出于完整性的考虑，我们将在这一节中给出它们的证明。
证明引理3.3.2需要用到正定算子平方根的概念，而这个概念又需要用到无限维希尔伯特空间H中厄米算子的谱分解原理。回忆定义2.1.16，如果一个算子
满足
，那么它是厄米算子。正如2.1.2节所定义的那样，一个投影算子PX与H的每个闭子空间X 都相关。H中的族谱是一类以实数λ为索引的投影算子
且实数λ满足如下条件：
现在我们可以对正定算子A 的平方根进行定义。因为A 是一个厄米算子，所以它享有谱分解：
那么可以将其平方根定义为
有了这些预备工作，我们可以给出如下证明。
引理3.3.2 、的证明：首先，对于任意的正定算子A，通过Cauchy-Schwarz不等式（参考[174] 一书的第68 页）我们可以得到：
即
(1) 对于所有的m>=0，都有
。
(2) 如果对于所有的m>=0 都有
，那么
。
注意对于任意的正定算子B 和C，
当且仅当对于任意的
都有
。那么从(1) 和(2) 可以推出
至此，我们完成了对引理3.3.2的证明。
基于引理3.3.2，接下来可以很容易地完成对引理3.3.3的证明。
引理3.3.3 的证明：假设E是一个量子算子，它的Kraus算子和表示（参考定理2.1.1）为
，
是D(H) 中的一个递增序列。那么通过引理3.3.2，我们可以得到：
最后，我们对引理3.3.4进行证明。
引理3.3.4 的证明：令
是
中的递增序列。那么对于任意的
是
中的递增序列。通过引理3.3.2，我们可以定义：
因为tr(.) 是连续的，所以满足
此外，可以通过线性关系在
的整体上定义
的定义式表明：
(1) 对于所有的m>=0，都有
。
(2) 如果对于所有的m>=0都满足
，那么
。
所以，这足以证明
是完备正定的。假设HR 是一个外部希尔伯特空间。对于任意的
，我们有：
那么对于任意的
，我们可以通过线性关系得到：
因此，如果A是正定的，那么对于所有n，
都是正定的，且
也是正定的。
3.7 文献注解
文献[221]对3.1节介绍的量子while 语句进行了定义，但它引用了许多前人设计的量子程序结构，比如Sanders和Zuliani以及Selinger。文献[227]对量子while循环的一般形式进行了介绍，并对它的性质进行了深入研究。本书的1.1.1节对现有的量子编程语言进行了讨论，将本章介绍的量子编程语言与前文中提到的量子编程语言进行比较很有意义。
3.2节和3.3节中的操作语义和指称语义的描述主要是基于文献[221]的。指称语义实际上最早是由Feng 等人在文献[82] 中提出的，但二者对指称语义的处理方式是不同的：[82]直接对指称语义进行了定义，然而在[221] 中，首先给出了操作语义，再从操作语义中推导出指称语义。Selinger提出了在转换规则中将概率和密度算子编码为局部密度算子的想法。Kashe是最早开始对量子计算中的域理论进行研究的。Selinger 在有限维希尔伯特空间的情况下得出了引理3.3.2 和3.3.4。文献[225] 对一般情况下的引理3.3.2 进行了证明，它本质上是通过对文献[182]中的定理Ⅲ.6.2进行修改得到的。Selinger 在文献[194]中最早提出了命题3.3.6 的一种表达形式。但目前命题3.3.6 的表述形式是基于文献[233] 中介绍的局部量子变量的概念给出的。
量子编程中的递归最早是由Selinger在文献[194] 中提出的。但本书3.4 节中提到的材料与文献[194] 和其他尚未发表的文献中的材料略有不同。
最后应当指出，本章本质上是对Apt、de Boer和Olderog在文献[21]中提出的经典while程序和递归程序的语义进行的量子化扩展。
