清华大学：量子程序设计研究的近期进展（应明生）

量子程序设计研究的近期进展 应明生( University of Technology Sydney,清华大学) 引言 八年前,我与冯元、段润尧、季铮锋三位老师一起在本刊发表 过一篇量子程序理论研究的综述[1]。这些年,这个领域有了比较 大的进展,我自己对于一些问题的理解也有所不同。因此,非常高 兴得到吴俊杰教授邀请在他主编的专辑中再写一篇这方面的文章。 量子计算机硬件的研制这几年有较大的进展,但目前离实用化 还有很大的距离(想必其他老师会在本专辑详加论述)。因此,这 篇文章面临的第一个问题是:我们现在研究量子程序是不是太早了 其实这个问題我回答不好,但为了把这篇文章继续写下去,请允许 我谈两件事情。首先,早在1996年Klil已己经开始考虑量子程序设 计的问题,此后20年这方面已经有大量的研究工作发表。第二件事 情则扯得有点远。我国正在大力提倡原始创新,而原始创新只有在 新领域机会多一点,在成熟的领域则机会很少。量子程序恰好是 个正在兴起的新领域,希望有更多的年轻人参与研究。 当然,量子程序设计研究的是:如何为将来的量子计算机设 计程序?文章写到这里则面临第二个问题:既然我们目前并没有实 用化的量子计算机,那怎样研究量子程序?惭愧的是这个问题我也 回答不好,但本文中我将较为全面地介绍近年来的一些进展。等读 者耐心读完本文后,您自己一定能够根据已有的研究工作(以及您 认为应该研究而还没有得到研究的问题),比我更好地回答这个问 题。由于已有文[1],本文主要讨论2008年以后的工作。 总的来说,到目前为止关于量子程序的研究主要围绕以下两个 主题开展[2]:(1)过去为经典计算机发展的程序设计理论、方 法和技术如何扩展到量子计算机上?(2)什么样的新程序设计模型 方法和技术能够更有效地发挥量子计算机特有的优势?由于量子系 统的一些新特性(体现在量子程序中,如量子数据不可克隆、进程 之间的纠缠、量子程序变元可观测量的非交换性),已有的一些程 序设计的理论、方法和技术不适用于量子程序,而需要引入一系列 全新思想。 二.量子程序设计语言及其实现

量子程序设计研究的近期进展 应明生(University of Technology Sydney, 清华大学) 一． 引言 八年前，我与冯元、段润尧、季铮锋三位老师一起在本刊发表 过一篇量子程序理论研究的综述［1］。这些年，这个领域有了比较 大的进展，我自己对于一些问题的理解也有所不同。因此，非常高 兴得到吴俊杰教授邀请在他主编的专辑中再写一篇这方面的文章。 量子计算机硬件的研制这几年有较大的进展，但目前离实用化 还有很大的距离（想必其他老师会在本专辑详加论述）。因此，这 篇文章面临的第一个问题是：我们现在研究量子程序是不是太早了？ 其实这个问题我回答不好，但为了把这篇文章继续写下去，请允许 我谈两件事情。首先，早在 1996 年 Knill 已经开始考虑量子程序设 计的问题，此后 20 年这方面已经有大量的研究工作发表。第二件事 情则扯得有点远。我国正在大力提倡原始创新，而原始创新只有在 新领域机会多一点，在成熟的领域则机会很少。量子程序恰好是一 个正在兴起的新领域，希望有更多的年轻人参与研究。 当然，量子程序设计研究的是：如何为将来的量子计算机设 计程序？文章写到这里则面临第二个问题：既然我们目前并没有实 用化的量子计算机，那怎样研究量子程序？惭愧的是这个问题我也 回答不好，但本文中我将较为全面地介绍近年来的一些进展。等读 者耐心读完本文后，您自己一定能够根据已有的研究工作（以及您 认为应该研究而还没有得到研究的问题），比我更好地回答这个问 题。由于已有文［1］，本文主要讨论 2008 年以后的工作。 总的来说，到目前为止关于量子程序的研究主要围绕以下两个 主题开展［2］： （1）过去为经典计算机发展的程序设计理论、方 法和技术如何扩展到量子计算机上？（2）什么样的新程序设计模型、 方法和技术能够更有效地发挥量子计算机特有的优势？由于量子系 统的一些新特性（体现在量子程序中，如量子数据不可克隆、进程 之间的纠缠、量子程序变元可观测量的非交换性），已有的一些程 序设计的理论、方法和技术不适用于量子程序，而需要引入一系列 全新思想。 二． 量子程序设计语言及其实现

