量子编程语言的形式化元级分析框架

可在www.sciencedirect.com在线获取理论计算机科学电子笔记338（2018）185-201www.elsevier.com/locate/entcs量子程序设计语言的形式化元级分析框架1Amy P.第2章加拿大渥太华大学电气工程与计算机科学学院摘要量子编程语言（QPL）的设计和开发是量子计算的一个重要而活跃的领域本文讨论了开发一种标准方法来验证QPL对主要量子计算概念的问题我们提出了一个框架，致力于元级分析的QPL，特别是，功能量子语言。为此，我们选择混合系统作为构建框架的工具。Hybrid是一个支持高阶抽象语法的逻辑框架，在此基础上，我们开发了一个用于QPL推理的直觉线性规范逻辑。我们提供了一个正式的证明，这个逻辑的一些重要的元理论属性，此外，展示了一些例子，可以解决建议的框架下保留字：量子λ演算，线性逻辑，混合，Coq1介绍量子计算有可能从根本上改变计算的方式。大规模量子机器的存在将成倍增加计算能力，并提供牢不可破的安全系统[4]。量子编程语言（QPL）是实现可靠的量子机器所需的一个组成部分，因为它们在高层次上引入了量子概念，允许更好地理解量子方面并增加对量子领域研究的访问QPL是由Knill[11]发起的，他提供了许多表达量子算法的约定（即，量子伪码）。QPL的发展已经为两种命令式语言发展，例如，[16]和[19]，以及函数语言，例如，[24]和[18]。QPL基于QRAM计算模型：量子状态或数据存储在RAM中，程序是更新这种全局量子的原始量子操作（或控制）序列。1电子邮件：myousri@uottawa.ca2电子邮件：afelty@uottawa.cahttps://doi.org/10.1016/j.entcs.2018.10.0121571-0661/© 2018作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。186M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185直觉线性S. L.混合HOAS在线客服OL类型OL操作语义OL的机械化元理论（例如，类型安全、保存、进步、健全）图1.一、QPL的正式元级分析框架国家[11]。 在编写高级量子语言和捕获量子方面的全部范围之间存在权衡，例如，无克隆和叠加特性。因此，在开发QPL时，确保所提出的语言、计算模型和操作语义（以及类型系统，如果有的话）在语言如何尊重量子特性以及如何处理量子非确定性（即，量子存储单元可以同时保持0和1值）和测量过程（即，基于某些概率确定存储单元的精确值在本文中，我们介绍了一个正式的框架，旨在规范量子语言的元级分析。这样的框架可以帮助语言设计者专注于增强语言规范本身，将许多正确性检查的细节留给所提出的框架。因此，随着语言的发展和研究这些变化的结果，只更新在每一步中被忽略的证明部分，我们在本文中关注的是函数式量子编程语言，它们通常映射到量子lambda演算[20]。量子演算相对于普通lambda演算提供的主要区别在于它解决了资源限制：量子变量（即，量子比特）是不可复制的（即，没有克隆），并且应该只消耗一次并且不能被擦除。这使得线性逻辑成为为类型化和非类型化量子lambda演算建模操作语义的一个很好的候选者为了避免让用户参与语言形式化的低级细节，例如，变量绑定和替换，我们选择使用混合系统[9]，这是一个支持高阶抽象语法（HOAS）的两级逻辑框架图1说明了我们提出的QPL Meta级分析框架的设计。OL代表对象语言，它是一种需要分析的编程语言。OL语法包含一种语言的所有可能的表达式的编码（通常包括在格式良好或其他类型的判断（如键入或评估）方面不正确的表达式）。Hybrid的使用涉及到定义一个规范逻辑（SL）。SL是独立于任何OL开发的，但是可以通过用于表达OL判断的原子谓词的参数来定制，例如， 分类和评估规则。 SL通常是一个可编程演算的形式化。我们选择实现直觉线性逻辑，其非常适合于建模QRAM计算模型，其允许直觉资源（即，控件）和线性资源M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185187(i.e.、量子数据）。中间块定义OL支持的类型的语法和基本属性。当然，在非类型化量子lambda演算的情况下不包括这个块。QPL设计者经常选择定义非类型演算来捕获最大数量的量子特征（即，构建量子图灵完备语言），这可以通过添加某些类型系统来实现。然而，所提出的框架支持图灵完备和不完备的QPL。然后使用形式化的语法和语义来推理OL，例如，证明主题约简（类型可靠性）或图灵完备性。我们正在Coq中实施拟议的框架[13]。本文介绍了建立在早期（未发表）工作[12]基础上的已完成工作，其中我们形式化了Proto-Quipper语言[18]及其一些元理论。在这里，我们从案例研究中概括出一个通用框架，重点是两个主要思想：概括SL并提供一组更完整和通用的元级别属性，可以被许多OL重用，并说明其在两个不同的QPL上的使用，即Proto-Quipper和Q[24]。虽然关于Q的工作还处于早期阶段，但它说明了框架的一般性质。本文的其余部分将更详细地讨论图1中的每个框2混合电路中的OL编码在本文中，我们使用的是作为Coq库实现的Hybrid版本这个库中的第一个文件（Hybrid.v）的目的是为表达OL的语法提供支持。核心是一个类型expr，它编码lambda项的de Bruijn表示。它在Coq中归纳定义如下：感应表达式：设置：=| CON：con -> expr| VAR：var -> expr| BND：bnd -> expr| APP：expr -> expr ->expr|ABS：expr -> expr.在这里，VAR和BND分别表示绑定变量和自由变量，var和bnd被定义为自然数。类型con是在定义用于表示OL的常数时要填充的参数。然后，该库包含一系列用于定义（expr→expr）→expr类型的运算符lambda的定义，这提供了使用HOAS表达OL语法的能力。将它的定义完全扩展到原语，给出了低级别的de Bruijn表示，当推理元理论时，它对用户是隐藏的。事实上，用户只需要CON、VAR、APP和lambda来定义OL语法的运算符。Hybrid库中的另外两个谓词将出现在证明开发中，proper：expr→Prop和abstr：（expr→expr）→Prop（其中Prop是Coq命题的类型）。正确的谓词排除了那些出现绑定变量而没有相应绑定器（悬空索引）的项。abstr谓词应用于lambda的参数，并排除类型为188M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185（expr→expr），不编码对象级语法。我们现在给出两个示例，填充在图1中右中框中。例1. 下面是Proto-Quipper[18]的上下文无关文法的一个片段，一个类型化的QPL。我们将使用这个例子来解释量子lambda演算的一般概念：T：：= qubit|T1T2A：：= 量子位|bool|A1A2|的1一个2|！一|Circ（T1，T2）t：：= q| ∗ |t1，t2一：：= X| Q（t、C、a）|真假 a 1 a 2 |λx.a|||||如果是1，则是2，否则是3|设x，y=a1ina2以上语法由语言类型和表达方式两部分组成。 我们有两种类型，量子类型T和允许复杂构造类型化的一般类型A。类型T是类型A的子集。爆破师！用于从线性类型创建可重复的类型箭头类型用于函数（即，lambda抽象）、用于键入两个表达式的张量积的Circ（T 1，T2）以及用于键入电路表达式（t，C，a）的Circ（T1，T2）。该表达式如下：电路C具有类型为T1的输入t，并产生类型为T2的输出a。请注意，输入和输出类型都是量程类型。与类型类似，原始Quipper有两种表达式：包括量子比特和这些量子比特的张量积的纯量子表达式t，以及一般表达式a。量子电路构造被认为是非纯量子表达式，因为它允许输出a具有一般表达式排序。然而，这个表达式必须评估为量子类型的表达式这个条件是通过类型和归约规则来强制执行的。请注意，如果我们强制输出表达式为纯量子排序，则此语言将不允许电路进行任何类型的计算，因此电路构造失去了它的意义和它的主要表现力。lambda抽象是这种语言的关键表达式，并提供了一种区分常规lambda演算和量子lambda演算的方法。对于表达式λx.a，约束变量x通常线性出现（即，仅一个实例）中。在Proto-Quipper中，约束变量的线性度是使用类型系统控制的，即，如果绑定变量的域是线性类型（即，前面没有Bang运算符）则X在A中出现一次;如果它是可复制的（即，前面有bang），则x在a中出现零次或多次。另一个重要的表达式是量子lambda演算独有的let语句。为了突出与函数式语言中常见的let语句的区别，我们注意到letx，y=a1ina2不等价于：令x = fst a1in令y = snd a1in a2.M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185189这里let语句的主要目的是允许通过一次访问表达式a1同时提取变量x和y。这样做的原因是为了遵守表达式a1的线性约束;注意，使用fst和snd需要多次访问a1。Proto-Quipper这种破坏类型为张量积的表达式的方式通常出现在量子lambda演算中，但可能采用不同的风格，正如我们将在下一个例子中看到的那样这种语言与常规lambda演算的另一个不同之处是包含了量子变量q。Q是所有可能的量子变量的可数无限集合。这些变量根据定义是线性的，并且它们的类型是明确已知的（即，量子位），因此在Proto-Quipper程序中没有明确指定。对于这种对象语言，con类型是用Econ类型实例化的，实现为：感应经济：设置：=Qvar：nat-> Econ |qPROD：经济|qAPP：经济|qABS：经济|qIF：经济学|qLET：经济学|Crcons：nat-> Econ.该定义为Proto-Quipper中的每个可能项提供了一个常数（即，在由上面给出的语法a定义的语言中）。自然数用于识别量子变量和电路，因为它们都同构于自然数的集合。我们不显式表示术语变量，因为它们在OL术语的HOAS表示中作为绑定变量使用这些常数，我们定义OL表达式。例如，函数应用定义如下：定义App：qexp-> qexp-> qexp：=fune1：qexp => fun e2：qexp =>（APP（APP（CON qAPP）e1）e2）.类型qexp是前面讨论的expr类型，其中参数con是用Econ实例化的。为了理解上面的定义，将HybridAPP构造函数视为表达式连接器可能会有所帮助，在本例中，它形成了一个包含e1和e2的列表。这个“列表”的第一个元素这种模式也可以在张量积的形式定义中看到，张量积是一种类似于二元运算的应用。在本例中，注释中仅定义差异（CON qPROD）：定义Prod：qexp-> qexp-> qexp：=fun e1：qexp=> fun e2：qexp=>（APP（APP（CON qPROD） e1）e2）.下一个例子是lambda抽象，我们可以清楚地看到HOAS的使用：定义Fun：（qexp-> qexp）-> qexp：=funf：qexp-> qexp =>（APP（CON qABS）（lambda（fun x => fx）））。这个例子展示了HOAS如何使用190M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185元级逻辑（这里是Coq），其中f的类型为qexp-> qexp，Coq函数fun x => f x中的绑定变量x表示Proto-Quipper lambda表达式中的绑定变量。注意lambda运算符的使用如前所述，将其定义完全扩展到原语给出了低级别的de Bruijn表示，它对用户隐藏，并且不会出现在进一步的证明开发中。 为了使这个表达式成为Proto-Quipper lambda抽象的有效表示，还需要另一个限制。我们必须排除不编码Proto-Quipper表达式的（qexp → qexp）类型的Coq函数。在定义表达OL语义的prog子句时，将使用abstr谓词强制执行此检查。OL句法的“有效”表征（也称为表征充分性）的一般问题特别是，我们必须证明，在由其语法指定的OL的术语和形式系统中的表示（在这种情况下，Coq中实现的Hybrid）之间存在双射。在[1]中讨论了lambda演算作为Hybrid中OL的表示充分性，并在[7]中详细证明。在[9]和[10]中讨论了使用混合时充分性证明的具体问题。Proto-Quipper包含lambda演算作为子语言，并且完整语言的表示充分性是这些其他结果的直接扩展。OL判断的推理规则表示的精确性也很重要。这样的证明主要是以纸上证明的形式进行的，因为它们涉及到语法的非正式和形式化的表示。对于Hybrid，这种证明的一个重要部分包括一个正式的结果，我们称之为内部充分性定理（见[10]）。下一节将讨论一个示例。下面的定义是let语句的形式化，它比前面的例子更复杂：定义Let：（qexp -> qexp-> qexp）-> qexp -> qexp：=fun f：qexp-> qexp-> qexp => fun e1：qexp =>(APP（CON QLET）(APP（lambda（fun x =>（lambda（fun y => f x y）e1））。Hybrid中的lambda运算符只支持单个绑定变量的lambda抽象。它不直接支持两个变量的乘积的绑定，这是let语句中的情况。一种解决方案是将乘积视为单个约束变量，然而，这需要使用fst和snd运算，我们希望避免这一点，因为如上所述，它们的使用违反了线性约束。相反，我们简单地使用lambda的级联出现（在这种情况下是两个），以咖喱的方式使用两个函数展开表达式（即，两个lambda抽象）。该表示符合线性条件。实施例2. 下面是Q [24]的上下文无关语法的一个片段的例子，一个无类型的QPL：a：：= x|R|A1，A2，.阿南|λ！x.a |λx.a|λx1，x2，.，x n.aM.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185191其中r是指量子变量，α1，α2，.， n是n个Q表达式的张量积（或线性模式）。Q和Proto-Quipper之间的一个主要区别是Q允许三种类型的lambda抽象：在线性变量上，绑定变量在函数体中只出现一次;在可重复变量上，绑定变量可能出现零次或多次;以及在n个元素的张量模式上。前两种类型之间的区别在Proto-Quipper中使用其类型系统，但第三种类型在Proto-Quipper中不受支持。然而，我们相信，使用用于表示Proto-Quipper的let语句的相同编码技术，在张量模式上对函数抽象进行编码是足够的，其中λ=x1，x2，.，x n.a展开为：λy0. 令<$x1，y1<$$>=y0in令<$x2，y2<$$>=y1in···令<$xn −1，xn<$=yn−2ina这种转换保证了x1，...，x n和y0，...，yn−2线性出现在表达式的主体中，只要x1，...，xn在原始表达式中线性出现。这个表示假设一个双操作数let将被添加到Q表示。必须证明这种转换的充分性，以确保表达式是等效的，语言与Proto-Quipper不同，Q的con的定义将包括两个不同的常数，即LABS和IABS。它也有常量qPROD和Qvar。第三种类型的抽象没有专用的常量，因为我们决定使用let语句对其进行编码（即，qLET）。线性和直觉抽象使用HOAS表示定义如下：定义LAbs：（qexp-> qexp）-> qexp：=funf：qexp-> qexp =>（APP（CON LABS）（lambda（fun x => f x）。定义Iabs：（qexp-> qexp）-> qexp：=funf：qexp-> qexp =>（APP（CON IABS）（lambda（fun x => f x）。请注意，在语法级别上，除了常量注释之外，两个lambda抽象都是相同的。正如我们将在下一节中看到的，真正的差异将在OL语义规则的编码中施加。还请注意，原始Quipper中的Fun定义包含（lambda f），而这里的两个定义包含（lambda（funx => f x））。这两个项是η-等价的;一般来说，Hybrid中的项在η-转换之前是等价的，这意味着任何一种形式都可以用来编码这样的OL表达式。3SL和OL推理规则的编码我们采用的直觉线性逻辑的序列作为SL（图1的左下角）具有形式Γ;ΔG，其中G是一个公式，Γ是公式的直觉上下文（一组公式），Δ是线性上下文（一组公式），并且Γ和Δ仅包含原子公式。对原子公式的限制对于我们到目前为止所考虑的例子是足够的，并且简化了使用混合的推理在[3]中，定义了一个直觉SL，它允许在上下文中使用更一般的公式。如果在我们的框架中未来的案例研究中需要这种普遍性192M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185⊗⇒∀►Γ;AAl初始化r，A;.A.A.i初始化T; ΔT TT-Rr; Δ1<$Br; Δ2<$C-Rr; Δ1， Δ2<$B<$CΓ;ΔB Γ;ΔC&-RΓ;ΔB&CΓ，A; ΔB-RΓ;ΔABΓ; Δ，A <$B -RΓ;Δ<$ABΓ; ΔλB [y/x]-RΓ; Δ λλ B收缩式Γ，A; Δ <$B弱化Γ，A1，A2;Δ ΔBA←−[G1， . ，Gm][GJ1， . ，GJn]∈[n]Γ;. i= 1，.， 米）的r;Δ iGJi （i = 1，.， n）的BCr; Δ 1. ΔnA图二. 购物中心规则使用相同的方法来扩展我们的线性SL应该是简单的，在报纸上。推理规则是一组公式（也称为子句），表示OL的推理规则，我们在展示推理规则时省略了它，因为它对每个OL都是固定的，并且在证明中不会改变。它们可以被认为是Γ的一个固定子集。特别是，我们感兴趣的直觉线性逻辑的MALL片段，其中包括连接词的乘法合取，加法合取，线性蕴涵，直觉蕴涵，和T的通用资源消费者。图2中给出了该逻辑的·规则（其中·表示空上下文）。请注意，“我们现在从上到下讨论规则。有两个初始规则，线性规则（l init）严格禁止除A之外的任何假设在Δ内存在，并且不关心Γ的内容。直觉规则（i init）严格要求一个空的线性上下文，而A应该在直觉上下文中如果它的操作数可以同时被线性证明，我们可以使用它，即， 它们不共享线性资源。另一方面，当操作数共享线性资源时，使用加法合取 因为它们都消耗所有资源，所以一次只能提供其中一个。蕴涵规则（R-R和- R）根据先行词A来自的上下文而变化。 R-R规则有一个通常的附带条件，即y不出现在Γ、Δ或B中。收缩和弱化的通常规则只适用于直觉主义语境。在bc规则中，[m]表示所有可能的子句实例（所有变量的实例化都在最外层量化的子句）。条款不M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185193任意公式，但具有由该规则的第一个前提所示的限制形式。向后应用这个规则相当于对A中的一个子句进行反向链接，实例化通用量化器，使得子句的头部匹配A。每个子目标都有一个假设，既有线性的，也有直观的。线性逻辑有许多形式化，例如，[5]在Abella和[15，23]在Coq。这些形式化的主要目的是处理线性逻辑的不同片段相比之下，我们使用线性逻辑作为中间逻辑来研究对象语言，如QPL。我们的目标更广泛，因为它包括两者。特别是，我们证明元级定理线性逻辑和齿轮我们的选择对那些有用的定理，在分析任何QPL。我们的形式化受到[9]中的工作的启发，该工作将有序直觉线性逻辑实现为Hybrid的Isabelle/HOL版本中的规范逻辑，其中它用于研究函数语言的操作语义的连续机器表示在我们的实现中，SL的公式被定义为归纳类型oo。这个定义为SL的每个连接词引入了常数：感应oo：设置：=| 原子：atm ->oo| T:oo| 连接词：oo -> oo ->oo| 和：oo -> oo ->oo| 杂质：atm -> oo ->oo| lImp：atm -> oo ->oo| 所有：（exprcon-> oo）-> oo。其中原子构造函数接受atm类型的原子公式并将其转换为SL公式。atm类型是为每种对象语言定义的，通常包括诸如typeof和isexp之类的谓词，其中前者是与QPL表达式及其类型相关的二元谓词，后者是一元良构谓词。构造函数T对应于通用消费者，Conj对应于乘法合取，And对应于加法合取。类型构造函数Imp和lImp对应于直觉和线性蕴涵，re-implication，在这两种情况下，左边的公式必须是一个原子。All构造函数接受一个函数作为参数，因此量化公式中的绑定变量在Coq中使用lambda抽象进行编码然后，SL谓词规则被形式化为类型为listatm ->listatm -> oo -> Prop的归纳谓词seq。第一个原子列表指的是直觉主义背景，而第二个列表包含线性原子。下面是一些在seq定义中形式化的规则的例子：归纳seq：listatm->list atm-> oo-> Prop：=| l init: forall (A:atm) (IL:list atm), seq IL [A] (atom A)| i init: forall (A:atm) (IL:list atm),In A IL-> seq IL nil (atom A)194M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185| s tt: forall (IL LL:list atm), seq IL LL T| m and: forall (B C:oo) (IL L L1 L2:list atm),split L L1 L2 -> seq IL L1 B -> seq IL L2 C ->序列IL L（Conj B C）| a and: forall (B C:oo) (IL L: list atm),seq ILLL B-> seqi ILL C-> seq ILL（和BC）| s bc: forall (A: atm) (IL LL: list atm) (lL iL: list oo) (b: oo),progAiLlL->splitseqL[] iL-> splitseq ILLL lL -> seqILLL（原子A）在这组规则中，我们不包括直觉语境的结构规则，如弱化和收缩。它们将在稍后被证明是可接受的，作为关于这个微积分的元定理的一部分，这对于帮助用户推理OL是很重要的。注意，我们使用类型列表来建模逻辑上下文。使用列表来建模集合，其中重复无关紧要，顺序没有意义，便于表示直观的上下文。特别地，Coq类型列表可以表现为集合，而不需要对它们施加限制然而，这并不直接适用于线性上下文，在线性上下文中，重复确实重要，尽管顺序不重要（即，如在多集合中）。对于这种情况，我们必须添加一个限制，使列表的行为隐式地像多重集一样。这个限制出现在乘法合取规则中，我们将序列的线性上下文与结论B和B连接起来，C使用split谓词。 具体地，在拆分L L1 L2中，列表L被两个列表L1和L2。这个谓词可以被看作是一个多集并运算符，因为它保留了每个元素在L1和L2中出现的次数，而不必保持在L中出现的顺序。例如，[A;B;C]的拆分可以是[A;B]和[C]、[C]和[A;B]、[A]和[C;B]或[B]和[C;A]。稍后，我们将陈述一个元级结构定理，表示这个谓词按要求工作，并且不具有可证明性。或者，我们可以使用Coq中现有的多集库。然而，我们发现这个库对于我们的目的来说太弱了，与列表库相比也不够丰富。由于我们的重点不是为多集构建一个库，因此我们选择了使用列表定义。我们想强调的另一件重要的事情是：在sbc规则中，谓词splitseq用于检查子目标列表的可证明性。谓词splitseq被使用两次;一次用于空线性上下文下的直觉子目标iL，另一次用于线性子目标lL。谓词seq和splitseq使用Coq的互感来定义。我们可以把splitseq看作是seq的推广，它证明了一系列的目标，而不仅仅是一个。splitseq谓词是在split谓词的帮助下定义的，这确保了用于证明子目标的线性上下文的并集遵守多集行为。为了保持简单，我们省略了seq谓词的一个额外的自然数参数，该参数允许在一个整数的高度上通过归纳进行证明M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185195推导 读者可参考[13]以了解全部细节。反向链接规则还依赖于类型为atm->listoo ->listoo -> Prop的归纳谓词prog，它编码OL的推理规则（例如其操作语义）。公式（progAIL L）如下：原子A（OL的推理规则的结论）在OL中为真，如果我们可以证明直觉子目标IL和线性子目标LL（一起表示OL规则的前提）列表中的每个成员稍后将给出我们的两个QPL的示例SL的实现是从[12]中的实现中显著推广的，因为我们已经证明了更多的元理论性质。由于这些属性可以应用于任何OL，这允许更完整地验证OL属性。例如，除了证明弱化和收缩是可容许的，我们还证明了切割规则对于直觉和线性上下文的可容许性。直觉规则形式化如下：引理seq cut aux：forall（a：atm）（b：oo）（ILL：listatm），seq ILLb -> seq（remove eq dec a IL）[]（atom a）->seq（remove eq dec a IL）该定理指出，如果我们从直觉假设列表IL中删除假设a的所有实例，并且发现a在新的假设列表下是可证明的，那么删除a并不影响b的可证明性。注意，remove（一个Coq列表操作）需要一个在atm类型上相等的可判定性的证明作为参数。另一方面，切割消除规则的线性版本只允许删除线性资源a的一个实例：引理seq cutlinear：forall（a：atm）（b：oo）（ILLseqIL（L ' ++ re m o v e on e eq de c a L ） b ） 。我们定义了remove one函数（在Coq列表库中不可用）来从列表中删除给定公式的一个副本。注意++是列表附加操作符的Coq表示法。弱化在直觉主义语境中的可接受性陈述如下：定理seq弱化cor：for all（b：oo）（ilil（for all a：atm，In ail-> In a需要强调的是，我们的线性逻辑版本不是有序的，即，资源在线性上下文中出现的这与[9]中定义的线性逻辑SL有很大不同。为了确保形式化逻辑确实遵守这个条件，我们已经证明了线性上下文的交换性质（即，线性上下文表现为多集），如下所述：定理seq交换cor：forall（b：oo）（illl196M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185seqil ll b->（对于所有a，count occ eq declla= count occ eq dec ll'a） - >s e q i l l l ' b 。其中计数OCC操作对给定列表中元素的出现次数进行计数。对于两个线性上下文ll和ll'，每个原子的出现次数相同，它们在列表中出现的顺序并不重要;它们在形式化SL中的任何有效证明中都是可交换的。这个定理的证明涉及到与count occ和remove one的定义有关的许多引理，即，与线性上下文的多集行为有关下面的两个示例说明了图1中左中的框。实施例3. 继续实施例1，Proto-Quipper分型判断具有形式Γ;Qa：A。在这个例子中，Γ是一个有限的类型声明集合，形式为x：A，其中x是一个变量，A是一个类型（A可以有这样的形式！C或否）。 Q是一个包含有限个量子变量集的量子上下文，通常是a中的自由量子变量。以下是Proto-Quipper lambda抽象类型规则的两个示例（共四个）：Γ，x：A; Q b：Bλr;Q<$λx.b：AB1Δ，x：！A; Qb：BλΔ;. λx.b：！一B2在规则λ1中，对于类型为B并且线性依赖于变量x的原始Quipper表达式b（即，x在线性类型为A的b）中只出现一次，则x上的lambda抽象产生类型为（AB）的函数。然后将此规则编码为专用于Proto-Quipper语言的prog子句的一部分，如下所示：| 数据库1 l：forall（T1 T2：qtp）（E：qexp ->qexp），abstrE-> validT（bang T1）-> validTT2->prog（typeof（Fun（fun x=> Ex））（arrowT1T2））[][（All（fun x：qexp=> Imp（isqexp x））（lImp（typeof x T1）（atom（typeof（E x）T2）]这里，类型qtp编码Proto-Quipper类型（在示例1中省略了其定义），validT检查此类型元素的某些格式良好条件，例如排除连续两次出现的bang。typeof谓词是归纳定义类型atm的构造函数，它将表达式与其类型相关联，而qexp是atm的构造函数，用于注释格式良好的表达式。如前所述，abstr谓词排除了不编码OL语法的qexp-> qexp类型的函数。 在此子句中，使用lImp为了确保约束变量x在函数E的主体中是线性的，即，这一假设将进入线性背景。还要注意Imp的使用;在我们的形式化中，良构性假设总是直觉主义上下文的一部分。最后，注意子目标出现在线性子目标列表中。 这是因为整个表达式Fun（fun x => Ex）的类型是线性的;它也可能包含量子变量，每个变量只能出现一次。直觉子目标列表为空。M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185197[C，a]→[CJ，aJ]条件[C，ifa then b else c]→[CJ，ifaJthen b else c][C，ifTrue then b else c]→[C，b][C，ifFalse then b else c]→[C，c]图三. if语句归约规则如果T如果F请注意，前面定义的类型oo及其所有构造函数（如atom）编码了必须为每个OL实例化的公式的通用版本。出现在prog子句中的常量原子，例如上面的一个，是Proto-Quipper的实例化版本。下面的prog子句对λ2规则进行编码，即，非线性约束变量情况：| 数据库1 i：forall（T1 T2：qtp）（E：qexp ->qexp），abstrE-> validT（bang T1）-> validTT2->prog（typeof（Fun（fun x=> Ex））（arrow（bangT1）T2））[][（All（fun x：qexp=> Imp（isqexp x）（Imp（type of x（bang T1））（atom（type of（E x）T2）]注意Imp的使用（在上面的子句中第二次出现），因为绑定变量的类型是可重复的。然而，子目标仍然必须是线性的，因为函数体仍然可以依赖于量子变量。相反，当函数体是非线性时，这些条件需要在直觉子目标列表中，即，它不包含线性类型的变量，特别是量子变量。图3显示了Proto-Quipper的归约规则的一个例子，特别是针对if语句。项[C，a]是回路闭包，其中a是依赖于由回路C产生的量子变量的原奎珀表达式，即，电路的输出。这些规则的相应正式表述如下：| ifr：对于所有C' b b' a1 a2，valid cC（Ifb a1 a2）-> valid cC~（是值b）->prog（还原C（If ba1 a2） C'（If b'a2））[atom（还原C bC 'b'）;atom（isqexpa1）;atom（isqexpa2）][]| 更真实的：对于所有Ca1 a2，valid cC（If（CON TRUE）a1 a2）->prog（reduceC（If（CON TRUE）a1 a2）Ca1）[atom（isqexp a1）;atom（isqexpa2）][]| falser: forall C a1 a2, valid c C (If (CON FALSE) a1 a2)->198M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185prog（reduceC（If（CON）a1 a2）Ca1）[atom（isqexp a1）;atom（isqexp a2）][]其中reduce是atm的构造函数，其编码→，并且因此将表达式与其简化表达式相关联，并且有效c确保回路闭包[C，a]形成有效闭包，即，a的量子变量属于电路的输出C.请注意，ifr规则仅在b不是值时才适用;否则此规则可以无限次地应用，而不会取得任何进展。当b是一个值时，应用另外两个规则之一，即，它表示布尔值True或False。回到充分性的问题，前面提到的内部充分性定理通常指出，如果一个特定的OL判断是可证明的，那么这个判断中的所有特别是，OL的格式良好性判断，例如Proto-Quipper的qexp，必须只适用于表示OL术语的qexp我们省略了细节，因为我们没有描述这里是qexp的规则，而不是非正式地描述它。例如，使用这个判断，我们可以证明判断类型的内部充分性。 这个特殊的定理指出，如果一个形式为seq iL lL（atom（typeofM T））的序列是可证明的，那么在关于上下文iL和lL的形式的假设下，序列seq iL []（atom（isqexp M））也是可证明的。换句话说，如果iL和lL是格式良好的上下文，并且M可以被证明存在于类型T中，则M是上下文iL中的格式良好的原始Quipper表达式。（参见[10]，了解简单OL的内部充分性示例实施例4. 我们选择通过考虑λ x.a和λ！x.a来自实施例2。令Γ和Δ分别是直觉和线性项变量的上下文。项λx.a（分别为λ！x.a）在Γ; Δ中是良构的，如果a在Γ，x; Δ（分别为Γ; Δ，x）中是良构的这些lambda表达式的prog子句如下：| lambda1: forall (M:qexp -> qexp), abstr M ->prog (is qexp (LAbs M))[][All（fun x：qexp=>lImp（isqexp x）（atom（isqexp（Mx）]| lambda2: forall (M:qexp -> qexp), abstr M ->prog (is qexp (IAbs M))[][All（fun x：qexp=> Imp（isqexp x）（atom（是qexp（Mx）]注意这两个规则之间的区别：线性蕴涵用于定义线性lambda抽象（它强制要求函数体包含x的一个副本），而直觉蕴涵用于定义直觉lambda抽象，它允许x的多个副本甚至零次出现。现在，我们通过展示一个示例元定理来结束我们的形式化，即主题归约（或类型可靠性）。下面的语句代表了这个定理在Proto-Quipper语言中的缩写形式，使用了前面提供的定义：定理主题归约：for allILLL CC' a a'，seq IL []（atom（reduct C a C'a'））->M.年Mahmoud，A.P.理论计算机科学电子笔记338（2018）185199seq ILLL（atom（typeof a A））-> seq ILLL（atom（typeofa 'A））。它被缩写是因为省略了适当性所需的上下文IL和LL上的某些条件。该定理指出，如果由量子电路C产生的表达式a简化为由量子电路C'产生的表达式a对于非类型化的编程 语 言 ， 上 述 定 理 的 相 应 语 句 将 略 有 不 同 ， 其 中 typeofatoms 将 被 替 换