子结构逻辑中序列演算的形式化元理论" - 线性逻辑Abella的微积分证明机器检查的证据

可在www.sciencedirect.com在线获取理论计算机科学电子笔记332（2017）57-73www.elsevier.com/locate/entcs子结构逻辑中序列演算的形式化元理论Kaustuv Chaudhuria，1 Leonardo Limab，2 Giselle Reisa，3aInriaLIX/E′colepolytechnique，FrancebFederalUniversityofPara'ba，Brazil摘要在研究微积分时，证明理论家经常需要证明系统的性质，无论是为了证明它们是“行为良好的”，适合自动证明搜索，相对于另一个系统是完整的，一致的这些证明通常涉及许多非常相似的情况，这导致作者很少详细地写它们，只指出一两个更复杂的情况。此外，大量的细节使它们对人类来说更容易出错另一方面，计算机非常擅长处理细节和重复性。在这项工作中，我们有正式的教科书证明的元理论的线性逻辑Abella的微积分。使用开发的基础设施，证明可以很容易地适应其他子结构逻辑。我们以一种直观和直接的方式将规则实现为子句，类似于逻辑编程，在显式上下文中使用多集运算。虽然证明是相当大的，他们的写作不超过几个星期，一旦正确的定义被发现。这是一个证据，证明机器检查的证明性质的微积分可以获得使用自然编码的大多数证明助手。关键词：序列演算，割消，形式化证明，线性逻辑，Abella1介绍顺序演算证明系统可能是用于公式化逻辑的最标准的技术。新的逻辑几乎总是根据微积分提出的。这样的建议通常也伴随着某些关于微积分的元定理。切割消除通常是要建立的第一件事之一其他的元定理包括恒等式归约，它显示了证明系统的内部完备性;建立连接词的极性的规则排列和反转引理;以及建立1kaustuv. inria.fr2leonardo. gmail.com3giselle. inria.frhttp://dx.doi.org/10.1016/j.entcs.2017.04.0051571-0661/© 2017作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。58K. 乔杜里等人/理论计算机科学电子笔记332（2017）57正常形式。虽然这个元理论非常重要，但证明很少详细说明，更不用说由证明助理正式检查了。一个很大的原因是，这些证明涉及到许多情况，这些情况有时在系统中的规则数量上是指数出版物中的一个常见方法是详细展示一两个典型案例，然后提到其余的是这种非正式的证明是有风险的。Girard自己低估了指数线性逻辑中割消的困难。终止证明需要一个更复杂的归纳措施，并在[4]中详细介绍。在文献[2]中证明了完全直觉线性逻辑（FILL）割消的一个错误，该证明的作者后来发表了一个完整的修正版本[3]。可证明性逻辑GL的可积演算GLSV的割消证明是许多争议的来源，直到[9]中解决并在[5]中使用Isabelle/HOL形式化。一些为双直觉主义逻辑提出的微积分在[15]中分析并修正了错误。最近在[13]中修正了模态逻辑嵌套系统的割消证明中的一个错误。这些证明的重复性和细节密集性使它们成为计算机化的良好候选者。然而，很少发现这样的证明沿着他们的非正式论点的路线形式化。事实上，这些证明的形式化需要对非正式证明中通常隐含的细节进行形式化。这些包括引理集和多重集，我们采取的标准（和不可见）的背景。我们认为，这种基础设施的发展和上下文操作的显式推理使得证明理论家不愿意正式化元理论证明。因此，我们决定将这种“民间智慧”付诸测试，并将线性逻辑的各种片段的几个微积分的元理论形式化。据我们所知，这是它的第一个形式化。我们遵循通常的教科书归纳证明的削减公式和/或证明高度的排名，重写削减到更小的削减。我们证明了几个系统的割容许性、推理规则的可逆性和广义恒等式。我们的研究结果表明，与一个良好的编码的多集及其属性，特定的元定理的形式化可以快速完成。此外，我们的形式化只使用基本定理证明技术，可以解释和本科生进行。所有需要的是证明理论和逻辑编程的基础知识。我们已经使用了证明助理阿贝拉为这项任务。我们的选择仅仅是出于对工具的熟悉程度。 到目前为止，编码不使用Abella的任何独家功能，可以在任何其他支持归纳的证明助手中复制（我们也有多集库的实现和一些Coq证明的元定理可在以下网站上找到该实施方案：https://github.com/meta-logic/abella-reasoning网站。K. 乔杜里等人/理论计算机科学电子笔记332（2017）57594本文的结构如下。我们在第2节中简要介绍Abella，并在第3节中继续编码。我们解释了如何实现多集，并展示了它们是如何用于指定的微积分规则。割消证明包含许多情况，我们对其中之一进行了详细的解释。通过密切关注第3节，我们应该能够将该方法推广到其他微积分。其他形式化的微积分及其元理论将在第4节讨论。2背景：Abella我们使用交互式证明助手Abella[1]来形式化我们不同的Meta理论证明.Abella背后的逻辑是直觉主义一阶逻辑的保守扩展;与本文相关的扩展是：• 纯粹的简单类型λ-演算作为术语语言，以及在这些术语上的原始等式谓词，其实现了与所有被视为构造器的未解释常数的αβη-等价。逻辑是建立在这个简单类型化的术语语言之上的，遵循Church的简单类型理论的设计 那里是一个专用于逻辑公式的类型prop，所有逻辑连接词都是作为目标类型prop的常量实现的;例如，conjunction_prop 的类型为prop→prop→prop，尽管我们将其内联编写为A_prop_B而不是卡里亚湾• 最小和最大固定点定义的谓词，即。，目标类型prop的常量。这样的定义配备了相应的归纳和共归纳规则，分别用于对假设和结论进行推理，并且可以另外展开，以用谓词的相应主体来替换谓词的任何实例。• 支持extensional universal（扩展泛量化）。外延变量，称为特征变量，允许在推理方程或案例分析期间由任意项实例化这可以通过以下公式你好（x=c）<$p（x）<$p（c）（对于某个常数c），这是可证明的，因为分析x=c具有用c实例化x的效果，减少了证明对p（c）的义务。 但是，阿克斯。x = c是不可证明的5-例如，它在模型中c是唯一的元素。 阿贝拉也有存在主义量化（quantification）和在两者之间起中介作用的内涵量化（intensionalquantification）;后者与本文无关Abella的全面介绍，包括本文中未使用的功能的讨论，可以在教程中找到[1]。G的证明理论，Abella的逻辑基础，在[7，8]和参考文献中描述不像许多其他流行的证明助手，如Coq，Agda，Isabelle等，Abella遵循关系方法，而不是功能方法来规范。关于Abella中项的方程理论不能被扩展为[4]更准确地说，在微积分G[7，8]中使用左引入规则来处理等式。5我们将s/=t定义为公式（s=t）的最小值。60K. 乔杜里等人/理论计算机科学电子笔记332（2017）57函数定义，因此术语语言只是由变量、常数、λ-抽象和应用构建的普通λ-项如果我们用两个常数z：nat和s：nat→nat声明一个自然数的nat类型，那么加法加的定义将根据nat→nat→nat→prop类型的关系给出，该关系将前两个参数与第三个参数中的和具体而言，这一定义具体如下：定义加号：nat-> nat-> nat->支持;加上zX X;plus（sX）Y（sZ） ：=plusXYZ.这个定义由两个用分号分隔的定义子句组成，每个子句都由一个头部和一个可选的主体组成，：=. 每个子句也隐含地在其大写的标识符上全局关闭。上面的第一个子句声明，对于任何X，原子加上zX X为真（子句中省略的主体代表真）。第二个分句说，对于每个X，Y和Z，原子plus（sX）Y（s Z）为真，当且仅当plusXY Z为真。此外，这个谓词被赋予了一个最小固定点的解释，意味着除了使用两个定义子句之一之外，没有其他方法可以导出plus stu（对于任何项s，t和u）注意，谓语的定义分句因此，迭代地展开关系可以是非确定性的和非终止的。为了证明关于这种最小不动点定义的定理，我们使用内置的归纳策略，它对每个定义都有相同的行为。作为说明，考虑以下定理：定理m+ z_2：对于lX，+sXzX.为了证明这个定理，我们需要对X的结构进行归纳（它是nat型的）。然而，由于Abella中唯一的归纳原则适用于最小固定点定义，我们需要将nats的结构具体化为这样一个定义：定义是_nat：nat->支持;is_nat z;is_nat（sX） ：=is_natX.因此，我们可以将定理表述如下：6定理m+ z_2：对于所有的X，m + z_2是x+x +z.注意，常量的类型签名本身并没有被赋予任何归纳原则，因为签名是开放式的;例如，它总是可以用nat类型的新常量来扩展。然而，没有这样的扩展可以证伪定理，因为is_nat谓词是不可扩展的。证明开始于对1的策略调用归纳，这表明第一个假设是_natX的归纳，称为归纳论点。由于is_nat有两个定义子句，因此需要考虑两种情况。在第一种情况下，我们将获得方程X =z，以便将is_natX与子句头is_natz相匹配;这反过来将（特征）变量X实例化为6具体的syntax为，T，：->，true，false，/\，\/，forall，exists，nabla。K. 乔杜里等人/理论计算机科学电子笔记332（2017）5761⊥⊥z，留给我们的义务是plus z zz，这很容易由plus的第一个子句证明。在第二种情况下，我们会得到X =sX1，其中X1是一个新变量，我们知道它是_natX1。现在的目标是plus（sX1）z（sX1），我们可以使用plus的第二个子句将其展开，以将其简化为plusX1zX1。因此，我们有义务从假设is_natX1证明plusX1zX1。为了归纳地结束这个循环，Abella通过归纳来推断归纳变元的大小，在本例中是is_natX。[7]归纳策略的最初运用产生了一个归纳假设IH：IH：对于所有X，是_natX 联系我们PlusX ZX在这里，is_natX *代表一个is_nat的实例，它严格小于目标中的初始is_natX事实上，目标被改写为：对于所有X，is_nat X @ - - >-加上X ZX其中注释@表示其大小使得每个带 * 注释的实例严格地更小。 展开假设is_nat X @严格地减小了它的大小，因此在它的第二个定义子句的情况下，我们得到一个新的假设is_natX1 *（其中X =sX1）。现在可以将其馈送到IH以获得plusX1 z X1，这就是我们完成证明所需的。尺寸标注表示线性排序尺寸的（强）归纳，但Meta理论证明充斥着更复杂排序的归纳，特别是词典排序。虽然Abella底层的逻辑G具有可以表示任何（可计算的）良序的一般它使用大小注释和循环归纳假设在阿贝拉需要进一步推广的词典编纂归纳。这是通过嵌套调用归纳策略创建的大小级别来实现的嵌套归纳最好用一个例子来解释：考虑阿克曼函数的这个关系定义，其中ack XY K代表K=A（X，Y）。定义ack ：nat->nat->nat->道具通过;ackzX（sX）;ack（sX）zK：=ackX（sz）K;ack（sX）（sY）K ：=existsK1，ack（sX）YK1/\ackXK1K.我们可能希望证明这是一个全关系，这是一个著名的不能单独用自然数归纳法来完成定理ack_total：对于所有X Y，is_natX->is_natY->existsK，is_natK /\ackXYK.在这种情况下，我们希望使用is_natX和is_natY的大小的字典排序进行归纳，即如果is_natX的大小严格较小，或者它保持不变而is_natY的大小严格较小，则可以使用归纳假设。在Abella中，我们使用以下调用来编写[7]最小固定点定义的每一个实例在直觉上都是等价的，除非在展开它有限次之后它能被证明是真的因此，带有子句的非终止定义如p X：=p（sX）将被解释为。这样定义的原子的大小是以这样一种方式定义的，即它大于它需要展开以确定它是真的次数这些尺寸注释的精确理论不在本文的范围内，但可以在[6]中找到。62K. 乔杜里等人/理论计算机科学电子笔记332（2017）57感应对1.感应2号。这产生了两个归纳假设，并将目标修改如下：IH1：对于所有X Y，为X * - - >- is_natY - - >- ...IH 2：对于所有XY，is_natX @->is_natY **->.=-期刊题录与文摘-期刊详细文摘内容forallXY，is_nat X@ - ->- is_natY@@ - >..哪里... 在每种情况下，is_existsK，is_natK/\ackX Y K。 假设IH 1是我们以前熟悉的：它只是意味着is_natX* 严格小于is_natX @。另一方面，假设IH2具 有 严格小于is_nat Y的is_natY **。这个假设也有一个假设是_natX @，它只能由相应的未修改的假设提供！重写的目标。请注意，@和@@注释彼此之间没有关系，只是表示后者是在对前者进行归纳的同时引入的。因此，is_natX @将展开以产生*注释，并且is_natY @@将展开以产生**注释。在本开发的其余部分，我们将遵循某种特定风格的规范，其中类型谓词（如is_nat）在证明中没有显式假设，而是通过对其他谓词的反转产生的再一次，一个例子最好地说明了这一点：再次考虑加关系，但重写，以便下面的定理成立：定理plus_is：对于所有XYZ，plusXYZ->is_natX/\is_natY/\is_natZ。这样写意味着我们永远不需要同时假设is_natX和plus例如，X Y Z，因为前者可以从后者导出。以下是我们如何修改plus的定义以保证plus_is：定义加号：nat-> nat-> nat->支持;pluszXX ：=is_natX;plus（sX）Y（sZ） ：=plusXYZ.plus_is的证明是通过关于plusX Y Z的直接归纳法。请注意，我们本可以在定义分句的主体中加入更多的is_nat连词，但上述选择是足够的。我们将选择尽可能少地改变自然定义子句，以产生必要的反演引理。3对对象语言进行在下文中，我们区分对象逻辑，我们正式建立元定理的逻辑和证明系统，以及元逻辑，这是形成Abella基础的推理逻辑G3.1编码对象公式在本文中，我们将专注于命题线性逻辑，既简化了介绍，并避免转移到对象类型系统的表示。线性逻辑的公式被编码为目标类型o的常数，这是Abella中为基于高阶的特定规范语言保留的类型。K. 乔杜里等人/理论计算机科学电子笔记332（2017）5763输入m，nato matm->o。类型十个，从o-> o-> o。第一种，倒O型。典型的是h，加上o->o->o。类型上，零。定义是调频 ：o - ->-支持;is_fm（atomA）;is_fm（natomA）;is_fm（tensAB） ：=is_fmA/\is_fmB;is_fm one;is_fm（parAB） ：=is_fmA /\is_fmB;is_fm bot;is_fm（wthAB） ：=is_fmA /\is_fmB;is_fm top;is_fm（plusAB） ：=is_fmA/\is_fmB; is_fm zero.Fig. 1.公式的定义遗传Harrop公式然而，在本文中，我们不会使用Abella的规范逻辑，所以我们重用o类型来访问内置于o列表中的方便的列表语法，使用类型olist。8图1给出了MALL单侧公式的线性逻辑公式的定义。 我们定义了一个新的谓词基本类型atm;由于类型签名在Abella中是开放式的，我们的开发将对这种类型的居民进行参数化。从这种类型中，原子和否定原子分别使用atom和natom构建。我们在单侧公式化中保持负正规形式的公式，所以唯一形式上被否定的公式是原子。与这些原子一起，我们定义谓词is_fm，用于归纳公式的结构3.2多重集MALL的单边微积分表示的关键要素是MALL上下文的定义，它必须满足以下要求。(i) 给定两个上下文Γ和Δ，我们必须能够判断它们在结构上是相同的，这意味着它们包含具有相同多重性的相同元素。(ii) 给定上下文Γ和Δ以及一个公式A，我们必须能够认识到，当将A加到Γ时，会产生一个在结构上与Δ相同的上下文。此操作是实现推理规则所必需的，因为它用于表示将主公式添加到规则的结论中，并将主连接符的操作数（如果相关）添加到前提。(iii) 进一步推广这一点，给定三个上下文Γ，Δ和Θ，我们必须能够也就是说，当将Δ的所有元素添加到Γ时，导致在结构上与Θ相同的上下文，即，，Θ是Γ和Δ的并或多集并。此操作不仅需要实现乘法规则（如乘法），而且还需要定义切割这里有一个比预期更大的设计空间第一次尝试可能是8阿贝拉具有单形模式系统。一个多态扩展正在进行中，当它可用时，将只有一个参数多态类型的列表。64K. 乔杜里等人/理论计算机科学电子笔记332（2017）57类型为_oo->prop .定义 is_list：olist ->支持; is_list nil;is_listt（A） *L） ：=is_oA /\is_listL.%adjJ一 K ：K是J与一插入某处定义adj：olist -> o->olist ->propby;adjLA（A **L）：=is_oA/\is_listtL;adj（B：：K）A（B：：L）：=is_oB/\adjKAL.%mergeJKL：JunionKequalsL.定义合并：olist ->olist ->olist ->prop by;merge nil nil;mergeJKL：=existsAJJLL，adjJJ一个J /\adjLLAL/\mergeJJK会;mergeJKL：=existsAKKLL，adjKKAK/\adjLLAL/\mergeJKKLL.%染JK ：J和K有的相同元件定义perm：olist ->olist ->prop by烫发零零;每米 ：=existsAKKLL，adjKK一个K /\adjLLAL/\permKKLL.图二. multisets的实现简单地使用olist作为上下文的表示，添加由list consing（：：）表示的元素，并使用list append连接上下文。 这使得上下文的归纳推理相当简单，但是，由于线性上下文在结构上是相同的模交换，它需要向系统添加显式的交换规则，这使得元理论复杂化。另一种可行的方法是仍然使用olist作为我们的表示，但将结构同一性的概念放宽如下：如果一个列表是另一个列表的置换，则两个列表在结构上相同。因此，我们需要一个谓词perm：olist->olist-> prop来识别列表排列。为了用这个修改过的概念来定义加法运算，我们可以继续使用列表cons，但这仍然需要一个显式的交换规则。相反，我们定义了一个广义的cons操作，称为adj，它在olist中的某个地方添加一个元素，不一定在头部。注意，这个定义仍然对元素的顺序敏感;例如，adj [b，c] a [a，b，c]成立，而adj [b，c]a [a，c，b]不成立。有了这个定义，用归纳法来定义perm就很简单了：如果两个列表是通过调整相同的元素产生的，那么它们是置换相等的最后，为了定义olists到置换的连接，我们简单地简化了这个过程：一个olist是两个olists的连接，写作merge，如果它是通过调整它们的元素产生的图2给出了我们刚刚描述的多重集的编码。它将adj作为原语，并在其上构建perm和merge。我们可能会认为perm是原始的，并以它的术语或其他组合来定义其他操作，但我们发现我们的选择相当直观。此外，Abella文件lib/merge.thm和lib/perm.thm包含关于多重集的定理，这些定理在微积分证明的转换中被广泛使用。其中包括一些简单的性质，比如merge定理perm_merge_1：所有JKLJJK. 乔杜里等人/理论计算机科学电子笔记332（2017）5765► ΓT2► 一个，一个初始化变量1，A ，B► Γ1、Γ2、A和B1r，A，B1B1你好► Γ，AΓ，B► Γ，AB&► Γ，T阿斯塔纳，A► Γ，AB阿夫特湾► Γ，AB图三. MALL的单侧微积分定义商城 ：olist ->支持;mallL：=existsA，adj（natomA：：nil）（atomA）L;mallL：=existsABLLJJKJK，adjLL（tensAB）L/\mergeJJKKLL/\adjJJ A J/\mall J/\adjKK B K /\mallK;mall（one：：nil）;mallL：=existsABLL J·K，加jLL（部分AB）L /\adjLLAJ/\adjJBK/\mallK;mallL：=existsLL，adjLLbotL /\malllLL;mallL：=existsABLL J·K，adjLL（wthAB）L /\adjLLAJ/\mallJ/\adjLLBK /\mallK;mallL：=existsLL，adjLLtopL;mallL：=existsABLLJ，adjLL （加上AB）L/\adjLL一个J /\mallJ;mallL：=existsABLLJ，adjLL （加上AB）L/\adjLLBJ J.图四、单侧MALL的编码合并JKL->每MJJJ->合并JJKL。我们还需要更复杂的引理，比如merge的结合性。Theoremmerge_asshole：for allJK LJKKLJKL 1 JKL 2，合并JKJK->合并KLKL->mergeJ KL JKL 1-> merge JK L JKL 2 - >烫发JKL 1JKL 2。这可以更生动地描述如下，其中箭头定义了要合并的前两个参数，并且“”表示perm。JK LJKKLJKL1系列 JKL2系列要证明这个定理，需要证明perm是一个等价的，特别是它是传递的，这是一个令人惊讶的不直观的归纳证明。这些性质通常被认为是理所当然的非正式证明削减消除。尽管如此，我们的经验是，形式化割消所需的多重集的每一个性质都可以通过直接归纳法得到证明3.3单面MALL我们已经使用上述多重集合的编码来定义经典线性逻辑片段的几个单侧和双侧的可积演算在这里，我们给出了一个说明的单边乘加片段（MALL）。此片段⊗&⊕66K. 乔杜里等人/理论计算机科学电子笔记332（2017）57定义双 ：o->O->支持;dual（atomA）（natomA）;dual（tensAB）（parAABB）：=dualAAA/\dualBBB; dual一个机器人;dual（plusAB）（wthAABB）：=dualAAA/\dualBBB; dual零顶。图五.一个不对称的对偶谓词。的形式是，其推理规则（无切割）可以在图3中找到。这个逻辑判断是用归纳定义的原子小L来编码的，其中L表示Γ。图4给出了mall的定义。每一个定义分句都精确地描述了推理演算的一条规则，其中分句的头部定义了推理规则的结论，分句的主体定义了前提。例如，第二个定义子句，首先使用adj从L中删除主公式十A B，产生LL;然后使用merge将其分为JJ和KK，之后将每个操作数添加到其中一个组件中以构建相应的小前提。请注意，我们没有明确的交换条款。然而，我们可以通过直接的归纳建立下面的定理理论mmall_perm：对于lKL，m allK->permKL->m allL。请注意，定理本身并没有说明小K和小L的大小，即使在交换是保高容许的情况下，在这个系统中也是如此。因此，单侧割容许定理需要以这样一种方式建立，即应用置换的结果的大小与归纳假设无关。事实上，我们将以这样一种方式建立单侧公式，即只有包含正变量的导数的高度-在聚焦的意义上-与切割公式有关。为此，我们定义了一个非对称谓词对偶，它将一个正公式与它的对偶联系起来，如图5所示。对于作为对偶的第二个参数的否定公式，我们将通过直接归纳来证明反演引理。定理bot_inv：对于所有JL，小L->adj J botL->小J。定理par_inv：对于所有LJJA B，mallL->adjJJ（parAB）L->存在KK LL，adj JJ A KK/\adj KK B LL/\mall LL。定理W_inv：对于所有LJJ A B，mallL->adjJJ（wthAB）L->存在sKKLL，adjJJAKK/\mallKK/\adjJJBLL/\mallLL.切容许定理然后使用我们的非对称对偶谓词如下：定理切割：对于所有A BJJ J KK K LL，对偶 A B->adjJJ A J ->mallJ ->adjKK BK->mallK->mergeJJKK LL->小LL。这个证明是通过对第一和第三个假设的嵌套归纳来进行的。这种嵌套编码了以下措施，以吸引归纳假设：由于对偶AB的情况分析，秩下降，或者秩保持不变，小J的高度，这代表包含的推导K. 乔杜里等人/理论计算机科学电子笔记332（2017）5767► r3，AEB► Γ1，A► Γ2，BβED1► Γ2，B► Γ3，A，B切割公式对的正半部分减小。为了说明证明，这里是在导出小J时应用的最终规则是π的情况。直观地说，我们希望实现以下减少：D1D2D2−1► Γ1、Γ2、A和B► Γ3，AB切~► Γ1，A► Γ2，Γ3，A切割切割切割被减少到两个较低等级的切割，即使切割的正确前提可以有更大的尺寸。注意对反演原理的诉求。在证明中，这对应于以下证明状态：IH：对于所有A BJJ J KK K LL，双 A B*->adj JJ A J -> mallJ ->adjKK B K->mall K-> mergeJJ KK LL-> mall LLH2：adj JJ（tens A1 B1）JH4：adj KK（par AA BB） KH5：mall KH6 ：mergeJJKKLLH7：adjLL1（tensA1 B1）JH8 ：mergeJJ1KK 1LL1H9 ：adjJJ1A1H10 ：商城J1**H11：调整KK1 B1 K1H12 ：商城K1 **H14：烫发JJLL1H15：双 A1 AA*H16：双 B1 BB*=-期刊题录与文摘-期刊详细文摘内容小型LL将par_inv应用于H4和H5产生新的假设：H17：adj KK AA KK2H18：adj KK2 BB LL2H19 ：商场LL2下一步是创建上下文Γ2， Γ3，A，这是B上第一次切割的结论。在当前证明状态下，这对应于合并KK1（T2）和KK2（T3，A1）。在合并上下文之后，我们可以应用归纳假设IH，对应于B上的切割，这给了我们以下新假设：H22：mergeKK1KK 2LH23：mallL现在我们需要在A上应用割，但是为了构建这个割的上下文，我们需要做几个手术首先，我们需要从上下文中辨别AA（A）L（Γ2， Γ3，Aλ）.这是通过merge_unadj_2定理完成的，它是多重集库的一部分。定理merge_unadj_2 ：对于所有JKLKKA，mergeJKL->adjKKAK->existsLL，adjLLAL /\mergeJKKLL.在应用这个引理之后，我们将有一个变量LL 3（Γ2， Γ3），因此我们可以将其与JJ 1（Γ1）合并，以得到A上的割的结论。现在可以应用IH来获得以下新假设。H24 ：adjLL3AA LH25：mergeKK1KKLL3H28：mergeJJ1LL3L1H29 ：购物中心L1► Γ1、Γ2、 Γ3► Γ1、Γ2、 Γ368K. 乔杜里等人/理论计算机科学电子笔记332（2017）57►这个例子几乎是完整的：我们只需要证明L1是LL的置换，然后在H29上调用mall_perm。观察到它们表示相同的上下文Γ1， Γ2， Γ3，但构造不同：LL是（Γ1，Γ2），Γ3，而L1是Γ1，（Γ2， Γ3）。我们可以首先将merge_perm_1应用于H6和H14以获得：H30：mergeLL1KKLL最后，我们可以对H8、H25、H26和H30应用merge_ascurry来获得所需的：H31 ：烫发当地雇员3.4指数情况虽然MALL的切割消除证明在细节上很长，但它并不特别困难，因为总是有一个切割要消除。对于指数，情况变得复杂得多，因为单一的切割规则不再足够，或者更准确地说，消除切割的终止措施要复杂得多。主要的问题是通过收缩规则来置换cutsDE？ΓD1，A！？ΓD1，A！► ？1！一► r 2，？AE？A.切割► ？1，A！► ？1！一► r2，？A，？A对照► r2，？剪得很短► ？1！一~► ？Γ1，Γ2，？一个小切口†► ？1，？Γ1、Γ2对照品你说呢？Γ1，Γ2？Γ1、Γ2cut的实例是有问题的，因为两个前提在技术上都不是严格的较低测度：左前提中的高度和切秩是相同的，而右前提是可以任意更大的切的结果这个问题可以通过多种方式来解决，例如通过将切割公式上的收缩次数作为度量的一部分来解决。然而，要正确地制定这样的措施，我们需要纳入多集排序，这是目前不支持Abella因此，我们使用一个不同的-但仍然是标准的-解决方案，即移动到具有形式为r; Δ的序列的二进微积分，其中r被解释为一个集合-即。，承认收缩和削弱-这积累了？-公式。这个上下文在二进制规则中被附加地处理，并且在公理规则中被允许为非空重要的是，通过将上下文分成区域，我们必须增加切割原则的数量，以说明两个区域中切割公式的出现具体来说，二元公式需要两个切割：Δ1，Ar;Δ2，Ar► Γ;Δ1，Δ2截线，截线► Γ; Δ诉诸归纳假说的条件现在更加复杂了。如果割秩较小，或者如果A的导数具有较低的高度，则可以使用IH，但是在两者保持相同的情况下，我们可以将割减少为ucut。的►K. 乔杜里等人/理论计算机科学电子笔记332（2017）5769►上述收缩问题再次出现，作为以下失职问题► rD;AΓ，AE;Δ，ADL► Γ，A;Δcut~► Γ; Δ► rD;A► rD;A► Γ;ΔΓ，AE;Δ，A乌库特► Γ; Δ，A-截割然而，由于允许一个ucut来证明一个cut是合理的，所以不存在终止问题。形式化这个证明需要对MELL（乘法指数线性逻辑）序列的表示进行一些修改，现在将其作为三元谓词mell：nat->olist->olist-> prop给出。 第一个论点tomell是导子高度的显式界限，它允许我们显式地推理高度，而不是根据最小固定点定义的隐式大小。这个高度在谓词在其定义子句的主体中的每一次递归出现中都显式地减少了一个;例如，下面是对应于的子句：;mell（sX）QLL：=存在sABLL，adjLL（十个sAB）L/\existsJJKK，mergeJJKKLL/\（ existsJ ， adjJJAJ/\mellXQLJ ） /\（existsK，adjKKBK /\mellXQLK）为了对两个切割之间的排序进行编码，我们需要在切割定理中引入一个额外的权重我们在Abella中编码如下：种体重类型类型重，轻重量.定义是权重：重量- ->-支持;is_weight light;is_weighttheavy：=is_weighttlight.请注意，is_weightheavy和is_weight light都是真的，但前者需要严格的展开操作才能导出。这对于排序两个cut是足够的，我们写如下：定理切割：对于所有ABXW，dualAB->is_natX->is_weightW->（W=light/light）对于所有JJ JKKK QL Y LL，adj JJAJ -> mell X QLJ ->adj KK B K-> mell Y QL K-> mergeJJ KK LL->存在Z，混合 ZQL LL）\/（W=重/\对于所有 QL QQ K Y，混合XQL （A） ：：nil）->（ adj QL B QQ-> mell Y QQ K->existsZ，mellZQLK）.第一个析取符代表cut，而第二个是ucut。证明开始了感应对1.感应对2.感应于3.其编码所需的词典学度量。注意，一旦定理被证明，每个析取可以通过分别用轻和重实例化W来单独获得。►70K. 乔杜里等人/理论计算机科学电子笔记332（2017）573.5双边微积分我们还实现了MALL的双边微积分的元理论。单侧公式和双侧公式之间的最大区别在于，每个连接词都有左引入规则和右引入规则，并且切割规则适用于箭头两侧的公式，而不是根据对偶性。因此，我们直接在is_fm上进行推理，而不是根据一个不对称的对偶谓词，这反过来意味着我们做了一个额外的嵌套归纳，而不是诉诸反演引理。削减现在在两个前提推导中向上排列，直到它们成为主要的。虽然由于推理规则的数量增加，证明现在更长了，但其中的成分基本上保持不变。值得注意的是，在双边系统中证明的切割排列可以用来显示MALL的切割消除策略的强归一化，给出切割的排序4相关工作我们当然不是第一个在证明助手中形式化切消证明的人我们在这里讨论这个方向上的其他几个项目，并将它们与我们的方法进行比较。这份清单远非详尽无遗。与我们的方法最接近的（在序列和多重集被编码的意义上），我们可以引用[5]和[18]。在[5]中，作者提出了一种在Isabelle/HOL中形式化微积分的通用方法对于主割消定理，弱化必须是可容许的。他们已经证明了可证明性逻辑的可证明性演算GLSV的割消，尽管在实践中他们证明了多重割而不是割本身的可接受性（这些规则被证明对他们的系统是等价的）。多重割的使用是为了避免割公式收缩的复杂情况，这也是我们处理指数的方法在[18]中，Pattinson和Schrüder关于余代数逻辑的割消的一个问题在Coq中得到了形式化.形式化发现了原公式中的一些错误，我们与Pattinson和Scr？der进行了讨论并加以纠正。作者在Coq中实现了多集作为setoids，列表作为底层类型，置换作为等价关系。我们对多重集的处理在很大程度上是相似的。作者还选择为固定大小的列表定义一种类型，作为编码的一部分与[5]一样，证明是由规则集参数化的为了避免将上下文的显式表示处理为多重集，一个常见的方法是为微积分规则找到一个不同的表示，这些规则只显式地提到主公式和辅助公式。 这是一条[14]、[17]、[10]和[19]的道路。在[14]中，作者用证明项注释了微积分的序列，将割消归结为这些项的类型检查问题。 由于逻辑框架是直观的， 收缩和削弱的是被迫接受所有这样的证明演算。这种方法的一个明显优点是避免了多集的显式表示;另一方面，项重写系统对K. 乔杜里等人/理论计算机科学电子笔记332（2017）5771实际的微积分规则只是一个非正式的论点，没有被独立验证。文[14]中提出的方法在文[17]中被用于形式化直觉逻辑聚焦完备性的证明。作者避免了显示“繁琐的可逆引理”，使用一个新的证明的完整性，从削减消除和广义身份。在这种形式化中证明了一些元理论性质。 看看他的证明聚焦的完整性可以在Abella中使用我们的结果进行形式化。我们的方法和[17]的方法之间的一个共同点是使用削减权重来建立词典度量。在[10]中开发了另一个关于几个系统的聚焦完备性的形式证明（在Coq中），使用逻辑的代数解释，这需要对微积分进行一些假设，即和谐（即，规则应该以“对偶”的形式出现很难看出这些思想如何能推广到亚结构的情况。在各种证明助手中的其他线性逻辑编码可以在[11，12，16]中找到。然而，这些工作的目标是获得线性逻辑的证明搜索引擎，因此没有编码系统的元理论属性的证明在[11]中，作者在Isabelle中实现了线性逻辑，并使用具有交换规则的微积分来避免实现上下文模置换。在[16]中使用相同的解决方案来实现Coq中的线性逻辑，尽管Cowley9后来的实现使用了上下文的置换。在[12]中，线