可在www.sciencedirect.com在线获取理论计算机科学电子笔记338（2018）79-95www.elsevier.com/locate/entcs构造型理论中使用Barendregt变量约定的λ演算Church-Rosser定理的机器检验证明Ernesto Copello1，2 Nora Szasz3 A'lvaroTasistro3乌拉圭蒙得维的亚大学摘要在这篇文章中，我们继续在[3]中开始的工作，在构造类型理论中推导出λ演算的新归纳原理，使用（历史上的）一阶语法，绑定变量和自由变量都只有一种名称，并使用基于名称交换的α转换利用这些原则灵活的框架，用于在证明助手的严格形式设置中模仿笔和纸的证明。我们在这里报告的一个成功的应用，即一个完整的证明教会Rosser定理。整个开发已经使用Agda系统进行了机器检查[5]。关键词：Lambda演算，形式元理论，类型理论1介绍让我们考虑一下Lambda演算项的定义：M，N：：= x|MN|λx.MFig. 1. Lambda演算语法其中x的范围是可枚举的变量集V。这种语法被认为是一个过于具体的层次，在这个层次上不能正式地发展微积分的元理论。原因是，只有在选择绑定变量的名称时，术语之间没有显著的差异1现就职于美国爱荷华州爱荷华大学，电子邮件：ernesto-copello@uiowa.edu2部分由一个由尼日利亚N acionaldeI n vestigaci'on eInn ovaci'on，Argentugu ay.3电子邮件：szasz，tasistro@ort.edu.uyhttps://doi.org/10.1016/j.entcs.2018.10.0061571-0661/© 2018作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。80E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）79也就是说，这是α等价的;因此，在句法层面上识别这样的术语是很自然的。在古典环境中，这相当于工作关于项的α-等价类做到这一点的一种方法是，通过选择所讨论的阶级的适当代表来在Barendregt的书[ 1 ]中给出了这种做法的一个在以前的工作[3]中，我们用以下方法证明了构造型理论中的BVC的一种形式：我们引入了一个递归原理，允许在具体项上定义强α相容函数，即：在上面介绍的语法上使用函数，使α等价项相等。这一原则允许人们在抽象的情况下，通过只考虑绑定变量不属于给定名称列表的情况来指定函数的值。该原理实际上是通过计算每个给定项的一个满足这种限制的规范α等价表示来实现的然后，指定的函数实际上对计算的代表进行操作α-转换是使用名称交换的基本操作来实现的，就像在名义技术中一样（例如参见[7]和[8]）。利用这一原理，我们已经能够定义例如替换操作，对于抽象，只考虑避免变量捕获的方便情况。此外，我们还介绍了相应的归纳原理，如图2所示。这个原理要求性质被证明是α相容的，也就是说，被α转换保持换句话说，它必须是由α等价具体项的识别所产生的抽象项的一个如前所述，归纳原理允许我们证明抽象的情况，只考虑绑定名称不属于给定名称列表的情况：P α相容（αx）P（x）（M，N）（P（M）P（N）P（M N））（λxs，λM，λx/∈xs）（P（M））<$P（λx. （M））（M）P（M）图二.阿尔法感应原理在这个公式中，我们使用下面的约定来确定量化器的范围：x，y，z，. . .在变量（的名称）上的范围，M，N，. . . range在λ项上，xs在变量列表上上述原理实际上是从普通的结构归纳法中具体推导出来的.作为第一个应用，我们使用Agda证明助手[5]开发了一些关于替换的元理论结果，这些结果将在下一节中提到在这项工作中，我们提出了λ项上的强化α归纳原理，可以用来满意地处理其定义涉及名称交换的关系，并且允许我们避免在绑定位置上的名称的有限列表，而不是E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）7981只是抽象的，但在任何术语。 通过这种方式，我们可以将λ-演算的元理论扩展到Church-Rosser定理，在形式化中正式再现BVC的形式。所获得的一套原则提供了一个灵活的框架，能够愉快地模仿笔和纸的证明在严格的正式设置的证明助理。最接近当前的工作是[10]，其中Urban和Norrish展示了如何在对λ项上的关系进行归纳时模仿BVC。他们通过证明平行约化的替换引理和类型关系的弱化引理来说明归纳原理的使用他们提出了两个归纳原则的关系，一个平行约化关系，另一个类型的关系。当对这些关系进行归纳证明时，它们能够避免变量名的有限集合作为粘合剂。为了证明这些强化归纳原理，它们要求关系定义规则满足以下前提条件：所有函数和边条件应该是等变的（即，通过名称置换保留），侧条件必须暗示所有约束变量在结论中不自由出现因此，他们必须修改原始关系的定义以满足这些前提条件，以便能够证明他们的归纳原理的可靠性本文中提出的所有定义和证明都已在构造类型理论[4]中完全形式化，并使用Agda系统[5]进行了机器检查。相应的代码是公开的，可在以下位置获得https://github.com/ernius/formalmetatheory-nominal-Church-Rosser在随后的文本中，我们用英语给出了相当详细的证明，以便它们能够清楚地说明它们的形式化是如何进行的。以下各节的结构如下：在第2节中，我们回顾了λ-演算的基本概念，以及我们以前工作中的一些定义和结果，这些定义和结果对于更好地理解本节中的材料是必要的。在第三节中，我们引入了两个新的关于λ项的加强α归纳原理，这将有助于证明本文的主要结果。第四节提出了β-约化的概念，并利用Tait和Martin-L？的标准方法证明了Church-Rosser定理，从而对并行β-约化进行了形式化和研究总体结论见第5节。2预赛变量属于一个可枚举的名称集，术语的归纳定义如图1所示。新鲜度关系表明变量在一个项中不会自由出现：定义2.1[新鲜度]x=/yx#yx#Mx#Nx#MNx#Mx#λy.Mx#λx.M82E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）79⎧⎨x/∈bM表示可变x个数据不发生在项M中的约束位置：定义2.2[/∈b]x/∈b yx/∈bMx/∈bNx/∈bMNx/=yx/∈bMx/∈bλy.M接下来是交换名称的操作。名称交换的有限序列（组合）构成了一个有限的名称排列，这是用于术语的重命名机制。交换的行为首先定义在名字本身：定义2.3[交换]（x y）z=y如果z=xx如果z=y如果x z<$y/=z，然后通过交换出现在一个术语中的所有名称，包括抽象位置，将其直接扩展到术语置换操作被定义为顺序应用一个 swap列表 我们通常用π来表示排列，一个置换π到一个项M被写为π M。（x y）π表示由置换（x y）和置换π组成的置换。在下一个定义中，我们给出了基于交换操作的α转换（α -conversion，αα定义2.4[Alpha等价关系]（αv）xαx（αa）MαMJNαNJMNαMJNJ（αλ）（λz/∈xs） （x z）M<$α（y z）Nλx.M<$αλy.N在[3]中，我们证明了这是一个等价关系，由置换运算（即，等变的）。替换操作是使用前一节中提到的α相容递归原理定义的，作为其直接结果，自动导出以下引理：引理2.5（α-相容代换）M<$αM J<$M[x：= N]= M J [x：= N]。利用[3]的归纳原理成功地证明了下列结果。E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）7983∼J引理2.6（替换保持α-转换）N<$αNJ<$M [x：= N]<$αM[x：= NJ]。引理2.7（置换下的π（M [x：= N]）<$α（π M）[（π x）：=（π N）]。下一个引理表明，替换与抽象互换，直到α-转化。这是因为假设确保了足够新鲜的粘合剂。引理2.8（替换与抽象互换xyx #Nn（λx.M）[y：= N]<$αλx. （M [y：= N]）。作为前面引理的结果，我们得到：引理2.9（置换复合）xy <$x #P <$M [x：= N][y：= P]<$αM [y：= P][x：= N [y：= P]]。下面的结果在我们以前的工作中没有被证明，所以我们详细地展示了它。引理2.10（交换替代变量）x #M<$（（x y）M）[x：= N]<$αM [y：= N].证据 我们在图2中使用α归纳原理。首先，对于任意名称x，y和项N我们考虑下列项上的谓词：<$（M）<$x#M<$（（xy）M）[x：=N]<$αM[y：=N]。我们必须证明，M是α相容的，也就是说，如果M<$αP和M，则M（P）。假设m（M）和x#P。 然后，由于新鲜度通过α保持，我们有，x#M。 然后我们继续如下：（（x y）P）[x：=N]={<$α等方差和引理2.5}（（xy）M）[x：=N]<$α{<$（M）和x#M}M[y：=N]= {引理2.5}P[y：= N]。现在我们可以开始正式的归纳了。我们展示了有趣的情况，即抽象之一：我们有x#λz.MJ，其中我们选择z/∈ {x，y}<$fv（N）。我们需要证明（（xy）（λz.MJ））[x：=N]α（λz.MJ）[y：=N]。 当x#λz.MJ和z x我们得到x#MJ。 我们可以这样推理：（（x y）（λz.M J））[x：= N]={交换定义}（λ（（x y）z）. （（x y）MJ））[x：=N]={z/∈ {x，y}}（λz. （（x y）MJ））[x：=N]<$α{引理2.8}λz。（x y）M J）[x：= N]）<$α{i.h. }λz。（MJ[y：=N]）<$α{引理2.8}84E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）79（λz.M）[y：=N]QE. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）7985前面的证明说明了通常的笔和纸的非正式实践，它使用BVC来假设绑定器在某些定义的上下文中足够新鲜，允许我们以一种天真的方式应用替换而不需要重命名。下一个结果是前一个引理的直接结果：引理2.11x #λy.M<$（（x y）M）[x：= N]<$αM [y：= N].3阿尔法归纳原则在本节中，我们介绍两个新的α-归纳原理。第一个如图3所示。P α相容（αx）P（x）（M，N）（P（M）P（N）P（M N））（λxs，λM，λx/∈xs）（（λπ）P（πM）λP（λx. （M））（M）P（M）图三.置换的阿尔法归纳原理它是图2所示的一个强化版本，在图2中，抽象情况的归纳假设允许我们假设身体中名称的所有排列的属性。这一原理对于处理在定义中使用置换运算的关系是有用的。我们将在下一节引理4.7的证明中展示这种情况的一个图3所示的具有置换的α-归纳原理可以用图4中的原理来证明，图4是在[3]中从λ-项的简单结构归纳法导出的，其方式与从普通数学归纳法导出自然数的完全归纳法非常相似。（x）P（x）（M，N）（P（M）P（N）P（M N））（λM，x）（（λπ）P（π M）λP（λx.M））（λM）P（M）见图4。 强排列归纳原理证据 （阿尔法归纳原理与排列）。变量和应用案例是直接的。对于抽象的情况，给定任何项M和变量x，我们必须证明P（λx.M）知道：（ππ）P（π M）（1a）（<$xs，<$MJ，<$y/∈xs）（（<$πJ）P（πJMJ）<$P（λy.MJ））（1b）设xs是如（1b）中的名称列表。 让我们进一步选择y，而不是xs，新鲜λx.M。则对所有的MJ，πJ，P（πJMJ）<$P（λy.MJ）成立. 所以取MJ=86E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）79J（xy）M有（<$πJ）P（πJ（（xy）M））<$P（λ y. （xy）M）。 当πJ（（xy）M）=（（xy）π）M时，我们可以利用（1a）得到P（λy. （x y）M），最终P（λx.M），因为P是α相容的，λx.M<$αλy。（x y）M.这最后一个α等价成立，因为我们在λx.M中选择了新的y。Q下一个归纳原理（图5）使我们能够在整个归纳过程中假设约束变量不在给定的有限名称列表xs中，而不仅仅是抽象情况。P α相容（αx）P（x）（<$M，N）（（<$y∈xs， y/∈bMN）<$P（M）<$P（N）<$P（MN））（λM，x）（（λy∈xs，y/∈bλx. M）<$P（M）<$P（λx.（M））（M）P（M）图五.强化α诱导原理证据（强化α-归纳原理）。为了导出这个原理，我们引入一个重写函数，使得给定一个名称xs和一个项M的列表，rewrite（xs，M）返回一个与M可α转换的项，该项不包含任何xs元素作为绑定器。为了证明P（M）对任何项M，我们进行如下。给定一个名称列表xs，一个α相容谓词P，以及以下假设：（x）P（x）（<$M，N）（（<$y∈xs， y/∈bMN）<$P（M）<$P（N）<$P（MN））（<$M，x）（（<$y∈xs， y/∈bλx.M）<$P（M）<$P（λx.M））我们通过对项的结构归纳证明了以下谓词：（二）<$（M）<$（（<$x∈xs）<$x/∈bM）<$P（M）（3）然后，我们在术语rewrite（xs，M）上使用这个谓词rewrite（xs，M），它在xs中没有绑定变量以获得P（rewrite（xs，M））。最后，由于P是α相容的，重写（xs，M）<$αM，我们得到P（M）对任何M成立。反过来，通过M上的结构归纳法证明f（M）是简单的，因为f∈b 的定义是syntax定向的：• 变量情况：直接。• 应用案例：我们需要证明对于任何M，N，都有n（MN），使得n（M）和n（N）成立。也就是说，我们必须证明P（MN），假设xs中的任何变量x满足x/∈b（MN）。然后，通过对f ∈b的syn直接定义，直接得到x/∈bM和x/∈bN，从而可以利用M和N上的归纳假设得到P（M）和P（N）.因此，我们有（2）中第二个断言的所有前提成立，因此它的结论P（MN）成立。E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）7987• 抽象情形：我们必须证明P（λy.M），也就是说，我们需要证明P（λy.M）知道xs中的每一个可变x都满足x/∈bλ y.M。根据定义，88E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）79f ∈b，我们有x=f y和x/∈bM. 我们可以将最后一个结果应用于归纳假设M，得到P（M）。最后，我们使用（2）中的第三个断言得到期望的结果。Q4并行Beta归约β-归约关系（→β）被定义为β-压缩（λx.M）NdβM[x：=N]的相容闭包（与句法构造函数）。Tyait和Martin-Lüof关于β-约化的经典连续性定理是建立在所谓的并行约化的连续性定理之上的，这种并行约化可以在一个步骤中“并行地”应用多个β-压缩我们在图6中给出了定义。（2005年）xx（a）MMJNNJMNMJNJ（β）（xxs，xz/∈xs）（x z）M<$（y z）Nλx.M<$λy.Nλx.M<$λy.PJN<$PJJPJ[y：=PJJ]<$αP（λx.M）NP见图6。 平行归约关系前三个规则与定义2.4中定义α-转换关系的规则具有相同的形式，这提供了我们希望这种并行约化与α-转换相容的证据，也就是说，如果M<$N，M<$αMJ和N<$αNJ，则MJ<$NJ。 我们将在引理4.5和4.6中证明这个性质。最后，请注意，（αβ）规则有一个涉及α-转换的额外前提其原因是，我们的替换操作修改了约束名的项，这是用我们的α-递归原理定义的结果如果没有这个额外的前提，我们就不能证明α在它的右边是α相容我们先来证明一些基本性质：引理4.1（R的重显性）好吧证据 图4中排列归纳原理的直接应用。Q引理4.2（Equivariance ofEq）门π M证据 通过归纳法，对“无”的定义进行了归纳。变量和应用案例是直接的。在抽象的情况下，我们有证明λ（π x）。（π M）<$λ（π y）。（π N）从规则（λ）的前提和相应的归纳假设。我们还可以排除变量（λ）E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）7989z的前提中提到的从域的置换π和理由如下：（x z）M（y z）N（i. h.）}π（（x z）M）<$π（（y z）N）<${定义为perm。}（（π x）（π z））（π M）<$（（π y）（π z））（πN）<${asz/∈ dom（π）then（π z）=z}（（π x）z）（π M）<$（（π y）z）（π N）<${（<$λ）规则}λ（π x）。（π M）<$λ（π y）。（π N）。在（πβ）的情况下，我们必须证明（λ（π x））。（π M））（π N）<$π P从前提λx.M<$λy.PJ，N<$PJJ和P<$αPJ[y：=PJJ].通过直接应用对应于前两个前提的归纳假设，我们得到：λ（π x）。（π M）<$λ（π y）。（π PJ）和π N<$π PJJ然后，使用第三个前提，我们可以推理如下：P<$αPJ[y：=PJJ]<$$>{<$α等方差}π P<$απ（PJ[y：=PJJ]）<${引理2.7}π P<$α（π PJ）[（π y）：=（π PJJ）]<${<$α对称性}（π PJ）[（π y）：=（π PJJ）]<$απP（四）我们用（4）和最后一个结果作为前提，使用（β）规则Q作为前面引理的直接结果，我们得到以下结果：推论4.3（抽象下的保留M <$N <$λx.M <$λx.N.下面的引理说明我们的平行归约关系被α-等价保持。这两个结果都是通过对平行归约关系的简单归纳得到的。引理4.4（R1的右α相容性）MN N αPMP。引理4.5（左α相容性）MαN NP M P。现在我们可以直接证明α-转化包含在并行约化中。引理4.6你好证据给定M<$αN，由于引理4.1对M <$α N是反相的，我们也知道M<$M。然后使用引理4.4，我们得到了想要的结果。Q由于基本上使用β-收缩，因此在任何步骤都不应该引入自由变量，因此保持新鲜度90E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）79//∈引理4.7（保持新鲜）x #MMNN.证据我们对项M使用置换的α-归纳原理（图3）。为了应用这一原理，我们必须证明，对于任何变量x，（M）是α兼容的，这是从新鲜度和并行约简的α兼容性得出的。现在，对于主要结果，我们只给出了归纳法的有趣的抽象情形（即对于一项λy，MJ）.因此，我们有x#λy.MJ和 λy.MJ<$λz.NJ ， 我 们 必 须 证 明 x#λz.NJ 。 现 在 ， λy.MJ<$λz.NJ 必 须 是 应 用（<$λ）规则的结果，因此我们得到它的前提（<$w/∈x s ）（yw）MJ<$（zw）NJ。 α-归纳原理允许我们在抽象情况下排除一些变量，因此我们也可以假设y=x。利用这个不等式和假设x#λy.MJ，我们通过定义得到x#MJ。现在让u是一个变量，使得u#NJ， u/∈xs且u=/x;nx#（yu）MJ是由于xy，x u和x#MJ.我们可以应用（λ）规则的前提，其中u为u/∈xs，我们得到（y u）M J<$（z u）N J。 我们对MJ和置换（yu）使用归纳假设，结合前面的两个结果得到x #（zu）NJ. 我们也有λu。（z u）N J<$αλz.N J因为u#N J。然后，由于α保持新鲜度，我们得到了期望的结果。Q我们现在可以证明下面的反演引理，它表明Takahashi [9]对并行归约的原始定义（我们在下一个定义中注意到了它这些引理将有助于证明我们的关系的钻石性质。xTxMTMJNNJMJNJMTMJλx.M<$Tλx.MJMTMJNNJ（λx.M）N<$TMJ[x：=NJ]见图7。 Takahashi引理4.8（λ-反演）λx.M<$MJ<$（ <$MJJ）（M <$MJJ<$λ x.M <$λ x.MJJ<$MJ<$αλx.MJJ）。证据通过定义λx.M<$MJ必须是应用（λ x）规则的结果;然后我们有M J在抽象λy.N中，并且存在变量xs的列表使得（z xs）（x z）M<$（y z）N。设MJJ=（xy）N，证明了MJJ满足本文的三个性质• 设z是一个变量，使得z/∈xs且z#λY.通过定义#，x#λx.M，然后，由于并行约简保持新鲜度，x#λy.N也成立。于是：E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）7991（x z）M（y z）N{交换等方差}（xz）（x z）M（x z）（y z）N{交换自逆}M（xz）（y z）N{（*）}M（x y）N（*）这里我们应用引理4.4，前提是（x z）（y z）N<$α（x y）N。这种交换取消属性要求z和x足够新鲜，因为它是这种情况。• 我们应用引理4.4，其中λx.M <$λy.N和上面得到的α-等价性来证明λx.M<$λx。（x y）N.• 为了证明λy.N<$αλx. （xy）N，因为x在λy.N中是新的，我们将y与x交换，得到α等价项λx。（x y）N（引理4.2）.Q引理4.9（β-反演）如果（λx.M）NP通过应用（λβ）规则以如下方式获得：（β） λx.M<$λy.MJN<$NJMJ[y：=NJ]<$αP（λx.M）NP则（<$M JJ）（λx.M <$λx.M JJ<$M JJ [x：= N J]<$αP）.证据 我们证明了MJJ=（yx）MJ满足本文的结论。• x#λx.M和λx.M<$λy.MJ，所以通过引理4.7x#λy.MJ。 然后我们可以将y与最后一项中的x交换，得到α等价项λx。（y x）MJ，使用引理4.2。然后，通过引理4.4，我们得到λx.M<$λx。（y x）MJ.• 对于第二个条件，我们的推理如下：（（y x）MJ）[x：=NJ]={交换交换性}（（x y）MJ））[x：=NJ]<$α {推论2.11}MJ[y：=NJ]<$α{假设}PQ定理4.10（n次代换引理）M<$M J<$N<$N J<$M [x：= N]<$M J [x：= N J]。并行约化的替换引理是Church-Rosser定理的核心，也是我们在[3]中的α-归纳原理未能捕获BVC的地方。如果我们对项M进行归纳，问题出现在beta应用程序案例 ， 特 别 是 当 术 语 是 redex 时 。 然 后 我 们 有 M= （ λy.P ） Q ， 我 们 需 要 证 明（（λy.P）Q）[x：=N]<$R[x：=NJ]。但是，正如我们在归纳法的应用情况下一样，原始的α-归纳原理没有给出关于粘合剂y的新鲜度信息。BVC的使用将允许我们选择与x不同的y，并且在N中是新鲜的，并且在这些新鲜条件下，我们可以使用引理2.8将替换推到抽象内部，而无需任何变量捕获。接下来，我们使用图5所示的强化α诱导原理来证明这个结果。92E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）79JJ证据给定项N，NJ使得N<$NJ，以及变量x，我们考虑以下项上的谓词：<$（M）<$（<$MJ）（M<$MJ<$M[x：=N]<$MJ[x：=NJ]）。α-相容，这是代换和α-相容的直接结果（引理2.5，4.4，4.5）。 然后，我们可以使用我们的强化α-归纳原理，通过对项M的归纳来证明，排除变量x，以及项N和NJ中的自由变量。我们证明了有趣的应用和抽象的情况下。• 应用实例：我们可以提供（P，Q）（（n/z∈{x} n/fv（N）n/fv（NJ），z/∈bPQ）n/f（P）n/f（Q）n/f（P Q））。我们有两个子情况，根据哪一个规则被用来减少应用程序P Q。·（PQa）规则子情形：我们有P<$PJ和Q<$QJ，我们需要证明（P Q）[x：=N]<$（PJQJ）[x：=NJ]。这个证明是（Escherichia）规则对归纳假设的直接应用。（λβ）规则子情形：给定（λy.P）Q<$R，我们必须证明（（λy.P）Q）[x：=N]<$R[x ： =NJ] 。 我 们 利 用 反 演 引 理 4.9 得 到 存 在 PJJ 使 得 λy.P<$λy.PJJ<$PJJ[y ：=QJ]<$αR.接下来，由于我们已经假设粘合剂y与x不同，并且也是新的N和N，我们可以推理如下：λy.Pλy.PJJ{i.h. }（λy.P）[x：=N]<$（λy.PJJ）[x：=NJ]<${引理2.8}λy。（P [x：= N]）<$λy. （PJJ[x：=NJ]）通过归纳假设，我们知道Q[x：=N]<$QJ[x：=NJ]。 如果我们证明：PJJ [x：= N J][y：= QJ [x：= N J]]<$αR [x：= N J]（5）我们将能够应用（λβ）规则并得到（λy）。（P[x：=N]））（Q[x：=N]）[x：=NJ]。 然后，使用新鲜度前提，我们可以取出子-在这个并行约简的左侧进行置换运算，并使用引理4.5，α-相容性，我们最终得到了想要的结果。只剩下证明（5）来结束这个子情形的证明同样，这里经典的非正式证明使用BVC。在这种情况下，我们也可以模仿这种做法，因为我们的归纳原理给了我们一个与x不同的绑定器y，并且在NJ中是新鲜的。然后，我们有新鲜度前提来成功地应用替换合成引理2.9，并在以下步骤中得出这个证明PJ J[x：=NJ][y：=QJ[x：=NJ]]nα{引理2.9}PJJ[y：=QJ][x：=NJ]={引理2.5和PJJ[y：=QJ]<$αR}R[x：=N]• 抽象情形：我们必须给出（λP，y）（λz∈{x} λfv（N）λfv（NJ）， z/∈bλy.P）λfv（P）λy.P）。我们将逆引理4.9应用于假设λy.P<$Q，得到存在QJ使得：·E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）7993P<$QJ，λy.P<$λy.QJ和Q<$αλy.QJ。然后，我们可以通过以下方式得出证明94E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）79我的意思是，我的意思是，兴奋}P[x：=N]<$QJ[x：=NJ]<${均方差}（y z）（P[x：=N]）<$（y z）（QJ[x：=NJ]）<${（<$λ）规则}λy.P[x：=N]<$λy.QJ[x：=NJ]<${引理2.8}（λy.P）[x：=N]<$（λy.QJ）[x：=NJ]<${引理2.5和Q<$αλy.QJ}（λy.P）[x：=N]<$Q[x：=NJ]Q在[10]中，作者通过归纳法对关系进行了推导，因此x，N，NJ在β-压缩规则定义上被普遍量化，并且他们被迫将我们在这个证明中能够假设的相同新鲜度前提-相比之下，我们对项M进行归纳以证明谓词m，因此我们能够在m的定义之外将这些变量保持为固定的上下文。然后，通过使用我们的强化α-归纳原理，我们也能够在证明的应用情况下模仿BVC，特别是在先前暴露的（β）规则子情况下。最后，我们证明了平行约化的钻石性质。我们将遵循Takahashi [9]的较短方法，而不是直接通过项的归纳来证明它（这很容易做到）。为此，我们首先定义 然后我们证明，对于任何项M，N，如果M<$N，则N<$M<$（引理4.11）。最后，作为这个结果的一个推论，直接得出了xx=x（λx.M）=λx.M（ xM）λ =x Mλ（（M1M2）M3）λ=（M1M2）λM3λ（（λx. M1）M2）=M1[x：=M2]见图8。 高桥引理4.11（星性质）M N M.证据通过对M.我们展示了有趣的应用和抽象的情况下。• 抽象情况：我们必须证明N<$（λx.M）<$=λx.M<$，知道λx.MN成立。我们可以利用逆引理4.8得到项N j的存在性，使得：N <$αλx.N J和M <$NJ。 我们现在可以应用归纳假设，然后应用推论4.3到M <$N J，得到λx.NJ<$λx。（M）.E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）7995∼联系我们关于我们J最后一个结果直接给出了引理4.5所期望的结果，因为我们知道N<$αλx.NJ。• 应用案例：我们有三个子案例。前两个对应于星形运算定义的第三和第四行，并且直接来自归纳假设。最后，redex的情况可以根据在其并行约简的最后一步中使用的规则（Rla）或（Rlb）·（λ x. M）规则子情形：我们有λx.M<$N和MJ<$NJ，我们需要证明NNJ<$（（λx.M）MJ）<$=M<$[x：=MJ<$]。我们开始将反演引理4.8应用于假设λx。得到存在NJJ使得N<$αλx.NJJ和M<$NJJ. 我们可以现在将归纳假设应用于后者，然后由推论4.3得出λx.N JJ<$λx.M <$。此外，我们还可以将归纳假设应用于前提Mj。 我们可以使用（λβ）规则组合最后两个推导出的平行约简，并导出（λx.N JJ）N J<$M <$[x：= M J<$]成立 。 从 这 个 结 果 中，我 们 直 接 得 到 所 需 的 结 果 ， 只 需 注 意 到NNJ<$α（λx.NJJ）NJ，因为N<$αλx.NJJ和NJ<$αNJ。因此，通过平行关系的左α相容性（引理4.5），我们完成了这个子情形。·（<$β）规则子情形：我们有以下假设：λx.M <$λyN，MJ<$NJ和N[y：= NJ]αP，我们需要证明P <$M <$[x：= MJ<$]成立。我们继续类似于前面的子情形，得到存在NJJ使得λy.N<$αλx.NJJ，NJJ<$M <$且NJ<$MJ<$。 然后我们应用替换引理（引理4.10）得到NJJ [x：= NJ]<$M jj[x：= MJ<$]，如果我们证明P<$αNJJ [x：= NJ]，我们可以使用左α相容引理4.5来完成证明。最后，我们证明最后一个alpha等价成立：Pα{假设}N[y：=N]α，由引理2.11得出，x#λy.N（（x y）N）[x：=NJ]=通过引理2.5作为（x y）NαNJJNJJ[x：=NJ]在前面的推导中，我们使用了新鲜度条件x#λy.N，它遵循λy.N<$αλx.NJJ，x#λx.NJJ，以及在α转换下保持新鲜度的事实。Q作为前面引理的直接结果，我们有以下结果：引理4.12（钻石性质）M N M P Q，N Q P Q。定义4.13[结论]一个关系是连续的，如果它的自反传递闭包具有菱形性质.96E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）79∗我们省略了下一个结果的证明细节，因为它们不涉及λ-项他们证明了在一个直接的方式在古典文学。引理4.14如果关系R具有钻石性质，则它是连续的。引理4.15如果一个归约关系R是连续的，那么它的自反和传递闭包R也是连续的。作为前面两个引理的直接应用，我们得到：引理4.16（C的连续性）这是必然的。如果我们现在考虑β-约化→β，我们有：引理4.17（→βα）=证据我们证明了双重包含。要证明（→βα），证明（→βα）就足够了。由引理4.6我们知道和→β可以通过对→β约化关系的直接归纳来证明。最后，为了证明（→βα），我们首先通过对的直接归纳证明（→βα）。然后，通过在上的单调性，我们得到<$<$（（→β <$<$α）<$）<$，并且期望的结果由的恒等式推出。Q利用最后两个引理，我们最终得到了Church-Rosser定理。定理4.18（Church-Rosser）关系式（→βα）是连续的。5结论我们已经介绍了关于λ演算的归纳原理，这些原理允许我们对通过识别α等价的具体项而产生的抽象项进行推理。这些原则适用于α相容谓词，即由α转换保持的性质，并允许我们通过选择所讨论的抽象项的方便代表来进行相应的证明，即通过避免属于显式提供的有限列表的绑定位置中的名称我们最终是从普通的关于（具体）项的结构归纳法中导出这些原理的。因此，我们对这种形式的Barendregt变量公约（BVC）进行了充分的论证。整个工作都是在构造类型理论中进行的，并使用Agda系统进行了机器检查，没有修改项的普通定义等式或制定任何类型的商构造。为了使整个实现工作，已经证明必须根据名称交换的基本操作来定义α转换，如Pitts和Gabbay形式化的方法可能是有用的，这可以通过我们的在Agda中的Church-Rosser定理的完整形式证明。在本文中，我们已经给出了这样的证明的英文摘要描述，虽然显示，E. Copello et al. /Electronic Notes in Theoretical Computer Science 338（2018）7997我 们 认 为 对 于 完 全 正 式 版 本 的 重 建 至 关 重 要 的 细 节 ， 可 在https://github.com/ernius/formalmetatheory-nominal-Church-Rosser 上 公 开 获得。在我们的发展中，平行归约关系的定义必须以这样一种方式表述，即确保该关系是α相容的。正因为如此，它看起来比Barendregt [1]或Takahasi[9]提出的经典模型更具体。 然而，我们能够证明反演引理，使我们 恢复原来的平行约化定义，从他们，我们能够重现高桥在类似的工作中，Urban和Norrish[10]也必须修改并行约化关系，以便导出关于并行约化的ad-hoc归纳原理，从而成功地证明该关系的替换引理。然而，它们不必确保并行约简的α相容性，因为在它们的形式化中，α-可转换项在句法上是相等的，因为它们在由α-等价表示的项的水平上工作，如[6]中所解释的。我们相信我们的方法是更直接和一般的，因为我们得到了一个简单的条件下，归纳原则，而不是在他们更复杂的关系。如替换定理证明的beta子情形所示，我们能够直接从我们的α-归纳原理推导出绑定的新鲜度条件，就像在BVC中一样，而不是在并行约简的定义中明确地强加它们作为我们的方法的另一个应用，我们已经能够以一种非常直接的方式形式化简单类型分配系统的主体归约定理的证明，这也可以在上述网站上公开获得。最后，我们已经概括了这里的技术暴露在一个框架的定期树与绑定器，从而获得愉快的治疗，例如元理论的系统F旁边的纯Lambda演算的方式的实例化。关于这项工作的报告可以在第一作者的博士论文中找到引用[1] 亨德里克·巴伦德雷