早期的量子程序研究集中在量子程序设计语言的设计及初步的 实现。早在1990年代及2000年代初就已经提出了几个高级量子程 序设计语言,这方面的简单介绍可参见[1] 最近这几年,由于受到量子计算硬件进展的刺激以及2010年 IARPA设立的量子计算机科学项目的推动,量子程序设计语言的设 计与实现方面有很大的进展,主要包括:(1) Microsoft的 LIQUi|> 3]。最近他们与ETHκ urich合作进一步地提出了量子程序编译 和优化的可扩展软件设计流[4];(2) Selinger组的 Quipper[5];(3) Princeton、UCSB等单位的 Scaffold[6,7]。(4) Raytheon BBN Technologies等的 QuaL[8,9]。特别值得指出的是,为了更好地实 现其编译器, Microsoft与 Selinger两个研究组在量子电路的优化方 面做岀了一些非常好的工作,较好地解决了单个量子比特电路优化 问题,但多个量子比特电路的优化进展不大。量子电路的优化远较 经典电路优化困难得多,经典电路的优化方法完全不适用,而需要 些很不一样的思路,比如单量子比特情形采用了一些初等代数数 论工具。随便提及,布尔代数为经典电路的分析与综合提供一种很 好的代数语言。文[10]曾为量子电路定义了一种代数语言,以便 对量子电路进行代数操作与推理。 在国内,南京大学徐家福、宋方敏、吴楠教授研究组在量子 程序设计语言及其实现方面做了大量的工作,在[11]第8节有 个很好的介绍。文[12]也曾定义了一个量子 flowchart语言。 三,量子程序的语义 程序设计语言的形式语义为程序提供了严格的数学描述。这样 的描述对于量子程序尤为重要,因为量子系统的一些特征违反人们 的直觉,理解起来很容易出错,而对于量子力学可能缺乏系统训练 的程序员则尤其如此。 量子程序语义的早期研究在[1]中已有介绍。这里只谈近几 年的一些工作。基于 Girard的 Geometry of Interaction( Abramsky Haghverdi-Scott范畴论形式), Haso与 Hoshino[13]找到了带递归 的函数式量子程序设计语言的一个语义模型。进一步地,利用线性 逻辑定量语义中的一些构造, Pagani, Selinger and valiron[14]定义 了带递归及无限数据类型的函数式量子程序设计语言的一个指称语 义。 Jacobs[15]为量子程序的 block构造给出了一个范畴论公理化。 Staton[16]为量子程序的等式推理提供了一个代数语义框架

早期的量子程序研究集中在量子程序设计语言的设计及初步的 实现。早在 1990 年代及 2000 年代初就已经提出了几个高级量子程 序设计语言，这方面的简单介绍可参见［1］。 最近这几年，由于受到量子计算硬件进展的刺激以及 2010 年 IARPA 设立的量子计算机科学项目的推动，量子程序设计语言的设 计与实现方面有很大的进展，主要包括：（1）Microsoft 的 LIQUi|> ［3］。最近他们与 ETH Zurich 合作进一步地提出了量子程序编译 和优化的可扩展软件设计流［4］; (2) Selinger 组的 Quipper ［5］; (3) Princeton、UCSB 等单位的 Scaffold［6, 7］。(4) Raytheon BBN Technologies 等的 QuaFL[8, 9]。特别值得指出的是，为了更好地实 现其编译器，Microsoft 与 Selinger 两个研究组在量子电路的优化方 面做出了一些非常好的工作，较好地解决了单个量子比特电路优化 问题，但多个量子比特电路的优化进展不大。量子电路的优化远较 经典电路优化困难得多，经典电路的优化方法完全不适用，而需要 一些很不一样的思路，比如单量子比特情形采用了一些初等代数数 论工具。随便提及，布尔代数为经典电路的分析与综合提供一种很 好的代数语言。文［10］曾为量子电路定义了一种代数语言，以便 对量子电路进行代数操作与推理。 在国内，南京大学徐家福、宋方敏、吴楠教授研究组在量子 程序设计语言及其实现方面做了大量的工作，在［11］第 8 节有一 个很好的介绍。文［12］也曾定义了一个量子 flowchart 语言。 三．量子程序的语义 程序设计语言的形式语义为程序提供了严格的数学描述。这样 的描述对于量子程序尤为重要，因为量子系统的一些特征违反人们 的直觉，理解起来很容易出错，而对于量子力学可能缺乏系统训练 的程序员则尤其如此。 量子程序语义的早期研究在［1］中已有介绍。这里只谈近几 年的一些工作。基于 Girard 的 Geometry of Interaction (Abramsky￾Haghverdi-Scott 范畴论形式) ，Hasuo 与 Hoshino［13］找到了带递归 的函数式量子程序设计语言的一个语义模型。进一步地，利用线性 逻辑定量语义中的一些构造，Pagani, Selinger and Valiron［14］定义 了带递归及无限数据类型的函数式量子程序设计语言的一个指称语 义。Jacobs［15］为量子程序的 block 构造给出了一个范畴论公理化。 Staton［16］为量子程序的等式推理提供了一个代数语义框架

