導讀
量子硬件設計與製造技術的飛速發展使得人們開始預言大於一百個量子比特的特定用途的量子計算機有望在 5-10 年內實現。可以想見，到那時候，量子軟件的開發將變成真正發揮這些計算機能力的關鍵。然而，由於量子信息的不可克隆性和糾纏的非局域作用等量子特徵，如何設計正確高效的量子程序和量子通信協議將是一個富有挑戰性的課題。
量子計算機的研發到什麼地步了？
隨著量子硬件設計與製造技術的飛速發展，量子計算正快步走入我們的生活。由於在計算速度方面具有超越經典計算的潛在優勢，以及可以提供絕對安全的密碼方案，量子計算的理論研究受到了廣泛的重視。在學術界： 歐盟第六框架將量子信息與量子計算的基礎結構作為重要研究內容，並集中了牛津大學、Bristol 大學、約克大學、巴黎七大、因斯布魯克大學以及 McGill 大學的研究人員；由英國工程與物理科學研究理事會(EPSRC)和國家 e-Science 中心共同資助、英國計算研究委員會負責的 UK Grand Challenges Exercise 中七個主題之一的 Journeys in Non-Classical Computation 將“Quantum Software Engineering”列為最主要內容；美國國家標準技術研究所、MIT、華盛頓大學、哥倫比亞大學、英國牛津大學、法國國家科學研究中心等著名學術機構已經開始量子軟件相關的研究； 密歇根大學開展了量子計算機體系結構以及量子設計自動化方面的工作。在工業界：2014 年，IBM 宣佈耗資 30 億美元研發下一代芯片，主要是量子計算和神經計算；2016 年 5 月，IBM 發佈了5 個量子比特的量子計算雲服務，並於 2017 年 3 月發佈 IBM Q 系統，目前已可以支持 16 個量子比特；2014 年，加州大學聖巴拉拉分校的知名物理學家 John Martinis 研究組加入谷歌研發量子計算處理器，並於 2016 年 9 月提出“量子霸權(quantum supremacy)”研製計劃，其目標是在 2017 年底前實現 50 個量子比特的處理器，從而超越目前傳統計算機的執行能力； 2017年11月，IBM宣佈成功構建並測量了具有類似性能指標的50個量子比特原型機；2018年1月，英特爾正式向QuTech 交付了首個 49 量子比特量子計算測試芯片；2018年3月，來自谷歌的研究人員報告了他們正在測試具有72個量子比特的量子計算機。基於以上進展，美國總統科學技術辦公室發佈量子信息文件稱： “預計幾十個量子比特、可供早期量子計算機科學研究的系統可望在 5 年內實現”。
圖 IBM Q計算中心內部圖，IBM最先進的量子計算機就放置在這裡。圖中，科學家正在通過IBM雲訪問其量子計算機。圖片來源：IBM。
為何要研究量子程序？
眾所周知，軟件是計算機的“靈魂”。一旦量子計算機研製成功，量子軟件的開發將變成真正發揮量子計算機作用的關鍵。另一方面，由於量子系統與經典世界相比有許多根本不同的特徵(如量子信息的不可克隆性、量子糾纏的非局域作用等)，正如人們所預料的，經典的軟件理論、方法和技術在很大程度上不能直接適用於量子軟件。 這就使得量子軟件的理論和方法成為一個富有挑戰性的課題，未來的量子程序和量子通訊協議的設計將會非常困難和容易出錯。在此背景下，對於量子程序設計和驗證就顯得尤為重要。
量子程序目前的研究主題有哪些？
量子程序設計研究的是如何為將來的量子計算機設計程序。總的來說，到目前為止關於量子程序的研究主要圍繞以下兩個主題開展： （1）過去為經典計算機發展的程序設計理論、方法和技術如何擴展到量子計算機上？（2）什麼樣的新程序設計模型、方法和技術能夠更有效地發揮量子計算機特有的優勢？由於量子系統的一些新特性（體現在量子程序中，如量子數據不可克隆、進程之間的糾纏、量子程序變元可觀測量的非交換性），已有的一些程序設計的理論、方法和技術不適用於量子程序，而需要引入一系列全新思想。
量子程序研究有哪些困難？
目前的量子程序研究都遵循“程序的數據流是量子的，但控制流仍然是經典的”這樣一個基本的思路。Selinger 將這個思路總結為一句口號：“量子數據，經典控制（quantum data,classical control）”。這個思路的提出是十分自然的，也是相對來說比較容易實現的，只需要在經典的程序設計語言中增加對於量子數據的操作，如 unitary 變換, 量子測量等。
但是，人們也認識到“量子數據，經典控制”的思想並不能最為有效地發揮量子計算特有的優勢。Altenkirch 與 Grattage提出了一個帶量子控制流的函數式量子程序設計語言 QML，並在其後一系列論文中系統地發展了相應的理論，甚至實現了編譯器。但是，現在看來這個理論並沒有完全成功。還有提出採用二次量子化方法（second quantization）解決這個問題, 因而定義了波色子（對稱的）與費米子（反對稱）量子遞歸模式。必須承認的是，我們對於量子遞歸還遠沒有完全徹底地理解。
圖 微軟推出的量子程序語言“Q#” （https://docs.microsoft.com/en-us/quantum/quantum-qr-intro?view=qsharp-preview）
插曲
2017年12月份微軟推出一門新的程序語言，名叫“Q#”（唸作Q Sharp），這是一個工具，可以幫助編程人員為量子計算機編寫軟件。另外，IBM和創業公司Rigetti Computing還為量子計算機開發了軟件。國內方面，2017年9月阿里巴巴引進密西根大學終身教授者施堯耘，擔任阿里雲首席量子技術科學家；12月份騰訊引進香港中文大學計算機系的副教授張勝譽正式出任量子實驗室負責人；2018年3月份，百度引進悉尼科技大學量子軟件和信息中心創辦主任段潤堯教授出任百度量子計算研究所所長。BAT引進的這三位負責人都偏向量子算法和軟件方向，展開了在量子計算和量子軟件方向的競爭。
圖 從左至右依次為施堯耘、張勝譽和段潤堯教授
總結
總的來說，雖然這一領域取得了一些可喜的進展，但目前的研究還非常零散，很多問題甚至還不清楚如何準確定義。這大體上有兩方面的原因：一、儘管最近幾年量子硬件設備的物理實現取得了長足的進展，但距離能夠運行真正實用的量子程序的通用量子計算機仍然非常遙遠。因此絕大部分傳統計算機科學家和程序設計和驗證的專家還持觀望態度，並沒有對這一領域給予足夠多的重視；二、由於量子程序和傳統計算機程序相比具有很大的不同，特別是由於量子疊加和糾纏的存在，量子程序的驗證往往非常困難。但是，我們有理由相信，量子程序理論和驗證的研究將會吸引越來越多計算機科學家的關注，從而帶動這一領域蓬勃發展。
本文節選自下列文獻（有興趣的可以訪問量子研究網站 http://quantum-study.com/information/1189.html 下載論文原件）：
馮元,應明生.量子程序驗證.軟件學報,2018,29(4)
應明生，量子程序設計研究的近期進展
閱讀更多 量子研究 的文章
