构造型理论中简单型Lambda演算的强规范化证明

可在www.sciencedirect.com在线获取理论计算机科学电子笔记351（2020）187-203www.elsevier.com/locate/entcs构造型理论中简单型Lambda演算的强规范化塞巴斯蒂安·乌尔乔利1A'lvaroTasistroNoraSzasz2乌拉圭蒙得维的亚大学摘要我们考虑了纯Lambda演算在构造类型论中的一个预先存在的形式化，它以一阶语法表示，只有一种名称和基于多重替换的alpha转换，以及简单类型到项的赋值系统。 最重要的是，Joachimski和Matthes给出的强规范化的巧妙证明，其主要引理通过对类型的完全归纳和对强规范化项的表征的从属归纳来进行，这反过来又证明了它们作为可访问部分的直接定义是正确的。一步β还原关系。 强规范化本身的证明，从而允许组成只是类型系统的直接归纳。整个开发过程使用Agda系统进行了机器检查。我们评估的优点和缺点的方法。关键词：形式元理论，Lambda演算，构造类型理论1介绍在[3]中，我们使用一阶语法给出了构造类型论中的Lambda演算的形式化，其中绑定变量和自由变量都只有一种名称，没有识别直到alpha转换的项，并使用多个（同时）替换作为基本操作。当时我们的目标是调查这种非常具体的方法是否适用于任何一种方式都可以完全正规化。这种方法在历史上植根于Curry和Feys [7]对微积分的详细元理论研究，其中（一元）替换被定义为对项的总元操作，在此基础上定义了微积分的所有相关关系，从alpha转换开始。替换的定义是通过在1Partiallysupported byyAgriciaNacionaldeI nvestigac i′one Inn ovaci′on（AN II），Agricultu ay.2电子邮件：{urciuoli，tasistro，szasz}@ ort.edu.uyhttps://doi.org/10.1016/j.entcs.2020.08.0101571-0661/© 2020作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。188S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187术语的大小，但其充分的公正性需要同时证明其使用因为重命名操作（即，当被替换的项是变量时）不改变其中被替换的项的大小。这使得它的形式化在例如构造类型理论和使用任何证明助手，现在可用，非常困难，甚至是不可能的。然而，如[11]中所建议的同时多重替换的使用带来了实现微积分元理论发展的可能性，该元理论同时是完全形式化的-接近于机器可检查的版本-并且是人类可读的。事实上，正如在[11，3]中所解释的那样，这种替换的使用使得有可能避免项大小的递归，因为当跨越抽象时，绑定名称被更改为适当的名称，并且相应的重命名被记录到扩大的多个替换中，该替换继续对抽象的主体进行操作因此，替换的效果可以通过结构递归给出一个简单的定义，这使得微积分的元理论也可以使用简单的归纳形式来追求似乎是合理的。绑定名总是被改变的事实也允许避免案例分析我们在[3，6]中的工作在某种程度上验证了前面的假设：我们能够对纯Lambda演算的元理论进行完全形式化，直到标准化定理，以及简单类型的Lambda演算（更准确地说，简单类型到项的分配系统），直到主题归约定理。我们从这些实验中得出的主要结论是，尽管必须明确考虑α转换，但工作量是可控的，正式的机器检查证明不是非常冗长，并且它们以详细的数学英语进行的演示可读且相当完整。我们还生成了一个基本的Agda库[2]，该库在[ 6 ]中被一位硕士生成功地使用和扩展在本文件中，我们希望继续前面的工作，目的是：- 针对日益复杂的挑战检验上述假设，- 取得进展的全面语料库完全正式元理论的λ演算。因此，我们解决的问题，正式证明强规范化的系统分配的简单类型的条款。我们选择形式化的证明方法是由于[8]，其中作者通过类型系统的简单归纳提出了弱规范化和强规范化的光滑证明。这些证明使用了一个主要引理，它允许处理归纳法中应用的困难情况，通过一个单独的关于类型的完整归纳法，以及一个从属归纳法，在强正规化的情况下，它继续描述最初在[13]中给出的强正规化项。在[8]中，为了形式化的方便起见，我们将避免使用向量符号来表示术语。此外，S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187189选择绑定名称的选项被使用，而无需进一步的麻烦。然后，例如，变量捕获没有考虑在内-当然，我们必须考虑在内。我们希望测试：- 我们的形式化仍然可以保持在合理的复杂度范围内，- 我们现有的Agda库可以继续支持这一额外的开发，- 电子证书是在一个新来者的能力范围之内的，他在完全形式化、使用证明助手，特别是Agda方面的经验有限。 实际上，这项工作构成了第一作者硕士论文的整个发展已经在结构类型理论中正式化，并在Agda系统中进行了机器检查[10]。相应的代码可在www.example.com上https://github.com/surciuoli/lambda-metatheory。我们现在继续发展本身。它的结构如下：在下一节中，我们提出了基本定义，并在此形式化–some from 在第3节中，我们给出了强正规化项的两个定义。第一个是更自然的一个，定义为一步beta归约的可访问部分，另一个是最初在[13]中给出的语法特征（以向量表示法）。后者的表述与谓词的强规范化中性词和强中心词归约是相互的。我们在第4节中形式化了第二个定义相对于原定义的可靠性证明。在第5节中，我们利用句法特征来证明简单类型的赋值系统中可类型化项的强规范化定理，最终由类型系统的直接归纳组成。最后，在第6节中，我们提出了总体结论。2预赛2.1语法我们从名称的可数类型V开始，也称为变量;也就是说，为了具体起见，我们可以将V=defN或V=defString。字母x、y、z与素数或子索引应代表变量。术语通常是归纳定义的-下面我们展示了抽象语法的语法定义2.1Λ中的术语由以下语法定义：M，N：：= x|MN|λxM。M，N，P，Q. . .范围在lambda项上。在具体的语法中，我们假设通常的约定，根据该约定，应用程序比抽象绑定得更紧定义2.2一个变量x在M中是自由的记为xM，它的反义词记为x#M，读作xfresh inM，就像在标称技术中一样。这两种关系都以标准的方式归纳190S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）1872.2取代我们使用多个（同时）替换，即将一个项与每个变量相关联的映射。实际上，我们必须处理的替换几乎在任何地方都是同一的，因此我们可以从空的替换i开始生成它们，它将每个变量映射为一个项，并应用更新操作，定义如下：定义2.3（替换更新）（σ，x：=M）是由下式定义的替换：（σ，x：=M）x=M（σ，y：= M）x = σx，如果x∈ x = y.每当需要时，我们将写[x：=N]作为（i，x：=N）的语法糖此外，我们经常考虑替换σ对自由变量的限制 一个给定的项M，记为（σ，M）。然后，我们也可以将fresh和free变量扩展到限制：定义2.4变量x在（σ，M）中是新的，并且对于所有y<$M，则x#σy。相反，x在（σ，M）中是自由的，记为：x<$（σ，M）i <$存在某个y<$M使得x <$σy.定义2.5（条款替换的效果）替换的效果项M上的σ由 M上的递归定义：x·σ=σx（MN）·σ=（M·σ）（N·σ）（λxM）·σ=λz（M·（σ，x：=z））其中z=χ（σ，λxM）（1）在等式（1）中，注意约束变量x总是被新变量替换。新的变量z是通过选择函数χ获得的，该函数计算（σ，λxM）中的第一个变量fresh，因此它不会捕获任何因替换而引入其作用域的名称（更多细节参见[3]除了实现捕获避免之外，使用多个替换和绑定变量的统一重命名允许我们采用简单的结构归纳，在进行替换推理时避免案例分析。我们将Mσ用作M·σ的语法糖，在具体的语法中，替换比应用更紧密。关于置换的以下性质在[3]中被证明：引理2.61. χ（σ，M）#（σ，M）2. X（i，M）#M3. M（σ，x：=Nσ）=M[x：=N]σ定义2.7（约束等式）（σ，M）=（σJ，MJ）i <$M和MJ共享相同的f ree变量和（x<$M）σx=σJx。那么，对于（σ，M）=（σJ，M），σ=σJ↓M将是糖S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）1871912.3Alpha转换定义2.8（阿尔法转换）你好：xαx下载app：MαMJNαNJMNMJNJλ：M[x：=z]<$αN[y：=z]λxM<$αλyN（*）（*）其中z#λxM，λyN。Alpha转换通过以下定义扩展到限制：定义2.9σ<$ασJ↓M=（<$x<$M）σx<$ασJx然后，下面的引理引理2.101. ι∼αι ↓M2. σ<$ασJ↓M<$N<$αP<$（σ，x：=N）<$α（σJ，x：=P）↓M接下来，我们展示一些在[3]中证明的和在我们的开发中需要的关于α的结果引理2.111.α是一个等价关系。2. y#（σ，λxM）<$M（σ，x：=y）[y：=N]<$αM（σ，x：=N）3. y#λxM<$λxM<$αλy（M[x：=y]）4. M<$αN<$λxM<$αλxN5. y#（σ，λxM）<$（λxM）σ<$αλy（M（σ，x：=y））6. x#M<$M<$αN<$x#N7. M<$αMJ<$σ <$ασJ↓M< $Mσ <$αMJσJ8. M<$αN<$Mσ=Nσ9. MαMι由此，一些有用的推论是直接的：推论2.121. z#（σ，λyM）<$M（σ，y：=z）[z：=Nσ]<$αM[y：=N]σ2. （λxM）N <$α（λyMJ）NJ<$M[x：=N]<$αMJ[y：=NJ]3. λxM<$αλyN<$M[x：=y]<$αN2.4β还原(One步骤）β-归约记为→β，它由以下规则定义定义2.13（β降低）β：（λxM）N→βM[x：=N]appL：∼192S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187M→βMJMN→βMJNappR：N→βNJMN→βMNJS. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187193λ： M→βMJλxM→βλxMJ多步归约写为→并定义如下：定义2.14（多步还原）M→NM→βNM→NM→N N→P我们将→扩展到替换，如下所示：定义2.15（n个代换的约化）σ→σJ=（nx）σx→σJx。在我们的发展中需要[3]中涉及→β的以下结果：引理2.161. x#M<$M→βN<$x#N2. x#（σ，M）<$M→βN<$x#（σ，N）3. σ→σJ <$Mσ→MσJ4. M→MJMN →MJN从现在起，除明确说明外，所有提交的结果均构成新的发展。引理2.17（替换与→β的相容性，直到→α）M→βN<$（βP）Mσ→βP<$αNσ证据通过归纳M→βN的导子。- 案例β：（λxM）N→βM[x：=N]。设P=M（σ，x = z）（1，z：= Nσ），z=χ（σ，λxM）。然后，我们需要证明：(i)（（λxM）N）σ→βP（ii）P<$αM[x：=N]σ.（一）以替代品的定义（定义）。2.5）我们有（（λxM）N）σ=（λz（M（σ，x：=z））Nσ，根据β规则，（λz（M（σ，x：= z））Nσ →βM（σ，x：=z）（i，z：=Nσ）。(ii)根据推论2.12.1。- 情形appL：MN→βMJN由M→βMJ得出。通过ind. hyp.我们知道存在一些Qs. t。Mσ→βQ<$αMJσ。利用appL规则，得到（MN）σ→βQNσ，而利用appL规则，得到QNσ<$α（MjN）σ.- 情况appR：MN→βMNJ由N→βNJ得出。 类似于苹果案。- 情况λ：λxM→βλxN由M→βN得出。我们必须证明：（i）（λxM）σ→βP和（ii）P<$α（λxN）σ，对某些P.第一个，hypo。我们知道存在一些PJs. t。M（σ，x：=z）→βPj<$αN（σ，x：=z）. 设P=λZPJ。 一方面，（i）紧接着λ规则和定义2.5。（ii）另一方面，根据引理2.11.4，我们有λzPJ<$αλzN（σ，x：= z）。此外，通过引理2.6.1我们得到z#（σ，λxM），因此通过引理2.16.2我们得到z#（σ，λxN）。最后，根据引理2.11.5，我们得到所需的λzPJ<$α（λxN）σQ引理2.18（α和→β的交换性）194S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187M<$αN→βP<$（<$Q）M→βQ<$αP证据 通过对M. 我们只展示有趣案例的证明。- 情况λxM<$αλyN→βλyP。 一方面，λyN→βλyP必须从N→βP（定义2.13）得出，并且根据引理2.17，有一项Qs. t。N[y：=x] →βQ<$αP[y：=x].此外，由推论2.12.3我们得到M<$αN[y：=x]。然后，通过ind.hyp。利用M<$αN[y：=x]→βQ ， 我 们 得 到 M→βQJ<$αQ ， 对 于 某 个 QJ ， 通 过 定 义 2.13 ， 我 们 得 到λxM→βλxQJ。另一方面，通过假设，使用引理2.11.6和2.16.1我们得到x#λyP，并且通过引理2.11.3，λyP<$αλxP[y：=x]。最后，λxQJ<$αλyP由引理2.11.4和<$α的传递性成立。- 情况（λxM）MJ<$α（λyN）NJ→βN[y：=NJ]。令Q=M[x：=MJ]。 由定义2.13我们得到（λxM）MJ→βQ，利用引理2.12.2我们有Q<$αN[y：=NJ]。Q引理2.19（α和→的交换性）M<$αN→P<$（<$Q）M→Q<$αP证据 利用引理2.18，很容易得出N→P的情形。Q2.5一元替换事实证明，在还原β-redex的过程中引入取代是方便的。它们将由一对变量与一个术语相关联，并伴随着几个变量重命名组成。定义2.20代换σ是变量x和项M一元σx M- i <$σx = M，对所有y <$= x，σy是一个变量。引理2.21（一元代换引理）1. 一元[x：=M]xM2. 一元σx M<$一元（σ，x：=N）xN3. y x<$Unaryσx M<$Unary（σ，y：=z）xM4. 一元σxy<$一元（σ，z：=M）zM证据 从定义上看很简单Q3强规范化项我们的目标是证明在简单类型的赋值系统中所有可类型化的项都是强规范化的。为此，我们将采取以下行动：在本节中，我们给出了强正规化项的两个定义。第一个（谓词sn）自然被引入作为一步beta归约的可访问部分。第二个（谓词SN）是[13]中引入的另一种句法表征，最初以向量表示法给出，并在[1]中在有点不同的上下文中进行了改编（即，使用类型化缩减）。S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187195我们现在将给出这两个定义以及它们的一些性质，以便在下一节中最终证明第二个定义相对于原来的定义的可靠性，即对于所有项M，SNM蕴涵snM。稍后，在第5节中，我们将通过证明简单类型赋值系统中所有可类型化的项都满足第二个定义（SN）来完成强规范化证明。3.1强规范化术语一项是强正规化的，当且仅当它在→β的可及部分：定义3.1（强规范化项的可访问性定义（M→βN→SnN）snM引理3.2（sn在α下的闭包）snM<$M<$αN<$sn N。证据通过对snM. 取N使得M<$αN和P使得N→βP。根据引理2.18，我们有Qs.t。 M→βQ<$αP。 因此，SNQ和通过IND。hyper.，因为Q<$αP，所以如所期望的那样，SnPQ引理3.3（sn的性质）1. SNx2. sn MN→N3. n（MN）nMnN4. snMsn（λxM）证据 （3.3.1）由于没有可能的方法使x→βM，X.（3.3.2）通过M→N的诱导。（3.3.3）通过对sn（MN）的诱导。（3.3.4）通过对snM.Q3.2强规范化项：一个句法定义现在我们引入强正规化项的第二个定义。为了做到这一点，我们必须定义三个相互归纳的谓词：强正规化项（SN），带中心词x的强正规化中性项（SNex）和强中心词归约关系（→SN）。定义3.4（SN、SNe和→SN）五：SNexx应用程序：SNexMSNNSNexMNne：SNexMSNMλ：SNMSNλxM实验：M→SNNSNNSNMβ：SNN（λxM）N→SNM[x：=N]appL：M→SNMJMN→SNMJNα：M→SNR R <$αNM→SNN196S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187→4SN的可靠性在本节中，我们将证明SN相对于SN是可靠的，即，每个项第一个谓词也在第二个谓词中。为了实现这一点，我们首先需要引入两个概念，即中性项的概念和不进入抽象的强规范化头部约简的4.1中性用语让我们称之为中立的迭代应用程序有一个变量作为头：定义4.1（中性术语）nexxxnexMnexMN我们将省略标题，只要方便就写neM。中性术语具有以下特性：引理4.2（ne在→β下的闭包）neM<$M→βN<$neN证据通过对neM.Q引理4.3（在app.下sn/ne的闭包）neMsnMsnNsnMN. 证据 通过对sn M，sn N的词典归纳，得出了一个新的结论. 假设MN→βP，并通过案例来证明snP：- 在 情况 P = MJN，其中MβMJ，利用引理4.2，我们得到neMJ。通过定义snM，我们得到snMJ，然后通过ind.hyp.，nP.- 在P=MNJ且N→βNJ的情况下，类似地使用snNJ进行。Q4.2强标准化压头减小定义4.4（强规范化水头归约）→sn是归约关系，定义为：β：snN（λxM）N→snM[x：=N]appL：M→SnMJMN→SnMJNα：M→snR R<$αNM→SnN引理4.5（推论）设M→snN且M→βP。则要么N<$αP，要么存在Qs. t。P→snQ和N→ Q。换句话说，设ΔL是M的最左外的Redex，而不是抽象内部的Redex：则N通过收缩ΔL从M获得。设Δ为M→βP中收缩的redex。如果Δ = ΔL，则N=P。 否则，设Q由P收缩ΔL得到，即P→snQ。如果在M→snN中舍弃Δ，则N=Q。 如果不是，那么N→βQ必然是通过收缩Δ-和可能的其他赎回而导出的证据通过对M→snN的归纳和M→βP的隶属分析，得出了M → snN的隶属分析。- 情形β：假设snN。-如果（λxM）N→βP由规则β得到，则我们立即得到P=M[x：=N]S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187197J→→- 如果（λxM）NβP由规则appL求出，则P为（λXMJ）N，MβM. J.令Q =MJ [x：= N]。 根据引理2.17和定义2.14，可以得出M[x：=N]→Q，然后使用定义4.4的规则β，我们得到P→snQ。- 如果（λxM）N→βP由规则appR得到，则P是（λxM）NJ，N→βNJ.设Q=M[x：=N]。现在我想，一方面，根据引理2.17，我们有M[x：=N]→Q。另一方面，由于snNJ由snN和引理3.3.2得出，我们可以再次使用定义4.4的规则β得到P→snQ。- 情形appL：假设M→snMJ。- MN→βP不能用规则β得到，因为在这种情况下M将是一个抽象。但是我们有M→snMJ，而→sn并不进行抽象。- 如果MN→βP遵循规则appL，则P是MJJN，我们有M→βMJJ。 的ind. hyp.给出了两种可能性：要么Mj<$αMJJ，要么存在某个QJ使得MJ→QJ且MJJ→snQJ.在第一种情况下，它紧跟着MJN<$αMJN。 否则，设Q=QJN，则根据定义4.4和2.14，我们得到MJN→Q和MJJN→snQ。- 如果MN→βP由规则appR得到，则P是MNJ，我们有N→βNJ。然后选择Q=MJNJ并使用→和→sn的定义。- 情形α：假设M→snR且R<$αN。 进一步假设M→βP。 的ind. hyp.给出R<$αP或存在Qs. t。R→Q和P→snQ。在第一种情况下，由R<$αN和R<$αP，我们得到N<$αP。在另一种情况下，由于R<$αN，从R→Q它也由引理2.19遵循N→Q。Q4.3关于Soundness为了证明SN蕴涵sn，我们还需要相应地证明SNe和→SN关于sn和→sn的可靠性。困难在于对应于SN定义中的exp规则的情况，其中SNM由M→SNN和SNN。 通过ind.hyp.我们有M→snN和snN，然后我们需要一种证明→Sn关系在Sn下向后闭合的方法。这就是下面引理4.8的目标。事实上，这个引理说明的是→sn也是合理的：如果我们有从M到N的→sn约化，并且N是强正规化的，那么M也一定是。这反映了→ sn关系背后的思想：它表征了所有的计算策略或可能的约简。回到引理4.8，它的证明是通过推导M→snN加上三个辅助结果接下来，我们需要证明snN和snM[x：=N]蕴涵sn（λxM）N。然而，在这方面，-引理4.6（弱头展开）设snN，snQ和Q<$αM [x：= N]。则sn（λxM）N.证据通过对snN和snQ的词典式归纳。假设对于某个P，（λxM）N→βP，然后通过证明snP的情况继续进行：198S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187→→⇒- 情况P=M[x：=N]。根据引理3.2和假设。- 情形P=（λxMJ）N，其中λxM→βλxMJ，这又必须从M→βMJ得出。根据引理2.17，对于某个R，我们有M[x：=N] →βR<$αMJ[x：=N]。然后，利用引理2.18，我们得到S，使得Q→βS<$αR。因此，由于S<$αMJ[x：=N]通过<$α的传递性，我们通过ind.hyp.sn（λXMJ）N.- 情况P =（λxM）NJ，由N得到βNJ.根据引理2.16.3，M[x：=N]→M[x：=NJ]。同样，通过引理3.2我们得到sn（M[x：=N]）。我们应用引理3.3.2来获得sn（M[x：=NJ]），然后通过ind.兴奋我们得到了sn（（λxM）NJ）.Q接下来，我们引入下面的引理，它将在后面的引理4.8中有用：引理4.7设M→snMJ以及M，N和MJN是sn。 然后是SN MN。证据通过对snM，snN的词典归纳，得出了一个新的结论.假设某MN→βP，并通过示出snP的情况进行：- 情形P = MJJN，其中M→βMJJ。根据引理4.5，要么MJ<$αMJJ，要么存在某个Q使得MJ→Q且MJJsnQ。 第一种情况由假设sn（MJN）和引理3.2得出。在第二种情况下，首先注意，通过引理3.3.2和定义2.14，我们得到了sn（QN）。然后，通过定义snM，我们有snMJJ，可以应用ind。兴奋总结一下，P。- 情形P=MNJ，其中N→βNJ。然后使用IND。兴奋和sn（MJNJ）。Q引理4.8（sn的向后闭包）设M→snN且snM。然后是snM。证据通过对M→snN的归纳。- 情形β：使用引理4.6。- 情况appL：假设M→snMJ和sn（MJN）。根据引理3.3.3，我们有snMJ和SnN.通过ind.兴奋我们有snM，使用引理4.7，我们得到sn（MN）。-情况α：使用引理3.2和ind。兴奋Q现在我们只需要两个预备结果：引理4.9（SNe相对于ne的可靠性）SNe xMnexM。证据通过对SNe×M的一个简单归纳，Q引理4.10M→SNNM→N证据 通过对M →SNN的归纳。- 情形α：M→SNN由M→SNP<$αN得到。 通过ind. hyp.我们有 M→N。此外，根据定义2.14，我们得到P→N。然后，通过α的传递性，我们有M→N。- 案例β。 根据定义2.14.- 情况appL：MN→SNMJN由M→SNMJ得到。 通过ind. hyp. 我们有M→N因此，根据引理2.16.4，我们有MN→MJN。Q最后，我们证明了强正规化项的另一种定义相对于可及性定义是合理的：S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187199定理4.11（SN的可靠性）1. SNM2. SNexM3. M→SN NM →SNN证据根据定义3.4，通过同时感应。- 情形v：通过引理3.3.1.- 情况app：必然地M=PQ并且SNex（P Q）从SNexP和SNQ获得。然后，在。兴奋我们有snP和snQ，根据引理4.9，我们得到neP。最后，通过引理4.3，我们得到了snP Q。- 病例ne：通过ind. hyp.- 病例λ：通过ind. hyp.然后是引理3.3.4。- 病例暴露：按个体分类。引理4.8- 病例β：通过ind. hyp.定义4.4- 病例应用：通过ind. hyp. 定义4.4Q5强正规化定理在这一节中，我们给出了简单类型Lambda演算中可类型化项的强规范化定理的证明5.1打字判断定义5.1类型由下面的语法定义，从基础类型类别τα，β：：= τ|α→ β。我们引入类型之间的排序，以便稍后对它们执行完整定义5.2当类型α是类型β的（结构）分支时，我们写α ≤ β;当它是真分支时，我们写α <$β。定义5.3将简单类型赋值给lambda项的系统如下：v：x∈Γx：Γxa：Γ<$M：α→βΓ<$N：αΓMn：βλ：Γ，x：α<$M：βΓλxM：α→β其中，Γ表示形式为x1：α1，x2：α2，.的变量声明的上下文（实现为有限列表），xn：αn。 在rulev中，x∈Γ意味着x被声明为在Γ中，并且Γx是在Γ中为x声明的（最后）类型以下是在[3]中得到证明的：引理5.4（弱化）设x #M和Γ <$M：α. 则Γ，x：β<$M：α。引理5.5（主语归约）Γ <$M：α<$M→N <$Γ <$N：α。►►►200S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）1875.2类型替换接下来，我们引入类型化替换（w.r.t.项M的自由变量）：定义5.6（σ，M）把在Δ -下的适当类型的项赋予在Γ中的变量，所有这些项都记为σ：Γ→ Δ ↓M- i，对于所有x<$Ms. t。x∈ Γ，则有Δ <$σx：Γ x。这些都是有用的，如果一个项M是可类型化的，那么Mσ也是可类型化的，如下面的引理-在[3]中证明-声明：引理5.7设Γ → Δ ↓M：α和σ：Γ → Δ ↓M。 则Δ <$Mσ：α。然后，下面的三个引理引理5.8设x #（σ，λyM）且σ：Γ → Δ ↓ λyM.则（σ，y：= x）：（Γ，y：α）→（Δ，x：α）↓ M。引理5.9设x #M且σ：Γ → Δ ↓ M。则（σ，x：= y）：（Γ，y：α）→（Δ，x：α）↓ M。引理5.10设Γ<$M：α. 则[x：= M]：（r，x：α）→ r ↓ M。我们以一些有用的一般结果结束这一小节。引理5.11设nexM和Γx：β。然后又道：1. ΓM：αα≤β2. ΓM：α→γ<$α<$β证据立 竿 见 影 的Q引理5.12u#M<$Mσ=M（σ，u：=N）证据 根据限制的平等性定义（Def.2.7）。Q5.3强正规化可以通过对给定类型系统的简单归纳来证明可类型项是强规范化的。为此，我们需要处理应用的情况，这将在定理（引理5.14）之后证明定理5.13（强正规化）Γ <$M：α<$SNM.证据 通过对ΓM的归纳：α。- 案例3.4：根据定义3.4.- 情形α：Γ<$MN：α由Γ<$M：β→α和Γ<$N：β得到。 Byind. hyp.我们得到SNM和SNN然后，由引理5.142（ii）我们有SNMN。- 案例分析：通过ind.好的。定义3.4现在我们可以把注意力转向主要引理。如前所述，它的目的是建立SNMN从SNM和SNN得出可类型的M和N，但是，为了达到这个目的，必须同时证明一些附加的结果。S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187201引理5.14设Γ <$M：α，SNN，σ：Γ → Δ ↓M，一元σx N和Γ <$x：β. 然后又道：1. （i）SNM σ，（ii）y x<$SNeσyMσ和（iii）α = β→γ <$SN MN.2. （i）SNMσ和（ii）α = β→γ <$SN MN。3. M → SNP <$Mσ → SNPσ。证据证明通过对类型β的结构的完全归纳和对M所索引的定义3.4的从属归纳来进行。所以，首先，取β，并假设它的所有真分量都是这样的。我们继续进行从属归纳：- 情形v：则M=y，我们必须证明1：（i）SNyσ，（ii）yσ =x<$SNeσyσ，(iii)α=β→γ→SNyN。对于（i），y=x或不。如果为真，则根据定义式2.20，我们有σy=N。 如果不是，-同样定义-σy=z是一个变量。要么case：SNσy. （二）如果是 x，那么根据定义3.4，我们有SNezz。作为（三）根据规则的规定3.4关于SNyy和SNN，然后是规则ne。- 情况app：则M=PQ并且SNeyPQ从SNeyP和SNQ得出，并且从ΓP：δ→α和ΓQ ： δ 得 出 ΓPQ ： α 。 我 们 需 要 证 明 1 ： （ i ） SN （ P Q ） σ ， （ ii ） y∈=x<$SNeσy（P Q）σ和（iii）α=β→γ<$ SN（P Q）N.第一，通过。兴奋我们有SNPσ和SNQσ。再说了，莱姆。5.7我们得到Δ<$Pσ：δ→α和Δ<$Qσ：δ。现在，我们要么y=x，要么不是。第一种情况是，Lem。4.9我们有nexP，因此由莱姆。5.11.2它遵循δ<$β。然后，对于（i），我们可以应用主索引。兴奋2（ii）M=Pσ，N=Qσ，β=δ，得到SNPσQσ如所期望的，其等于SN（P Q）σ相反，如果y x，则通过ind。兴奋(ii)我们得到SNeσyPσ。 此外，根据SN的定义，它遵循SNeσyPσQσ，因此SN（P Q）σ。(ii)刚刚被证实。(iii)与案例V类似。- 情况ne：则SNM从SNeyM得出，并且2直接由主ind.hyp。1 ㈠和㈢。- 情形λ：则M=λyP，SNλyP从SNP得出，并且Γ<$λyP：δ→<$从Γ，y：δ<$P：<$。我们需要证明2：（i）SN（λyP）σ和（ii）SN（λyP）N。 对于（i），我们有（λyP）σ=λzP（σ，y：=z），其中z=χ（σ，λxP）。我们现在按情况进行：y=x或不。在第一种情况下，在我们可以应用ind.hyp之前。对于SNP和（σ，x：=z），我们需要证明Γ，x：δ<$x：β。然而，这并不必然遵循，因为δ是相当任意的。然而，我们可以如下进行：让我们固定一些u=χ（i，P）。首先，通过引理2.6.1我们有u#（i，P），因此通过引理2.6.2得到u#P。现在，通过引理2.6.1我们有z#λxP，然后通过引理5.8得到（σ，x：=z）：Γ，x：δ→Γ，z：δ↓P，因此通过引理5.9有（（σ，x：=z），u：=v）：Γ，x：δ，u：β→Δ，z：δ，v：β↓P对于任何v。此外，通过引理5.4，我们有Γ，x：δ，u：β<$P：ε，然后通过Def。5.3我们得到Γ，x：δ，u：β<$u：β。此外，通过引理2.21.2我们有一元（σ，x：=z）xz，因此通过引理2.21.4我们得到一元（（σ，x：=z），u：=v）u v。现在，由于SNv，我们可以应用ind.hyp。并得到SNP（（σ，x：=z），u：=v）。然后，通过引理5.12P（（σ，x：=z），u：=v）=P（σ，x：=z），因此SNP（σ，x：=z）。最后，根据定义式3.4的λ规则，我们得到了SN（λxP）σ。另一方面，如果y=x，那么根据引理2.21.3，我们有一元（σ，y：=z）xN，因此我们可以应用ind.hyp。以获得SNP（σ，y=z）202S. Urciuoli et al. /Electronic Notes in Theoretical Computer Science 351（2020）187因此以同样的方式导出SN（λyP）σ。关于（ii），首先注意，由于α=β→γ，它遵循β=δ，因此Γ，y：β<$y：β。然后，由引理2.21.1，我们有一元[y：=N]yN和Lem。5.10我们有[y：=N]：Γ，y：β→Γ↓P，因此我们可以应用ind.hyp. (i)并获得SNP[y：=N]。最后，通过定义式3.4的β规则，我们得到（λyP）N→SNP[y：=N]，从而通过exp规则，我们可以得到SN（λyP）N。- 例exp：则SNM从M→SNP和SNP得出，我们需要证明2：（i）SNMσ和（ii）SNMN。 （一）主要内容：3我们Mσ→SNPσ和ind. 2（i）SNPσ，则由规则exp得到SNMσ。 （二）、因。(ii)在SNP上，我们有SNPN，因此通过应用于M→SNP 的规则 appL， 我们得到MN→SNPN ， 因此通过 exp， 我们可以导 出SNMN，如所期望的。- 情形β：则（λxM）N→SNM [x：= N]由SNN得出，我们需要证明3：（（λxM）N）σ→SNM [x：= N] σ。首先，注意到在定义式2.5中，我们有（（λxM）N）σ=（λzM（σ，x：=z））Nσ，其中z=χ（σ，λxM）。 此外，由主ind. hyp. 1（i）我们有SNNσ，因此根据定义式3.4的β规则，我们有（λzM（σ，x：=z））Nσ→SNM（σ，x：=z）[z：=Nσ]。此外，Lem。2.6.1我们得到z#（σ，λyM ）， 因此通过Cor 。2.12.1 我们有M （σ，x： =z） [z： =Nσ]<$αM[x：=N]σ。最后，我们可以利用定义式3.4的规则α得到（（λxM）N）σ→SNM[x：=N]σ。- 情况appL：则MN→SNMJN从M→SNMJ得出，并且我们必须证明3：（MN）σ→SN（MJN）σ。通过ind. hyp. 我们有Mσ→SNMJσ，因此通过appL规则，我们可以在两侧应用Nσ，得到MσNσ→SNMJσNσ，由定义2.5，它等于（MN）σ→SN（MjN）σ。- 情形α：则M→SNP遵循形式M→SNN和N<$αP，我们需要证明3：Mσ→SNPσ。通过ind. hyp. 我们有Mσ→SNNσ和Lem。2.11.8我们得到Nσ=Pσ，因此通过引理。2.11.1我们得到Nσ<$αPσ，然后根据定义式3.4的α规则，我们可以导出Mσ→SNPσ。Q6结论应结合导言中所述的期望来评估上述工作我们首先将相关性分配给形式化版本