帶你讀《量子程式設計基礎》之三：量子程式的文法與語義

點選檢視第一章 點選檢視第二章

第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(.) 是連續的，是以滿足

此外，可以通過線性關系在

的整體上定義

的定義式表明：

(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程式和遞歸程式的語義進行的量子化擴充。