量子数据：简单类型λ演算的博弈语义和量子编程的可靠性结果

理论计算机科学电子笔记270（1）（2011）41-57www.elsevier.com/locate/entcs量子数据Yannick Delbecquea，1，2加拿大蒙特利尔麦吉尔大学计算机科学学院摘要本文提出了一个简单类型λ演算的博弈语义，它具有qbits常数和相关的量子操作。由此产生的语言表达能力足以编码任何量子电路。该语言使用扩展变量的概念，类似于具有模式匹配的函数式语言，但适应于处理张量积的需要。博弈语义是从经典的博弈语义构建的，使用量子干预作为问题，测量结果作为答案。给出了语义的可靠性结果关键词：游戏语义，量子编程语言，量子游戏。1引言高阶量子编程语言开发中的一个重要问题是找到一个合适的结构来定义指称语义。以前的量子λ演算工作是基于量子数据应该线性使用的想法，因为它不能被复制。这个想法是通过添加量子张量类型操作和禁止重复的类型规则来实现的这种方法看起来很自然，但经典-量子相互作用的行为往往是违反直觉的，这使得构建适当的语法和类型规则变得困难。由于无法为完整的量子λ演算找到指称语义，我们仍然缺乏一个完整语言的可靠性结果来验证所做的选择例如，在Selinger和Valiron [14，16]开发的量子λ演算的第一次介绍中没有给出指称他们在[15]中提出了量子λ-演算线性部分的指称语义;他们的解释是在有限维希尔伯特空间上的完全正映射使用此受限1这项研究得到了NSERC（加拿大）2电子邮件地址：yannick@delbecque.org1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.01.00542Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）语言允许他们避免找到一个结构的问题，该结构可以完全模拟高阶量子编程语言中量子数据和经典数据之间可能的相互作用。本文提出了一种新的λ演算，它具有额外的结构，使之能够表示量子数据的处理所提出的语言的目标是使用指称语义来证明可靠性，在指称语义中，量子状态和操作被表示为策略，该策略使一些人根据量子力学定律选择动作。我们提出的模型是建立在游戏语义的思想与量子策略，描述量子状态和量子操作的行为我们在本文中定义的语言引入了新的特征和思想。也许其中最重要的一个是，我们禁止抽象的一部分张量的未知qbit的形式xy。这是由于抽象应该使用qbit类型的程序之间的对应关系直观地解释这一事实。qbit和 qbit类型的（qbitqbit=qbit）。这似乎是有问题的，因为这应该是具有两个输入qbit的函数之间的对应关系，这可能处于某种纠缠态，而函数只使用分离的qbit。这样做的结果是，在所提出的语言中没有张量类型操作，只有n个 qbit的类型qbitn我们使用扩展变量，这是变量的张量，以跟踪量子比特变量之间可能的纠缠。最后，该模型迫使我们区分已知和未知qbit的张量，从而导致张量操作的三种不同类型的规则。2具有量子数据的2.1语法我们现在介绍一个量子数据语言（QDL）的λ-演算。QDL的语法是经典的简单类型λ演算，带有配对和条件，具有额外的结构，使语言具有足够的表达能力来编码量子数据的通常操作，可以用量子电路的低级形式描述首先，我们需要引入一种语法，它允许我们在张量积中引用特定的qbit。 一个扩展变量是一个形式为x1<$··<$xn的表达式，其中xi是变量使得xixj如果ij。 两个扩展变量x1<$···<$xn和y1<$···<$ym是不相交的，如果对于所有i，j，xi/=yj。两个这样的扩展变量可以连接形成一个新的扩展变量x1···xny1···ym。请注意，当我们使用x1<$··<$xn来引用任意扩展变量时，n = 1的情况也是可能的。 为了简化符号，我们使用x代替x1<$··<$xn，使数字n隐式。Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）432×⇒表1 QDL分型规则。Γ， Δ，x：Ax：AΓ，Δ0：bool Γ，Δ 1：boolΓ， Δ，x：AM：Bτ，Δ λx。 M：A/BΓ， Δ1<$M：A<$BΓ， Δ2<$N：AΓ， Δ1， Δ2MN：BΓ， Δ1<$M1：A1Γ，Δ2<$M2：A2Γ， Δ1， Δ2均为M1，M2均为A1×A2Γ， ΔΣM：A×BΓ，ΔfstM：AΓ， ΔΣM：A×BΓ， Δλ和M：AΓ， Δ1P：布尔Γ， Δ2M：AΓ， Δ2N：A卢恩r， Δ1， Δ2，如果P则M，否则N：Ar， Δ 2，如果P则M，Γ， Δ1<$Q：qbit<$（n+1）Γ， Δ2，b：bool，x：qbitn<$M：Ar， Δ1， Δ2，b，x=measiQinM：AΓ，ΔM：qbitn Γ，Δ UM：qbitnΓ，ΔQ：qbitnΓ， Δ1M1：qbitnΓ， Δ2M2：qbitmΓ， ΔλmeasQ：boolΓ、Δ1、 Δ2► M1 M：qbit|Δi|=r， Δ1，x1：qbitnM1：qbitnr2， Δ2，x2：qbitnΓ， Δ，Δ，xx：qbitM：qbit| Δ i|={xi}1 21 2 1 2r， Δ1，x：qbitnM1：qbitnM1nM1：qbitnM2：qbit n M 2：qbit n M 1：qbitn M2：qbitnM1：FV（M1）\|Δ 1|={x1}FV（M2）|Δ 2|=QDL的术语递归定义如下：M、N、P：= x| ∗ |0 |1 |ρ|南卡罗来纳州|fstM|sndM|MN| λ x。M|如果M则N，否则P|设b，x = measiM in N|测量Q|嗯，其中b、x、y是如上定义的扩展变量，i >0是自然数， ρ可以是任何密度矩阵，U是对应于酉变换U的超算子。大多数语法由标准的λ演算操作组成项UM是对应于将酉变换应用于由项M描述的状态的操作。测量操作语法letb，x=measiMinN意味着项M的qbiti被测量，并且此后测量结果在N中可作为b访问，并且所得状态可作为X. 注意，变量b和x在N中是有界的。 为了测量单个qbit，我们使用更简单的语法measQ。M中的自由变量集记为FV（M）。QDL的类型如下：A，B：= bool|不|Qbit_n|A×B|一个大的。其中n >0。 类型bool是布尔常量的类型，AB和AB分别是对和函数的类型。类型qbitn是n个qbit上的量子态记法qbit<$n隐式地代表乘积qbit<$··<$ qbit;我们使用记法qbit<$n<$ qbit<$m来表示qbit<$（n+m），尽管这里没有n类型的运算。QDL的分型规则见表1。我们假设上下文Γ包含44Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）√表2QDL概率缩减。Mpλx. M ′N qVM1 p V1M2q V2VVMNpqM[V/x]MpV1，V2第一次世界大战V1Pp0MqVifP thenM elseNpqVΣM1，M2MpV1，V2第二代M-2000Pp1NqifP thenM elseNpqVΣQ<$qρMb/m，x/1[m] ρ [m]< $rV.Σpm设b，x=measiQinMpmqrVQqρ。pm= trΣ[m]iρ ，m= 0， 1测量Q pmmpm= tr[m]iρ ，m= 0， 1M1pV1M2qV2M1M2pqV1V2MpρUMpU（ρ）没有qbit变量，并且上下文Δk仅包含qbit变量。本文件通篇将使用这一惯例。涉及经典运算的规则对应于类型化λ-演算的标准类型化规则的直接适应。量子常数、量子测量和幺正操作的规则是直接的-病房 这三个张量规则允许我们取两个qbitn和qbitm并创建类型为qbitn（n+m）的项。这三种情况之间的区别是由于已知或未知的量子比特必须被不同地处理。如果r，Δ <$M：qbit <$n，M是一个已知的qbit，当它不依赖于Δ中的某个量子态变量时，即， 如果FV（M）≥ |Δ |= 0。 如果FV（M）|Δ|仅包含扩展变量x，则由M表示的量子态取决于量子变量x的值，因此是未知的。分型规则不允许一个未知的量子态依赖于一个以上的其他量子态。还要注意的是，术语xx不是良好类型的，因为它不是一个有效的扩展变量。 我们还必须禁止像λx这样的重复术语。x ≠ x，所以我们要求线性地使用qbit变量。示例2.1量子 传送 可以 被 实施 在 的 量子数据λ-演算考虑以下QDL隐形传态项：传送：λx。设bx，y <$z = meas1cnot12（（H x）<$[β00]）in设by，zJ= meas1y <$z in如果bx，则如果by则U00zJ否则U01zJ其他如果by则U10zJ否则U11zJ其中幺正超算符Ubxby是隐形传态协议的通常校正幺正操作，[β00]是贝尔态（|00元+|11分）/2。使用类型推理规则，我们可以推导出该类型的teleport：qbit<$ qbit。任何量子电路都可以以类似的方式实现为QDL项Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）45一一一一一一一一一输入qbit被表示为qbit变量x，如果需要，其用辅助qbit张量化。然后可以将酉变换应用于结果项。最后，测量操作用于提取结果。量子数据λ演算的操作语义被给出为项和值之间的大步长概率约简关系MpV值是由下式递归定义的项：V，W：= 0 |1 |∗ |ρ |λx。M|西韦夫|V.约简关系由表2中给出的规则定义。经典操作的操作语义使用标准归约规则定义。量子操作约简规则使得量子项的约简遵循量子力学的规则。例2.2远距传送项ρ以概率1降为ρ。3指称语义3.1概率博弈语义学本文提出的博弈语义是使用Danos和Harmer [3]引入的概率博弈语义的定义来构建的。我们在这里给出了概率博弈语义的基本定义和事实的概述定义3.1竞技场A是一个三元组（MA，λA，λA），其中MA是一组移动，函数λA：MA→ {O， P}×{ Q， A}×{ I， N}是一个标记，它将移动分配给两个玩家对手和玩家，并告诉我们哪些移动是问题，哪些是答案，以及它们是初始还是非初始移动，最后►AMA×MA是一个关系，称为使能关系，使得（A1）如果a≠AB，则λOP（a）/=λOP（b），λQA（a）λQA（b），（A2）如果λIN（a）= I，则λA（a）= OQI，（A3）如果a∈b且λQA（b）= A，则λQA（a）= Q，其中，函数λOP、λQA和λin是λA，由A A a集合{O， P}，{Q，A}和{I， N}。我们使用约定M X，其中X是从移动标签集合{O，P，Q，A，I，N}中获取的上标列表，表示用这些标签标记的移动集合。因此，竞技场中的移动有各种类型，对使能关系的约束通过限制在给定过去的交互的某个点可以进行哪些移动来限制竞技场中可能的交互。条件（A1）强制只有玩家移动才能使对手移动，反之亦然，（A2）要求所有初始移动都是对手的问题，最后（A3）说答案只能通过问题来实现。A中的一个局是一个移动序列s∈M<$。这并没有考虑使能关系;我们定义一个正当的游戏是这样一个游戏，在这个游戏中，46Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）► ►►一一一QA非初始移动b有一个指针指向移动a的前一次出现，移动a的值为Ab。我们最终需要强制两个玩家交替。合法策略是一种正当策略，其中对手和玩家交替使用;我们用LA表示A中的合法策略集合。请注意，因为所有初始移动都是对手移动，所以对手总是第一个移动。奇数和偶数长度的合法局集分别用L奇数和L偶数表示。例3.2boolarena定义为Mbool={？，0，1}λbool（？） =（O， Q， I）且λbool（0）=λbool（1）=（P， A， N）且具有使能关系？0，1.例3.3空的竞技场I是完全没有移动的竞技场在I中唯一合法的策略是空策略ε。设sa∈ LA. 从a开始并跟随调整指针，总是会导致初始移动b的发生，我们称之为a在sa中的遗传调整器。我们可以看到，每一个合法的策略都将被划分为子策略，每一个子策略都由一个给定的初始策略所遗传地证明的所有策略的出现所组成。这些子播放称为线程。一局合法棋的当前线，以对手的一步棋结束，用[sa|是a出现的sa的线程。如果sa以玩家移动结束，则当前线程由[s]定义|a. 我们希望当前的线程是合法的打法，因此有必要对合法的打法施加一个额外的条件：如果对于每个以玩家移动结束的子打法ta，a的正义者在[ t]中，则合法的打法s是好线程的|. 在一个好的线程发挥，球员总是发挥在最后一个线程的对手发挥。给定区域A、B，乘积A→B和箭头A →B运算分别定义如下：• MAB=MA+MB（不相交并）• λA<$B=[λA，λB]（copairing）• mABnimAn ormBn.• 是个B=MA+MB• λAB中OPλA，λA，λA• MABni mAn或mBn或λIN（n）=λIN（m）= I.B A中OP其中λA 反转两个参与者的角色，λA使A的所有移动都不姓名首字母缩写。 产品领域A和B直观地理解为对手的每个 在竞技场AB中，对手在B中进行初始移动后，在每次轮到他时，玩家可以选择在B中使用他的一个移动或在A中使用对手移动。给定竞技场A中的合法策略s，设下一个A（s）={a∈MA|sa∈LA}是集合在比赛结束后可以合法进行的所有行动中。定义3.4参与人的概率策略是函数σ：Leven→[0， 1]使得σ（s）= 1且σ（s）≥Σb∈next（sa）σ（sab）Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）47σ（s）∗→A中策略σ的迹集是偶数长度合法对策的集合，它们被σ赋予非零概率：记为Tσ。一个策略σ是确定的，如果对所有s∈ Tσ，σ（s）= 1。可以用条件形式描述概率策略σ。的概率σ（b|sa）= σ（sab）是参与者选择玩b的概率，游戏SA策略的组合是程序各部分之间的交互在游戏语义中编码的方式 给定两个策略σ：AB和τ：BC，我们定义一个新的策略σ;τ：AC，通过让σ和τ 在给出合成的定义之前，有必要将这种相互作用的概念形式化。A、B、C的交互作用集为IA，B，C={u ∈（MA+ MB+ MC）|u|AB∈ LAB，u|BC∈ LBC，u|AC∈ LAC}其中u|AB是通过删除C的移动而获得的u的子序列，对于u也是如此。|公元前关于U|AC有点不同，因为从u中删除B的移动及其相关指针可能会留下A或C的移动，这些移动被B-移动所公正，而没有公正者。在这种情况下，我们定义了我们的正义，|AC如下：C中的移动a被B中的移动b所调整，将被A或C中的第一个移动所调整，我们通过从u中的调整指针追溯到a。在交互作用IA ，B ，C中s ∈ L A C的见证集wit（s）是交互作用u∈ IA，B，C的集合，使得u|AC= s。两个策略σ：A B和τ：B C的组合现在可以定义如下：Σ[σ;τ]（s）=u∈wit（s）σ（u|AB）τ（u|BC）。身份策略（或所谓的“模仿策略”）id A：A A在组合方面是中性的它被定义为使玩家复制对手在相应组件之间移动的策略。形式上，这被定义为具有跟踪.JevenjT（1A（s））=s∈ LAlAR|是的。S|AR = s|AR .使用迄今为止定义的所有结构，可以定义一类竞技场和概率策略。以Arena为对象，态射AB是AB中的策略。策略的合成是所需的合成，恒等策略是恒等态射。它是结合的，并且在[3]中表明概率策略在复合下是封闭的 此类别也是对称的么半群 运算是一个张量积，它作用于morphisms如下。给定σ：A→C和τ：B→D，s∈ L甚至′ ′，我们（A至B）（A至B）集合[στ]（s）= σ（s|AC）τ（s|CD）。所有的相干同构都很容易定义使用模仿策略的变体。线程在游戏语义中扮演着重要的角色，它是一种描述策略的方式，这些策略用侧事件（如商店）对程序进行这是通过48Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）一一s∈L迫使玩家仅使用当前线程中可用的有限信息，而不是使用可以从整个先前游戏中提取的所有信息，包括在其他线程中进行的移动一个策略σ是好线程的，如果Tσ只包含好线程的策略。注意这种情况迫使玩家在对手玩的最后一个线程中回答给定两个好线索策略sab∈ L偶和ta∈ L奇，其中[sa|=[ta|，我们定义匹配（sab，ta）为唯一合法播放选项卡，b如[ sa]所示|. 如果sab∈ Tσ，t∈ Tσ，a∈ next（t）和[sa|=[ta|意味着σ（sab）σ（s）σ（（match（sab，ta））=.σ（t）这个条件的含义是，如果玩家根据σ进行游戏，玩家选择他的答案的概率仅取决于当前线程，即σ（b|sa）= σ（b|ta）。微分方程ΔA：A→A →A → A定义为微分方程，迹集甚至AAlAr|一|A∈idAl J.S.J|Ar∈ idAr. 这是类似于身份策略的定义：Δ指示参与者在A和它的两个副本Al和Ar之间使用复制策略。 A中可能的冲突通过将根据左或右复制播放进行的不同线程移动分开来解决还有一个唯一的策略Q AI，即迹为{ ε }的平凡策略。两个线程无关策略σ：A的配对B和τ：AC定义为σ，τ= ΔA;στ。 因此当参与人使用配对策略时他在B的初始移动后使用σ，在C的初始移动后使用τ。对于每个区域A，（A，ΔA， QA）是一个余项。在[8]中证明了一个策略σ：AB是线程独立的当且仅当σ是一个可商同态。 使用范畴论[9]中的一个已知事实，这意味着将竞技场和概率策略的范畴限制为线程独立策略是一个很好的方法。笛卡尔闭范畴注意，像πA：A<$BA这样的投影策略是被定义为复制策略，使玩家复制对手3.2量子竞技场为了对QDL的量子部分进行建模，我们必须定义一个可以将量子数据表示为策略的领域。 这个竞技场的定义与bool竞技场类似。游戏开始时，对手询问玩家对当前量子状态进行量子测量的测量结果。玩家Opponent可以使用的量子测量类型是Peres引入的称为干预算子的量子测量的一般描述[11]。这项措施-LY. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）49Σ？[1]？[n]1nM1Mn？EmF测量过程被认为是测量设备与待测量的量子系统的单一相互作用，随后是对组合系统的投影测量设D（H）是H上密度矩阵的集合，SD（H）是迹小于1的Hermitian正算子的集合. 量子干涉在Hilbert空间H上，超算子E={Em：SD（H）→SD（Hm）}由测量结果m索引，使得对于任何状态ρ。 如果系统最初处于状态ρ，则执行量子干预以概率pm= tr（Em（ρ））产生结果m，并使系统处于状态Em（ρ）/pm。注意，空间HBm可以取决于测量结果。设H是一个Hilbert空间。竞技场[H]是一个竞技场，在那里问题是形式、、、？E？为Em：SD（H）-SD（Hm）。E的可能答案是可能的测量结果m。 在这个舞台上的一出戏是一系列的动作E？[1]m1··· E？[n]mn其中量子干涉E？[k]可能都是不同的。一个quntumsteρ由一个pr obistrategy[ρ]来修改。in[H]。这是一个很好的-.egy [ρ]由权重[ρ]EM...EΣm= trE... E（ρ）。超算子的构成和通常一样，但我们使用一个方便的约定：如果E的定义域与F的上定义域不匹配，我们设EF=0。 这个约定与超算符的量子力学解释是一致的：一个不可能的操作被赋予概率为零。注意，策略[ρ]是线程独立的：最后一个问题的答案总是依赖于前面的问题，这些问题通常修改了初始状态[ρ]。使用这些策略，我们现在可以表示任何保迹超算子F，将HA中的状态作为策略。这个策略用[F]表示;它让玩家通过测量输入状态来回答关于输出状态的问题，下面的典型玩法描述了这种方法：[英][HA][HB]E？E？FM.量子干涉是量子干涉吗？Σ获得用F组成每个干预Em。 QDL的所有量子操作都使用这个基本方案的变体来解释。特别地，酉策略是上述的特殊情况，其中F是与酉运算U相关联的超算子U。新的量子干涉是如何从最初的E产生的？激发量子干涉的使用：用其他量子测量形式主义（如投影测量）实现类似的方案将不允许像保迹超算子那样普遍地表示量子操作。？[1]第一章M？[n]50Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）卢恩量子力学[5，10，7]的一致历史方法与用于定义策略[ρ]的方案之间存在相似之在“精神”上有一个明确的联系，因为两者都从这个角度来看，用于表示量子操作F的上述想法是新的，并且可以是在该上下文中思考量子操作的结构化方式3.3指称语义学的定义我们现在使用上一节中定义的量子领域来定义QDL的指称语义。首先，类型解释如下：[[bool]]=bool[[T]]=Tqbitn=qbitn[[AB]] =[[A]][[B]][[AB]]=[A]][[B]]arenaqbitn是对应于n个qbit的状态空间的arenaC2n其他领域的操作直接取自经典游戏语义。竞技场T有一个可能的偶数长度游戏：？因此，除了空策略之外，只有一个可能的策略。我们把这个策略记为。类型操作×和分别对应于竞技场操作和。给定上下文r = x1：A1，.，xn：An，我们将[Γ]]设为[[A1]]··[[An]]。我们现在转向项ΓM：A的解释[M]的定义。这个定义是通过对ΓM：A的推导的归纳得出的。在基本情况下，我们必须处理变量和常数项。对于变量，使用投影策略πA：[Γ]<$ [[A]]→[[A]定义Γ，x：A<$x：A的解释。常数0、1和1的表示是标准常数策略。一个量子态常数ρ：qbit被解释为qbitn中的量子策略[ρ]。我们描述了涉及量子操作或新思想的归纳情况其他情况下解释使用经典游戏语义学的标准思想。由于线性约束，[Γ， Δ1， Δ2]的定义与博弈语义中使用的条件句的通常定义不同假设[[P]]：[[r]][[Δ1]]bool和[M]]，[[N]]：[[r]][[Δ2]][[A]]已经被定义了。使用与对称策略相关的对称策略和复制策略Δ，我们可以定义一个策略r：（[r] [[Δ1]][[Δ2]]）（[[r] [[Δ1]]）（[[r]][[Δ2]]）这 重组的输入 舞台与这战略，我们 可以定义[[ifPthenMelseN]为组合r;[[P]]qualid;cond（[[M]]，[[N]]），其中cond（[[M]]，[[N]]）：bool（[[r]][[Δ2]]）[[A]]是使用条件策略操作定义的，通常由以下思想定义。给定任意两个竞技场A和B以及两个策略σ，τ：A→B，Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）51我cond（σ，τ）：（boolA）B是一种策略，它通过在bool分量中要求一个布尔b来让玩家回答B中的初始移动，然后让玩家在分量A和B中使用策略σ（如果b= 1）和τ（如果b= 0）。我们处理的第一个量子操作是测量情况。假设[[Q]]：[[r]][[Δ1]]qbit（n+1）和[M]]：[[r]][[Δ2]]boolqbitn已经被定义了。 我们可以定义[设b，x=measiQinM]为组合r; [[Q]]; measi; [[M]其中measi是如下所述的策略。设C是对应于规范是量子干涉的基础。如果第一步是在qbit竞技场中的一个问题，那么玩家使用左方案，如果第一步是在bool竞技场中，那么玩家使用右方案。qbitn（n+1）measiboolqbitE？E？CQC（m，b）M？Bqbit（n+1）米亚斯岛 布尔位？I C.I.CBBE？E？阿吉尔岛MM其中E <$F代表量子干涉{Em1<$Fm2}（m1，m2）。重要的是要指出，在正确的方案中，玩家必须询问对手两次。 由于第一次干预改变了状态，对手对第二个问题E的回答？这取决于给出的第一个答案这是本文中描述的语义中唯一一个需要多个线程的qbit_n领域的实例。由于测量的副作用，我们不得不使用线程相关的策略来描述量子态。这是我们被迫假设qbit类型是线性的，因为线程相关策略不能使用通常的Δ复制策略复制。相比之下，量子λ演算的大量工作通过不可克隆定理证明了线性假设的必要性。这里有三种张量情况要处理。在第一种情况下，我们张量两个已知的qbit。假设这些策略ΣΣΓ, Δ1,x1:qbit⊗n►M1:qbit⊗nΣΣ andΣΣ Γ, Δ2,x2:qbit⊗m►M2:qbit⊗mΣΣ已经定义，其中FV（Mi）\|Δ i|i= 1，2. 策略[M1<$M2]]定义为组合r;[[M1]]<$[M2]，其中策略[M1]<$[[M2]]为52Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）121 1 22定义如下：([[r] [[Δ1]]）（[[r]][[Δ2]]）的1.an[[M]][[M]]◦量子位元qbitE？B1.BKM参与人回答m到E的概率是多少 在相互作用s = a1. an和t = b1. bk是tr（Emρs <$ρt）。注意，当我们取两个输出量子场的张量积时，我们必须取经典输入场的经典博弈积。在第二种情况下，我们张量两个qbits，每个构造从未知的qbits。这个例子与第一个例子类似：假设ΣΣΓ, Δ►M: qbit⊗nΣΣandΣΣΓ, Δ►M:qbit⊗mΣΣ已 经 定 义 ， 并 且 FV （ Mi ） |Δi|={xi} 。 策 略 [M1<$M2]] 被 定 义 为 合 成r_id;[M1]]<$[[M2]，但这一次策略[M1]<$[[M2]必须使用以下方案定义：（ [[Γ]<$[[Δ]] ） <$ （ [[Γ]<$[[Δ]] ） <$qbit<$n<$qbit<$[[M1]]<$[[M2]]<$qbit<$n<$qbit<$m1 2E？的1.anB1.BME？（FsGt）MM其中Fs和Gt分别是Player在[M1]]和[[M2]]中使用的两个保迹超算子。第三个张量规则适用于已知和未知状态都是张量的情况.在这种情况下，我们必须使用条件准备策略，定义为：卢恩布勒姆Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）531 1 22在前两种情况下使用的方案的组合。 假设ΣΣΓ, Δ,x:qbit⊗n►M:qbit⊗nΣΣandΣΣΓ, Δ►M:qbit⊗mΣΣ已经定义，并且FV（M1）\|Δ 1|={x}和FV（M2）|Δ 2|=0。策略[M1<$M2]被定义为组合r; [[M1]]<$[[M1]]，此时张量策略[M1]<$[[M2]被定义为方案（[[Γ]]<$[[Δ]]）<$qbit<$n <$（[[Γ]<$[[Δ ]]）[[M1]]<$[[M2]]<$qbit<$n <$qbit<$m1 2E？的1.一个kB1.BlE？（FsGt）MM玩家决定如何回答第一个问题E？[2 ][3][4][5][6][7][8][9][10][11][12][12][13][14][15][16][17][18][19][19][1ak，准备;我们假设这个状态是由超算子Fs准备的。在此之后，玩家将在[r]]中开始交互，以了解如何从其输入构建由项M1表示的状态。 在这种情况下，我们假设这个构造对应于一个超算子Gt，其中t = b1. bl是[[r]]部分中的相互作用。 最初的问题，然后转化为问题（FsGt）E？在输入区域qbit_n中，并且答案被复制回输出区域。4健全性现在我们转向证明上一节中定义首先，我们需要一个替换引理。引理4.1对于任何具有量子数据项Γ， Δ1，x：A<$M：B和对于x∈FV（M），我们有r， Δ1， Δ2=M[N/x]：B和[[M[N/x]=r; id= [[N]];[[M]]证据 这一点通过对M.Q下面的命题指出，当一个项M以概率p减少到某个值V时，相应的策略[M]]和[V]使参与者以概率p以相同的方式进行博弈。54Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）命题4.2如果M<$pV，则对于所有良好开的sab∈ T（[[V]]），我们有[[M]]（b |sa）= p [[V]]（b |sa）。证据通过结构归纳法推导出MpV.大多数证明遵循经典情况的通常论证我们跳过这些，专注于涉及量子运算的对于测量操作，首先考虑单个qbit的情况。假设[[M]的行为是[[ρ]的概率为p。假设测量值M以概率p tr减少到0（|0 ⟩⟨ 0 |ρ）。策略[measM]是组成[M]]; meas，通过归纳假设，使用此策略的任何交互都将表现为一种相互作用，使用策略的行动[ρ]; meas.通过定义[ρ]，该策略表现为bool中的常数策略0，概率为tr （ |0 ⟩⟨ 0 |[001 pdf 1st-31files][001 pdf 1st-31files][001 pdf 1st-31files][001 pdf1st-31files]（|0 ⟩⟨ 0 |ρ）。一般的测量情况是类似的。为了处理张量运算归约规则，假设当M1<$pV1和M2<$qV2时命题成立，并假设M1<$M2<$pqV1<$V2。由于[M1<$M2]的定义有三种情况，因此必须分别考虑在第一种情况下，M1和M1都是在类型上下文中没有出现qbit类型的自由变量的项。通 过 定 义 [M1<$M2]]=rid;[M1]][[M2]] ， 通 过 归 纳 假 设 ， 这 将 表 现 为[M1<$M2]]=rid;[V1]][[V2]]，概率为pq。这两种情况是相似的，只是[[M1]]和[[M2]的定义在每种情况下都是不同的Q下一个结果是充分性，与前一个结果相反。对于经典的λ-演算，我们使用一个可计算性谓词来证明QDL的充分性。下面的定义与可计算性的通常定义之间的主要区别是使用扩展变量。请注意，扩展变量或线性的存在对该定义没有任何重大影响。定义4.3QDL项M是可计算的，如果(i) M闭于M：A且A = bool，T或qbit，且若对所有sab∈ T（b|我们有[M]]（b|sa）=p [[V]]（b|sa），然后MpV，(ii) x1：A1，.，xn：An M：A和对于所有可计算闭项ΓN1：A1，.. . ，r∈Nn：Anw有一个向量M[N1/x1，. . ，Nn/xn]是可比较的，(iii) M是闭的，其中M：A是闭的，对于所有闭的N，其中N：A是闭的，MN可以计算。引理4.4所有的QDL项都是可计算的。证据通过对M.涉及经典结构的证明部分遵循经典博弈语义中的通常模式，因此我们在这里关注量子运算。使用可计算性的定义，我们可以假设M的建筑成分是可计算的闭项。最有趣的情况是测量，因为它涉及到一个特定于QDL的参数。我们从一个qbit测量情况开始假设M=measNY. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）55其中N是qbit类型的封闭可计算项。假设V是布尔值，并且[M]]（b |sa）= p [[V]]（b|对于所有开好的sab ∈ T（[[V]]）。当玩家使用[M]]时，典型的打法是[[N]]测量我是一个很好的朋友？C？MM在哪里C？是对应于正则基中的投影测量的量子干涉。设p为使用[N]]得到答案为0的概率，1−p为答案为1的概率。虽然不可能推断出哪个状态ρ用于回答C？利用这些概率，我们知道如果参与人使用ρJ= p| 0 ⟩⟨ 0|+（1 −p）|1 ⟩⟨ 1|而不是ρ，我们会得到和上面一样的策略。由于measρJ<$p0，我们根据需要得到该measρ<$p0。我们使用类似的论证来处理一般的测量情况。对于酉操作，上述问题不会发生，因为策略[UM]] = [[M]];[U]提供了所有量子干预E的测量概率？.这允许我们通过格里森定理找到一个状态ρ，使得[M]]以概率p表现得像[ρ]。利用这一点和关于M的归纳假设，我们得到了预期的结果。Q不确定性是最后一个引理的直接推论定理4.5设M是bool，T或qbit n型闭项.如果对于所有开好的sab ∈ T（[[V]]），我们有[[M]]（b |sa）= p [[V]]（b |sa），则我们有MpV。为了给出最终结果，我们需要为QDL引入必要的上下文等价概念一个B型上下文C[−]有一个A型洞是一个C[−]项有一个特殊变量 在上下文C[−]中的项N的无捕获替换记为C[N]。定义4.6两个封闭项M1：A和M2：A在上下文中是如果对于每个具有类型A的洞的接地类型上下文C[-]，C [M1]pv[M2]P.V.下面的合理性结果是使用标准参数从一致性和充分性得出的。定理4.7（合理性）设M1和M2具有两个闭QDL项.如果[[M1]] = [[M2]]，则M1<$M2。56Y. Delbecque/Electronic Notes in Theoretical Computer Science 270（1）（2011）5结论和今后的工作我们引入了一种新的量子λ-演算，并利用博弈语义学的工具，得到了一个可靠性结果，验证了它的语法和类型系统的结构。语言的一些重要特征，如线性和张量操作的不同形式，直接使用用于建模语言的量子策略的属性来激发。游戏语义学方法允许我们直接对语言的经典和量子结构进行建模，并且可以使用经典游戏语义学的思想扩展到具有额外功能（如递归）的语言博弈语义通常通过对策略进行适当的限制来获得完全抽象的结果。这里的主要目标是为量子编程语言引入一种新的模型虽然我们获得的可靠性结果证实了使用量子博弈来建模量子类型的有用性，但自然的下一步是寻求QDL的完全抽象结果。主要的困难是，没有已知的特征，在[HA][HB]中的形式[F在这个舞台上的bilistic战略Gleason因此，这里的一个完整的抽象结果将是理解如何描述量子过程的一个重大进展在这种情况下，障碍与高级类型语言通常的微妙之处无关。我们没有充分探讨本文所介绍的量子竞技场的范畴性质例如，我们可以考虑形式为[H]的竞技场的范畴和对应于量子运算的概率策略。这个范畴或它的一些子范畴可以为与量子力学相关的范畴结构提供新的模型[1，2，13]。最后，请注意，有一种方法可以放松本文中给出的量子领域的定义，即放弃[H]中的问题由H上的量子干涉组成的条件。由此产生的竞技场允许对手在任何空间使用量子干涉。这种可能性在[4]中很有用，可以模拟配备λ演算的量子存储器，它可以包含可变大小的量子态。在该语言中，量子数据只能通过语言中的引用来使用;这使得线性约束变得不必要，因为不可克隆定理并不禁止对一个qbit的多个引用在这种情况下，量子策略的性质也被用作语言构建的指导，进一步证明了量子策略在高阶量子编程语言研究中的有用性。引用[1] Abramsky，S.和B. Coecke，A categorical semantics of quantum protocol，in：Proceedings of the 19thIE