在量子程序的最弱前置条件语义的研究中,早在2006年 D Hondt 与 Panangaden[17]就提出了将量子谓词定义为本征值在单位区间 中的物理可观测量( Hermitian算子)。这是一个一旦说出来以后大 家都觉得极其简单的想法,但对于进一步的发展却很重要。文[18] 考虑了一类特殊的量子谓词一投影算子,从而使得量子逻辑中发展 起来的一些方法可应用于量子程序的谓词转换器语义。需要特别指 出的是,量子程序最弱前置条件语义的研究中存在着一个特有(经 典程序所没有)的困难:对于非交换的量子谓词( Hermitian算子), 其析取、合取无法定义。 四.量子程序的分析 程序分析技术在编译器设计及程序优化等方面有着重要的应用 在 Scaffold[6]的编译器 Scaffco[冂]中已经采用了数据流分析的 些方法,分析量子程序中的纠缠并检查是否违反不可克隆原理。 文[7]也考虑了执行时间估计的问题。 文[19]首先研究了有限维 Hilbert空间中循环体( loop body)为 unitary 算子的量子循环程序的终止问题。文[20]将[19]中的 些主要结釆推广到循环体为一般超算子( super-operator)的情形,并考 虑了平均执行时间的问题。这项工作中采用的主要技术是超算子的 矩阵表示及 Schroedinger-Heisenberg对称性。按照[20]提出的将量 子 Markoⅴ链作为量子程序语义模型的想法,量子程序的终止问题可 以看作量子 Markoⅴ链的一类可达性问题。因此,应圣刚、李杨佳等 在[21,22]中仔细研究了量子 Markoⅴ链及量子自动机的可达性。 值得一提的是, Markov链的可达性分析往往归结为图论中的相应问 题。但这些图论工具并不适用于量子 Markov链,因此作为量子 Markoⅴ链可达性分析所需的数学工具,文[21]初步建立了一种 Hilbert空间中的新图论。这种新的图论本身似乎就很值得研究。 Perdriⅸ与 Jorrand[23,24]将抽象解释( abstract interpretation) 技术引入量子程序分析,特别是程序中的纠缠及其演化的分析 Honda[25]进一步地分析了可用 stabilizer formalism描述的这一类 特殊量子程序中的纠缠。量子程序中的纠缠分析看来是一个重要的 问题,但文[冂]与[23,24,25]中的工作还是非常初步的,希望有 更加深刻的研究 五,量子程序的验证

