理论计算机科学电子笔记270（1）（2011）121-128www.elsevier.com/locate/entcs关于量子和概率线性λ演算（延伸摘要）Beno Valiron1Laboratoire d’Informatique de Grenoble,摘要在本文中，我们给出了一个完全完备的模型的线性概率代数演算。该模型是基于随机关系范畴的Kripke语义。我们勾勒出这与量子计算的关系。关键词：概率计算，量子计算，贝尔不等式，线性代数演算，克里普克语义，完全正映射，多项式。1引言Selinger和Valiron [6]使用完全正映射的范畴CPM给出了线性量子lambda-演算的完全抽象语义这种语义不是满射的，因此无法区分类别中是程序的表示的映射和不是的映射在[4]中提供了一阶情况的满射语义语义学使用范数的概念来确定哪些完全正映射是项的表示;也就是说，这些完全正映射恰好是迹非增映射。然而，范数的概念未能提供高阶函数的适当表征[5]。在本文中，我们将我们的研究限制在[6]中描述的语言的概率片段。我们使用多面体的概念来描述语言的形象，并勾勒出如何使用这样的结果来描述量子计算相对于概率计算的信息论能力最后，我们提供了一个完整的和完整的指称语义的概率的片段，使用Jung和Tiuryn [3]的思想的线性微积分。1电子邮件：benoit. imag.fr1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.01.011122B. Valiron/Electronic Notes in Theoretical Computer Science 270（1）（2011）121不2线性量子微积分我们回想一下[6]中定义的用于量子计算的线性类型lambda演算术语和类型分别为：M，N，P：：= x| λx.M|MN|南卡罗来纳州| ∗ |Ω|设x，y=M，N|设M= N中的M|如果P那么M否则N|0 |1 |meas|新|U，A，B：：=AB|不|AB|位|Qbit，其中x的范围是项变量。我们提醒读者，Ω对应于发散项，关于类型判断的定义，我们参考[6]。这种语言在完全正映射的范畴CPM中得到解释[4]。这些类型按以下方式解释[[bit]]= 1，1，[[qbit]]= 2，[[A <$B]]=[[AB]]=[[A]<$[[B]]。在这个扩展的摘要中，我们只回忆布尔0和1的定义，并请读者参考[6]来解释所有项：[[0]] =（1， 0）∈C2，[[1] =（0， 1）∈C2。使 用 该 语 言 ， 可 以 模 拟 公 平 的 掷 硬 币 ， 例 如 使 用 程 序 meas （ H（new0））：bit，其中H对应于Hadamard门这个词的解释是（1，1）。使用类似的技术（和2 2可能使用术语Ω），可以得到模拟不公平硬币的术语表示为（a，b），其中a，b0且a+b≤1。3概率线性lambda演算我们可以修改第2节的语言，以删除量子方面，并获得一种纯粹的概率语言为此，我们只需要改变常量。我们用一组常数c（a，b）替换meas，new和U，每对实数（a，b）对应一个常数，使得a，b0且a+b≤1。通过删除类型qbit来修改类型。我们只剩下以下术语和类型：M，N，P：：= x| λx.M|MN|南卡罗来纳州| ∗ |Ω|设x，y=M，N|设M= N中的M|如果P那么M否则N|c（a，b）|0|1，A，B：：=AB|不|AB|点在这个上下文中，术语M在CPM中的语义是对于某些自然数m和n从Cm的向量到Cn的向量的完全正映射。请注意，在这种情况下，完全正映射与（部分）随机映射相同。从[0， 1]m映射到[0， 1]n。 文[6]中给出的结果专门针对这种情况，并且语义是完全抽象的。B. Valiron/Electronic Notes in Theoretical Computer Science 270（1）（2011）121123−−−→Σ4Bell不等式贝尔实验[1]如下。考虑一台量子机器，它最大程度地纠缠两个量子比特A和B1|0 ∗ ⊗ |1 ∗ −| 1 ∗ ⊗| 0分）|0∗)并将量子位A发送给爱丽丝，将量子位B发送给鲍勃。假设Alice和Bob可以独立地选择以下三个基{a，b，c}中的一个来测量他们的量子比特：1√3 1√3|0分，|0 b =2 | 0分+ 2分|1个月，|0 c =2| 0 ∗−|0∗ −2|1个月，√3 1√3 1|1 ∗ |1 b =| 1b∗=2 |0 ∗ − 2 |1个月，|1 c=2 |0分+2分|1美元。问题是计算在两个不同的基上测量A和B时获得相同输出的概率。人们可以在高阶量子计算的背景下解释这个实验。首先，机器使两个量子比特纠缠在一起：它产生一个映射EPR：T →qbit<$qbit。然后，Alice和Bob各自取一个量子比特，选择一个基，并进行测量：他们执行的测量是一个函数f：qbittrit→bit，其中trit=T T T。 可以将此函数curry为fJ：qbit→（tritbit）该算法可以用组合来T−E−P−R→qbit<$qbitf′<$f′（三比特）位）。该算法产生一个类型为（tritbit）的项（tritbit）。这种类型是经典的，人们可能想知道这个术语的外延是否是概率线性微积分中的术语的外延。贝尔不等式精确地表明，情况并非如此。换句话说，在概率线性lambda演算中可表达的术语精确地对应于物理学家所知的局部隐变量理论。考虑经典类型A（即不包含qbit）。在本文的其余部分，我们将开发一种方法来确定[A]]的向量，这些向量可由概率线性微积分中的一个项表示。这可以被看作是贝尔不等式到任何高阶类型的推广5概率演算正如在[2]中，用第3节的概率线性微积分编写的程序可以被也就是说，任何有效类型判断ΔDM：A的表示都可以重写为概率和[[ΔDM：A]]=αi[[ΔDNi：A]]我124B. Valiron/Electronic Notes in Theoretical Computer Science 270（1）（2011）121Σ1nJ[[c（a，b）]]=[if c（a，b）then1else 0]][[M（if c（a，b）thenN1else N2）]]=[if c（a，b）thenMN1else MN2]][[M，ifc（a，b）thenN1elseN2]]=[ifc（a，b）thenM，N1elseM，N2]][[λx.if c（a，b）thenN1else N2]]=[[if c（a，b）then λx.N1elseλx.N2]][[if（if c（a，b）then M else N）then P else Q]]=[[if c（a，b）then if M then P else Q else if N then P elseQ]]表1重写if项的规则。其中每个αi0和iαi≤1，并且其中Ni不包含任何常数项c（a，b）。证明的思想如下：首先，请注意，[[ΔD if c（a，b）then M else N：A]]= b·[[Δ D M：A]]+ a·[[Δ D N：A]]。因此，为了使结果为真，需要能够发送一个项M，将一个常数项c（a，b）转化为一个形式为如果c（a，b）则M1elseM2的项，其中M1和M2满足某个不变量. 由于语言是线性的，这是可能的。作为证明的开始，考虑表1中的等式，方向从左到右。6解释为多面体确定性术语（即没有出现c（a，b）的那些共享特殊性质：命题6.1给定一个类型上下文Δ和一个类型A，存在有限个确定性项Ni（直到β等价）使得Δ D Ni：A。这个命题来自于语言是线性的这一事实：人们可以枚举所有可能的（无CUT）类型派生。我们可以更进一步：命题6.2任何A型的确定性闭项都有形式（xi，.，x i）∈ [[A]]，其中对于所有j，x i是0或1。它允许我们陈述以下定理：定理6.3集合[[A]]中的向量集是某个线性概率规划通过表示的图像，它们是凸0 - 1-多面体（即其顶点具有以下形式（x1，...，x n）∈ [[A]]，其中每个x i是0或1）。以下是一些例子(i) [bit]类型的确定性闭项是Ω、0和1。也就是说，容许向量的多面体被（0，B. Valiron/Electronic Notes in Theoretical Computer Science 270（1）（2011）1211250），（1， 0）和（0， 1）所张成126B. Valiron/Electronic Notes in Theoretical Computer Science 270（1）（2011）1212(ii) [ bit T ]类型的确定性闭项是Ω，λx.if x then<$else Ω，λx.if xthen Ω else<$and λx.if xthen <$else <$。也就是说，容许向量的多面体被（0，0），（0， 1），（1， 0）和（1， 1）所张成。(iii) [[（bitT）T]类型的确定性闭项具有Ω的形式，λf.设λ= f0，λf.设f=f0。也就是说，容许向量的多面体被（0，0），（1，0）和（0，1）所张成。7多面体不是合成的为概率线性代数演算开发一个完整的语义的天真想法如下。考虑一个类别，其对象是多面体，其映射是将多面体发送到多面体的CPM映射。然后解释这个类别中的语言。事实证明，这是行不通的。事实上，如果是这样，映射C2→C2应该由判断x：（bitT）TDM：bit表示。然而，对应于（（位T）T）位的形式为λf。设f = f（λx.if x then a else b）在c中，其中c在{0，1}上，a和b在{0，Ω}上。对应的顶点为（0，0，0，0），（1，0，0，0），（1，0，1，0），（0，0，1，0），（0，1，0，1），（0，1，0，0），（0，0，0，1）。单位映射对应于向量（1，0，0，1），它不在这些向量所张成的多面体中最接近的近似值是1（1，0，0，1）。因此，虽然多面体提供了一个合理的语义，但它们不足以表征概率语言的可定义映射。8概率线性演算的完备语义我们构造的多面体是包含原点的闭凸集P。于是，他们就这样定义了一种规范，||= min { λ||v∈ λP }。|v ∈ λP}.我们将把范数的概念扩展到荣格和蒂伦的工作中，并定义我们称之为线性克里普克逻辑关系：我们考虑向量元组的范数，而不是考虑单个向量8.1一种玩具语言考虑以下概率线性微积分的简化版本术语M，N：：= x A|Ω A|c（μ）|λx A.M|MN|如果P那么M否则N，类型甲乙丙：：= bit|AB，其中0≤μ≤ 1。B. Valiron/Electronic Notes in Theoretical Computer Science 270（1）（2011）121127一WW五号B−−−→−−→一8.2线性Kripke逻辑关系考虑集合C的一个小范畴，其卡氏积是一个monoidal结构，包含对象T={*}。 我们将在C的每个对象w上定义一个逻辑关系，作为规范||−||w在元组（x i）i∈w上，其中x i∈ [[A]]，对所有i∈ w。基础类型的关系必须满足以下兼容性属性：如果f：v→w是C中的映射，则w v||位≤ 1→||（x f（i））i ∈v| bit ≤ 1。||bit ≤ 1.此外，仍然在接地类型位，范数应该满足范数公理：w w w||位≤||（x i）i||钻头+||（y i）i||比特，||bit,||比特0，||bit0,w w||位=||λ|（x i）i|||比特，||bit,||bit = 0 i比特i x i = 0。||bit = 0iff∀ix i= 0.最后，没有人应该拥有||T位=||+的 |B|+|b| 我们将关系式对于更高的类型，如下所示：||w被 定 义 为 ：||wisdefinedasthemaxi mumof||(gf(j)(xi))j⊗i∈w′⊗v||w′⊗v,wh e r e f: wJ||A ≤ 1。||A≤ 1.AB→ w∈ C，（x i）i∈v∈ [A]这样，Wein将（gf（j）（xi））ji∈w′v解释为元组（h（k））k∈w′v，其中h是映射wJvfidwvgxA、B[[AB]][[A]]−−→[[B]]我们将编写||X||为||（十）||T. 我们称之为（||−||w）w∈| C|，A∈型a范数A A aarity。引理8.1给定w ∈ |C|而A型，||− ||W满足兼容性性质和规范公理。8.3健全性引理8.2（合理性）对于所有闭项M：A，||[[M]] ||A≤ 1。证明遵循[3]中提出的思想。我们将扩展环境的概念定义为一对（φ，ρ）部分映射，其中φ：Var→| C|并且其中ρ是一个映射，它将一个元组（x i）i∈φ（xA）赋给变量x A，其中x i∈ [[A]]。 如果Δ={x1：A1，.，xn：An}，我们用φ（Δ）代替φ（x1）<$··<$φ（xn）。 我们将类型判断的扩展解释定义为元组[[x1：A1，.，xn：An <$M：A]] ρ，φ=（xi）i∈φ（x1）<$··<$φ（xn），其中，对于所有i，xi∈ [[A]]，并且其中ρ和φ的域是集合{x1，.，x n}。引理8.2的证明是通过结构归纳法完成的。我们首先证明，对于所有的类型判断x1：A1，.， x n：A nM：B，适用于所有扩展环境128B. Valiron/Electronic Notes in Theoretical Computer Science 270（1）（2011）121A我.一位一1n（φ，ρ）such chthat||φ（xi）≤ 1，不等式y||φ(xi)≤1,theinequality||[[x1: A1,..., x n：A nM：B]]||φ(x1)⊗···⊗φ(xn)≤1ρ，φB满意了。然后，我们使用以下结果得出结论。引理8.3给定一个环境ρ，l∈φ′ e是值为{*}的常数映射，令ρ′e是将（ρ（xA））赋给xA的映射。 n[[ΔM：A]]ρ<$，φ<$=（[ΔM：A]]ρ）。Q8.4完整性完备性结果是通过选择一个精心设计的范畴C来获得的。对于每个类型A，用BA表示[A]]的典范基定义范畴C如下：对象是乘积BA1×···× BAn，箭头是对象上的恒等式约 定 8.4 当 考 虑 集 合 BA 时 ， 我 们 将 使 用 隐 式 顺 序 （ 1 ， ... ， 0 ） ， . ，（0，...，①的人。我们利用文法规则推广了BA1× ··· ×BAn定义8.5设UA1，.，An 是元组，（[[M]]（a1）· · ·（ann））（a1，...，an）∈BA1×···×BAn·· <$M：A1An比特，引理8.6集合U A1，.，n是凸的，其内部包含原点。证据凸性是使用表示的如果和Ω项。起源在内部的事实来自于一阶和高阶类型之间的对应。Q引理8.7考虑元组（xi）i∈BC1×···×BCk，其中对于所有元组i，xi∈[[A1···AnB]]。则对所有的a∈ BA1×······×BAn，xi（a1）······························································ （an）等于（x i）a1···an，x i在a1······································ a n的坐标。此外，其规范||(x (a ) ··· (a))||（十）||B C 1 ×···×B C k||BC1 ×···×BCki1n（a1，.，an）Bi iA1·······AnB8.8.8定义具有不同arity的范数（||− ||w）w∈| C|，A∈Type at ground类型如下：单位球||−||BA1×···×BAn 是UA，...，A.引理8.9（完备性）给定x ∈ [[A]]，||（十）||A≤ 1，存在闭项M使得[[M]]= x。定理8.10元素x ∈ [[A]]可由概率λ项表示当且仅当对于所有具有变元数的范数（||−||w）w∈| C|，A∈Type，范数||≤ 1。||≤ 1.9结论B. Valiron/Electronic Notes in Theoretical Computer Science 270（1）（2011）121129我们考虑了在[6]中描述的线性量子微积分的概率片段。我们解释贝尔不等式在这个高阶的背景下。130B. Valiron/Electronic Notes in Theoretical Computer Science 270（1）（2011）121利用凸多面体给出了一种计算高阶广义Bell不等式的方法.多面体解释不提供组合语义。最后，我们为概率线性代数演算的一个片段起草了一个完整的组合语义确认我要感谢彼得·塞林格提出了刻画可定义的高阶概率函数的问题，并在第7节中提供了反例。引用[1] Bell，J.美国， 关于爱因斯坦-波多尔斯基-罗森悖论，《物理学1》（1964年），页。195-200[2] 达诺斯河谷和R.S. 概率博弈语义学，计算逻辑学报3（2002），pp. 359-382.[3] Jung，A. J.Tiuryn，A new characterization of lambda definability，in：Proceedings of TLCA245-257[4] Selinger，P.，计算机科学中的数学结构（Mathematical Structures in Computer Science）14（2004），pp. 527-586[5] Selinger，P.，Towards a semantics for higher order quantum computation，in：P.塞林格，编辑，QPL'04的会议记录127-143[6] Selinger，P.和B.Valiron，量子线性函数语言的完全抽象模型（扩展抽象），在：P. Selinger，编辑，Proceedings of QPL123-137
