Coq中的一阶线性逻辑的形式化证明及聚焦线性逻辑的完备性机械化

可在www.sciencedirect.com在线获取理论计算机科学电子笔记338（2018）219-236www.elsevier.com/locate/entcs在Coq中实现聚焦线性逻辑Bruno Xavier和Carlos Olarte1Universidade Federal do Rio Grande do Norte（UFRN），Natal，BrazilGiselle Reis2卡耐基梅隆大学，卡塔尔维韦克·尼加姆CentrodeInform'atica，UniversidadeFederaldaPara'baJoZaoPesso a，Brazil，andFortiss，Munich，Germany摘要线性逻辑被用作开发编程语言、逻辑框架和并发模型的基础（和灵感）。线性逻辑的割消和聚焦的完备性是它的两个基本性质，已经在这样的应用中被利用。割消保证了线性逻辑的一致性，并具有所谓的子公式性质。聚焦是一种证明搜索的规则，它被引入以减少搜索空间，但已被证明具有更大的价值，因为它允许指定可用证明的形状。 本文用Coq语言形式化了一阶线性逻辑并且使切割消除的证明和聚焦的完全性机械化。此外，所实现的逻辑被用来编码对象逻辑，例如在线性逻辑框架中，并证明适当性。保留字：线性逻辑，聚焦，Coq1介绍线性逻辑是由Girard[12]在 30多年前提出的，但它仍然是计算机科学家和证明理论家，被用作编程语言，并发模型[18，8，19]和逻辑框架的基础[16]。这种发展依赖于线性逻辑的两个基本性质：割消[11]和聚焦的完备性[1]。1Carlos Olarte的工作得到了CNPq、STIC AmSud-Capes项目“EPIC：EPistemic Interactive Concurrency”（Proc. No 88881.117603/2016-01）和项目FWF START Y 544-N23的支持。GiselleReis由卡塔尔国家研究基金（成员）资助的NPRP 7-988-1-178卡塔尔基金会）。在此所作的声明完全是作者的责任https://doi.org/10.1016/j.entcs.2018.10.0141571-0661/© 2018作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。220B. Xavier等人/理论计算机科学电子笔记338（2018）219割消法指出，任何具有割规则实例的证明：► Γ，A Δ，A► Γ、 Δ可以转化为同一个公式的证明，而不需要任何切割规则的实例这个定理的两个主要结论是：（1）系统的一致性，即（2）所有的证明都满足子公式性质，即：，公式A的证明，只包含子公式A. 聚焦是Andreoli[1]提出的一种证明搜索规则，它通过强制共享一些结构属性（如可逆性）的规则被分组在一起来约束证明。聚焦的完备性是指如果一个公式有一个证明，那么它就有一个聚焦的证明。切割消除和聚焦的结合允许构建强大的线性逻辑框架。依靠这两个属性，证明搜索得到了很大的改进。此外，这些属性可以用于设计证明的类型，从而允许指定/编码许多不同的证明系统（例如，微积分，自然演绎和tableaux系统）为不同的逻辑[16，17]。本文给出了一阶经典线性逻辑（LL）在Coq语言中的形式化，包括割消和聚焦完备性的证明.据我们所知，这是Coq中一阶线性逻辑的元理论的第一个形式化（见第6节）。我们的主要贡献如下：(1) 量化器：文献中大多数割消的形式化都是处理命题系统的（见第6节）。LL的一阶量化器是第5节充分性结果的基础。我们使用参数HOAS技术[4]（即，，Coq中的依赖类型）以在元逻辑中编码LL量化器。这减轻了指定替代和新鲜度条件的负担。然而，它是有代价的，因为替换引理和替换下的结构保持需要被假设为公理（见第2节的细节）。(2) 聚焦完备性：虽然一些证明系统的割消定理已经被形式化，包括命题线性逻辑[3]，但据我们所知，这形式化的证明正是Andreoli[1]提出的证明。它涉及到一些非平凡的证明转换。(3) 编码证明系统：通过依赖线性逻辑本集团使用财务处理以达致最高程度的充足性（即：从规则到部分推导）。这是通过在LL框架中可用的工程推导来匹配编码证明系统的推导来完成的。我们建立了一个自动处理证明的整个否定阶段的策略，使证明对规范/程序员来说更短更简单。机械化校样类似于纸上校样，非常直接。我们证明了这一点，通过编码系统LJ的直觉命题逻辑到LL。B. Xavier等人/理论计算机科学电子笔记338（2018）219221A组B组|1一 B|⊥乘法形式化文件A组B组|0A&B|不添加剂阶逻辑A.A.量化的A.A.&，连同它们的单位和一阶量化器：||(4) 上下文的处理：LL的一个主要挑战来自于这样一个事实，即上下文被视为多组公式，而不是集合（由于缺乏弱化和收缩）。我们证明了交换规则在LL中是可容许的，即，如果τ r在LL中可证且rJ是r的置换，则τ rJ在LL中可证。我们使用库态射的Coq很容易替代，在任何证明，等价的多集。为了做到这一点，我们扩展了Coq中的多集标准库，增加了额外的定理。此外，我们开发了在我们的形式化中（自动）处理大多数多重集证明的(5) 归纳措施：虽然更宽松的措施的高度推导可以用作归纳措施（例如，，公理规则可以有任何n的高度n），我们决定仔细遵循在切割消除证明中使用的归纳措施和聚焦的完整性，例如。，[25]和[1]。因此，我们的证明完全反映了文献中描述的程序我们的形式化可以在https://github.com/meta-logic/coq-ll上找到，论文的组织结构紧密遵循文件的结构。第2节介绍LL的语法，代码片段来自于JavaScript。v. 第三节讨论了LL的不同的递归演算和一个集中的系统（SequentCalculi. v）。第4节给出了几个关于LL的结果：结构性质（SequentCalculiBasicTheory 。 v）、剪切消除（ Cut_Elim.（五）完整性（Completeness）。v）。第5节展示了我们的形式化的应用，以证明正确的编码LJ到LL（LJLL。v）。第6节讨论了相关工作和今后的工作。我们在这里提出一些最重要的定义和定理证明中的关键情况。值得注意的是在归纳定义中），并且我们还稍微改变了符号以提高可读性。此外，在定理的陈述中，所有的变量都隐含地普遍量化。读者可以随时查阅源文件中的完整定义和证明。2线性逻辑电路线性逻辑（LL）[12]是一种资源意识逻辑，在这个意义上，公式在证明过程中使用时会被消耗，除非它们被标记为指数？（他的对偶是！），在这种情况下，它们的行为是经典的。LL连接词包括加性连接词和析取连接词，以及它们的乘法连接词和A、B、.. . *= a|一个字面||||||（一）主要问题时，在证明助理是如何编码量化器。乍看之下，我们可以考虑以下分别用于泛量化公式和存在量化公式的构造函数fx和ex的朴素| fx：（var→公式）→公式|例如：（var→公式）→公式！一？一指数222B. Xavier等人/理论计算机科学电子笔记338（2018）219|→|→||||||||||||为了定义这些公式中的项的变量替换，有必要将项类型定义为以下项的并集，例如：、var s和函数s;并且还从头开始实现替换。这意味着处理变量捕获和项的相等。如果通过元水平β -还原处理替代，就有可能避免这种不必要的官僚主义。这意味着一个量化的mulaQx.F（Q∈{λ，λ}）被表示为Q（λx.F），其中λ是一个元级绑定器。在这种情况下，我们有：| fx：（术语→公式）→公式|例如：（术语→公式）→公式这种方法被称为高阶抽象语法（HOAS）或λ树syn-tax[21，15]。在函数框架中，类型（term→formula）覆盖了该类型的所有函数。这是不可取的，因为它允许函数，称为外来术语[6]，对术语进行模式匹配，并为每种情况返回结构上（或逻辑上）不同的公式。请注意，在关系框架中，这不是问题，因为所有定义都必须具有元层次上的命题类型（不同于对象逻辑的公式类型这个问题的解决方案是要求该术语是无人居住的类型，或者如下量化所有类型| fx：对于所有T，（T →公式）→公式|例如：对于所有T，（T →公式）→公式然而，在这两种规范中，都不可能编写计算公式大小的函数（可以找到对这些问题的良好描述在http://adam.chlipala.net/cpdt/html/Hoas.html）。在[4]中提出的一个解决方案包括参数化T类型的量化变量不在量化器的构造器中这种方法称为参数HOAS。使用这种技术，线性逻辑章节Sec_lExp.变量T：类型。（* 构建变量的参数 *）归纳项：=（*项 *）| var（t：T）| cte (e: A) (* variables and constants *)| fc1（n：nat）（t：term）| fc2 (n: nat) (t1 t2: term). （* 函数族 *）归纳aprop：=（* 原子命题 *）| a0：nat → aprop（* 0-ary谓词 *）| a1：nat → term → aprop |a2：nat → term → term → aprop。（* 谓 词 家族 *）归纳lexp：=（* 公式 *）atom（a：aprop））perp（a：aprop）（*positive/negated atoms *）topbot 0 1（* units *）张量（F G：lexp） par（FG：lexp）（* 乘法 *）加上（F G：lexp） witH H（FG：lexp）（* 添加剂 *）bang（F：lexp）quest（F：lexp）（*exponentials *）ex（f：Tlexp）fx（f：T lexp）.（* 量词 *）结束Sec_lExp.常数项的类型A是全局参数。 一阶项的签名包括分别具有一个和两个参数的函数fc1和fc2族。在每种情况下，第一个参数（nat）是标识符，即，函数的名称。原子命题可以是0元（a0）、一元（a1）或二元（a2）谓词。与函数一样，自然数充当标识符。代码的其余部分应该是自解释的。我们注意到更一般的构造函数B. Xavier等人/理论计算机科学电子笔记338（2018）219223||→→||→→|→对于使用参数列表（任意长度）的函数和谓词，可以定义。然而，目前的签名对于我们的编码来说已经足够通用了，它大大简化了符号。在Sec_lExp节中定义的所有类型都由类型T参数化。因此，例如，top的类型不是lexp，而是forallT：Type，lexpT。因此，对于任何类型T，表达式top T的类型为lexp T（例如，top nat：lexp nat）。显然，线性逻辑公式的定义必须与T无关。特别是，它不应该允许对T类型的项进行模式匹配。因此，线性逻辑公式的类型Lexp被定义在所有类型T上（即，，它是依赖类型）。这同样适用于原子和术语：定义术语：=对于所有T：类型，术语T。（* type for terms *）定义AProp：=forall T：Type，aprop T. （* type for atomic proposals *）定义Lexp：=forall T：Type，lexp T.（* 公式类型*）因此，连接词必须是T上的函数，例如，定义Top：Lexp：=funT top. （* 公式T*）定义Atom（P：AProp）：Lexp：=funT atom（P T）. （* 构建原子命题 *）定义张量（F G：Lexp）：Lexp：=funTtensor（F T）（G T）. （* 式FG*）由于T永远不会被析构，因此在上面的代码中出现的所有T都可以用“_“（意思是“无关“）替换这意味着任意类型T作为参数传递，并且它不会干扰公式的结构一些即将到来的证明进行结构归纳的LL公式F：Lexp。然而，由于Lexp是一个（多态）函数，而不是一个归纳类型，Coq 在[4]之后，是归纳地定义封闭公式的概念如下：感应闭合T： Term→Prop：=| cl_cte：对于所有C，ClosedT（Cte C）| cl_fc1：对于所有n t1，ClosedT t1 → ClosedT（FC1 n t1）| cl_fc2：对于所有n t1 t2，ClosedT t1 → ClosedT t2 → ClosedT（FC2 n t1 t2）。感应闭合A： AProp→Prop：=| cl_a0：对于所有n，ClosedA（A0n）| cl_a1：对于所有nt，ClosedTt→ClosedA（fun_funca1n（t_））。| cl_a2：对于所有n t t'，ClosedT t → ClosedT t' → ClosedA（fun _fa2 n（t _）（t' _））。感应闭合：Lexp道具：=cl_atom ： forallA ， ClosedAAClosed （ AtomA ）cl_perp ： forallA ， ClosedAAClosed （ PerpA ）cl_one：Closed Onecl_tensor ： forallF G ， ClosedFClosedGClosed （ TensorF G ）cl_fx：forallFX，Closed（Fx FX）[...]这样的定义排除了在类型Term中以及因此在原子命题和公式中出现开放项varx。现在，我们需要的公理，只有封闭的结构可以建立：公理ax_closedT：for allX：Term，ClosedT X.公理ax_closedA：对于所有A：AProp，ClosedA A。公理ax_closed：对于所有F：Lexp，Closed F.上面的陈述不能在Coq中证明，主要是因为它不可能在函数类型（如Term）上进行归纳。这将需要，例如。Coq中归纳结构演算[2]本身的Meta模型。让我们224B. Xavier等人/理论计算机科学电子笔记338（2018）219⇒⇒J给出一些直觉，为什么这些公理与Coq理论是一致的。这将澄清我们强加给Lexp的封闭条件。如果1是谓词P的标识符，c是A类型的常数，则公式P（c）可以定义为定义Pc：Lexp：=funT：TypeAatom（a11（ctec））。然而，当x是自由变量时，同样的练习对P（ x）不起作用。如果我们写 定 义 Px ： Lexp ： =有 趣 的 T ： 类 型 atom （ a11（var？？））. ，然后“？？” 必须是T的居民。 由于我们对T一无所知，我们无法命名它的元素，Px永远不会类型检查。因此，项和公式都必须是封闭的（没有自由变量）。项的函数表示的另一个结果是，我们需要Coq标准库的函数可拓性公理来检查两个项/公式是否相同：公理functional_extensionality_dep：forall{A}{B：A→Type}，forall（f g：forallx：A，Bx），（forallx，f x=g x）→f= g.粗略地，给定两个函数f和g，我们得出f=g，如果f（x）=g（x）对所有x。替代品。根据量化器的定义，应该对T → lexp类型的公式进行替换，其中T是参数。 遵循与前面相同的思想（和[4]中一样），我们为这样的公式定义一个类型Subs作为（封闭的）依赖类型：定义Subs：= forall T：Type，T → lexp T。 通过量化所有的T，我们可以防止函数破坏项并改变公式的结构。现在我们需要定义一个替换的包装器这个替换函数将S：Subs和X：Term作为参数，并返回一个Lexp。第一步是将Coq的β -归约应用于S，X的类型（实例化forall）和X（第一个这种约简的结果是lexp（term T）类型，它不同于Lexp，定义为forallT：lexpT。一个lexpT由函数flatten：lexp（term T）→lexpT构造，它定义在一个由T参数化的部分中。定义Subst（S：Subs）（X：Term）：Lexp：=funT：Typeflatten（S（term T）（X T））.例如，以下步骤应用λx。T <$Q（f（x），c），为常数d。最终的Lexp居民被注释掉。定义S：Subs：= fun（T：Type）（x：T）tensor top（atom（a21（fc11（var x））（cte c）. 定义t1：术语：= fun T（cte d）。评估Subst S t1中的计算。（* 结果：funT：类型1张量1（atom（a24（fc11（cte d））（cte c）*）公式的复杂性。 即使现在有可能通过封闭定义来推理公式的结构，我们的一些证明也是通过归纳公式的权重来进行的。 我们的定义遵循标准定义（即：，W（T）= 0，W（F<$G）= 1+W（F）+W（G）等）。对于任意两项t和tJ，应该是W（F[t/x]）=W（F[t/x]）的情况。这是真的，因为替换不能对项t执行这个简单的事实在Coq中需要额外的工作首先，我们定义两个公式何时等价于绑定变量的模重命名（某些情况被省略）：电感xVariantT：项T→项T|x v t _var：forall x y，xVariantT（var x）（var y）B. Xavier等人/理论计算机科学电子笔记338（2018）219225T||→→→||→|→阿斯塔纳，A→→？►ΓW什么？A，？一个C2I型1，A型B2，B1r，A，B►Γ⊥r，A[x/e]r，A[x/t]► 一个，一个r1，r2，A► Γ，AB1r，► Γ，A阿夫特湾► Γ，AB► Γ，T阿斯塔纳，A► Γ，AB阿夫特湾► Γ，AB► ？A1，...，？An，A！► ？A1，...，？啊，！ 一► 你，？一► 你，？一► 你，？一Fig. 1.线性逻辑引入规则：e是新鲜的，即，不出现在r中。xvt_cte：forall c，xVariantT（cte c）（cte c）[...]电感xVariantA：aprop T apropTxva_eq：对于所有n，xVariantA（a0 n）（a0 n）xva_a1：foralln t t'，xVariantT t t'xVariantA（a1 n t）（a1 n t '）[.]电感电流UptoAtoms：lexp T lexpTeq_atom：forallAAUptoAtoms（ ex（ FX））（ ex（ FX[...]对于类似于上面给出的关于贴近度的论证，我们需要添加如下公理：Subs和Lexp的居民不能根据其论证做出选择公理ax_subs_uptoAtoms：forall（ T TUptoAtoms（FX T t）（FX T' t '）.Axiom ax_lexp_uptoAtoms：forall（T T '：Type）（F：Lexp），maxUptoAtoms（F T）（F T '）.因此，可以证明权重函数（定义为Exp_weight）所需的结果：定理subs_weight：对于所有（FX：Subs）x y，Exp_weight（Subst FX x）= Exp_weight（Subst FX y）。我们还形式化了命题线性逻辑，包括本节以及第3节和第4节中的所有定理。在命题的情况下，公式的类型是标准归纳类型，不需要参数（多态）定义。因此，上面的公理都不需要。在一阶情况下，删除这些公理将等于，例如，在一个更高的层次上正式化粘合剂和替代品。这绝对不是一件容易的事（见例如，[9，10]），我们不会免费获得从PHOAS方法继承的所有好处（例如，根据定义，替换是捕获避免）。3相继式演算单侧（经典）一阶线性逻辑的证明系统如图1所示。 一个公式的形式为Γ，其中Γ是公式的多重集合（即，交换是隐含的）。虽然这个系统是文献中通常使用的系统，但LL的集中证明系统配备了更多的结构。如Andreoli[1]所示，可以将收缩（C）和弱化（W）纳入引入规则。关键的观察是，公式的形式？F可以收缩，&⊕226B. Xavier等人/理论计算机科学电子笔记338（2018）219AΘ：r1，Aθ：r2，Bθ：r，Aθ：r，B&变弱了这意味着这样的公式可以像经典逻辑中那样处理，而其余的公式则被线性处理。这反映在所谓的二元序列中的语法中，二元序列具有两个上下文：► Θ，F：F：F，FcopyI► Θ：r，？F► Θ，F：Γ► Θ：aθ，a► Θ：Γ1， Γ2，A和B► Θ：Γ，AB这里，Θ是一组公式，而Γ是一组多重公式。将该线性逻辑中的πΘ：Γ解释为线性逻辑中的πθ？Θ， Γ在哪里？Θ ={？一|A∈ Θ}。然后，可以定义LL的证明系统，而不需要明确的弱化（隐含在上面的规则I中）和收缩（隐含在例如，副本和附件）。请注意，只有线性上下文Γ在前置条件中被分割完整的证明系统可以在[1]中找到。二元系统的规则被指定为归纳定义的谓词。以下代码是二元系统（在我们的文件中称为sig2）定义的摘录：归纳sig2：list Lexp→list Lexp→Prop：=| sig2_init：对于所有B L A，L=mul=（A+）：：[A-] → → B; L|sig2_bang：对于所有B F L，L=mul=[！ [F] → C_2H_2O;[女]→ βB;L| sig2_ex：对于所有B L FX M t，L=mul=E{FX}：：M → B;（SubstFX t）：：M → BB;L| sig2_fx：对于所有BL FX M，L=mul=（F{FX}）：：M→（对于所有x，N B;[SubstFX x]++M）→C18B; L[...]给定一个原子命题A：Aprop，A+和A−分别表示Atom（A）（A）和Perp（A）（A）。给定替换FX：Subs，LL量化器表示为E{FX}和F{FX}。通用量化器的规则依赖于Coq最后，++是列表连接。对于M和N的多个集合，M=mul=N表示M是多个等价于N的集合。Coq的图书馆Coq. 集. 多集将多集定义为袋（类型A→nat），从而指定给定类型A的每个元素的出现次数。对这样的袋子进行分析是很困难的，自动化也变得更加棘手。使用列表作为多集的表示似乎是一个更好（也更干净）的选择。事实上，库CoLoR（http://color.inria.fr/）遵循这个方向。CoLoR是相当普遍的，并且在其他几个定理中，形式化了关于数据结构的属性，例如关系，有限集，向量等。集. 多集，并使用Coq的多重性定义来定义多集等价。我们的Multisets模块不使用这种转换。相反，它直接使用Coq。列出具有计算给定元素出现次数的机制的列表。我们还为我们的形式化和实现的自动技术添加了一些有用的定理（例如，solve_permutation），它消除了我们在开发中所需要的关于多重集诱导措施。在我们的证明中，我们通常需要测量B. Xavier等人/理论计算机科学电子笔记338（2018）219227|→►+−|→►&推导以及所使用的切割的数量（和复杂性）。出于这个原因，我们还指定了其他变体的规则，其中这些措施是明确的。例如，在以下系统上进行切割消除的证明：归纳sig3：nat→nat→listlexp→listlexp→Prop：=sig3_init：forall（B L：listlexp）A，L=mul=（A）：：[A]00 ;B; Lsig3_CUT：for all（BL：listlexp）n cwh，sig3_cut_generalw h n c B LS n S c;B;L[...]使用sig3_cut_general： nat→ nat→ nat→list lexp→list lexp→Prop：=|sig3_cut：for all.→ m c1;B;F：：M→nc2;B;F：：N→sig3_cut_general.|sig3_ccut：for all.→ m c1;B;（！F）：：M→ n c2;F：：B;N→sig3_cut_general.请注意，有两个切割规则：Cut（sig3_cut）和Cut！（sig3_ccut）。第二条规则是在4.1节所示的割消证明中需要的。我们稍后证明，只有切割规则（sig2）的系统是等价的sig3。sig 3中的序列采用形式n<$c;B;L，其中n是推导的高度，c是使用切割规则的次数，B和L分别是经典和线性定义sign3_cut_general还明确了以下度量：w（切割公式的复杂度）和h=m+n（切割高度，包括切割规则的两个前提的高度）。这些措施在第4.1节中将是有用的。3.1聚焦系统聚焦最早是由Andreoli [1]提出的，作为一种证明的学科，以减少非决定论。证明分为两个交替的阶段：否定阶段只包含可逆规则，而肯定阶段只包含不可逆规则。连接词，T，？，则具有可逆的引入规则，因此被归类为负数。剩下的连接词是，1，，！，均为阳性。公式根据其主要连接词继承其极性，例如。，AB为正，A B为负。在LL• θ：Γ在这个阶段，L中所有的负公式都被引入，所有的正公式和原子都被移到Γ中。• θ：Γ在这个阶段，所有在A词根的正连接词都被引入。让我们提出一些规则。► Θ：ΓA，Lθ：ΓB，L► Θ：ΓθAB，Lθ：Γ1► Θ：Γ1， Γ2<$A<$B► Θ：ΓθPD► Θ：Γ，Pθ► Θ，P：ΓπPD► Θ，P：Γθ► Θ：ΓNR► Θ：ΓN12228B. Xavier等人/理论计算机科学电子笔记338（2018）219►&⊥&请注意，聚焦（focusing）当公式列表L为空时，负相结束然后，使用决策规则D1（线性）和D2（经典）来开始新的正相。最后，当当前聚焦公式为负时，释放规则切换到负阶段。这种对证明的限制有两个主要的应用：它大大减少了证明搜索空间，并允许规范设计证明，如我们在第5节中所示。聚焦系统（三系统）的规则被形式化为以前的规则。我们用WAB;M;UP L表示负相，用WAB;M;DW F表示聚焦于F的正相。类似于（未聚焦）的三进制系统sig2，我们也为三进制系统定义了一个具有显式推导高度的版本（TriSystemh）， 我们后来证明是等价的。三系统的一个有趣的特点是，我们可以定义自动策略来处理消极阶段。例如，公式p−q−k（？p+）（？q+）证明如下：示例：[] ; [];UP（[（p-q-）？p+？q+]）。用unfold p;unfold q; InvTac证明。负相（* 负相 *）eapply tri_dec2 with（F：=p+）. （* 在经典上下文上应用决策规则 *）eapplytri_dec2 with（F：=q+）.Qed。我们首先分解所有的负连接词并存储原子（NegPhase）。然后，我们必须证明两个序列（由于规则）。为了证明这些序列，我们只需要决定分别关注公式p+和q+。“... ” notation in Coq applies the tactic 检查原子的极性并在需要时应用初始规则）。3.2结构性质利用强归纳法的高度的导数，我们显示了上述系统的几个结构性质。例如，我们证明了等价的多重集证明了相同的公式（保持推导的高度定理sig2h_exchange：B1 = mul = B2 → L1 = mul = L2 → n <$B1; L1 → n <$B2; L2。此外，使用库态射，我们能够在证明过程中轻松地替换等价的多集（使用策略重写）。此外，我们证明了经典背景下的高度保持弱化和收缩定理weakening_sig2h：n <$B; L → n <$B ++ D; L.定理compression_sig2h：n <$F：：F：：B; L → n <$F：：B; L。三元系统也证明了类似的性质。唯一有趣的情况是交换焦点上下文（在完整性证明定理等价上箭头：n <$B;M;UP L→L=mul=L' →存在m，m ∈ B ; M ; UP L '.在这种情况下，由于最后一个上下文是一个列表而不是一个多集，因此不会保留派生的高度。这个定理的证明需要一些引理来证明负连接词的可逆性特别是，在一个B. Xavier等人/理论计算机科学电子笔记338（2018）219229&►►►►► →►►B; M;UP L+ +[a] + +L'，在负相期间，可以在证明期间的任何时间对公式a进行工作。这些结果对应于以下定理（所有变量都是泛量化的）：定理等价于上：B;UP（L++[T]++L '）。定理等价Bot：Bot B;M;UP（L++L' ） → B ; M ;UP（L++[] ++L '）。定理等价于：B;M;UP（L++[F] ++L► B;M;UP（L++[F G]++L '）。定理等价Par：n<$B;M;UP（L++[F;G] ++L'）→ <$B ; M ; UP（L++[ F G ] ++ L '）.等价同步定理：M++[F] ;UP（L++L '）→ B ; M;UP（L++[F]++L '）。定理等价于所有：（对于所有x，m;UP（L++[SubstFXx]++L► B; M;UP（L++[F{FX}]++L '）。定理等价性：n <$B++[F] ;M;UP（L++L'）→ B ; M;UP（L++[？F]++ L '）。这些引理的证明是通过归纳L中公式的复杂性之和进行的（即，总结L中公式的复杂性）。异步F谓词断言F是一个否定公式。4元理论本节介绍了我们的系统中形式化的主要结果：割消（对于二元系统）和聚焦系统的完备性。因此，作为一个推论，我们证明了所有这些系统（二元，三元，有/无切割规则和有/无措施）的等价性，并证明了LL的一致性。给出了主要定理的证明的关键情形和相应的策略。为此，我们将使用以下符号。我们开始使用然后，我们编写相关步骤（使用Coq例如：HI： 对所有m=n，m B;M;UP L存在 x，xB;M++L（* 归纳假设 *） H1：nB;M;UP LG：B;M++L（* 当前目标 *）（*在H1中应用H1以得出H2 *）H2：存在x，x B;M++L（*使用H2中的反演，我们显示H2（* 通过在H2' * 中使用充分性（有/无措施）得出G在涉及三元系统的证明中（第4.2节），聚焦原则很容易确定证明中的下一步/目标在这些情况下，我们不使用注释来解释证明，而是直接使用Coq粗略地说，这些策略对应于三元系统（TriSystem）的逻辑规则的一种应用。我们注意到，4.1节中的一些证明对应于可以找到的标准的双线性变换，例如，在[25]中。4.1切割消除证明的结构如下。主要定理在于表明，一个证明与一个削减可以取代证明与零削减。回想一下，切割次数的测量在系统sig3中是显式的（如c）：230B. Xavier等人/理论计算机科学电子笔记338（2018）219►►►►►►|−→−|−|−|−引理cut_elimination_base：n <$1;B;L→existsm，m <$0;B; L。这个引理代表了我们在一个派生树中消除最上层割的情况。证明，通过对切割公式（w）和切割高度（h）的复杂性进行双重归纳，即，切割规则的前提高度之和。这个引理的证明需要几个额外的引理/情况：(i) 基本情况对应于w=h= 0。割公式是一个单位或一个原子命题。此外，由于h =0，这两个前提要么是初始规则，要么是T。我们将这些情况归为下列定理。定理cut_aux：L=mul= M1 ++ M2 →0<$0; B;F：：M1 →0<$0; B;F<$：：M2 →存在m，m <$0; B; L.(ii) 在公式不是主公式的情况下，我们必须置换割并减少归纳测度h。例如，在其中一个切前提中使用规则100的情况被证明如下：H：n1<$0; B;a：：F：：T（* 0切割，高度n1. “a”是切割式 *）Hn 1：Sn1<$0; B;a：：F <$G：：THn2：n20; B;a：：M2（*0次切割，高度n2*）HI：对于所有h= n1+ n2→关于切割高度G：存在 m：nat， m<$0;B; F<$ G：： T++ M2的归纳假设（*在H和Hn 2上应用切割以得出Hc*）Hc：S（max n1 n2）=1 ;B; F：：T ++ M2（* 使用HI产生免剪切校样Hc' *）Hc '：x =0 ;B; F：：T++ M2（* usingexistswitht：=Sx the newgoalis G(iii) 当切割公式在两个前提下都是主要的时，我们用更简单的公式进行（可能的几个）切割例如，在《公约》的情况下：H1：S（maxn m）<$0;B;F<$G：：（M1++M2）（* 切割公式为F*G*）H2：S n 0<$0;B;F<$ G <$：：DH3： m=0; B; F：： M1H4： n=0; B; G：： M2H5：n0 0;B;G：：中文（简体）HI：对于所有w= w（ F G）→关于权重的归纳假设G：存在m0：nat，m0 |−0; B; M1 ++ M2 ++ D（* 在H4和H5上应用切割以得出H6*）H6：S（max n n 0）1 ; B;F：：（M2++D）（* 在H6上使用HI以产生免剪切校样H6' *）H6'：x 0 ; B ; F：：（M2++D）（*在H3和 H6上应用剪切以得出 H7*）H7：S（max mx）1 ;M1+ +M2+ +D（*在H7上使用H1以产生免剪切校样 H7（* 从H7' * 得出G案件时！是切割公式和主要要求和附加规则停！Δ，！Fθ，Fθ：Γ► Θ：Δ， Γ我们证明是可接受的（下面的定理sig2_iff_sig3）。该规则在sig3系统中编码（构造函数sig3_ccut）。然后，我们将一个Cut应用程序转换为一个Cut！降低切割高度：H1：S n0;B; [！ F]H2：S n00;B;？ F：：LH3：n0;B; [F]H4：无0;F：：B;LHI：对于所有h<=S（n + n0），切割高度G的归纳假设：存在m0：nat，m00;B;L（* 在H1和H4上应用ccut以得出H5*）H5：S（max（Sn）n 0）1;B;L（* 使用HI以获得免剪切校样H5（* 从H5' * 得出GB. Xavier等人/理论计算机科学电子笔记338（2018）219231(iv) 取消应用Cut！是相似的。使用上面的所有引理，割消的证明考虑了Coq生成的所有情况（包括对称情况）。 最后一步是证明，具有任意数目的割的证明可以被转换成没有割的证明。这可以很容易地通过归纳切削次数和使用以前的结果来完成：定理cut_elimination：for allB L n c，n |− c;B;L→存在m，m| −0 ;B; L.作为推论，我们可以证明LL的一致性定理一致性：sig3 n c [][]sig3 n c [][0]sig3 n c [][].现在我们可以证明切！规则是可容许的，因此，具有（sig3）和不具有（sig2）该规则的系统是等价的：定理sig2_iff_sig3：sig 2 B;L参与sig 3 B; L.4.2聚焦的完整性下面的定理表明，集中证明可以被二元系统模仿：定理合理性：LexpPos M → n| −F− B; M; A →| −− B; M ++（箭头2LL A）。其中谓词LexpPos声明列表/多重集合M中的所有公式都是正的，函数Arrow 2LL只是将“L“转换通过推导n的高度的归纳，证明很容易：我们只需要应用与集中证明中使用的完全相同的规则逆定理的证明，即，当然，完整性更重要。首先，我们证明了3.1节中的可逆性定理（对于负相位）。然后，我们证明了正规则的应用可以切换：定理InvCopy：|− F − B++[F];M;UP（F：：L）→LexpPosM→| − F − B++[F] ;M;UP L. 定理InvEx：|− F − B;M;UP（SubstFX t：：L）→LexpPosM→| − F − B;M++ [E{FX}];UP L. 定理InvPlus：|− F − B;M;UP（F：：L）→LexpPosM→| − F − B;M++[F <$G] ;UP