在量子程序的最弱前置条件语义的研究中，早在 2006 年 D’Hondt 与 Panangaden［17］就提出了将量子谓词定义为本征值在单位区间 中的物理可观测量（Hermitian 算子）。这是一个一旦说出来以后大 家都觉得极其简单的想法，但对于进一步的发展却很重要。文［18］ 考虑了一类特殊的量子谓词－投影算子，从而使得量子逻辑中发展 起来的一些方法可应用于量子程序的谓词转换器语义。需要特别指 出的是，量子程序最弱前置条件语义的研究中存在着一个特有（经 典程序所没有）的困难：对于非交换的量子谓词（Hermitian 算子）， 其析取、合取无法定义。 四．量子程序的分析 程序分析技术在编译器设计及程序优化等方面有着重要的应用。 在 Scaffold［6］的编译器 ScaffCC［7］中已经采用了数据流分析的 一些方法，分析量子程序中的纠缠并检查是否违反不可克隆原理。 文［7］也考虑了执行时间估计的问题。 文［19］首先研究了有限维 Hilbert 空间中循环体(loop body)为 unitary 算子的量子循环程序的终止问题。文［20］将［19］中的一 些主要结果推广到循环体为一般超算子(super-operator)的情形，并考 虑了平均执行时间的问题。这项工作中采用的主要技术是超算子的 矩阵表示及 Schroedinger-Heisenberg 对称性。按照［20］提出的将量 子 Markov 链作为量子程序语义模型的想法，量子程序的终止问题可 以看作量子 Markov 链的一类可达性问题。因此，应圣刚、李杨佳等 在［21，22］中仔细研究了量子 Markov 链及量子自动机的可达性。 值得一提的是，Markov 链的可达性分析往往归结为图论中的相应问 题。但这些图论工具并不适用于量子 Markov 链，因此作为量子 Markov 链可达性分析所需的数学工具，文［21］初步建立了一种 Hilbert 空间中的新图论。这种新的图论本身似乎就很值得研究。 Perdrix 与 Jorrand［23， 24］将抽象解释（abstract interpretation） 技术引入量子程序分析，特别是程序中的纠缠及其演化的分析。 Honda［25］进一步地分析了可用 stabilizer formalism 描述的这一类 特殊量子程序中的纠缠。量子程序中的纠缠分析看来是一个重要的 问题，但文［7］与［23, 24, 25］中的工作还是非常初步的，希望有 更加深刻的研究。 五．量子程序的验证

