论文部分内容阅读
近年来,突破传统计算领域种种束缚的量子计算,越来越受到人们关注。一方面,随着电子器件越做越小,其功能开始受到量子效应的干扰,致使传统计算机的能力无法继续保持如Moore定律描述的那般高速增长。而基于量子效应的量子计算设备,有望解决这一难题。另一方面,量子计算机模型向强Church-Turing论题提出了重大挑战:存在某些量子算法不能用Turing机有效地模拟。越来越多的人相信,量子计算比经典计算具有更强的计算能力。因此,对量子计算的研究具有非常重要的意义。
量子程序设计语言是量子计算领域的重要研究课题。设计和实现通用量子计算机上的高级程序设计语言,是一件非常有意义的工作。它可以用于验证量子算法的正确性,探求通用量子计算机的可行性,也有助于深化对量子力学中许多问题的理解。对量子程序设计语言的研究主要集中有3个方向:语言设计、处理系统实现以及形式语义。
2006年,本文作者参与设计、实现了量子程序设计语言NDQJava。NDQJava语言是国内首个量子程序设计语言,具有严谨、简明、实用等良好性质,对量子程序设计领域以及量子计算其他领域都有推动作用。
作为NDQJava语言的后继工作,本文的工作重点是研究其形式语义,尝试对各量子成分的含义作系统化、形式化地描述。选取指称语义来描述NDQJava语言的主要原因是:与其他形式语义(如操作语义、公理语义)相比,指称语义更加严谨、清晰和易懂。本文的工作主要包括以下几个方面:
1.修订了NDQJava语言:上一版本的NDQJava中存在关键词缺失,分隔符不统一等缺憾,本文对此作了修正和完善,使语言变的更加严谨;本文还用结构归纳法,重新NDQJava语法:这种描述比BNF定义的语法有更强的逻辑性和更好的数学性质,有利于在此基础上构造数学对象(即“指称”),进而给出语言的指称语义。
2.自底向上地构造了NDQJava语言各量子成分的指称语义:“自底向上”体现了指称语义中一个重要原则“语义应当是复合性的”,即程序段的指称应当建立在其子段指称的基础上;本文寻找到描述复杂的量子表达式适当的途径:以λ项来简化酉操作复杂的语义,以值-状态有序对来描述量子操作的副作用;本文还攻克了二个技术难点:如何确定量子类型的指称对象以及怎样在指称语义中体现量子测量的非确定性。
3.分析了一个典型的量子程序的执行过程:初化、酉操作、测量,正确描述了量子系统在这一过程中状态演化;同时还利用定义的指称语义证明了这一量子非确定程序的正确性。
理论和实践充分说明,本文给出的指称语义可以清晰、正确地描述NDQJava语言程序的含义,证明量子程序的正确性。它对其他量子语言的语义研究有借鉴价值,进而对量子程序设计语言乃至整个量子计算研究领域也有促进作用。