线性代数λ-演算：量子物理逻辑与概率类型系统的程序推理

−−理论计算机科学电子笔记270（2）（2011）219-229www.elsevier.com/locate/entcs线性代数的纯量系统Fλ-演算：量子物理逻辑Pablo Arrighi1 Alejandro D'ıaz-Caro2Universit'edeGrenoble，Laboratoire摘要线性代数λ-演算[2]扩展了λ-演算，使α项的任意线性组合成为可能。t + β。联合由于可以在该微积分中表示总和上的不动点，一个无限的概念产生，因此无限的形式。因此，为了保证一致性，t t并不总是减少到0 本文为线性代数λ-演算提供了一个类System F型系统，它保证了正规化，不需要这样的限制，t t总是减少到0。此外，这个类型系统还跟踪“类型的数量”。因此，它可以被看作是概率类型系统，保证项定义正确的概率函数。 它也可以被看作是追求量子物理学的一步。Curry-Howard同构逻辑[12]。关键词：类型理论，量子逻辑，概率λ演算，Curry-Howard1介绍近年来，许多研究人员试图开发量子编程语言[6，10]。这种语言的目的之一是表达量子程序，但这并不是一个足够好的理由，因为已知的算法并不多。一个更重要的原因是提供一个框架来推理表达这些算法的程序事实上，在经典计算机科学中，可以通过几个形式定义的逻辑来表达程序背后的推理它们提供了一个重要的框架，在其中推理和证明有关计算过程的属性通常1电子邮件：Pablo. imag.fr2电子邮件：Alejandro. imag.fr3一个完整的版本，详细的证明，可以在arXiv：0903.3741找到，一个完整的期刊版本正在进行中。1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.01.033220P. Arrighi，A.Díaz-Caro/Electronic Notes in Theoretical Computer Science 270（2）（2011）219这些逻辑是通过研究语言的类型系统而产生的[12]。与我们的动机相关的是，已经有了量子逻辑[4]，它是在量子计算之前开发的。然而，它与量子程序的关系并不明确。因此，需要一种逻辑来帮助我们隔离某些量子算法背后的推理;即，这将提供一种工具来探索某些算法（如Grover的[ 9 ]和Shor的[ 11 ]）背后是否存在一些典型的而不是想出一些 我们使用线性代数λ-演算（Lineal）[2]的原因是因为它的优点是不受特定类型系统的约束（它是无类型的），并且它是最小的，但它足够通用，可以描述任何量子计算。本文的目的是建立一个线性代数λ-演算的Curry系统，它能够处理类型中的标量，从而在某种程度上减少类型的数量，遵循叠加的思想，即一个项属于一个类型的数量。在这个意义上，这个标量类型系统是研究计划中的一个步骤，该计划寻求通过Curry-Howard同构获得的形式量子物理逻辑;它本身也很有趣，因为它与概率系统、线性逻辑（LL）、克隆等的关系。 （请参阅第5条）。这项研究还有另外两个产品首先，由于线性可以表示和上的固定点（例如，没有什么禁止项t应该减少到t+t），它有无限性，因此有无限形式（例如，t-t）。因此，为了保证连续性，t-t不应该减少到0。这一规则必须限于封闭的正规项[2]。由于本文为线性代数λ-演算提供了一个类似System F的类型系统，因此保证了所有项的规范化，这消除了对此类限制的所有需求，使Lineal成为一种更直观的语言：在类型化版本中，t−t总是减少到0。 此外，通过跟踪“类型的数量”，我们的类型系统已经准备好作为概率类型系统运行;保证术语定义正确的概率函数。虽然后一个结果不是我们的主要目的，但这确实定义了概率类型的λ-演算[5]。我们现在对线性代数λ-演算（线性）做一个小的概述[2]。第二节介绍标量类型系统及其语法、等价和推理规则。第3节显示了主题约简属性，使系统具有一致性。第4节显示了这个系统的强归一化属性，使我们能够解除上述约简规则中的限制。在第5节中，我们讨论了这种类型系统的含义，即它与概率演算和线性逻辑（LL）的关系。第6节给出了我们的结论。P. Arrighi，A.Díaz-Caro/Electronic Notes in Theoretical Computer Science 270（2）（2011）2192211.1线性代数λ-演算简单地说，线性代数λ-演算是λ-演算加上对项进行任意线性组合的可能性 考虑一种一阶语言，称为标量语言，至少包含常数0和1以及二进制函数符号+和×。那么向量语言是一种双排序语言，有一个向量排序和一个标量排序，由下面的术语语法描述：t：：= x |λx t|（t t）|0 |α。不|t + t其中α具有标量的种类，并且项包含向量变量但不包含标量变量（参见[2，sec.详情见附件III）存在用于标量重写系统的重写规则，其与环的公理兼容，并且存在用于被分成4组的向量的16个AC重写规则：• 基本规则，如u +0→u和α。（u + v）→α。u + α。v.• 因子分解规则，如α。u+ β。u→（α + β）。联合• 应用规则如u（v+w）→（u v）+（u w）。• Beta约简：（λxt）b→t[b/x]，其中b是基向量（即抽象或变量）。因式分解和应用规则具有“v + w正常关闭”的限制这类问题类似于无穷形式∞−∞。例1.1可以定义定点运算符，如Y=λy（（λx（y+（xx）（λx（y+（xx）然后，设b是一个基向量，所以（Y b）简化为b+（Y b），所以如果对规则没有限制作为因子分解规则，那么项（Y b）−（Y b）将简化为（1 +（−1））。（Yb），其减少到0。然而，注意它也会减少到b+（Yb）−（Yb），从而打破连续性。通过在因式分解规则中要求u闭正规，避免了这个问题（参见[2，sec.（二）详情。2标量类型系统类型集由以下抽象语法定义T= U|第十章不|α。不|0，U = X| U → T|第十章U其中α∈ S，（S，+，×）是交换环.请注意，U的语法称为单位类型，不允许标量，除非在箭头的右侧。我们还定义了类型之间的等价关系如下：定义2.1设α，β∈S，T∈T。 我们定义一个类型等价·α。0 0·0. T 0·1.T T·α。（β.T）<$（α × β）.T·<$X.<$. T<$α. 公司简介典型的System F规则被更改为处理标量，如下所示222P. Arrighi，A.Díaz-Caro/Electronic Notes in Theoretical Computer Science 270（2）（2011）219► ►0r，x：U轴[U]Γu：α。（U→T）Γv：β.U→EΓ（u v）：（α×β）.TΓ，x：Ut：TΓλxt：U→T→I[U]中文（简体）T[U/X]X：=U中文（简体）中文（简体）有hX∈/FV（Γ）的∑I[X]联系我们轴0Γu：α.TΓv：β.T+IΓu +v：（α+β）.T中文（简体）Γα。u：α.TsI[α]其中U∈U和Name[Cond]表示一个规则族3主题缩减下面的定理确保了类型化被归约保留，使我们的类型系统保持一致。定理3.1（主语归约）设t→tJ.然后是r t：TrtJ：T。证据通过检查每个归约规则保持类型来进行证明。由于大量的这种减少规则的证明是高度技术性的，有27个辅助引理。 下面是一些有趣的例子Q引理3.2（α-单位）<$T ∈T，<$U ∈ U，<$α ∈S使得T <$. U.引理3.3（补）设S n是一个允许深度n证明的集合。 设Sn= Γ u + v：T. 则δ，γ，r，s，其中δ + γ = α，max（r，s） t ∈ [[T]<$]。定理4.8（可靠性）Γ D t：T <$Γt：T。证据（略）我们通过推导ΓDt：T的归纳证明了这一点（事实上，为了加强归纳假设，对T的Q定理4.9（SN对于λ 2 la）Γ Dt：Tt是强正规化的。证据 设ΓDt：T。 则根据定理4.8，Γt：T，因此根据定义4.7，如果<$（xi：Ai）∈Γ，xi∈[[Ai]]<$$>则t∈[[T]]<$. 注意，根据引理4.6，[[Ai]]是饱和的，那么xi∈[[Ai]]，因此t是强正规化的，因为[T]SN也由引理4.6.Q定义4.10设（·）q是从T\{0}到T（λ2la）的映射，定义如下：（α.X）q= X（α.<$X.T）q=<$X.Tq（α.A→B）q=Aq→Bq（A[B/X]）q=Aq[Bq/X]<$T1<$T2，Tq=Tq记法Γ q={（x：T q）|（x：T）∈ T}，且0q = T.引理4.11（与λ 2 la的对应关系）Γt：T <$Γ qDt：T q.证据设n是导出Γt：T的最小步骤数。我们用n上的归纳法来进行。224P. Arrighi，A.Díaz-Caro/Electronic Notes in Theoretical Computer Science 270（2）（2011）219基础病例（n= 1）(i)轴[U]r，x：U（r，x：U）q= rq，x：Uq，所以由axa，（r，x：U）qDx：Uq。Q(ii)对于任意T ∈ T（λ 2 la），由ax0a，Γ qD0：T，取0 =T。联系我们归纳情形在所有情形中，如果A<$0，我们可以对任意T∈T（λ 2 la）取Aq = T，并且通过使用类型等价，它仍然有效。根据归纳假设(i)Γu：α。（U→B）Γv：β.U因此，通过Γu v：（α×β）.B→Ea→E ，ΓqDu v：Bq=（（α×β）.B）q.(ii)r，x：U，t：AΓλxt：U→A中文（简体）→I[U]由归纳假设Γq，x：UqDt：Aq，所以由→Ia，ΓqDλxt：Uq→Aq=（U→A）q.根据归纳假设(iii)X：=UΓ qDt：（<$X.B）q= X.B q， 因此， ΓqDrt：B[U/X]q q(iv)t：T中文（简体）[X]t：B [U/X]。通过归纳定理，我们得到了：Tq，soby， a，ΓqDt：<$X.Tq=（<$X.T）q。(v)Γu：α.AΓv：β.AΓu+v：（α+β）.A通过归纳假设，我们得到了：ΓqDu：Aq和ΓqDv：Aq，所以by+Ia，ΓqDu +v：Aq=（（α+β）.A）q.(vi)联系我们Γα。t：α.AsI[α]根据归纳假设，ΓqDt：Aq，所以根据αIa，α。x：Aq=（α.A）q.Q定理4.12（强正规化）T t：T t是强正规化的。证据 根据引理4.11ΓqDt：Tq，则根据定理4.9t是强正规化的。Q定理4.12确保了所有的可类型项都有一个范式，因此我们不需要对Lineal的归约规则进行闭范式的限制，因为它们只是由于在无类型设置中不可能检查规范化属性而存在这是语言的一个重要简化再举个例子1。1，像Y这样的术语在这个类型设置中是不允许的，因为所有的术语都是强规范化的。所以我们没有无穷大，因此可以放弃对这也强化了重写中的规范化和代数中有限范数的表达例4.13给定一个复杂项t。如果t有一个类型，那么它必须是强正规化的，因此有一个像α这样的项。t−α。t可以通过因式分解规则简化为（α − α）。t. 这在一步中减少到0，而不需要减少t。+IP. Arrighi，A.Díaz-Caro/Electronic Notes in Theoretical Computer Science 270（2）（2011）2192252442八、true+8. “凡所有相，皆是虚妄。5讨论5.1计算内容通过将我们的标量限制为正实数，标量类型系统可以被视为概率类型系统。例如，可以键入函数f：：= λx {x [1]。（true+ false）][1. true+3. false]}：B→B，类型系统用作保证函数保持概率总和为1（参见[2，sec.III]有关{}和[]符号的详细信息，它们与本讨论无关）。该术语可以被视为一个函数，如果它接收到true，则返回true和false的均衡分布，但如果它接收到false，它返回更多假比真。 我们可以问，如果它得到1，结果会是什么。（true + false）：F. 1 .一、（true + false）−→3 52预测，概率总和为1。为了使这种直觉更加形式化，让我们用标量的规则和语法来定义一个类型系统，其中有效的类型是经典类型（即 所有其他类型都是中间类型：定义5.1我们将概率类型系统定义为标量类型系统，并有以下限制：· S=R+，• 概率类型系统中的上下文是元组（x：C）的集合，使得C在经典类型的集合CU中，即不含任何标量的类型• 类型变量运行在经典类型上 ， 而不是单元类型，即 的家人XIE[X：=C]规则只接受C∈ C，• 在以下意义上，最终的代数是良构的：<$C∈ C，任何可导的代数：C是良构的，即使导子在中间阶段有标量出现。我们定义一个权重函数来检查一个项是否是项的概率分布：定义5.2设ω：Λ→R+是一个函数，其归纳定义为：ω（0）= 0ω（t1+t2）=ω（t1）+ω（t2）ω（b）= 1ω（α. t）=α×ω（t）ω（t1t2）=ω（t1）×ω（t2）其中b是基向量。因此，我们可以阐明以下定理，该定理表明概率类型系统中具有良构类型的每个项都可以简化为权重为1的项：定理5.3（概率论中的项的权为1）设Γ_t：C是良构的，则ω（t↓）=1.证据（略）利用t ↓上的结构归纳法，证明了Γ <$t：α.C<$ω（t↓）=α.Q226P. Arrighi，A.Díaz-Caro/Electronic Notes in Theoretical Computer Science 270（2）（2011）219nαi+m=1。i=1j=122√则上述定理意味着i=1由[2，命题2]，闭正规项具有形式<$nα i.λxti+<$mλxuj，因此，概率类型系统，标量类型系统的一个简单变体将Lineal专门化为概率高阶λ-演算。5.2计算内容：量子计算在[2，sec. IV]它示出了如何以原始方式编码量子比特和门。这种编码在标量类型系统下不再起作用。这是因为条件函数必须在每个分支上具有相同的类型，在这种情况下，它们必须在其类型中具有相同的标量例5.4阿达玛门在无类型演算中编码如下：H=λy{y[1]。（false+ true）][101. （false-true）]}。在这种情况下，2 21 1每个门的分支都是不同的：（false + true）：02. （（1 +1）. B）102。B，1。（假-真）：101。（（1−1）. B）100。因此，不可能给予阿达玛门的这种编码，因为每个分支具有不同的类型。这是一个微不足道的结果，因为我们只用大小和符号来表征向量 在类型系统的未来版本中，我们计划能够区分量子位向量和非量子位向量，允许每个分支在这个例子中返回量子位向量。这可以通过跟踪类型的正交性来完成。量子性问题已经在量子编程语言如QML中提出[1]。5.3制定逻辑内容我们可以以一种独创的方式使用Curry-Howard同构：我们可以从标量的推理规则中删除所有项，而不是在已经设置的逻辑和我们的类型系统之间建立关系，并建立标量逻辑。这个标量逻辑（SL）是第一个从量子计算启发的语言的类型系统的Curry-Howard同构中获得的非平凡逻辑。从这个意义上它不是我们为了传达先验意义而制造的特别逻辑，而是通过在量子编程语言上应用良好建立的方法而自然和合法地产生的逻辑。本节讨论的是试图理解这种逻辑的后验意义。 它有点非正式，是实验性的，但提供了几个直观结论，最后得到一个明确的结果（定理5.7）。SL似乎计算了我们在一个命题的证明中所提出的命题的证明的数量。例如，+I规则表明，为了证明2.A，我们需要在证明树中存在A的两个证明。然而，我们立即看到，这一系列规则有一个问题，因为它们简单地说，如果我们对一个命题有一个证明，那么我们就有许多证明。如果我们要删除这一系列规则，我们将失去主体归约（特别是在规则α中）。u + β。u→（α + β）。u），所以我们需要添加一个替代的类型规则，例如P. Arrighi，A.Díaz-Caro/Electronic Notes in Theoretical Computer Science 270（2）（2011）219227Γα。u：δ.TΓβ. u：γ.TΓ（α + β）。u：（δ+γ）.T根据这个交替规则，我们仍然能够导出I[·]是一个定理，但是在这个过程中，我们必须重复证明A α次，以便得到α.A，因此这种证明计数解释在某种程度上仍然成立（注意，每个α现在都是自然数）然而，考虑复制器<$λx2.x：<$X.X→2.X，它允许·==================► λx2.x：λX.X→ 2.X[X：=A]··λx2.x：A→2.Aλt：A→E►（λx2.x）t：2.A不需要证明A两次;即有一个固定的证明方法来证明2.A来自A的单一证明。 因此，我们只能说，如果我们确实使用替代规则来代替sI[·]，则前计算解释成立，但仅在削减消除之后;即。在导出树中删除所有→ E。计数证明的想法，因此将它们视为资源，非常类似于线性逻辑（LL）[7]或有界线性逻辑（BLL）[8]。然而，LL和BLL不仅计算可用资源的数量，还使得无法添加新资源。在LL中，上下文对我们可以使用的资源数量有一个明确的限制 另一方面，在SL中，我们正在计算我们使用模割消的证明数量，但没有什么阻止我们使用更多的证明。为了使这更正式，让我们引入一些符号：注5.5我们用Γ<$A <$ Δ <$B表示我们有一个证导的事实：Γα··ΔβB也就是说，除了ΓA之外没有任何其他叶子（树的所有其他叶子都是ax[·]或ax0规则），我们可以将ΔB作为导出树的结论我们称之为元蕴涵，因为一般情况下，我们可能有Γ <$A <$Δ <$B，但不是A→B，由于→I[·]规则的特殊形式，我们可能有。对于SL中的实例，我们根本不能有箭头左边的任何类型，只有U类型。我们的讨论是由Γ<$A <$ Δ<$B和A→B之间的区别来限定的。在SL中，我们没有A→2.A对所有A，只有对U，这可能意味着把U解释为LL的有界命题。然而，这种解释太脆弱了;考虑引理3.2：我们知道任何A<$α.U，因此上面的复制子<$XX →2.X仍然能够产生2.A，甚至不需要依赖于A。因此，我们清楚地有了Γ <$A<$ Γ <$2.A，不像LL中，A是否是U我们现在将看到与LL的更强联系是否可以以不同的方式出现。LL的这是元组的经典编码，参见[2，第IV节]）。在这里，我们再次没有A→AA对于所有A，仅对于U（更正式地考虑额外的类型等价228P. Arrighi，A.Díaz-Caro/Electronic Notes in Theoretical Computer Science 270（2）（2011）219（α.U）（β.V）.. （UV））。同样，这意味着把U解释为LL的有界命题，但这又 失 败 了 ， 因 为 我 们 有 ， 与 LL 不 同 ， 不 管 A 是 否 是 U ， 都 有 ， Γ<$A<$Δ<$A<$A然而，这一次的关键区别在于，没有固定的证明方法来进行克隆。事实上，如果A <$α.U，那么形式为<$X.X → X <$X的复制机肯定不会产生（α.U）<$（α.U）= A<$A，而是产生α。（UU），在LL中无法表达。对于非单位类型，从A导出AA的证明方法关键地依赖于A我们将这种直觉描述如下：引理5.6（标量逻辑规则是确定性的）设R是一个类型规则，设Q i，QJi，i = 1，.，n是连续的。然后Q1，...，Qn{R}SQ′1， . ，Q′nS′Ri，QiQJi} SSJ因此，我们可以将fl定义为一个类型规则树，并将fl看作是一个从序列列表到证明的函数。这就是我们在前面的讨论中非正式地称之为证明方法定理5.7（不可克隆）$n使得λA， λ（ΓλA）是ΓλAλΔA A。请注意，我们的不可克隆允许作为见证者的一个实例（ΓA 的证明方法，但不允许相同的证明方法对任何类型都有效。因此，在SL中不存在用于进行克隆的普适证明方法，这非常类似于在LL中不存在用于进行克隆的普适上下文Γ。请注意，通过用Γ上的量子化替换Γ上的量子化，则定理5.7是LL的一个众所周知的结果。然而，SL对“禁止克隆”的表述方式可能更符合量子理论。量子理论指出，不可能有一个通用的克隆机器，但允许克隆特定载体的机器。将Γ解释为机器可能比将Γ中的资源理解为机器更自然6结论摘要• 标量类型系统可以被看作是一个概率类型系统，保证概率函数被很好地定义。• 作为定理4.12的一个直接结果，在约化规则中取消了一些限制，不仅允许闭正规项的因式分解，而且允许强正规项的因式分解，所有可类型化项都是。• 定理5.7可能表明这种方法比LL方法更符合量子理论思想，因为在SL中，限制放在克隆机器上而不是资源上• 这个标量类型系统是迈向未来向量类型系统的第一步。标量类型系统能够处理类型向量的大小和符号在未来的系统中，我们将处理方向，即。类型的加法和正交性。P. Arrighi，A.Díaz-Caro/Electronic Notes in Theoretical Computer Science 270（2）（2011）219229确认我们要感谢GillesDoweek、BenoZahitValiron、Fr'ed'ericProst、JonathanGrattage、Simon Perdrix和Philippe Jorrand进行了富有启发性的讨论。引用[1] Altenkirch，T.，J. J. Grattage，J.K. Vizzotto和A.Sabry，An algebra of pure quantumprogramming，Electronic Notes in Theoretical Computer Science170（2007），pp.23比47[2] Arrighi，P.和G.Dowek，Linear-algebraic λ-calculus：higher-order，encodings and concilience，Lecture Notes in Computer Science（RTA17比31[3] 巴伦德雷格特P.，[4] Birkho，G.冯·诺依曼（J. von Neumann），《量子力学的逻辑》（The logic of quantummechanics），Annals of Mathematics37（1936），pp. 823-843[5] Di Pierro，A.，C. Hankin和H. Wiklicky，概率λ-演算和定量程序分析，逻辑与计算杂志15（2005），pp.159比179[6] 盖伊，S。J.，Quantum Programming Languages：Survey and Bibliography，Mathematical Structures inComputer Science16（2006），pp. 581-600[7] Girard，J.-是的，Linear logic，Theoretical Computer Science50（1987），pp. 1-102.[8] Girard，J.-是的，A. Scedrov和P.J. Scott，Bounded Linear Logic：A Modular Approach toPolynomial-Time Computability，Theoretical Computer Science97（1992）.1比66[9] 格罗弗湖K.，一种用于数据库搜索的快速量子力学算法，在：STOC212-219.[10] Selinger，P.，量子编程语言的简要概述，在：函数和逻辑编程，计算机科学讲义2998（2004），pp。1比6[11]肖尔山口W.，量子计算机上的素数分解和离散算法的多项式时间算法，SIAM Journal on Computing26（1997），pp.1484-1509年。[12] 索伦森湾H.和P. Urzyczyn，“关于Curry-Howard同构的讲座，第149卷（研究在逻辑和数学基础），美国纽约州纽约市，2006年。