无类型λμ-演算的并行约简及连续性研究:结构规则的分析和正确证明

52理论计算机科学电子笔记42（2001）网址：http://www.elsevier.nl/locate/entcs/volume42.html15页无类型λμ-演算巴巴健介1九州大学福冈812-8581日本广川幸男2九州大学福冈812-8581日本藤田健越3岛根大学邮编：690-8504摘要已知类型λμ-演算是强正规化的和弱Church-Rosser的，因此是连续的。事实上，Parigot用“Tait-and-Martin-L o？f“方法给出了一个并行约简，以提供类型λμ-演算的连续性。然而，钻石属性并不适用于他的平行还原。无类型λμ-演算的推论不能从有类型λμ-演算的推论中导出，而且据我们所知还没有得到证实。 我们分析粒度的约简规则，然后引入一种新的并行约简，使重命名约简和连续结构约简都被看作是一步并行约简。证明了新的平行约化公式具有钻石性质，从而给出了无型λμ -演算的相合性的正确证明.新的并行约简的菱形性质也适用于包含对称结构约简规则的λµ -演算的按值调用版本。1电邮地址： baba@i.kyushu-u.ac.jp2电子邮件地址：hirokawa@cc.kyushu-u.ac.jp3电邮地址： fujiken@cis.shimane-u.ac.jp2001年由ElsevierScien ceB出版。 诉 操作访问和C CB Y-NC-ND许可证。马场、虹川、藤田531介绍Parigot项[α]M将α索引为M的一个类型，项μα.M有一个由M中的α索引的类型。这些构造器提供了经典的证明，同时可以被认为是函数式编程语言的控制算子。近似地，我们可以把[a]M看作（抛出一个M），把μa.M看作（捕获一个M）。λµ项M定义如下：M：：= x| λx.M|MM| µα.M|[α] M微积分有以下基本的归约规则。β约化：（λx.M）N→M[x：=N]结构简化：（µα.M）N→µα.M[[α]w：=[α]（wN）]重命名：[β]（µα.M）→M[α：=β]我们假设对λ-演算[2，11，12]有一些熟悉。在结构简化中，替代定义如下：1. x [[α] w：=[α]（wN）]= x2. （λx.M）[[α] w：=[α]（wN）]= λx.M [[α] w：=[α]（wN）]3. （MM）[[α] w：=[α]（wN）]= M [[α] w：=[α]（wN）] M [[α] w：=[α]（wN）]4. （μβ.M）[[α] w：=[α]（wN）]= μβ.M [[α] w：=[α]（wN）]5-1. （ [β] M）[[α] w：=[α]（wN）]=[β]（M [[α] w：=[α]（wN）] N）如果α= β5-2. （[β] M）[[α] w：=[α]（wN）]=[β] M [[α] w：=[α]（wN）]如果α/=β在[15]中，Parigot概述了λµ演算的连续性证明。他提出了平行归约，并声称平行归约的钻石性质：如果M<$N，则N <$M<$。这里M是通过减少M中的所有赎回而获得的项。M染色体通常被称为M染色体的“完全发育”[2]。降偏公式是基于“T ait-and-Martin-L o？f“方法，并对该方法进行了说明在[20]中，该方法适用于多种约化系统的相合性证明。然而，该方法的直接应用并不适用于λ µ演算。实际上，[15]中的平行约化公式并不具有金刚石性质，另见[5]中的观察。要证明这种一致性并不像它看起来那样微不足道。已知λµ演算是强正规化[16，17]和弱Church-Rosser的。对于演绎的概念，这两个性质产生了类型化项[6，7]的一致性[2]。但是无类型λμ-演算不是强正规化的。例如，项（λx.xx）（λx.xx）没有正规马场、虹川、藤田54⇒⇒/form.令人尴尬的是，就我们所知，关于无类型λμ-演算的一致性的正确证明从未发表过我们认为，平行约化不具有金刚石性质的原因在于结构约化规则的顺序性。 考虑项M =（μα. [α]（μβ. [α]x））y，它有一个重命名的redex和一个结构redex。我们有项N1=（μα）。[α] x）y和N2= μα。[α]（μβ. [α]（xy））y）分别通过重命名和结构化约简，很好然后我们有M N1和M N2。如果金刚石性质成立，那么N1和N2可以在一步约简中约简为相同的项M。然而，这在这里是不可能的在结构约简之后，M中重命名redex的为了使残差返回到重命名的redex，我们需要另一个结构化步骤还原我们认为这样一个连续序列的结构约简作为一个一步并行约简。有了这样的公式，我们可以证明平行约化的强钻石性质。M =（µα. [α]（μβ. [α]x））yR/S联系我们公司简介N1=（µα. [α] x）yN2= μα。[α]（μβ. [α]（xy））y）SS/❅❅❘µα。[α]（xy）R/D联系我们我们把λµ-演算看作是一种编程语言，把归约看作是一种计算。λµ演算的归约规则捕获了带有控制的函数式编程语言的机制[9，4，8]。然而，我们不能应用一个任意的减少实现的编程语言。我们通常会制定一个缩减策略。按值调用λµ-演算λµv首先由Ong和Stewart考虑[14]。λµv演算包含另一个约简规则，称为“对称结构约简”，N（μα.M）→ μα.M [[α] w：=[α]（Nw）]。注意，即使整个系统是连续的，子系统也不总是连续的。因此，即使我们忽略对称结构约化规则，λµv的连续性也不会产生λµ的连续性。我们还将为λµ-演算的按值调用版本制定一个适当的并行约简，并证明强钻石性质。本文讨论了无型λμ-演算，λμ-项的定义与原来的定义不同.例如，合式项（[α]M）N不是原始λμ-演算中的项，因为[α]M马场、虹川、藤田55不是一个无名的名词，而是一个有名的名词。 是否符合类型证明自由的λμ-演算仍然对原始的λ μ-演算有效吗？我们在下面几节中定义的平行归约关系包含在归约规则的传递闭包和自反闭包中，因此原始项的完全展开也是原始项。因此，我们的证明方法对于最初的λµ-演算的情况仍然是完全可靠的2λμ-演算的并行约化我们在下面定义平行缩减 规则1 -8是将Tait-and-Martin-L？f方法直接应用于β -约化、结构约化和重命名而得到的。本文介绍了最后一条推理规则9它结合了一个重命名和一个连续序列的结构减少。很容易看出，“→“的传递闭包和响应闭包与“”的传递闭包是相同的定义2.11. xx MMJJ2. λx.MJλx.MJMMNJJN3.MNNMMJ4. µα.Mµα.MJMMJ5. [α]M[α]MJMMJNNJ6. （λx.M）N<$MJ[x：=NJ]MMJJNNjJ7. （µα.M）N µ α.M [[α] w：=[α]（wN）]MMJ8. [β]（μα.M）μ M J [α：= β]M<$MJN1<$N1J·· · Nn <$NnJ9. [β]（（μα.M）N1·· ·Nn）<$MJ[[α]w：=[β]（wN1J·· ·NnJ）]我们定义一个项M的完全展开M_n如下：定义2.21. M=x。则M=x。2. M=λx.M1. 则M=λx.M1= λ x.3. M=M1M2。3.1M1=λx.M3。 则M=M3[x：=M2]。3.2M1=μ α.M3。则M=μα.M3<$[[α]w：=[α]（wM2<$）]。3.3M=M1M2o.w.马场、虹川、藤田56⇒⇒⇒ ⇒⇒⇒⇒ ⇒⇒/4. M=μ α.M1。 则M=μ α.M1。5. M=[α]M1。5.1M1=μ β.M2。 则M=M2[β：=α]。5.2M1=（μ β.M2）N1·· ·Nn. 则M<$=M2<$[[β]w：=[α]（wN1<$·· ·Nn<$）].5.3M=[α]M1o.w.3平行还原[15]中的一致性证明中的一个空白可以由下面的引理中的（2）来弥补如果没有规则9，（2）就不成立。引理3.1（1）如果MM J和NN J，则M [x：= N]M J [x：= N J]。(2) 如果MMJ和NNJ，则M[[α]w：=[α]（wN）]MJ[[α]w：= [α]（wNJ）]。(3) 如果M<$MJ，则M [β：= α]<$MJ[β：= α]。证据（ 1）可以很容易地通过对MM J的结构的归纳来证明。（3）是平凡的。(2)也可以通过对M MJ结构的归纳来证明。大多数案件都是例行公事。非平凡的情况是当M MJ的最后一个推论是8或9时。为了节省篇幅，我们只解释了8的情况。案例8. 最后一个推理规则是8。通过定义M<$MJ，M和MJ具有M=[β]（μγ.M1）的形式，MJ=M1J[γ：=β]，则M<$MJ具有以下形式：M1M1J8M=[β]（μγ.M1）<$M1J[γ：=β]=MJ由于γ是一个约束变量，我们可以假设γf=α。案例8.1. α=β。然后我们得到以下结果：M[[α]w：=[α]（wN）]= （[α]（μγ.M1））[[α]w：=[α]（wN）]=[α]（（μγ.M1[[α]w：=[α]（wN）]）N），MJ[[α]w：=[α]（wNJ）]= M1J[γ：=α][[α]w：=[α]（wNJ）]=M1J[[α]w：=[α]（wNJ）][[γ]w：=[γ]（wNJ）][γ：=α]。通过对M1<$M1J的归纳假设，我们有M1 [[α] w：= [α]（wN）]<$M1J[[α] w：=[α]（WNJ）]. 故我们有[α]（（μγ.M1[[α]w：=[α]（wN）]）N）M1J[[α]w：= [α]（wNJ）][[γ]w：= [α]（wNJ）][γ：=α]通过规则9。因此引理成立。案例8.2. α= β。马场、虹川、藤田57然后，替换给出以下结果：马场、虹川、藤田58⇒⇒→英/阿M[[α]w：=[α]（wN）]=（[β]（μγ.M1））[[α]w：=[α]（wN）]=[β]（μγ.M1[[α]w：=[α]（wN）]），MJ[[α]w：=[α]（wNJ）]==M1J[γ：=β][[α]w：=[α]（wN）]M1J[[α]w：=[α]（wN）][γ：=β].通过对M1的归纳假设，我们有M1 [[α] w：=[α]（wN）]<$M1j[[α] w：= [α]（ WNJ）]. 因此，我们有[β]（μγ.M1 [[α] w：=[α]（wN）]）M1J[[α]w：= [α]（wNJ）][γ：= β]。因此引理成立。✷定理3.2对任意λμ-项M和MJ，如果M <$Mj，则Mj <$M <$。证明是通过归纳的结构，M MJ，并显示在附录中。定理3.3若M <$M1且M <$M2，则存在某个M3使得M1<$M3且M2<$M3。证据 设M3= M。那么定理3.3由定理3.2成立✷由于“→“的传递闭包和自反闭包定理3.4无类型λμ-演算是合流的。4按值调用λμ-演算Ong和Stew- art首先提供了λµ-演算的按值调用版本与按名调用系统[15，16，17]相比，在按值调用系统中可以更多地采用某种约简规则;所谓的对称结构约简[15]，使得N（μα.M）μα.M[[α]w：= [α]（Nw）]。 已知的是，添加这样的归约规则会破坏连续性，除非上述项N是值的形式。在本节中，基于[5，6，7]中的观察，引入了作为扩展形式的V：：= x| λx.M|[α] M这个概念在值替换和由下面定义的结构归约或对称结构归约一个有洞的上下文E[]像往常一样被定义，这样，E：：= [ ] |EM|V E.设n≥0，M是一项.我们将E[N]写成En[En−1[··E1[N]··]]，其中每个i[ ]都是V[ ]或[ ]M的形式。为了简单起见，这样的i还表示值V或项M。马场、虹川、藤田59按值调用λµ-演算由以下归约规则组成：βv-约化（λx.M）V→vM[x：=V]结构约化（μα.M1）M2→vμα.M1[[α]w：=[α]（wM2）]对称结构约化V（μα.M）→vμα.M[[α]w：= [α]（V w）]重命名约化[β]（μα.V）→vV[α：=β]这个重命名规则与[14]中的重命名规则不同这种区分在扩展形式的价值观下是必不可少的，从CPS翻译的角度来看，这种形式的重新命名也是自然的，如[5，6，7]。我们将证明，新的并行归约也可以适用于证明λµ-演算的按值调用系统的一致性，与[14]中直接使用并行归约相反。为了证明这一点，我们定义并行归约如下：定义4.11. X xMMJ2. λx.Mλx.MJMMJNNJ3.MNMJNJ4. µα.Mµα.MJMMJ5. [α]M[α]MJMM JVNJ6. （λx.M）VMJ[x：=NJ]MMJNNJ7. （µα.M）Nμα.MJ[[α]w：= [α]（wNJ）]MM JVNJ8. V（μα.M）μα.MJ[[α]w：= [α]（NJw）]VMJE1E1J·· ·EnEnJE=En[· ·E1[]··]EJ=EnJ[· ·E1J[]··]9.[α]（E [μβ.V]）MJ [[β] w：= [α]（EJ [w]）]现在可以看到，→v的传递闭包和自反闭包是等价的。的传递闭包。引理4.2（1）如果VM，则M也是值的形式。(2) 如果MN和VNJ，则M [x：= V]N[x：=NJ]。(3) 如果MMJ和NNJ，则M[[α]w：=[α]（wN）]MJ[[α]w：= [α]（wNJ）]。(4) 如果MMJ和VNJ，则M[[α]w：=[α]（V w）]MJ[[α]w：= [α]（NJw）]。(5) 如果MMJ，则M[β：=α]MJ [β：= α]。马场、虹川、藤田60E··E··E(6) Letn≥0。 LetE[]=En[··E1[]··]和E J[]=EnJ[··E1J[]··]。IfMMJ和EiEiJ（1 ≤ i ≤ n），则M [[α] w：=[α]（E [w]）] M J [[α] w：=[α]（EJ [w]）].命题4.3对任意λμ-项M，存在M ∈ M，使得对任意N，N ∈ M，只要M∈ N。证据通过归纳法对的推导。在这里，完整的发展M可以归纳地给出如下：定义4.41. M=x。则M=x。2. M= λx.M。 则M = λx.M。3. M=M1M2。3.1M1=λx.M3和M2=V2。 则M=M3[x：=V2]。3.2M1=μ α.M3。则M=μα.M3<$[[α]w：=[α]（wM2<$）]。3.3M1=V1，M2=μ α。M4。则M=μα.M4<$[[α]w：=[α]（V1<$w）]。3.4M=M1M2o.w.4. M=μ α.M1。 则M=μ α.M1。5. M=[α]M1。5.1M1=E[µβ.V2]。则M=V2[[β] w：=[α]（E [w]）]，其中E[]定义为En[· ·E1[]··]，或E[]=En[· ·E1[]··]且n≥0。5.2M=[α]M1o.w.我们只给出[α]M1的情形M。其余的案件也可以按照类似的模式进行审判。1. [α]的情况[α]M1（E[µβ.V]）：1-1. MN= [α]N1 由 E[μβ.V]N1 以 5 ： 1-1-1 导 出 。E[µβ.V]µβ.V：在这种情况下，μβ.VN1=μβ。N2由V导出N2乘4，其中N2也是一个值。 根据归纳假设，我们有N2V，因此，N=[α]（μβ.N2）V[β：=α]=M由 9得到1-1-2. E[µβ.V]En[·· E1[µβ.V]· ·]（n≥1）：由于E1[μβ.V]不是一个值，因此En[·· E1[μβ.V]· ·]N1必须由以下公式导出：E1[µβ.V]N2J和EjEjJ（2≤j≤n），其中N1=nJ[2J[N2J]]。在这里，我们有两种情况1和两个推导每一个1-1-2-1. E1[µβ.V]V1（µβ.V）：1-1-2-1-1. V1（μβ.V）N2J= N3JN4J3：由µβ导出。VN4J和V1N3J由于μβ.VN4J=μβ.N5J必须从VN5J导出4、我们有N5JV由归纳假设，其中N5J也是一种价值。 设E1J为N3J[ ]，其中N3J 是一种价值。 那么归纳假设给出N3JV1缩写为E1JE1。从Ej（2≤j≤n）的归纳定理出发马场、虹川、藤田61→w e也有一个v e EjJEj，则由y 9得到[α]（EnJ[··E1J[μ β.N5J]··]）V[[β]w：=[α]（En<$[··E1<$[w]··]）].1-1-2-1-2. V1（µβ.V）N2J=N3J[[α]w：= [α]（N4jw）]由V1N3J和VN4J乘8：归纳假设给出 N3jV1和 N4jV2。由替换引理可知，we有veN4J[[β]w：=[β]（N3Jw）]V[[β]w：=[β]（V1w）]，其中N4J也是一个值，并且在替换下值是封闭的.对Ej（2≤j≤n）的归纳定理也给出了Ejj∈Ej. 因此，使用f9衍生物[α]（EnJ[· ·E2J[μβ.N4J[[β]w：=[β]（N3Jw）]]··]）（V[[β]w：=[β]（V1<$w）]）[[β]w：=[α]（En<$[· ·E2<$[w]··]）]，其右手边等于V<$[[β]w：=[α]（En<$[· ·E1<$[w]··]）]，其中E1是V1[]。1-1-2-2. E1[µβ.V]（µβ.V）M2：在这种情况下，我们对（μβ.V）M2N2J通过使用3或7。每种情况都可以按照与上述两种情况类似的模式进行验证例1-2. MN=NJ [[α] w：= [β]（EJ [w]）]由V导出NJ和EiEiJ（1≤i≤n），其中E[]=En[· ·E1[]··]且EJ[]=EnJ[· ·E1J[]··]：代换引理在归纳假设中的连续应用。2. 否则：归纳假设的直接应用✷最后，可以确认按值调用λμ演算的连续性，因为它具有钻石性质。定理4.5按值调用的无类型λμ-演算具有汇合性质。5相关工作和进一步问题归约的顺序性并行还原是一个非常清晰和直观的想法，这意味着同时减少多个赎回（存在于术语中）。它常用于证明归约系统的相合性然而，一个简单的降准公式并不总是有效的。λμ-演算就是这样一种归约系统。我们已经推断，困难来自于结构性缩减的顺序性。因此，我们建议，一个连续的序列的结构约简应被视为一个步骤的并行约简。正如Takahashi [20]所指出的那样，这个想法也不适用于λ n−1，即，具有η-展开的λ -演算：Mλx Mx 证明了λη-1的连续性 在[1，13]中。Jay和Ghani[13]通过引入“并行扩展”证明了这一一致性马场、虹川、藤田62→ → → →···Mλx1.Mx1λ x1x2.Mx1x2λx1x2x3。Mx1x2x3。VanRaams- donk [18]引入了“超发展”的概念来证明正交组合约化系统的连续性。超发展是一个还原序列，其中除了从初始项下降的赎回之外，在还原期间创建的一些赎回可能会收缩。这些工作的一个关键思想是克服一些序列性的减少。在目前阶段，我们还不能表明，一般说来寻找这种顺序性的一些判据是进一步的工作之一一个更多的减少规则Parigotµα。[α]M→M如果α在M中没有自由出现.考虑项M = μα。[α]（μβ. [γ]x）yz）。则M有η-redex和关于定义2.1规则9的redex。各Redex的减少在下图中以“η”和“RS”表示µα。[α]（μβ. [γ]x）yz）❅η∗❅❅❘Rs❄µα。[γ]xS✑✰✑（µβ. [γ] x）yz S✑✰✑（µβ. [γ]x）z“RS”，我们达到了μα。[γ]x与一步并行还原。 如果我们首先应用η，我们有（μβ）。[γ] x）yz，从这里我们不能到达μα。[γ]x与一步并行还原。然而，我们可以通过计算a来克服这种情况。一系列的结构性削减作为一个步骤。基于这一思想，我们也得到了一个关于η的平行约化公式，但为了简单起见，这里省略了形式上的描述。无型λμ-演算的实际应用为了使λµ-演算在实际应用中得以实现，我们需要实现一些机器。事实上，Bierman [3]，de Groote [10]和Selinger [19]提出了这样的抽象机器并分析了它们的行为。然而，所有这些机器本质上都是顺序的。我们期望我们的并行约简可以产生这些机器的自然扩展。马场、虹川、藤田63确认作者非常感谢推荐人提供的有用意见。引用[1] Akama，Y.：On Mints[2] 巴伦德雷格特临：《The Lambda Calculus》，第2版，1984年阿姆斯特丹北荷兰[3] Bierman ， G. M ： A Computational Interpretation of the λµ-Calculus ，UniversityofCambridgeComputerLaboratoryTechnicalReport448（1998）.[4] Felleisen，M.，D. P. Friedman，E. Kohlbecker和B.杜巴：顺序控制的句法理论，理论计算机科学52（1987），205[5] Fujita，K.：经典证明演算I，计算机科学讲义1345（1997），321[6] Fujita ， K. ： Exploratory Typed λµ-Calculus for Polymorphism and Call-by-Value，Lecture Notes in Computer Science1581（1999），162[7] Fujita ， K. ： Domain-Freeλ µ-Calculu s ， InformatiqueT h′eoriqueetApplications，forthcoming.[8] Gri Bern，T.：A Formulae-as-Types Notion of Control，Conference Recordof 17th ACM Symposium on Principles of Programming Languages（1990），47[9] de Groote ， Ph. ： On the Relationship between the λµ-Calculus and theSyntactical Theory of Sequential Control ， Lecture Notes in ComputerScience822（1994），31-43.[10] de Groote，Ph.：一个环境机器的λµ-演算，数学结构在计算机科学中，出现。[11] Hindley，J. R.：[12] Hindley，J. R. 和j. P. Seldin：[13] 杰伊角B.和N. Ghani：The Virtues of Eta-expansion，LFCS report ECS-LFCS-92-243（1992）.[14] 翁 角 ， 澳 - 地 -H. L. 和 C. A. Stewart ： A Curry-Howard Foundation forFunctional Computation with Control ， Proc.24th Annual ACM SIGPLAN-SIGACT Symposium of Principles of Programming Languages（1997）。[15] Parigot，M.：λµ-演算：古典自然演绎的数学解释，人工智能讲义624马场、虹川、藤田64（1992），190马场、虹川、藤田65⇒[16] Parigot，M.：二阶经典自然演绎的强规范化，Proc.8th IEEE Symposiumon Logic in Computer Science（1993），39[17] Parigot，M.：二阶经典自然演绎的强规范化证明，J.Symbolic Logic62（4）（1997），1461[18] van Raamsdonk，F.：Confluence and Superdevelopment，Lecture Notes inComputer Science690（1993），168[19] Selinger，P.：名称调用λµν-演算的实现，手稿。[20] Takahashi，M.：并行约简在λ-演算，信息和计算118（1995），120附录：定理3.2定理3.2对任意λμ-项M和MJ，如果M <$Mj，则Mj <$M <$。证据 通过对M<$MJ的结构的归纳，1. M=x。然后我们有M=MJ=x。所以我们有MjM。2. M=λx.M。则M<$MJ具有以下形式。M1M1J2M=λx.M1<$λx.M1J=MJ通过归纳，我们得出了M1j=M1n的结论. 我们得到了MJ=λx.M1jλx.M1=M。3. M=M1M2。3.1. M=（λx.M3）M2。然后我们得到了一个veM_j=M_3_j[x：=M_2_j]和M_J的最后一个推理规则是3或6。3.1.1. 最后一个推理规则是3。则M<$MJ具有以下形式。M3M3J2λx.M3<$λx.M3JM2M2J3M=（λx.M1）M2<$（λx.M3J）M2J=MJ通过归纳总结，我们将M2 j分为M2j，M3J分为M3j. 应用规则6，我们有一个（λx.M3J）M2J<$M3<$[x：=M2<$]。 这是我的荣幸。马场、虹川、藤田66⇒⇒J⇒⇒3.1.2. 最后一个推理规则是6。MMJ具有以下形式。M3M3JM2M2J6M=（λx.M3）M2<$M3J[x：=M2J]通过归纳总结，我们将M2 j分为M2j，M3J分为M3j. 根据引理3.1（1），它遵循M3J[x：=M2J]M3<$[x：=M2<$]。 T husMJM和定理成立。3.2. M =（μa.M3）M2。那么M<$MJ的最后一个推论是3或7。3.2.1. MMJ的最后一个推理规则是3。则M<$MJ具有以下形式。M3M3Jµα.M3µα.M3J4M2M23M=（μα.M3）M2（μα.M3J）M2J通过归纳总结，提出了M2j=M3j =M2j=M3j= 应用规则7，wehe（μαM3J）M2Jμ α.M3<$[[α]w：=[α]（wM2<$）]。因此，MJM和定理成立。3.2.2. MMJ的最后一个推理规则是7。则M<$MJ具有以下形式。M3M3JM2M2J7（μα.M3）M2μα.M3J[[α]w：=[α]（wM2J）]通过归纳总结，提出了M2j=M3j =M2j=M3j=适用于-在引理3.1（2）中，wehaveμa.M3J[[α]w：=[α]（wM2J）]<$μa.M3<$[ [α]w：=[α]（wM2<$）]. 因此，MjM和定理成立。3.3. M= M1M2，M1不是λ-抽象或μ-抽象。则M∈=M1<$M2<$，M∈MJ具有以下形式.M1M1JM2M2J3M=M1M2M1JM2J=MJ通过归纳总结，我们将M1 j=M1j，M2J=M2j。我们有M1JM2JM1M2。 因此定理成立。4. M=μα.M1。然后我们有M=μα.M1和MMJ有以下形式。M1M1J4µα.M1µα.M1J通过归纳，我们得出了M1j=M1n的结论. 根据规则4，我们µ α.M1Jµ α.M1。 因此定理成立。马场、虹川、藤田67⇒5. M=[α]M1。5.1. M=[α]（μβ.M2）。则我们有M=M2[β：=α]. M Mj的最后一个推理规则是5或8。5.1.1. MMJ的最后一个推理规则是5。则M<$MJ具有以下形式。M2M2J4µβ.M2µβ.M2J5M=[α]（μβ.M2）<$[α]（μβ.M2J）=MJ通过归纳总结，我们提出了M2 j =M2j的观点. 适用规则8。然后我们have[α]（μ β.M2J）<$M2<$[β：=α]. 因此，M∈MJ和定理成立。5.1.2. MMJ的最后一个推理规则是8。M2M2J8M=[α]（μβ.M2）<$M2J[β：=α]=MJ通过归纳和论证，我们得出了M2 j=M2J=M2j的结论. 应用引理3.1（3）。然后wehav e M2J[β：=α]<$M2<$[β：=α]，因此MJ<$M<$。5.2. M =[α]（（μβ.M2）N1···Nn）.则我们有M=M2[[β]w：=[α]（wN1···Nn）].最后一个推理规则M<$MJ是5或9。5.2.1. MMJ的最后一个推理规则是5。则M<$MJ具有以下形式。（μβ.M2）N1<$QJN2<$N2J· ··NnNnJ3，···，3（μβ.M2）N1·· ·NnQJN1J·· ·NnJ5M=[α]（（μβ.M2）N1·· ·Nn）<$[α]（QJN1JNnJ）=MJ则（μβ.M2）N1<$QJ的最后一个推理规则是3或7。5.2.1.1. （μβ.M2）N1<$QJ的最后一个推理规则是3。则QJ=μβ.M2JM2M2J对于某个M2J，M<$MJ具有以下形式。4µβ.M2µβ.M2JN1N1JN2N2J· ··NnNnJ3，···，3（μβ.M2）N1·· ·Nnn（μβ.M2J）N1J·· ·NnJ5M=[α]（（μβ.M2）N1·· ·Nn）<$[α]（（μβ.M2J）N1JNnJ）=MJ通过归纳总结，我们得出M2J<$M2j，N1J<$N1j·· ·，NnJ<$Nnj.第九条规则。则weh ave[α]（（μ β.M2J）N1J·· ·NnJ）<$M2<$[[β]w：=[α]（wN1<$·· ·Nn<$）]. 因此，MjM成立。5.2.1.2. （μβ.M2）N1<$QJ的最后一个推理规则是7。马场、虹川、藤田68⇒···则M<$MJ具有以下形式。M2M2JN1N1J7（µ β. M2）N1μ β。M2J[[β]w：=[β]（wN1J）]N2N2J· ··NnNnJ3，···，3（µ β. M2）N1·· ·Nn（μ β. M2J[[β]w：=[β]（wN1J）]）N1J·· ·NnJ5M=[α]（（μ β. M2）N1·· ·Nn）<$[α]（（μ β. M2J[[β]w：=[β]（wN1J）]）N1J····························································································································NnJ）=MJ通过归纳总结，我们得出M2 j=M2j，N1J=N1j的结论。 根据引理3.1（2），我们有一个M2J[[β]w：=[β]（wN1J）]<$M2<$[[β]w：=[β]（wN1<$）]. 另手，我们有一个N2JN2，NnJ第9条. 然后我们有通过归纳总结，我们可以得出以下结论：应用[α]（（μβ.M2J[[β]w：=[β]（wN1J）]）N2J·· ·NnJ）<$ M2<$[[β]w：=[β]（wN1<$）][[β]w：=[α]（wN2<$· ··Nn <$）]=M2[[β]w：=[α]（wN1<$N2<$·· ·Nn<$）]。因此，M∈MJ和定理成立。5.2.2. MMJ的最后一个推理规则是9。则M<$MJ具有以下形式。M2<$M2JN1<$N1J·· · Nn<$NnJ9[α]（（μβ.M2）N1·· ·Nn）<$M2J[[β]w：=[α]（wN1J·· ·NnJ）]通过归纳，本文提出了M2J<$M2n，N1J<$N1 n，·· ·，NnJ <$NN N N N NN nn的概念。应用引理3.1（2）和（3），我们有一个M2<$[[β]w：=[α]（wN1J·· ·NnJ）]<$M2<$[[β]w：=[α]（wN1<$·· ·Nn<$）]. 因此，MjM和定理成立。5.3. M= [α]M1且M1不是M1=μβ.M2或M1=（μβ.M2）N1···Nn的形式。然后我们有M<$=[α]M1<$且M<$MJ具有以下形式。M1M1J5[α]M1[α]M1J通过归纳总结，我们得出了M1 j=M1j的结论. 应用规则5，我们有一个ve[α]M1J<$[α]M1<$。 因此定理成立。✷