2018, Vol. 29
2. 计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;
3. 清华大学 计算机系, 北京 100084
2. State Key Laboratory of Computer Science(Institute of Software, The Chinese Academy of Sciences), Beijing 100190, China;
3. Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
随着量子硬件设计与制造技术的飞速发展, 量子计算正快步走入我们的生活.由于在计算速度方面具有超越经典计算的潜在优势, 以及可以提供绝对安全的密码方案, 量子计算的理论研究受到了广泛的重视.在学术界:欧盟第6框架将量子信息与量子计算的基础结构作为重要研究内容, 并集中了牛津大学、Bristol大学、约克大学、巴黎七大、因斯布鲁克大学以及McGill大学的研究人员; 由英国工程与物理科学研究理事会(EPSRC)和国家e-Science中心共同资助、英国计算研究委员会负责的UK Grand Challenges Exercise中7个主题之一的Journeys in Non-Classical Computation将“Quantum Software Engineering”列为最主要内容; 美国国家标准技术研究所、麻省理工学院、华盛顿大学、哥伦比亚大学、英国牛津大学、法国国家科学研究中心等著名学术机构已经开始量子软件相关的研究; 密歇根大学开展了量子计算机体系结构以及量子设计自动化方面的工作.在工业界:2014年, IBM公司宣布耗资30亿美元研发下一代芯片, 主要是量子计算和神经计算; 2016年5月, IBM公司又发布了5个量子比特的量子计算云服务, 并于2017年3月发布IBM Q系统, 目前已可以支持16个量子比特; 2014年, 加州大学圣巴拉拉分校的知名物理学家Martinis研究组加入Google公司研发量子计算处理器, 并于2016年9月提出“量子霸权(quantum supremacy)”研制计划, 其目标是在2017年底之前实现50个量子比特的处理器, 从而超越目前传统计算机的执行能力; 2017年10月, Intel公司发布了17个量子比特的量子计算芯片, 交付给其荷兰合作伙伴QuTech使用.基于以上进展, 美国总统科学技术办公室发布量子信息文件称:“预计几十个量子比特、可供早期量子计算机科学研究的系统可望在5年内实现”.欧盟委员会于2016年7月发布《量子宣言》, 宣布将支持一项10亿欧元的量子技术旗舰计划.《量子宣言》对量子计算机的研制做出了详细部署, 计划5年内发展出量子计算机新算法, 5年~10年用大于100个量子比特的、特定用途的量子计算机解决化学和材料科学难题.澳大利亚近年来专注于硅基、磷掺杂的量子计算方案, 并于2016年初成立了硅基半导体量子计算国家实验室.在国内, 中国科学技术大学、清华大学、国防科技大学、南京大学等在量子计算和量子软件基本理论、量子密码的理论与应用、量子计算机的物理实现等方面的工作卓有成效.
众所周知, 软件是计算机的“灵魂”.一旦量子计算机研制成功, 量子软件的开发将变成真正发挥量子计算机作用的关键.另一方面, 由于量子系统与经典世界相比有许多根本不同的特征(如量子信息的不可克隆性、量子纠缠的非局域作用等), 正如人们所预料的, 经典的软件理论、方法和技术在很大程度上不能直接适用于量子软件.这就使得量子软件的理论和方法成为一个富有挑战性的课题, 未来的量子程序和量子通信协议的设计将会非常困难和容易出错.在此背景下, 对于量子程序和协议的形式化验证就显得尤为重要.本文将回顾这两个方面一些已有的研究结果, 重点放在本文两位作者所在研究组(清华大学、University of Technology Sydney)的工作, 并兼顾其他相关研究.对顺序量子程序, 我们将分别讨论基于程序语言的验证和基于语义模型(两种量子Markov链)的验证.前者的好处在于结构化和易用性; 后者则与语言无关, 因此发展出的理论可以适用于不同的程序语言.模型检测是计算机系统, 包括硬件和软件系统形式化验证的一种重要技术, 由于其完全机械化并可提供错误诊断信息, 在工业界得到了广泛的应用.本文将着重介绍这一技术在量子系统中的推广和应用.
总的来说, 我们将会看到, 虽然这一领域取得了一些可喜的进展, 但目前的研究还非常零散, 很多问题甚至还不清楚如何准确定义.这大体上有两方面的原因:(1)尽管最近几年量子硬件设备的物理实现取得了长足的进展, 但距离能够运行真正实用的量子程序的通用量子计算机仍然非常遥远.因此, 绝大部分传统计算机科学家与程序设计和验证的专家还持观望态度, 并没有对这一领域给予足够多的重视; (2)由于量子程序与传统计算机程序相比具有很大的不同, 特别是由于量子叠加和纠缠的存在, 量子程序的验证往往非常困难.但是, 我们有理由相信, 量子程序理论和验证的研究将会吸引越来越多的计算机科学家的关注, 从而带动这一领域蓬勃发展.
1 量子语言与程序逻辑自20世纪90年代以来, 程序语言的设计与实现就是量子程序研究的主要内容.特别是最近几年, 由于受到量子计算硬件进展的刺激以及2010年IARPA设立的量子计算机科学项目的推动, 量子程序设计语言有了很大的进展.主要包括:(1)微软公司的LIQUi| > [1], 及其最近与苏黎世ETH合作提出的量子程序编译和优化的可扩展软件设计流[2].2017年12月, 微软公司推出程序语言Q#, 以及集成在开发工具Visual Studio中的量子模拟器Q# library[3]; (2) Selinger组的Quipper[4]; (3)普林斯顿大学、加州大学圣巴拉拉分校等单位合作的Scaffold[5]; (4) Raytheon BBN Technologies等的QuaFL[6, 7].另外, 应明生等人定义了一种代数语言[8], 以便对量子电路进行代数操作与推理, 并引入了一个量子flowchart语言[9].
程序分析技术在编译器设计及程序优化等方面有着重要的应用.在Scaffold的编译器ScaffCC[5]中已经采用了数据流分析的一些方法, 分析量子程序中的纠缠并检查是否违反不可克隆原理.文献[10]首先研究了有限维希尔伯特空间中循环体(loop body)为酉算子的量子循环程序的终止问题.文献[11]将文献[10]中的一些主要结果推广到循环体为一般超算子的情形, 并提供了计算平均执行时间的一般性方法.这项工作中采用的主要技术是超算子的矩阵表示及薛定谔-海森堡对偶性.注意到微软公司新近推出的Q#语言[3]已经支持循环, 这一工作可以用来分析Q#程序的正确性.Perdrix与Jorrand[12, 13]将抽象解释(abstract interpretation)技术引入量子程序分析, 特别是程序中的纠缠及其演化的分析.Honda[14]进一步分析了可用stablizer formalism描述的一类特殊量子程序中的纠缠.
1.1 量子程序的Hoare-Floyd逻辑量子程序验证研究的一个重要方面是发展适用于量子计算的程序逻辑.Brunet与Jorrand[15]提出了将Birkhoff-von Neumann量子逻辑应用于量子程序推理的方法.Baltag与Smets[16]发展了一种可用于量子系统中信息流形式化的动态逻辑.冯元等人[17]发现了关于量子程序的一些有用的推理规则.
1969年Turing奖得主Hoare在另一Turing奖得主Floyd工作的基础上提出了程序的公理语义, 通常称为Floyd-Hoare逻辑.这个逻辑的完备性定理则由Turing奖得主Cook于1978年证明.此后, Floyd-Hoare逻辑成为程序验证的逻辑基础, 在程序设计方法学中处于核心地位.Hoare逻辑的核心概念是Hoare三元组, 用来描述一段程序代码如何改变计算机的内存状态.Hoare三元组具有形式{P}C{Q}, 这里, C是一段程序代码, P和Q是逻辑公式, 分别称为C的前置条件和后置条件.Hoare三元组可以有两种解释, 一种是部分正确性(partial correctness):如果在C被执行前P成立, 而且C终止, 则在C执行之后Q必然成立; 另一种是完全正确性(total correctness):如果在C被执行前P成立, 则C必然终止, 并且在C执行之后Q成立.由此可见, 完全正确性比部分正确性要求更高.Hoare逻辑通过为命令式编程语言的所有构造提供公理和推理规则, 从而使得该语言下的所有程序的部分正确性和完全正确性都可以进行(部分)自动化证明.
在量子计算领域, Chadha、Mateus和Sernadas[18]给出了量子程序在只允许有界迭代的限制下的一个Floyd-Hoare型证明系统; Kakutani[19]试图将den Hartog的概率Hoare逻辑推广到量子情形.但这些尝试都不成功.应明生[20]建立了一个真正完整的量子Folyd-Hoare逻辑, 证明了其(相对)完备性.值得指出的是, 量子Floyd-Hoare逻辑完备性的证明用到了与经典Floyd-Hoare逻辑完备性的证明很不一样的方法, 需要采用一些分析数学的技术.最近, 中国科学院软件研究所詹乃军教授研究组[21]基于Isabelle/HOL设计实现了一个量子Floyd-Hoare逻辑的定理证明器.
2 基于语义模型的量子程序验证量子程序验证的另一个思路是直接基于语义模型.在量子计算发展的初级阶段, 各种量子程序设计语言和量子计算模拟环境层出不穷, 但目前还没有任何一种语言占据主导地位.所以, 发展基于语义模型的程序验证理论和验证工具就显得尤为重要.
基于Girard的Geometry of Interaction(Abramsky-Haghverdi-Scott范畴论形式), Hasuo与Hoshino[22]找到了带递归的函数式量子程序设计语言的一个语义模型.进一步地, 利用线性逻辑定量语义中的一些构造, Pagani、Selinger和Valiron[23]定义了带递归及无限数据类型的函数式量子程序设计语言的一个指称语义.Jacobs[24]为量子程序的块(block)构造给出了一个范畴论公理化.Staton[25]为量子程序的等式推理提供了一个代数语义框架.在量子程序的最弱前置条件语义的研究中, D’Hondt与Panangaden[26]提出了将量子谓词定义为本征值在单位区间中的物理可观测量(Hermitian算子).文献[27]考虑了一类特殊的量子谓词——投影算子, 从而使得量子逻辑中发展起来的一些方法可应用于量子程序的谓词转换器语义.需要特别指出的是, 在量子程序最弱前置条件语义的研究中存在经典程序所没有的困难, 即对于非交换的量子谓词, 其析取和合取无法定义.
与经典程序一样, 顺序量子程序也可以使用Markov链作为其语义模型.与以上介绍的模型相比, 基于Markov链的语义模型更适合程序的形式化验证, 特别是模型检测.在以下两个小节中, 我们将分别介绍两种量子Markov链模型以及适用于各自模型的形式化验证方法.
2.1 Ⅰ型量子Markov链模型Markov链是描述概率系统行为和统计模型的重要的数学工具, 它描述了系统从一个状态到另一个状态转换的随机过程.该过程是“无记忆”的, 即下一状态的概率分布只由当前状态决定, 而与之前的状态无关.数学上, 一个Markov链可以由如下三元组描述:
| $M = (S, {s_0}, P), $ |
其中, S是一个有限状态的集合, s0∈S是初始状态,
可达性是经典确定性系统和概率系统模型检测的一个基本问题, 很多其他的形式化验证问题都可以归结为可达性分析.对Ⅰ型量子Markov链模型, 应圣刚等人[28]详尽分析了可达性(reachability)、重复可达性(repeated reachability)和持续性(persistence)等性质, 这些性质对于量子程序的终止(termination)、量子通信协议的公平性(fairness)等的分析具有重要意义.特别地, 文献[28]证明了, 类似于经典Markov模型, 量子Markov链的状态空间也可以分解为若干基础强连通分支(bottom strongly connected component, 简称BSCC)和唯一最大暂留子空间(transient subspace)的正交直和.俞能昆等人[29]将这一模型推广到含有并发行为的量子程序, 考虑了在公平(fairness)条件下并发量子程序的终止问题.李杨佳等人[30]研究了带不确定性选择的Ⅰ型量子自动机, 其中, 系统的演化由一组酉算子描述, 而可达状态集则为系统状态空间的闭子空间的布尔组合.在一般情况下, 最终可达性(eventual reachability)、全局可达性(global reachability)、最终永远可达性(ultimately forever reachability)和无限经常可达性(infinitely often reachability)等问题都是不可判定的.然而, 如果可达集可以表现为不带否定连接词的布尔组合, 那么后面3个问题则可判定.值得一提的是, 经典Markov链的各种可达性分析往往都归结为图论中的相应问题.但由于在Ⅰ型量子Markov链中, 并不存在一个预先设定的有限状态结合, 这些图论工具并不能直接用来进行可达性分析.为了解决这个问题, 文献[28]初步建立了一种希尔伯特空间中的新图论, 对这种新的、能为量子Markov链的分析提供合适数学工具的图论的研究将是一个非常有趣和重要的课题.
2.1.2 一般性质的形式化验证上一节我们讨论了Ⅰ型量子Markov链的可达性分析.如果希望分析或验证量子程序更复杂的性质, 一个首先必须解决的问题是如何定义一种可以表达这些性质的时序逻辑.由于量子测量会改变量子系统的状态, 对于这样的时序逻辑的定义并不是一件容易的事情.目前这方面的研究刚刚起步.
2.2 Ⅱ型量子Markov链模型量子程序和量子通信协议往往也包含经典变量, 按照Ⅰ型量子Markov链模型的做法将这些变量全部用量子系统进行表示是非常低效的, 而且会占用宝贵的存储和计算资源.因此, 在实际的建模和验证中, 往往需要把经典变量和量子变量区别对待.在此思想指导下, 我们定义了Ⅱ型量子Markov链模型, 使其同时具有经典状态空间和量子状态空间.这一模型虽然并不带来表述能力上的提高, 但在程序和协议分析时却能带来方便.具体来说, 一个Ⅱ型量子Markov链是如下的四元组
Ⅱ型量子Markov链对于模型检测的优点主要来自如下两个方面:(1)模型检测的结果对于所有输入量子态都成立, 这对于量子程序的验证尤其重要.比如说, 程序的终止问题通常表现为一个超算子ε.那么, 对于任何一个输入态ρ, 该程序终止的概率就是tr(ε(ρ)); (2)由于Ⅱ型量子Markov链具有有限的经典状态空间, 经典模型检测的技术能够有望推广到量子系统的检验中.同时, 由于硬件实现的困难, 在可以预见的将来, 量子计算机的纯量子计算部分规模不会太大, 这也使得我们不必太关心模型检测技术经常会遇到的状态爆炸问题(在量子计算中也许应该是维数爆炸问题).
2.2.1 计算树逻辑模型检测在经典模型检测中, 我们往往借助于时态逻辑, 特别是计算树逻辑(computation tree logic, 简称CTL)和线性时间逻辑(linear time logic, 简称LTL)来描述一大类性质.文献[31]定义了一种计算树逻辑QCTL(quantum computation tree logic), 它是经典的概率计算树逻辑PCTL的量子推广.与PCTL一样, QCTL的逻辑公式也分为状态公式和路径公式两大类, 但其语义的定义由于处理的是超算子(而非PCTL中的概率)而变得非常复杂.对于经典Markov系统, PCTL语义的定义需要借助在无限长路径的集合上引入某种概率测度[32].相应地, 在Ⅱ型量子Markov链中, 我们需要定义超算子值的测度(super-operator valued measure).有趣的是, 对于向量值测度[33]的Kluvanek-Caratheodory-Hahn扩展定理在这其中起到了重要的作用.在此基础上, 文献[31]将经典的模型检测算法推广到处理超算子的情形, 从而给出了Ⅱ型量子Markov链模型检测PCTL性质的多项式时间算法.
基于文献[31], 我们和中国科学院软件研究所张立军教授研究组合作开发了一款模型检测工具QPMC[34].该工具使用了一种类似于概率模型检测工具PRISM[35]的语法, 可以对简单量子程序和协议的QCTL性质进行自动化验证.Anticoli等人[36]将Quipper语言描述的电路翻译到Ⅱ型量子Markov链, 然后用QPMC进行验证.
2.2.2 线性时序逻辑模型检测文献[37]进一步考虑了线性时间性质, 特别是能够用ω-正则语言表示的性质.由于超算子不具有整环性质, 对ω-正则性质的模型检测具有经典Markov链不会遇到的困难.有趣的是, 通过把Ⅱ型量子Markov链转化成Ⅰ型量子Markov链, 并利用在文献[28]中发展起来的利用Ⅰ型量子Markov链对希尔伯特空间进行直和分解的结论, ω-正则性质的模型检测可以转化为Ⅰ型量子Markov链上的BSCC分解问题.由于文献[28]中的空间分解算法是多项式的, 因此Ⅱ型量子Markov链对于ω-正则性质的模型检测具有经典Markov链相同的时间复杂度.
2.2.3 带递归的Ⅱ型量子Markov链模型为了描述带过程调用(procedure call)的量子程序, 文献[38]定义了Ⅱ型递归量子Markov链.该模型结合了经典递归Markov链[39]和Ⅱ型量子Markov链的特征, 其表述能力等价于将转移函数的取值由概率替换为超算子的概率下推自动机.根据不同的应用场景, 文献[38]考虑了3种Ⅱ型递归量子Markov链的可达性问题:经典状态可达性(classical state reachability)、量子状态可达性(quantum state reachability)和量子状态空间可达性(quantum subspace reachability).有趣的是, 这3种可达性问题都可以转化成计算某个多项式方程组的最小解的问题, 其中, 每个方程的系数都是量子状态空间上的超算子.对于Ⅱ型递归量子Markov链的一个重要的子类, 即线性Markov链, 3种可达性问题都可以在多项式时间内解决.对于一般的情形, 量子状态空间可达性问题也存在多项式时间算法; 而程序分析的牛顿迭代法[40]则可用来有效地近似描述前面两种可达性所对应的超算子.
3 量子通信并发系统验证量子通信并发系统研究的主要动因有两点.首先, 普遍认为量子通信的实用化会比量子计算机早很多, 而量子通信并发系统的研究可以为量子通信协议的设计、分析与验证提供理论基础和工具.其次, 大型的量子计算机还非常遥远, 但最近美国总统科学技术办公室发布的量子信息文件预计几十个量子比特、可供早期量子计算科学研究的系统可望在5年内出现[41].因此, 一个自然的想法是如何将多个小型量子计算机组成分布式系统以解决经典计算机所不能解决的问题.实际上, 十多年前物理学家就已经开始研究分布式量子计算, 而并发问题在分布式量子程序设计中是不可避免的.
为了形式化地描述量子通信并发系统, 法国国家科学研究中心莱布尼茨实验室的Jorrand和Lalire首先提出了一种量子进程代数QAlg[42], 并为其建立了概率分支互模拟语义[43].但该方法只是经典进程代数的简单扩充, 甚至无法避免出现违背量子不可克隆原理等基本原则的进程.英国诺丁汉大学的Gay和Nagarajan提出了一种量子语言CQP[44], 融合了Pi演算的通信原语和量子力学的酉变换和测量.CQP的一个显著特点是提供了一个类型系统以保证量子进程的物理可实现性.然而, 这些方法都无法有效地刻画含纠缠的量子输入和输出.基于经典CCS理论, 文献[45, 46]提出了量子进程代数qCCS.通过引入量子自由变量, 在语法的层面上保证了所有量子进程都是物理可实现的.这样做既可以刻画量子态不可任意克隆等量子系统的特征, 又可以避免CQP中定义的繁杂的类型系统, 从而使得并发系统语义的研究更为简洁和方便.为了对进程中出现的量子自由变量加以赋值, 文献[45, 46]定义了量子上下文的概念, 用来精确表述含纠缠的量子输入和输出.
3.1 量子进程的互模拟互模拟关系是进程代数的核心概念, 刻画了系统的行为等价性.直观地讲, 如果两个系统中任何一个的任何行为都可以被另一个系统模拟, 并且这种模拟可以递归地一直进行下去, 那么, 它们就称为是可互模拟的.对于经典系统, 互模拟具有某种同余性质, 即任意进程构造符都保持互模拟关系.这一性质保证了在一个复杂系统中, 将任何一个子进程替换为与其互模拟的另一个进程并不会改变整个系统的任何可观测行为.对于复杂系统的模块化设计以及验证通信系统的通用可组合安全性(universally composable security), 具有非常重要的意义.
对于量子通信并发系统, 由于纠缠的非定域性特征, 复合系统中某一部分的行为可能会改变其他部分的状态, 这使得寻找能够在并行复合下保持的互模拟关系变得非常困难.QPAlg和CQP中已有的互模拟都不是同余关系.通过引入超算子作用下的闭条件(closed under super-operator application), 冯元等人[47, 48]为qCCS中的进程定义了一种真正意义上同余的互模拟关系, 并解决了在这种关系下qCCS的递归方程解的唯一性问题.不久后, 邓玉欣等人[49]将这一思想简化, 提出了类似于Pi演算中的开互模拟关系(open bisimulation).文献[50]进一步把符号互模拟[51]的概念推广到qCCS, 从而给出了判定量子进程互模拟的有效算法.
3.2 近似互模拟进程的互模拟关系是一种“刚性”的概念, 系统各部分概率的细微改变都可能破坏这种脆弱的关系.考虑到在量子计算与量子通信中, 噪音都是一个不可忽略的因素, 文献[46, 48]将经典进程代数的近似互模拟概念推广到qCCS, 并由此出发定义了量子进程空间上的伪度量(psudo-metric), 这一度量在不同进程构造符下保持非扩张(nonexpansiveness).非扩张性是互模拟关系的同余性的推广, 它保证了在复杂系统中, 将子进程P替换为另一个进程P'时, 整个系统的行为改变不超过P和P'之间的距离.由于全体量子操作构成一个连续谱, 因此量子进程之间的近似互模拟显得更加直观和自然.作为应用, 文献[46, 48]证明了由任何完备的量子逻辑门集合生成的量子进程在所有量子进程的集合中关于该伪度量是稠密的, 从而说明了qCCS框架下逻辑门的完备性和量子电路框架下量子逻辑门的完备性是一致的.
3.3 基于概率分布的互模拟以上所讨论的互模拟关系都是基于进程格局(configuration, 表现为一个进程-量子状态对)的, 在很多情况下, 对于进程的区分度太强.Kubota等人[52]为qCCS的量子测量提供了一种额外的语义, 即当测量产生的概率分布中所有格局都具有相同的可见动作时, 其语义描述为合并所有测量结果所对应的超算子(因此不会产生任何概率分支).这样扩充的qCCS可以有效解决概率行为都是由测量所引起的量子进程的互模拟问题.然而, 正如在量子密钥分发BB84协议中所阐述的那样, 如果概率行为是系统本身的随机性引起的, 那么这种方法就不适用了.另外, 判断一个量子测量是否引起不同可见行为的量子格局本身就是一个困难的问题, 有时候甚至依赖于后续的环境输入.为解决这些困难, 文献[53]采用了一种不同的处理方式, 即保持qCCS原有的量子测量语义, 但把基于格局的互模拟推广到格局的概率分布上.判断两个概率分布(无论其是由测量引起的, 还是系统本身的随机性引起的)是否互模拟时, 相互模拟的量子进程对应的量子状态总是组合在一起进行考虑.类似的思想也用来讨论量子Lambda演算中项(Lambda terms)的等价性[54].文献[53]还把近似互模拟推广到格局的概率分布上, 用以检验量子通信协议的复杂安全性特征, 这些特性无法在以往的互模拟概念下得到证明.作为应用, 文献[53]证明了BB84协议在接收-重发攻击下, 与理想系统的互模拟距离随着安全参数(security parameter, 对于BB84协议来说就是所消耗的qubit个数)的增加按指数级降低, 从而说明了该协议的正确性和渐进安全性.
3.4 互模拟检测工具可以预见, 量子通信并发系统的研究将对复杂量子协议的设计、分析和验证起到积极的推动作用. Ardeshir-Larijani等人[55, 56]研究并实现了一种简单的量子进程等价性检测, 可用来验证Teleportation等具有某种确定性的量子程序和协议的正确性, 即对给定的量子输入状态, 任何不确定性或并发分支都产生同样的量子输出状态.Kubota等人开发出基于qCCS的软件工具[52], 用于检测量子进程的互模拟.英国Glasgow大学的研究小组正在着手qCCS符号互模拟的软件实现.最近, 我们和新加坡南洋理工大学刘扬教授研究组合作开发了工具QUBET(quantum bisimulation checking and emulation tool), 利用qCCS对量子通信系统进行仿真和互模拟检测, 并提供了易扩展的架构和用户友好的图形化界面.
4 展望需要指出的是, 本文所讨论的量子程序和量子协议都遵循“程序的数据流是量子的, 但控制流仍然是经典的”这样一个基本的思路.Selinger将这个思路总结为一句口号:“量子数据, 经典控制(quantum data, classical control)”.这个思路的提出是十分自然的, 也是相对来说比较容易实现的, 只需要在经典的程序设计语言中增加对于量子数据的操作, 如酉变换和量子测量等.
但是, 人们也认识到“量子数据, 经典控制”的思想并不能最为有效地发挥量子计算特有的优势.Altenkirch与Grattage[57]提出了一种带量子控制流的函数式量子程序设计语言QML, 并在其后一系列论文中系统地发展了相应的理论, 甚至实现了编译器.但是, 现在看来, 这个理论并没有完全成功, 特别是一般程序的量子叠加的严格语义这一最为核心的问题并没有得到明确的定义.在没有递归(也没有循环)的情况下, 如果整个程序中测量都可以移到最后一步, 则带量子控制流的程序的语义比较容易定义, 本质上就是量子的multiplexor.如果中间过程有量子测量, 这个问题就变得非常困难了.Badescu与Panangaden在文献[58]中对这个问题有一些有趣的讨论.直到最近, 受到量子随机游走(quantum random walks)的启发, 文献[59]找到了一种真正能够实现量子控制流的量子程序设计模型.文献[59]第6章通过引入算子值函数的卫式复合, 进一步定义超算子的卫式复合, 从而由量子程序的半经典语义导出纯量子语义, 并解决了这一问题.正如文献[58]中所指出的, 带量子控制流的量子递归是一个非常困难的问题, 需要全新的思想.文献[59]第6章提出采用二次量子化方法(second quantization), 解决了这个问题, 定义了波色子(对称的)与费米子(反对称)量子递归模式.必须承认的是, 我们对于量子递归还远没有完全彻底地理解, 这也是量子程序理论和方法需要进一步研究的重要问题.
| [1] |
Wecker D, Svore KM. LIQUi|>: A software design architecture and domain-specific language for quantum computing. arXiv. org, vol. quant-ph. p. arXiv: 1402. 4467, 19-Feb-2014. |
| [2] |
Häner T, Steiger DS, Svore K, Troyer M. A software methodology for compiling quantum programs. arXiv. org, vol. cs. PL. p. arXiv: 1604. 01401, 06-Apr-2016. |
| [3] |
The Q# Programming Language. 2017. https://docs.microsoft.com/en-us/quantum/quantum-qr-intro?view=qsharp-preview |
| [4] |
Green AS, Lumsdaine PL, Ross NJ, Selinger P, Valiron B. Quipper-A scalable quantum programming language. In: Proc. of the PLDI. 2013. 333-342. |
| [5] |
JavadiAbhari A, Patil S, Kudrow D, Heckey J, Lvov A, Chong FT, Martonosi M. ScaffCC: Scalable compilation and analysis of quantum programs. arXiv. org, vol. quant-ph. pp. arXiv: 1507. 01902-17, 08-Jul-2015. |
| [6] |
Lapets A, Roetteler M. Abstract resource cost derivation for logical quantum circuit descriptions. In: Proc. of the 1st Annual Workshop on Functional Programming Concepts in Domain-Specific Languages-FPCDSL 2013. New York, 2013. 35-42. [doi: 10.1145/2505351.2505358] |
| [7] |
Lapets A, da Silva MP, Thome M, Adler A, Beal J, Roetteler M. QuaFL: A typed DSL for quantum programming. In: Proc. of the 1st Annual Workshop on Functional Programming Concepts in Domain-Specific Languages-FPCDSL 2013. New York, 2013. 19-26. [doi: 10.1145/2505351.2505357] |
| [8] |
Ying MS, Feng Y. An algebraic language for distributed quantum computing. IEEE Trans. on Computers, 2009, 58(6): 728–743.
[doi:10.1109/TC.2009.13] |
| [9] |
Ying MS, Feng Y. A flowchart language for quantum programming. IEEE Trans. on Software Engineering, 2011, 37(4): 466–485.
[doi:10.1109/TSE.2010.94] |
| [10] |
Ying MS, Feng Y. Quantum loop programs. Acta Informatica, 2010, 47(4): 221–250.
[doi:10.1007/s00236-010-0117-4] |
| [11] |
Ying MS, Yu N, Feng Y, Duan R. Verification of quantum programs. Science of Computer Programming, 2013, 78(9): 1679–1700.
[doi:10.1016/j.scico.2013.03.016] |
| [12] |
Perdrix S. Quantum entanglement analysis based on abstract interpretation. In: Proc. of the SAS. 2008. 270-282. [doi: 10.1007/978-3-540-69166-2_18] |
| [13] |
Jorrand P, Perdrix S. Abstract interpretation techniques for quantum computation. In: Gay S, Mackie I, eds. Semantic Techniques in Quantum Computation. Cambridge: Cambridge University Press, 2009, (6): 206-234. |
| [14] |
Honda K. Analysis of quantum entanglement in quantum programs using stabilizer formalism. Electronic Proc. in Theoretical Computer Science, 2015, 195(1): 262–272.
[doi:10.4204/EPTCS.195.19] |
| [15] |
Brunet O, Jorrand P. Dynamic quantum logic for quantum programs. Int'l Journal of Quantum Information, 2011, 2(1): 45–54.
[doi:10.1142/S0219749904000067] |
| [16] |
Baltag A, Smets S. LQP:The dynamic logic of quantum information. Math. Struct. in Comp. Science, 2006, 16(3): 491–525.
[doi:10.1017/S0960129506005299] |
| [17] |
Feng Y, Duan R, Ji Z, Ying MS. Proof rules for the correctness of quantum programs. Theoretical Computer Science, 2007, 386(1): 151–166.
[doi:10.1016/j.tcs.2007.06.011] |
| [18] |
Chadha R, Mateus P, Sernadas A. Reasoning about imperative quantum programs. Electronic Notes in Theoretical Computer Science, 2006.
[doi:10.1016/j.entcs.2006.04.003] |
| [19] |
Kakutani Y. A logic for formal verification of quantum programs. In: Proc. of the ASIAN. 2009. [doi: 10.1007/978-3-642-10622-4_7] |
| [20] |
Ying MS. Floyd-Hoare logic for quantum programs. Trans. on Programming Languages and Systems, 2011, 33(6): 1–49.
[doi:10.1145/2049706.2049708] |
| [21] |
Liu T, Li Y, Wang S, Ying MS, Zhan N. A theorem prover for quantum hoare logic and its applications. arXiv. org, vol. cs. LO. p. arXiv: 1601. 03835, 15-Jan-2016. |
| [22] |
Hasuo I, Hoshino N. Semantics of higher-order quantum computation via geometry of interaction. Annals of Pure and Applied Logic, 2017.
[doi:10.1109/LICS.2011.26] |
| [23] |
Pagani M, Selinger P, Valiron B. Applying quantitative semantics to higher-order quantum computing. In: Proc. of the POPL. 2014. [doi: 10.1145/2578855.2535879] |
| [24] |
Jacobs B. On block structures in quantum computation. Electronic Notes in Theoretical Computer Science, 2013, 298: 233–255.
[doi:10.1016/j.entcs.2013.09.016] |
| [25] |
Staton S. Algebraic effects, linearity, and quantum programming languages. In: Proc. of the 42nd Annual ACM SIGPLAN-SIGACT Symp. New York, 2015. 395-406. [doi: 10.1145/2775051.2676999] |
| [26] |
D'Hondt E, Panangaden P. Quantum weakest preconditions. Mathematical Structures in Computer Science, 2006.
[doi:10.1017/S0960129506005251] |
| [27] |
Ying MS, Duan R, Feng Y, Ji Z. Predicate transformer semantics of quantum programs. In: Gay S, Mackie I, eds. Semantic Techniques in Quantum Computation. Cambridge: Cambridge University Press, 2009, (8): 311-360. |
| [28] |
Ying S, Feng Y, Yu N, Ying MS. Reachability probabilities of quantum Markov chains. In: Proc. of the CONCUR. 2013. 334-348. [doi: 10.1007/978-3-642-40184-8_24] |
| [29] |
Yu N, Ying MS. Reachability and termination analysis of concurrent quantum programs. In: Proc. of the CONCUR. 2012. 69-83. [doi: 10.1007/978-3-642-32940-1_7] |
| [30] |
Li Y, Ying MS. (Un)deciddable problems about reachability of quantum systems. In: Proc. of the CONCUR. 2014. 482-496. [doi: 10.1007/978-3-662-44584-6_33] |
| [31] |
Feng Y, Yu N, Ying MS. Model checking quantum Markov chains. Journal of Computer and System Sciences, 2013, 79(7): 1181–1198.
[doi:10.1016/j.jcss.2013.04.002] |
| [32] |
Vardi YM. Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of the FOCS. 1985. [doi: 10.1109/SFCS.1985.12] |
| [33] |
Diestel J, Uhl J. Vector Measures, vol. 15. Providence: American Mathematical Society, 1977. |
| [34] |
Feng Y, Hahn EM, Turrini A, Zhang L. QPMC: A model checker for quantum programs and protocols. In: Proc. of the FM. 2015. 265-272. [doi: 10.1007/978-3-319-19249-9_17] |
| [35] |
Kwiatkowska MZ, Norman G, Parker D. PRISM 4. 0-Verification of probabilistic real-time systems. In: Proc. of the CAV. 2011. [doi: 10.1007/978-3-642-22110-1_47] |
| [36] |
Anticoli L, Piazza C, Taglialegne L, Zuliani P. Towards quantum programs verification-From quipper circuits to QPMC. In: Proc. of the RC. 2016. [doi: 10.1007/978-3-319-40578-0_16] |
| [37] |
Feng Y, Hahn EM, Turrini A, Ying S. Model checking Omega-regular properties for quantum Markov chains. In: Proc. of the CONCUR. 2017. 35: 1-35: 16. [doi: 10.1007/978-3-540-78499-9_22] |
| [38] |
Feng Y, Yu N, Ying MS. Reachability analysis of recursive quantum Markov chains. In: Proc. of the MFCS. 2013. 385-396. [doi: 10.1007/978-3-642-40313-2_35] |
| [39] |
Etessami K, Yannakakis M. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. Journal of the ACM, 2009, 1.
[doi:10.1145/1462153.1462154] |
| [40] |
Esparza J, Kiefer S, Luttenberger M. Newtonian program analysis. Journal of the ACM, 2010, 57(6): 1–47.
[doi:10.1145/1857914.1857917] |
| [41] |
Advancing Quantum Information Science: National Challenges and Opportunities. 2016. https://www.whitehouse.gov/sites/whitehouse.gov/files/images/Quantum_Info_Sci_Report_2016_07_22%20final.pdf |
| [42] |
Jorrand P, Lalire M. Toward a quantum process algebra. In: Proc. of the 1st Conf. on Computing Frontiers on Computing Frontiers. New York, 2004. 111-119. |
| [43] |
Lalire M. Relations among quantum processes:bisimilarity and congruence. Mathematical Structures in Computer Science, 2006, 16(3): 407.
[doi:10.1017/S096012950600524X] |
| [44] |
Gay S, Nagarajan R. Communicating quantum processes. In: Proc. of the POPL. 2005. [doi: 10.1145/1040305.1040318] |
| [45] |
Feng Y, Duan R, Ji Z, Ying M. Probabilistic bisimulations for quantum processes. Information and Computation, 2007, 205(11): 1608–1639.
[doi:10.1016/j.ic.2007.08.001] |
| [46] |
Ying MS, Feng Y, Duan R, Ji Z. An algebra of quantum processes. ACM Trans. on Computational Logic (TOCL), 2009, 10(3): 19–36.
[doi:10.1145/1507244.1507249] |
| [47] |
Feng Y, Duan R, Ying MS. Bisimulation for quantum processes. In: Proc. of the POPL. New York, 2011. 523-534. [doi: 10.1145/1926385.1926446] |
| [48] |
Feng Y, Duan R, Ying MS. Bisimulation for quantum processes. Trans. on Programming Languages and Systems, 2012, 34(4): 1–43.
|
| [49] |
Deng Y, Feng Y. Open bisimulation for quantum processes. In: Proc. of the IFIP TCS. 2012. [doi: 10.1007/978-3-642-33475-7_9] |
| [50] |
Feng Y, Deng Y, Ying MS. Symbolic bisimulation for quantum processes. ACM Trans. on Computational Logic, 2014, 15(2): 1–32.
[doi:10.1145/2579818] |
| [51] |
Hennessy M, Lin H. Symbolic bisimulations. Theoretical Computer Science, 1995, 138(2): 353–389.
[doi:10.1016/0304-3975(94)00172-F] |
| [52] |
Kubota T, Kakutani Y, Kato G, Kawano Y, Sakurada H. Semi-Automated verification of security proofs of quantum cryptographic protocols. Journal of Symbolic Computation, 2016, 73: 192–220.
[doi:10.1016/j.jsc.2015.05.001] |
| [53] |
Feng Y, Ying MS. Toward automatic verification of quantum cryptographic protocols. In: Proc. of the CONCUR. 2015. 441-455. |
| [54] |
Deng Y, Feng Y, Lago UD. On coinduction and quantum Lambda Calculi. In: Proc. of the CONCUR. 2015. 427-440. |
| [55] |
Ardeshir-Larijani E, Gay SJ, Nagarajan R. Equivalence checking of quantum protocols. In: Proc. of the TACAS. Berlin, Heidelberg, 2013, 7795(33): 478-492. [doi: 10.1007/978-3-642-36742-7_33] |
| [56] |
Ardeshir-Larijani E, Gay SJ, Nagarajan R. Verification of concurrent quantum protocols by equivalence checking. In: Proc. of the TACAS. Berlin, Heidelberg, 2014, 8413(42): 500-514. [doi: 10.1007/978-3-642-54862-8_42] |
| [57] |
Altenkirch T, Grattage J. A functional quantum programming language. In: Proc. of the LICS. 2005. 249-258. |
| [58] |
Bădescu C, Panangaden P. Quantum alternation:Prospects and problems. Electronic Proc. in Theoretical Computer Science, 2015, 195(1): 33–42.
[doi:10.4204/EPTCS.195.3] |
| [59] |
Ying MS. Foundations of Quantum Programming. Elsevier Science, 2016.
https://www.elsevier.com/books/foundations-of-quantum-programming/ying/978-0-12-802306-8 |