如第三节所述,量子系统的许多特征违反人们的直觉。因此, 将来的量子程序设计员可能更容易犯错误。这就使得量子程序的验 证成为一个重要的问题。 量子程序验证研究的一个主要的方面是发展适用于量子计算的 程序逻辑。 Brunet与 Jorrand[26]提出了将 Birkhoff- von neumann 量子逻辑应用于量子程序推理的方法。Blg与 Smets[27]发展了 种可用于量子系统中信息流形式化的动态逻辑。在只允许有界迭 代的限制下, Chadha, Mateus与 Sernadas[28]给出了量子程序的 个 Floyd-Hoare型证明系统。冯元等[29]发现了关于量子程序的 些有用的推理规则。 Kakutani[30]试图将 den hartog的概率 Hoare 逻辑推广到量子情形。文[31]建立了一个真正完整的量子Floyκd Hoare逻辑,特别是证明了其(相对)完备性。至此,顺序量子程 序的逻辑基础已经建立起来了。但分布式、并发量子计算的程序逻 辑还完全处于空白状态(其重要性参见下一节)。 在量子程序验证工具方面, Anticoli[32]将 Quimper翻译到 超算子值(量子) Markov链[33,34],然后用针对这类 Markov链 的模型检测工县QPMC[35]验证。最近,中国科学院软件研究所 詹乃军教授研究组基于 Isabelle,/HOL设计实现了一个量子 Floyd Hoare逻辑定理证明器。为了提高其自动化程度,有必要硏究量子 程序不变量与 ranking函数的生成算法。有一段时间,我们甚至不懂 得如何定义量子程序的不变量。最近,我们找到了解决这个问题方 法,并将量子程序不变量生成问题转换为半正定规划( Semidefinite Programming)问题。对于 ranking函数的生成,现有的数学工具似乎 不足以解决这个问题,我们可能需要自行发展必要的数学工具,特 别是量子 martingale及 supermartingale理论, 五.量子通讯并发系统 量子通讯并发系统研究的主要动因有二。首先,普遍认为量子 通讯的实用化会比量子计算机早很多,而量子通讯并发系统的研究 可能为量子通讯协议的设计、分析与验证提供理论基础和工具。其 次,大型的量子计算机还非常遥远,但最近美国总统科学技术办公 室发布的量子信息文件预计几十个量子比特、可供早期量子计算机 科学研究的系统可望在5年内出现[36]。因此,一个自然的想法是 如何将多个小型量子计算机组成分布式系统解决经典计算机所不能 解决的问题。实际上,十多年前物理学家就已经开始研究分布式量 子计算。今年初Bl(ates[37也曾预测量子计算云服务将在十年内出

如第三节所述，量子系统的许多特征违反人们的直觉。因此， 将来的量子程序设计员可能更容易犯错误。这就使得量子程序的验 证成为一个重要的问题。 量子程序验证研究的一个主要的方面是发展适用于量子计算的 程序逻辑。Brunet 与 Jorrand［26］提出了将 Birkhoff-von Neumann 量子逻辑应用于量子程序推理的方法。Baltag 与 Smets［27］发展了 一种可用于量子系统中信息流形式化的动态逻辑。在只允许有界迭 代的限制下，Chadha, Mateus 与 Sernadas［28］给出了量子程序的一 个 Floyd-Hoare 型证明系统。冯元等［29］发现了关于量子程序的一 些有用的推理规则。Kakutani［30］试图将 den Hartog 的概率 Hoare 逻辑推广到量子情形。文［31］建立了一个真正完整的量子 Floyd￾Hoare 逻辑，特别是证明了其（相对）完备性。至此，顺序量子程 序的逻辑基础已经建立起来了。但分布式、并发量子计算的程序逻 辑还完全处于空白状态(其重要性参见下一节)。 在量子程序验证工具方面，Anticoli［32］将 Quipper 翻译到 超算子值（量子）Markov 链［33, 34］，然后用针对这类 Markov 链 的模型检测工具 QPMC［35］验证。最近，中国科学院软件研究所 詹乃军教授研究组基于 Isabelle/HOL 设计实现了一个量子 Floyd￾Hoare 逻辑定理证明器。为了提高其自动化程度，有必要研究量子 程序不变量与 ranking 函数的生成算法。有一段时间，我们甚至不懂 得如何定义量子程序的不变量。最近，我们找到了解决这个问题方 法，并将量子程序不变量生成问题转换为半正定规划(Semidefinite Programming)问题。对于 ranking 函数的生成，现有的数学工具似乎 不足以解决这个问题，我们可能需要自行发展必要的数学工具，特 别是量子 martigale 及 supermartigale 理论。 五．量子通讯并发系统 量子通讯并发系统研究的主要动因有二。首先，普遍认为量子 通讯的实用化会比量子计算机早很多，而量子通讯并发系统的研究 可能为量子通讯协议的设计、分析与验证提供理论基础和工具。其 次，大型的量子计算机还非常遥远，但最近美国总统科学技术办公 室发布的量子信息文件预计几十个量子比特、可供早期量子计算机 科学研究的系统可望在5年内出现［36］。因此，一个自然的想法是 如何将多个小型量子计算机组成分布式系统解决经典计算机所不能 解决的问题。实际上，十多年前物理学家就已经开始研究分布式量 子计算。今年初Bill Gates [37]也曾预测量子计算云服务将在十年内出

现。这样,并发问题在分布式量子程序设计中不可避免。 目前关于量子通讯并发系统的工作主要是量子进程代数及其在 量子通讯协议验证中的应用。 Errand与Iirc[38]、Gay与 Nagarajan [39、冯元等[40,41]分别定义了量子进程代数QPAg、CQP、 qCCS。一个困难的问题在于找到有纠缠的并行复合保持的互模拟 这个问题是量子情形特有的,因为在经典进程代数中没有纠缠。冯 元等在[42,43]中解决了这个问题。考虑到量子计算与通讯中量 子噪音是一个不可忽略的因素,文[41,43]还研究了量子进程的近 似互模拟。基于qCS, Kubotα[44,45]设计实现了量子密码协议验 证的软件工具。 此外,Gay等[46]、冯元等[33,35]以及文[47]将模型检 测( model-checking)技术分别推广到可用 stabilizer formalism描述的特殊 量子系统以及一般的量子系统。 Ardeshir- Larijani等[48,49]研究了 量子通讯协议的等价性检测。俞能昆等[50]考虑了公平条件 ( fairness)下并发量子程序的终止问题。目前这方面的研究尚只涉 及量子系统的一些比较简单的性质(如可达性)。如果希望分析或 验证量子程序的更复杂的性质,一个首先必须解决的问题是定义 种可以表达这些性质的时序逻辑。由于量子测量会改变量子系统的 状态,这样的时序逻辑的定义并不是一个容易的问题。事实上, 些物理学家在20多年前为了别的目的已经做过一些尝试,但并没有 完全成功。另一个重要的问題是如何验证量子性质(如纠缠)。最 近许多物理学文献讨论这个问题,但如何采用计算机科学的工具更 好地解决这个问题尚未得到考虑。 需要特别指出的是,虽然关于量子通信并发系统已经有不少 的研究工作发表,但我们对于量子纠缠、 nonlocality、 contextuality等 量子特征在这些系统中的作用与影响还没有很好的理解。 六.从“数据叠加”到“程序叠加” 前面五节中论及的量子程序研究都遵循“程序的数据流是量 子的,但控制流仍然是经典的″这样一个基本的思路。 Selinger将这 个思路总结为一句口号:“量子数据,经典控制( quantum data, classical control)”。这个思路的提出是十分自然的,也是相对来说 比较容易实现的,只需要在经典的程序设计语言中增加对于量子数 据的操作,如 unitary变换,量子测量等。 但是,人们也认识到“量子数据,经典控制”的思想并不能 最为有效地发挥量子计算特有的优势。 Altenkirch与 Grattage[51]

现。这样，并发问题在分布式量子程序设计中不可避免。 目前关于量子通讯并发系统的工作主要是量子进程代数及其在 量子通讯协议验证中的应用。Jorrand与Lalire [38]、 Gay与Nagarajan [39]、冯元等［40, 41］分别定义了量子进程代数 QPAlg、CQP、 qCCS。一个困难的问题在于找到有纠缠的并行复合保持的互模拟， 这个问题是量子情形特有的，因为在经典进程代数中没有纠缠。冯 元等在［42，43］中解决了这个问题。考虑到量子计算与通讯中量 子噪音是一个不可忽略的因素，文［41, 43］还研究了量子进程的近 似互模拟。基于qCCS, Kubota［44, 45］设计实现了量子密码协议验 证的软件工具。 此外，Gay等［46］、冯元等［33, 35］以及文［47］将模型检 测(model-checking)技术分别推广到可用stabilizer formalism描述的特殊 量子系统以及一般的量子系统。Ardeshir-Larijani等［48, 49］研究了 量子通讯协议的等价性检测。 俞能昆等［50］考虑了公平条件 （fairness）下并发量子程序的终止问题。目前这方面的研究尚只涉 及量子系统的一些比较简单的性质（如可达性）。如果希望分析或 验证量子程序的更复杂的性质，一个首先必须解决的问题是定义一 种可以表达这些性质的时序逻辑。由于量子测量会改变量子系统的 状态，这样的时序逻辑的定义并不是一个容易的问题。事实上，一 些物理学家在20多年前为了别的目的已经做过一些尝试，但并没有 完全成功。另一个重要的问题是如何验证量子性质（如纠缠）。最 近许多物理学文献讨论这个问题，但如何采用计算机科学的工具更 好地解决这个问题尚未得到考虑。 需要特别指出的是，虽然关于量子通信并发系统已经有不少 的研究工作发表，但我们对于量子纠缠、nonlocality、contextuality 等 量子特征在这些系统中的作用与影响还没有很好的理解。 六． 从“数据叠加”到“程序叠加” 前面五节中论及的量子程序研究都遵循“程序的数据流是量 子的，但控制流仍然是经典的”这样一个基本的思路。Selinger 将这 个思路总结为一句口号：“量子数据，经典控制（quantum data, classical control）”。这个思路的提出是十分自然的，也是相对来说 比较容易实现的，只需要在经典的程序设计语言中增加对于量子数 据的操作，如 unitary 变换, 量子测量等。 但是，人们也认识到“量子数据，经典控制”的思想并不能 最为有效地发挥量子计算特有的优势。Altenkirch 与 Grattage［51］