量子程序推理中的霍尔式演算

理论计算机科学电子笔记158（2006）19-39www.elsevier.com/locate/entcs关于强制量子程序的推理R. Chadha1，2P. Mateus1，3 A. Sernadas塞尔纳达斯1，4CLC，Department ofMathematicsInstitutoSuperiorT′ecnico Lisbon，Portugal摘要提出了一种用于推理基本量子命令程序状态的逻辑。 该逻辑的模型是通过将概率附加到量子态和经典态对上而得到的系综。状态逻辑是用来提供一个健全的霍尔式演算的量子命令式程序。通过证明Deutsch算法的正确性来说明微积分。保留字：量子命令程序，外生语义，霍尔逻辑。1介绍量子程序的推理在信息处理、安全、分布式系统和随机算法等领域有着巨大的应用潜力。这吸引了对量子态[34，33，24，7]和量子程序[20，31，2，11，4，32，5]的推理的研究。我们在这里提出另一种工具来推理量子程序。 这项工作是第一次尝试提供霍尔式推理的量子1由FCT和FEDER通过POCI通过QuantLog POCI/MAT/55796/2004项目提供支持。对Rohit Chadha的额外支助来自联邦贸易委员会和联邦发展局的SFRH/BPD/26137/2005号赠款。2 电子邮件地址：rchadha@math.ist.utl.pt3 电子邮件地址：pmat@math.ist.utl.pt4电子邮件地址：acs@math.ist.utl.pt1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.04.00320R. Chadha等人/理论计算机科学电子笔记158（2006）19使用定量状态逻辑的命令式程序。这方面的其他工作[5]使用传统的定性逻辑来推理量子态[8]。一个Hoare断言[17]是一个形式为{δ1}P{δ2}的三元组，如果程序P在满足δ1的状态下开始并且P停止，则P在状态满足δ2。本文中的霍尔逻辑受到动力学逻辑的启发和概率程序的Hoare逻辑[30，13，22，26，9，6]。我们使用的定量量子态逻辑允许我们对概率和振幅进行推理，而定性量子逻辑则适合于对观测的正交性进行推理。本文提出的Hoare逻辑是一种基本的量子命令程序设计语言.编程语言使用经典和量子内存。内存的经典部分是由标准的命令式编程结构操作的：赋值。存储器的量子部分由标准计算基中的酉变换和测量的通用集合操纵。为了简单起见，我们只假设一个有限的内存。我们也有其他标准的重要编程结构：顺序组合，替代组合和有界迭代。因此，终止不是问题，因为我们没有发散迭代。这种受限的编程语言足够方便地模拟几个已知的量子程序。实际上，它和电路一样，对于每个n∈N的n元全函数是计算完备的.编程语言的状态是（离散和有限支持的）经典和量子态对上的子概率分布，此后称为系综。概率分布的模型测量的结果。子概率分布对模拟备选作文是有用的.此外，如果我们像我们计划的那样，用无界迭代来增强我们的编程语言，那么子概率测度是处理随机数的自然解决方案。这也是概率程序的情况[21]。编程语言的语义是集合空间中的内映射状态逻辑是通过采用外生语义方法[29，12，25]来丰富给定的基本逻辑来设计的-丰富逻辑的模型是具有附加结构的给定基本逻辑的模型集。在我们的例子中，经典和量子记忆态（以下称为纯态）构成了基本逻辑的模型。 基本逻辑本身是[24，7]中提出的量子逻辑的变体。基本逻辑具有由实数和复数解释的术语。在这些复数项中，有一些项表示量子记忆状态的振幅。基础逻辑是由比较实项的比较公式和使用R. Chadha等人/理论计算机科学电子笔记158（2006）1921常见的命题连接词基本逻辑的公式称为纯状态公式。状 态 逻 辑 ， 以 下 简 称 为 Ensemble Exogenous Quantum PropositionalLogic（EEQPL），包含用于推理基础逻辑实项期望的项。我们对复数项没有期望，但我们可以推理复数项的实部和虚部。EEQPL中的项（称为期望项）是使用加法和乘法从这些表示期望的项构建的。有两个原子EEQPL公式（也称为期望公式）：n γ表示纯态公式γ以概率1为真，p1≤p2表示期望项p1小于期望项p2。然后，使用命题连接词和，以及条件构造/γ，从这些原子构建EEQPL公式。 公式γ/γ满足a如果通过消去不满足γ的纯态测度而得到的模型满足γ，则用公式γ/γ来处理替代成分，则用公式γ/γ来我们还给出了EEQPL的一个合理的公理化，并简单地讨论了完备性。这个逻辑是从[6]中概率程序的状态逻辑改编而来的。利用EEQPL公式给出了一个合理的Hoare逻辑。霍尔逻辑的主要贡献是以最弱前提形式给出的酉变换和度量运算度量算子公理和择一合成规则分别改编自[6]中的概率抛动公理和择一合成规则我们设想通过进一步扩展状态逻辑来实现完整的Hoare逻辑，但这超出了本文的范围本文的其余部分组织如下。第2节介绍了编程语言的语法和语义。语法，语义和一个健全的公理化的状态逻辑EEQPL是在第3节。声音霍尔逻辑在第4节中给出，并在第5节中用一个例子（Deutsch算法）加以说明。我们总结了结果和未来的工作在第6节。2强制量子程序我们介绍了一个基本的命令式量子语言与混合存储器。在内存中，我们有布尔和自然寄存器和量子位。我们还将量子比特生成为量子自然寄存器（qunits）。 请记住，量子位是 二维希尔伯特空间中的单位向量。 q单位是N维希尔伯特空间中的单位向量，其中N是2的幂。 记忆的经典部分是通过经典的命令结构来操纵的的22R. Chadha等人/理论计算机科学电子笔记158（2006）19▢ ▢▢▢ ▢▢ ▢▢ ▢ ▢ ▢ ▢ ▢▢▢▢存储器的量子部分通过幺正变换和测量算子来操纵。测量总是在固定（计算）基础上进行，结果存储在经典寄存器中。在我们介绍完整的语言之前，我们介绍签名。 我们假设一个固定大小的存储器，为此，我们定义集合M={0，.，M− 1}。我们有四种寄存器：• 布尔寄存器{bk：k∈M}在2 ={ 0， 1}中取值;• 自然寄存器{nk：k∈M}，其取值于N ={0，.，N− 1};• 量子布尔寄存器（量子位）{qbk：k∈M}，其取值于H（2）=C2的单位球中;以及• 量子自然寄存器（qunits）{qnk：k∈M}在H（N）=CN的单位球中取值。我们继续介绍编程语言的语法和语义。2.1语法我们有在集合N上解释的项表达式。这些术语，以下称为自然表达式，在BNF中定义如下：ν：=n c（ν+ν）（ν ν）其中n是自然寄存器，c∈N。我们也有布尔表达式：β：=b （ν≤ν）f t （βиβ）其中b是布尔寄存器，f和t分别对应于值0和1。对于酉变换，我们只使用一个泛集。任何酉变换都可以使用这组变换来近似。转换表达式为：U：= IX：qb X：qn（ν，ν）H：qbH：qnS：qb（ν，β）S：qn（ν，ν）（U U）（qifqbthenUelse U）（qcaseqnd 0：U，.，N−1：U）其中I是单位元，X：qb是作用于量子位qb的泡利X算子，H：qb是作用在qb上的阿达玛算子，S：qb（ν，β）是作用在qb上的移位算子，相移由ν和β参数化，如将在第2.2节中解释的。（qifqbthenU1elseU2）是qb控制的酉变换，它是控制非变换R. Chadha等人/理论计算机科学电子笔记158（2006）1923▢ ▢ ▢ ▢ ▢ ▢▢▢▢←←转型其他的酉变换是对q单位的扩展。在量子交替和量子情况表达式中，量子寄存器保护不应该在主体表达式的目标中。转换表达式的目标是一组量子位和量子单位，定义如下：• return（ I）;• return（ X）;• target（ X：qn（ν1，ν2））={qn};• return（ H：qb）={qb};• return（ H）={numerals};• target（ S：qb（v，β））={qb};• target（ S：qn（ν1，ν2））={qn};• target（U2U1）= target（U1） target（U2）;• target（（qifqbthenU1elseU0））=target（U0）<$target（U1）其中假设qb/∈target（U0）<$target（U1）;•目标（（qcase qbd0：U0，.，N−1： UN−1））=target（U0）. ∪target（U N−1）其中假设qb/∈target（U0）. 目标值（UN−1）。最后，编程语言的语句是：s：= skip b <$βn <$νU b惠qbn惠qn（s;. ;s）（ifbthens else s） （casend 0：s，.，N−1：s） （n次重复s）其中，bβ和nγ是对经典寄存器的赋值，U是酉变换表达式，b惠qb和n惠qn是量子寄存器在计算基中的测量，其值存储在所指示经典寄存器，其余语句是命令式语言的常用结构。 在替代和迭代程序中，守卫不能成为身体变化的目标，也就是说，不应该在身体中被修改。 变革的目标可以直接定义。 这样做是为了确保迭代程序总是终止，并与量子替代幺正变换保持一致。2.2语义程序被解释为集合之间的映射。直觉上，系综是纯态的（次）概率测度。纯态是一对状态，其中一部分将值分配给经典存储器，另一部分将量子态分配给量子存储器。我们现在正式定义这些定义。24R. Chadha等人/理论计算机科学电子笔记158（2006）19MHM经典赋值v是向经典存储器寄存器提供值的映射即v∈ 2 M×N M。量子估值|H=H （2M×NM） =C （ 2M×NM ） 的 单 位 向 量 。 一个 purestate 是一个pairσ=（v，|其中rev是一个经典赋值，|量子估值是一种量子估值。设k是所有纯态的集合。一个集合ρ是一个离散的子概率测度，它在有限支集上。 如果ρ（π）= 1，则称系综是正规的。我们首先定义自然表达式和布尔表达式的语义。给定一个经典赋值v，其表示归纳定义如下：• [[n]]v=v（n）;• [[c]]v=c modN;• [[ν1+ν2]]v=（[[[ν1]]v+[[ν2]]v）modN;• [[ν1ν2]]v=（[[[ν1]]v[[ν2]]v）modN;• [[b]]v=v（b）;• [[ν1≤ν2]]v=（[[[ν1]]v≤[[ν2]]v）;• [[f]v= 0;• [[t]]v= 1;• [[β1<$β2]]v=（[[[β1]]v≤[[β2]]v）。变换表达式被解释为上的酉算子，H= H（2×N）。 给定qb，H可以被视为张量积H=HqbH]qb[.空间Hqb是对应于qb的H的张量因子，并且H]qb[是对应于其余量子寄存器的H同样，我们可以定义Hqn和H]qn[。作用在H的因子HJ上的酉变换U通常用dbyUHj表示。转换X：q b被解释为XHqb和IH]qb的张量乘积[其中X是P值X操作符，I是整数。回想一下，作用在二维希尔伯特空间上的输入向量的振幅。广义P-A-uli算子Xn1n2行为在H（N）上，|n1次和|输入向量的n2次方。H：qb的变换是由HHqb的张量表示的，其中H是阿达玛算子。类似地，变换H：qn被解释为HHqn的张量形式。 其中H是Walsh-Hadamard算子.请注意，Walsh-Hadamard算子仅当N是2的幂时才在H（N）相移变换Sθd（2）使基的振幅元件|d × e2π/θH.转型S：qb（ν，β）被解释为aSθd的张量积Hqb [1]qb[其中θ是ν的解释，d是β的解释。它对qunit的推广是显而易见的。此外，委员会认为，由于ρ是一个离散测度，我们经常会将ρ（{σ}）与ρ（σ）混淆，因为ρ是唯一的，R. Chadha等人/理论计算机科学电子笔记158（2006）1925⊗DD[[β]]v[[v]]v12H[[qn]]vH][[qn]]v[12H[[qn]]vH][[qn]]v[由它的质点决定最后，回顾量子交替的概念[28]。给定作用在H上的酉变换U0和U1]qb[，我们用qbcontrolled（qb，U1，U0）表示作用在H上的酉变换，使得：• 01- 02|0⟩⊗|ψ⟩)=|联系我们|- --• 01-02|1⟩⊗|ψ⟩) =|1张图片U1|好吧类似地，我们引入qncontrolled（qn，U0，. ，UN−1）：• qncontrolled（qn，U0，. ，UN−1）（|0⟩⊗|ψ⟩)=|联系我们|- --• ...• qncontrolled（qn，U0，. ，UN−1）（|N − 1|ψ⟩)= |N − 1UN−1|好吧形式上，给定一个经典赋值v，变换表达式的表示如下：• [[I]]v=IH;• [[X：qb]]v=XH[[qb]]vIH][[qb]]v[;• [[X：qn（ν，ν）]]=X[[ν1]]v[[ν2]]v<$I;• [[H：qb]]v=HH[[qb]]vIH][[qb]]v[;• [[H：qn]]v=HH[[qn]]vIH][[qn]]v[;• [[S：qb（ν，β）]]v=S[[ν]]v[[β]]vIH[[qb]]vH][[qb]]v[;• [[S：qn（ν，ν）]]=S[[ν1]]v[[ν2]]v<$I;• [[U2U1]]v=[[U2]]v[[U1]]v;• [[(qifqbthenU1elseU2）]]v=qb控制d（qb，（[[U1]]v）H]qb[，（[[U2]]v）H]qb[）;• [[(qcaseqnd 0：U0，.，N− 1：UN−1）]] v =qn控制器d（qn，（[[U0]]v）H]qn[， .. . ，（[[UN−1]]v）H]qn[）.证明了对于U上的任意变换，[[U]]v=IH]target（U）[UJ其中UJ作用于H目标（U）。在提供程序语句的语义之前，我们需要一些辅助符号给我们一个经典的评价，我们不应该被vbk所取代。价值，与v一致的求值，除了返回d的bk。类似地，我们引入vnk。首先，我们看到了下面的一幅内部地图：• ηbk←β（v，|ψ⟩)=(vbk• ηnk←ν（v，|（vnk）vv26R. Chadha等人/理论计算机科学电子笔记158（2006）19、|ψ⟩);、|ψ⟩);• ηU（v，|（v，[[U]] v |ψ>）。R. Chadha等人/理论计算机科学电子笔记158（2006）1927∈0⎡⎪⎪1⎡0⎪12⎡⎪ǁ| ⟩ ǁΣσ∈Σ⎡我不知道你在说什么⎪⎪|1⟩对于d2，我们表示为byPqbk|d从H到它的子空间通过对空间资源的扩展或预处理，|dwithH]q bk[. 类似地，weint rotPqnk|d对于d∈N.有了这些投影仪，我们就能够定义下面的映射给出了一个纯态返回一个系综：BK2vJ=vbk1⎢qbk|0⟩CUP|0⟩|吉吉夫P|0⟩2|ψ⟩• （δbk1惠q bk2（v，|）（vJ，|J⎪qbk2|ψ⟩ǁ|ψ⟩ǁvJ=vbk1qbkCUP|1⟩|吉吉夫P|1⟩2|ψ⟩|ψ⟩ǁ|ψ⟩ǁ⎪qbk2vJ=vbk1⎢qbk|0⟩CUP|0⟩|吉吉夫P|0⟩2|ψ⟩• （δnk惠q nk（v，|）（vJ，|J.克|ψ⟩ǁ|ψ⟩ǁvJ=vbk1N−1| ⟩qb2qbkCUP|N−1|ψ⟩ǁ if⎪⎣|JP|N2ψ−1⟩我不知道你在说什么Pqbk2|N−1⟩最后，我们引入一些符号来表示对系综的限制• 对于d ∈ 2，ρ|b：d是ρ 的子度量，定义如下：ρ|b：d（v，|ψ⟩)=ρ（v，|如果v（b）= d;且ρ|b：d（v，|否则为0;• 类似地，对于d∈N，ρ|n：d如下：|n：d（v，|ρ（v，|n）如果v（n）= d;和|n：d（v，|否则为0。一个陈述s的指称是集合上的一个endo-map[[[s]]]，归纳定义如下：• [[skip]]（ρ）=ρ;• [[bk<$β]]（ρ）=ρ（ηbk<$β）−1;• [[nk<$v]]（ρ）=ρ（ηnk<$v）−1;• [[U]]（ρ）=ρ（ηU）−1;• [[b惠qb]]（ρ）=• [[n惠qn]]（ρ）=<$σ∈<$ρ（σ）δbk1惠qbk2（σ）;ρ（σ）δnk1惠qnk2（σ）;28R. Chadha等人/理论计算机科学电子笔记158（2006）19||d=0时×▢▢我的d=0时• [[第1条;...... ; sm]]（ρ）=[[[sm]]（. （[[s1]]（ρ））. ）的情况下;• [[（ifbthens1elses0）]]（ρ）=[[s1]]（ρb：1）+[[s0]]（ρb：0）;• [[（casend0：s0，.，N−1：sN−1）]]（ρ）=<$N−1[[sd]]（ρ|n：d）;• [[(n重复s）]]（ρ）=<$N −1[[s]] d（ρ|n：d）。3系综逻辑我们现在介绍逻辑推理有关合奏，我们的编程语言的状态该逻辑是通过采用外生语义学方法丰富量子逻辑[24]而构建的。[24]中的量子逻辑模型是量子赋值。首先，我们丰富了量子逻辑来解释经典寄存器。因此，我们有一个逻辑来推理纯态。然后，我们的逻辑的语义模型外生地获得通过采取（子）纯状态的概率措施。我们将我们的逻辑称为外生量子命题逻辑（EEQPL）。3.1语法语言的句法有两个层次，一个层次是关于纯状态的推理，另一个层次是关于集合的推理。我们首先给出了逻辑的语法来推理纯态。该语法使用两种术语，实数和复数术语，它们采用实数和复数形式的值。复数项还将包括表示量子估值的幅度的项。为此，我们从定义赋值项开始，它指定H=H（2MNM）的计算基的基元素赋值是赋值约束的列表，其指定了基元素中所有寄存器的值。BNF形式的赋值约束的语法是：ω：= qb：2 qn：Nω，.， ω。赋值项是指定所有量子寄存器（M个量子位和M个量子单元）的值的赋值约束。基本元件ω的振幅由振幅项ωω表示|t.实际条件的范围是1001，... 你... 而复数项的范围为1，... 你... .实数和复数项的语法由以下BNF给出：：= r |ζ|：=（|t/（+）（）（β D;）R. Chadha等人/理论计算机科学电子笔记158（2006）1929Øи▢ ▢ ▢| ⟩▢ ▢▢▢ ▢ ▢▢条件是ω是赋值项，r是计算实常数。这些术语大多数是不言自明的。唯一需要解释的项是替代项（β D1;2）。 如果β为真，则该项的计算结果为1，否则为2纯状态公式的集合是由布尔表达式β和比较公式（≤）使用命题连接词（f和и）构建的：γ：= β （β ≤ β） f（γи γ）。如果纯态的经典赋值为1，则布尔表达式β为真。其他公式的解释与预期一致。像往常一样，其他经典的连接词（，H，H，）作为缩写引入。例如，（γ）表示（γ（f）。对于集合公式的语法，我们使用关于期望值的推理的术语。特别地，我们有项（d γ），它表示γ诱导的子概率测度上的的期望值（即，，通过消除γ不满足的部分上的测量）。期望项的集合由下式给出：p：= r （ρ d γ）（p + p）（p p）.系综公式是由必要性公式（δ/γ）、条件公式（δ/γ）和比较公式（p≤p）利用命题连接（δ/γ和 δ/γ）建立的δ：=（δ/γ）（p ≤ p）δ/ （δ/δ）。必要性公式（δγ）成立的条件是γ在概率为1的情况下为真，条件a公式（δ/γ）成立的条件是它在由γ导出的次概率测度上为真，其它公式的解释也如预期的那样。 请注意，（γ）不是一个模态（例如，我们没有公式（（γ）。为了简单起见，我们选择将概率与可能性混淆。可以像[25，6]中那样保持这种区别。像往常一样，其他经典的连接词（g，）作为缩写引入。例如，（gγ）代表（γ）。3.2语义我们准备给出语言的精确语义我们首先定义实项和复项的语义，以及纯态公式。给定一个纯态σ=（v，n），复项和实项的表示以及纯态公式如下：30R. Chadha等人/理论计算机科学电子笔记158（2006）19⎨Σ=σvγ• [[r]]σ=r;• [[v]]（v，|[v] v;• [[1+2]]σ=[[1]]σ+[[2]]σ;• [[<$1<$2]]σ=[[<$1]]σ[[<$2]]σ;• [[Re]]σ=Re[[]]σ;• [[Im]]σ=Im[[]]σ;• [[Arg]]σ=Arg[[]]σ;• [[|ζ|]]σ=|[[]]σ|;• [[<$1+i<$2]]σ=[[<$1]]σ+i[[<$2]]σ;• [[1ei2]]σ=[[1]]σei[[2]]σ;• [[ω|t]]σ=[[ω]]|- --• [[1+2]]σ=[[1]]σ+[[2]]σ;• [[<$1<$2]]σ=[[<$1]]σ[[<$2]]σ;• [[(βD β1; β2）]]（v，|（掌声）[[1]] if[[[β]] = 1;[[• [[β]]（v，|[[β]]v;• [[<$1≤<$2]]σ=（[<[<[<$1]]σ≤[[<$2]]σ）;• [[f]]σ= 0;• [[γ1<$γ2]]σ=（[[[γ1]]σ≤[[γ2]]σ）。对于系综公式的语义，我们需要定义由纯态公式γ导出的测度。给定系综ρ和纯态公式γ，由γ诱导的测度ργ是ρ的子测度，使得如果[ γ ]] σ = 1，则ρ（σ）=<$ρ（σ）。0.00否则最后，给定系综ρ，期望项和系综公式的表示如下：• [[r]]p=r;• [[（ [σd γ）]]ρ =σ∈ε[[σ]]σργ（σ）;• [[p1+p2]]ρ=[[p1]]ρ+[[p2]]ρ;• [[p1p2]]ρ=[[p1]]ρ[[p2]]ρ;• [[([（dγ）]]ρ=（[[[（1 dγ）]]ρ=ρ（n））;R. Chadha等人/理论计算机科学电子笔记158（2006）1931a：= x <$r <$（a +a）<$（aa）。→∈• [[（δ/γ）]]ρ=[[δ]]ργ;• [[p1≤p2]]ρ=（[[p1]]ρ≤[[p2]]ρ）;• [[numb]]numb=0;• [[δ1<$δ2]]ρ=（[[[δ1]ρ≤[[δ2]]ρ）。3.3公理化公理化需要三个新概念，一个是期望重言式，第二个是有效的分析公式和基替换，第三个是有效的纯态公式。考虑使用经典连接词和→从一组可数的命题符号Q构建的命题公式。期望公式δ称为期望重言式，如果存在Q上的命题重言式ε和从Q到期望状态公式集的映射χ，使得δ与εχ重合，其中εχ是通过将所有出现的ε替换为ε，→替换为ε，q∈Q替换为χ（q）而从ε例如，期望公式（（y1≤y2）<$（y1≤y2））是重言式的（例如，从命题重言式q→q）。现在，假设一个可数的变量集X={xk：k∈N}，并考虑从X构建的以下公式集：κ：=（a≤a）（κκ）我们将把这种语言的公式称为分析公式。分析公式是在实数上解释的，为此我们需要给逻辑变量x k赋值。我们说映射u：XR是一个赋值。在给定赋值u的情况下，解析公式κ的解释是直接的.我们说一个解析公式κ是有效的，如果它对每个赋值u都有效。 一个基替换σ是从变量X的集合映射到期望项的集合。然后，可以将替换σ从解析公式集合（归纳地）扩展到期望公式集合如果一个纯态公式γ对所有纯态都成立，则称它成立ρρ我们将不讨论有效状态公式的公理化，尽管通过修改[24，7]中的公理化可以得到完整的递归公理化。EEQPL的公理和推理规则在表1中列出，在下面的组中可以更好地理解。公理ETaut说预期重言式是公理。以来32R. Chadha等人/理论计算机科学电子笔记158（2006）19H[FAdd]（d（γHγ））=0）12►ⓈH HHH12 121 23 4 56 78910111213141516171819 19 1HH ≤≤1 2 12（dγ1）（∅（γ1Hγ））公理[ETaut]对于每个期望重言式δ，[Oracle]其中κ是有效的分析公式，而σ是一个基取代。[Meas]（（Hdf）= 0）（1）（？） （1）A（ （dγ））[2019 -01 - 22]（ （γи γ））（（ 1dγ）（ 1 dγ）[2019 -02 - 13]（（γи（）（（dγ）（（dγ））[Lin]n（（H（r1< $1+r 2< $2）dγ）=（r 1（H< $1dγ）+r 2（H< $2dγ）[QTaut]γ对于每个有效的纯态公式[ElimNec]<$$>γ<$（（H1 dγ）=（H1dt））[Dist]（δ1δ 2）/γ）（（δ 1/γ）（δ 2/γ）[ElimCond]<$（p1≤p2）/γ）<$（（p1≤ p2））|H ））推理规则[PMP]δ1，（δ 1<$δ 2）<$δ 2[Cond]δ/γwheneverδ表1由于概率重言式集合是递归的，所以没有必要详细说明重言式推理的细节。Oracle公理说，如果κ是一个有效的解析公式，σ是一个基替换，那么σ（κ）是一个有效的EEQPL公式。 公理Ora- cle是有争议的，因为有效的分析公式的集合不是递归的。如果我们在任意实闭域而不是实数中工作，则递归公理化是可能的。然而，这超出了本文的范围。公理Meas说空集的概率是0。 FAdd的ax-iom是概率的有限可加性的结果。Mon 1公理是概率单调性的一个结果。Mon 2公理是期望的单调性，Lin公理是期望的线性性。5例如，两个计算实数的相等是不可判定的R. Chadha等人/理论计算机科学电子笔记158（2006）1933⊃⊃由（对于每个经典状态公式γ1，公理QTaut将纯态公式与期望公式联系起来。请注意，由于有效纯公式的集合也是不可递归的，这也类似于公理Oracle。然而，如果我们处理代数闭域，我们可以实现递归公理化[7]。公理ElimNec允许我们将必然性公式重写为比较公式，因此它就像一个消元规则。公理Dist说连接词分布在条件结构上。公理ElimCond消除了条件构造。期望项（p≤p）|（H dγ1）1 2（Hd（γ1Hγ））在E中，limCond是通过替换所有出现的（dγ1）而推理规则PMP是期望蕴涵的肯定前件式推理规则Cond说，如果λ是一个定理，那么λ/γ也是。这种推理规则对于证明等价元定理是有用的，并且类似于模态逻辑中的推广规则通常，我们说一组（可能是无限的）公式Γ导出γ，记作Γδ，如果我们可以用Γ中的公式作为假设，从公理和推理规则建立δ 请注意，在应用Cond规则时，我们只允许使用逻辑定理（而不是任何假设或推导中的任何中间步骤）。 上述的一套公理和规则是合理的：定理3.1EEQPL是合理的。请 注 意 ， 我 们 还 可 以 证 明 ， 作 为 消 元 规 则 （ ElimNec 和ElimCond）的结果，每个期望公式δ等价于一个公式η，而没有任何必要性和条件子公式。如果我们假设实值和复值的集合在一个有限集合上变化，那么上述公理和规则的集合将是弱完备的。这种限制足以推理大量的量子程序和协议。这种限制的EEQPL的弱完备性的证明遵循[24，7，6]的风格，但超出了本文的范围。在没有这个限制的情况下，这个公理化的完备性然而，在概率逻辑的背景下，以前的工作[1]暗示递归公理化可能是不可能的。34R. Chadha等人/理论计算机科学电子笔记158（2006）19▢|⟨|⟩⟨|⟩⟨|⟩⟨|⟩22224量子霍尔逻辑我们准备好定义霍尔逻辑。像往常一样，霍尔的断言是：θ：= δ {δ}s {δ}。霍尔断言的满足被定义为：• ρuDδi[[[δ]]uρ=1;• 当ρ u D δ 1时，ρuD {δ1} s {δ2} i <$（[[s]]u（ρ））u D δ2。语义蕴涵如预期的那样定义。4.1公理化下面定义了我们量子编程语言的一个合理的霍尔演算。我们在下面讨论公理和推理规则。公理。跳过和分配的规则是标准的。有趣的公理是酉变换（UNIT）和测量（MEASB）。一元变换酉变换的公理类似于同时赋值，其中根据酉变换将幅度项更新为新的幅度项。为了简单起见，我们只给出了量子比特上的酉算子的公理，而q单位上的酉算子的公理也可以类似地得到。请注意，在酉变换（UNIT）规则中，δ⟨ω|tU ω|t 是通过替换每个振幅的每次出现而获得的公式termωt 通过 Uωt 其中振幅项 Uωt由归纳法定义关于U为了简洁起见，我们在这里考虑的基本情况下，其中U是阿达玛和相移算子。对于Hadamard算子（H：qb），振幅项（H：qb）ωt定义为：• n（H：qb）（ω1（qb：0）ω2）|t=<$1<$ω1（qb：0）ω2|t<$1+<$1<$ω1（qb：1）ω2|t• n（H：qb）（ω1（qb：1）ω2）|t=<$1<$ω1（qb：0）ω2|t< $ −<$1<$ω1（qb：1）ω2|t对于相移算子（S：qb（ν，β））和ω包含（qb：0）的情况，振幅项ω（S：qb（ν，β））ω|t定义为：• n（S：qb（v，β））（ω1（qb：0）ω2）|特蒂斯R. Chadha等人/理论计算机科学电子笔记158（2006）1935βν1HHη|01b，qb由期望项mb，qb（ n（dγ））+mb，qb（（ 其中，B、B、C、C、D、D、E、E、（？dγ））和mb，qb（（（d））定义如下。• b = 0，b = 0，c = 0，b = 0，b= 0，c =0， d（γ））=（pqbmb，qb（γ）d（mb，qb（γ））√1010（（ωβ）H（ν = 0））D e i2π/1π（ω1（qb：0）ω2）|t（ωβ）H（v = 1））D e i2π/2<$（ω1（qb：0）ω2）|t...（β）H（ν =（N − 1）D e i2π/N<$（ω1（qb：0）ω2）|t（ω1（qb：0）ω2））. ））ω包含（qb：1）的情况类似。测量. 测量公理（MEASB）的灵感来自于概率投掷公理[6]。测量就像一个概率分配：它以一定的概率将被测量的量子比特设置为1的公式δb是通过将每次出现的b替换为β而获得的公式，公式δn是把n的每一次出现都换成ν而得到的公式。为了简单起见，我们只给出了量子比特上的度量公理在MEASB中首先要注意的是，我们只考虑公式η，而不考虑必要性和条件子公式。这不是一个限制，因为每个EEQPL公式都等效于一个这样的公式（见第3.3节）。同样在规则中，公式（γ）b =0，b =0，c =0，b =0，b=0，c=0，（dγ））+mb，qb（（H（dγ））是公式，其中每个期望项（dγ）的每次出现都是定义项mb，qb（（dγ））以处理（概率）情况其中量子位QB的测量结果为1。该定义使用了三个辅助定义：pqb，mb，qb（γ）和mb，qb（γ）。直觉上，pqb是问题所在，1 1 1 1测量的能力产生1。 如果测量结果为1，则比特b被设置为0并且幅度项被重新归一化。项mb，qb（γ）和mb，qb（γ）相互递归地定义以处理这个问题。1 1“分配”。从形式上讲，1 1 1 1• m1（b）=t;b， qb• m1（ω1（qb：0）ω2|return 0;b，qbmb，qb（ω1（qb：1）ω2|t）• m1（ω1（qb：1）ω2|（1）=1;p1QB36R. Chadha等人/理论计算机科学电子笔记158（2006）19βν►{1}|1睿的2简洁。m=0（0公理[TAUT]δifδ is a EEQPL重言式;[SKIP]{δ}skip{δ};[ASGB]<${δb}b<$β{δ};[ASGR]<${δn}n<$v{δ};[UNIT]δ（ω|t（UHω|t1}U{δ}[ME ASB]{η|（γ）}b优惠mb，qb（（H<$dγ））+mb，qb（（H<$dγ））推理规则[SEQ]{δ0}s1{δ1}，{δ1}s2{δ2}{δ0}s1;s2{δ2}[IF]{η0}s1;b←t{η2}{η1}s2;b<$f{η3}<${η0Ybη1}（ifbthens1elses2）{η2Ybη3};[CONS]δ0<$δ1，{δ1}s{δ2}，δ2<$δ3<$ {δ1}s{δ3};[OR]{δ0}s{δ2}，{δ1}s{δ2}{δ0<$δ1}s{δ2};[AND]{δ0}s{δ1}，{δ0}s{δ2}{δ0}s{δ1<$δ2}• pqb=0表2|t|其中，如果ω = ω 1（qb：1）ω 2且0，则ω ↓ qb = 1，否则-|where ω ↓qb = 1 if ω = ω1(qb: 1) ω2and 0 other-我们刚刚给出了mb，qb（γ）和mb，qb（γ）的基本情况，1 1b，qb推理规则。推理规则Seq、CONS、OR和AND是标准的。替代构造的推断规则IF（ifbthen. 别的... ）的启发来自于[6]中的替代构造的推理规则。请注意，在推理规则IF中，我们只考虑公式，没有任何必要，条件子公式。此外，式ηYbηJ是式（（η/b）（ηJ/b））的缩写。我们还没有给出交替构造情况和迭代构造重复的规则。构造case可以用替换构造if写成聚焦变量。迭代结构repeat反过来可以使用结构case和顺序组合写成缩写。ω：ω↓qb=1（d））可以类似地定义。R. Chadha等人/理论计算机科学电子笔记158（2006）193721|⟩Hoare演算的可靠性证明紧密遵循[6]中关于概率规划的证明。唯一有趣的情况是测量公理和if-then-else构造。测量公理的可靠性可以通过调整[6]中的概率抛公理的证明来证明，对于替代构造也是如此。定理4.1霍尔演算是可靠的。5样例我们用一个例子来说明我们的演算，Deutsch算法。Deutsch算法 Deutsch算法[10]的目的是检查具有一个输入位b的布尔函数f是否为常数。传统上，它涉及在两个不同的输入上计算f，并检查结果是否相同。在量子中，我们只需要f的一个求值以及两个辅助量子和一个由下式构造的幺正变换Uf，F.幺正变换Uf作用于两个量子比特，并将计算基元|x，y= 0 |x，y<$f（x）<$.假设两个量子位qb1和qb2，我们的编程语言中的Deutsch算法D可以写为：D=df（H：qb）;（H：qb）;Uf：（qb1，qb2）;（H：qb1）;b惠qb1最初，量子位处于状态0， 1。在Deutsch算法的末尾，b位告诉函数是否为常数。 如果0，则函数为常数，否则为非常数。因此，如果你假设我们在EEQPL中有函数符号f，那么我们必须证明{（qb1：0，qb2：1）|t= 1（f（0）= f（1））} D {（b = 0）}和{（qb1：0，qb2：1）|t= 1（f（0）/= f（1））} D {（b = 1）}.为了简洁起见，我们只展示f（0）=f（1）= 1的情况下的第一个目标 我们可以添加函数符号f，也可以添加我们语言中的酉变换Uf然而，为了避免繁琐的方法，我们将在前提条件中避免f（0）= f（1）= 1，并扩展<$Uω的定义|在哪里• Uf（qb1：0，qb2：0）|t= qb1：0，qb2：1）|t t;38R. Chadha等人/理论计算机科学电子笔记158（2006）19⟨|⟩⟨|⟩H.H.010222二、{（（Hpqb1d（0 = 0））+（Hpqb1d（1 = 0）=（H1 d（t）}(((Hpqb1d（0 = 0））+（Hpqb1d（1 = 0）=（H1 d（t）TAUT0五、{ 0}{1}（|⟨ 00 |t+10|t|2个以上|⟨ 01|t+11|t|2））= 1}• Uf（qb1：0，qb2：1）|t= qb1：0，qb2：0）|t.qb1：1出现在振幅项中的情况很容易定义。因此，我们将只说明判断：{（qb1：0，qb2：1 |t= 1）}D{（（b = 0））}.在证明中，我们将qb1：x，qb2：yt表示为xyt.还请记住第4节中定义的特殊术语spq b1和pq b1。1 01 .一、 （ （b= 0））（（ 1 d（b = 0））=（1 d（t））TAUT03 .第三章。（pqb1=1）b惠qb1{（（H1 d（b= 0））=（H1 d（t）}MEASB0四、{（pqb1= 1）}b优惠qb2{（（H1 d（b= 0））=（H1 d（t）））}条件：3，2四分卫1H：qb1{（p= 1）}单位六、{ 0}{1}（|⟨01|t+11|t|2个以上|⟨00|t+10|t|2））= 1}Uf：（qb，qb）{（pqb1=