Howe方法及其在证明函数式语言上的应用相似性的有效性方面的研究

理论计算机科学电子札记164（2006）85-104www.elsevier.com/locate/entcsHowe保罗·布莱恩·利维1英国伯明翰大学摘要Howe方法是一种著名的证明函数式语言上的各种应用双相似性（或相似性）是同余（或预同余）的技术。它通过构造具有某些特殊性质的给定关系的扩展来进行。该方法可用于确定性和不确定性语言，但在后一种情况下，它有一个奇怪的限制：它要求语言的语法是无穷的。例如，这就排除了具有可数和类型的语言，并且在文献中一再引起问题。在本文中，我们给出了一个变化的豪的方法，称为“无限豪的方法”，避免了这个问题。该方法涉及定义两个扩展的原始关系的相互coinduction。这两个扩展都具有Howe扩展的关键属性在本文的第一部分，我们将看到这是如何在具有可数和类型的按值调用语言中工作的。在第二部分中，我们看到当我们使语法非良基时，该方法继续工作。更确切地说，我们表明，使用混合归纳/共归纳的参数，各种形式的应用相似性和bisimilarity保存的任何替代上下文。关键词：Howe1介绍1.1确定性语言在[1]中引入了确定性λ-演算上的应用模拟和互模拟的概念它们模仿了并发理论中的模拟和互模拟的概念一个闭项被看作是一个进程，它的计算结果是一个λ-抽象，然后等待被提供一个操作数。与其他形式的模拟/互模拟一样，为了使这些形式有用，有必要证明当扩展到非闭项时，最大的这种（称为应用相似性和双相似性）是预同余。文[1]用指称的方法证明了这一点。Howe [6]引入了一种纯粹的操作技术来证明应用相似性是预同余，称为“Howe方法”。该技术包括1电子邮件：pbl@cs.bham.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.06.00686P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85我将相似性扩展到一个明显相容的关系2，并且具有一些特殊的性质，使其成为一个模拟。因此，它与相似性相吻合。那篇论文并没有证明应用性双相似性是一个全等性。但在确定性的设置中，没有必要直接证明这一点。 相反，我们可以做的是首先证明观测前序和等价性分别是模拟和互模拟。它遵循• 应用相似性与观测前序一致• 应用双相似性、相互应用相似性和观测等价性都是一致的。这条推理路线在[5，14]中提出然而，在非确定性的3设置中，所有这些巧合都失败了：应用双相似性严格比相互应用相似性更好，而相互应用相似性又严格比观察等价性更好[8，13]。(This这是为了简化问题，因为有各种各样的应用相似性和双相似性，以及观察等价性。此外，至少可以肯定的是，在非确定性函数语言上，应用双相似性比观察等价性更自然因此，证明应用双相似是一个同余的问题变得重要。在第二篇论文[7]中，Howe通过证明Howe扩张的传递闭包是对称的来解决这个问题。在[13]中给出了这种方法的推广，以证明精化相似性--一种不是双相似性的变体--是预同余。这个论证使用了下面的（R是R的自反传递闭包。）命题1.1设Ri是A i上的自反二元关系，其中i ∈ I。 如果我是一个人，（R）=（R i）作为i∈IAi上的关系。i∈Ii∈I第二个方向（这是一个要求我是有限的）说，鉴于一个有限维的长方体，从一个顶点到另一个顶点现在假设S是一个前序的相容闭包。 显然，这是一种报复。 它可能不是传递的，但它的传递闭包S被Prop.1.1中的任何项构造函数θ保持，将I设置为θ的arity。因此，S是相容的。这是论证的本质，无论是豪的版本还是皮彻的版本但这有一个奇怪的局限性：它只能在每个项构造函数都是无穷大时才能工作。这是一个奇怪的限制，因为它完全是语法上的。 从从语义的角度来看，人们经常想用，例如，可数[2]兼容关系是由语言中的每个项构造函数保持的关系[3]更准确地说，是在一个不稳定的非确定性环境中。HoweP.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）8587和类型。因此，这种限制在文献中一再引起问题并不奇怪。• 文[13]研究了具有可数和型和可数积型的非确定语言。正如在第142页上所解释的，豪的方法不能证明双相似性是一般的全等性--只适用于一类有限的片段。• 在[13]中，研究了细化相似性。正如在第150页上所解释的，豪• 独立地，在[12]中，研究了具有可数和类型的非确定性语言HOPLA;但不能证明应用双相似性是一个同余（第8页，性质（vi））。本文的贡献是给出了Howe方法的一个变体它包括定义两个原始关系的扩展-“向前和向后扩展”-通过相互共归纳。(For一个无穷语言，这些分别是Howe扩展和它的对偶。每一个都具有Howe扩展所享有的用于显示模拟的相同的特殊属性向前和向后扩展是不兼容的，但是它们的交集是兼容的，这是足够的。1.2非良好基础的已经证明了无限豪这里的困难是需要证明双相似性是由非良基上下文保持的，但我们看到该方法实现了这一点。我们的解释依赖于在[5，8]中开发的关系演算。由于归纳和共归纳的复杂混合，不使用微积分就很难把论证说清楚。1.3论文结构本文研究了三种语言的递增序列：• L0，其术语语法是无穷的•L1，其术语语法是无限宽的•L2，其术语语法是非良基的。这些是具有可数非确定性的按值调用语言在定义了L0和L1以及应用相似性和双相似性的各种形式之后，我们回顾了Howe88P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85(i) 各种形式的应用相似性是L0和L1(ii) 各种形式的应用双相似性和精化相似性是L0上的预相合。我们将这篇评论分为两个部分。一部分，我们指定的“核心”，是共同的豪的方法和无限豪的方法。它描述了Howe扩张的性质，并说明了它们如何暗示该扩张是一个模拟。在第二部分中，我们给出了Howe扩张的具体构造我们还看到如何使用Prop.1.1来证明（ii）。然后，我们描述了无限豪最后，我们继续到L2，我们在7.1节中定义它。在考虑了一个关系在所有上下文中都是封闭的意味着什么之后（7.2节），我们在7.3节中证明了向前和向后扩张的交集满足这个性质。因此，各种形式的应用相似性和双相似性都具有这种性质。2按值调用演算我们定义语言L0和L1。L0的类型如下：共归纳定义A：： =i∈IA i| A→A其中，我在有限集合上的范围（产品类型可以毫无困难地包括在内。）我们写0表示空和类型，nat表示唯一类型A，使得A=（0→ 0）+A。L1的类型是相同的，除了I在可数集上的范围上下文 是一个序列x ：A0，.，xn−1 ：n-1个不同的标识符，Q关联类型。 重命名的ΓΔ是一个函数，它取每个标识符（x：A）∈Γ到一个恒等式（q（y））∈Δ。微积分，如在[8]中，将值与普通项区分开来（不清楚如何使豪的方法在没有这种区分的情况下工作）。因此有两个判断：Γ<$M：B表示M是B型项，而Γ<$vV：B表示V是B型值。这种类型的按值调用λ演算被称为细粒度。语法在图中归纳定义1.一、我们把M写成x。N对于首先执行M的顺序计算，当它返回一个值V时，继续执行N，x绑定到V。这是用莫吉的语法用let写的关键字pm代表“模式匹配”。对于每个n∈N，nat型的闭值n以明显的方式定义。任何一个最小值都是mθ{Mi}i∈I的唯一值，其中P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）8589你呢？：natr，x：A，rJvx：AV：AΓ，x：A<$M：B令V为x。M：BV：A返回V：ArM：Ar，x：A<$N：BrM到x。N：BvV：AΣˆı∈IvV：i∈IAiΓ，x：Ai<$Mi：B（<$i∈I）r，x：AM：BΓvλx.M：A→BΓvV：A→B关于VW：BFig. 1. 具有可数不确定性的• θ是元I的项构造函数（L0的有限集，L1的可数集）• {Mi}i∈I是M的直接子项，可以是项或值。特别地，每个标识符都是arity 0的term构造函数设Γ和Δ为上下文。• 一个重命名的ΓqΔ可以应用于任何项ΓM：B以获得项Δ q<$M：B，并且同样地应用于值。−−→V/x•一个代换Γ Δ是一个函数，它将每个标识符（x：A）∈Γ取为一个值ΔΔVx：A。我们可以将其应用于项ΓM：B以获得项−−→ΔM[V/x]：B，同样也是一个值。这些操作是归纳定义的[3，4]。A型闭项M的运算行为由三部分给出[11，8]：• 关系M<$V，其中V是类型A的闭值，这意味着M可以返回V• 一个谓词M，意味着M可以发散• 一个关系M<$QV，其中V是A型闭值的集合，这意味着M必须返回某个值，V是可能性的集合。这些关系在图中定义二、它们由以下结果联系起来命题2.1设M是A型闭项，V是A型闭值集。则M<$QVi <$M/V且V ={V|MV}。Γ►v⟨ˆı,V⟩:i∈IAi当{i，x <$.Mi}i∈I：B时，90P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85归纳定义（Inductive definition）？卢恩n∈NM[W/x]mV设W为x。MVreturnVM<$WN[W/x]<$V M至x。NVM[W/x]mV（λx.M）WV[W/x]Vpm，Was{i，x.Mi}i∈IVˆı∈I共归纳（coinductive）定义M[W/x]mm设W为x。MMM到X。NMVN[V/x]M到X。NM[W/x]mm（λx.M）W[W/x]mmpm，Was{i，x.Mi}i∈Iˆı∈I必须收敛（归纳定义）？Q{n|n∈ N}M[W/x]ΩV设W为x。MQVM<$QWN[W/x]<$QVW（<$W∈ W）returnVQ {V}M到X。NQV WW∈WM[W/x]ΩV（λx.M）W<$QV3关系[W/x]Vpm，Was{i，x.Mi}i∈IQV图二. 操作语义ˆı∈IP.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85913.1基本建设因为本文使用了大量关于关系的推理，所以我们在这里收集了基本属性。92P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85X定义3.1（i）一个闭关系R将一个关于存在于其上的闭项的二元关系和一个关于存在于其上的闭值的二元关系与每个类型A相关联(ii) 一个开关系R将一个关于驻留在它上面的项的二元关系与每个r A相关联，将一个关于驻留在它上面的值的二元关系与每个值r v A相关联，对于任何重命名的r q Δ，所有这些都由q <$保留。(iii) 我们将项和值上的恒等关系写成id，将恒等关系限定为标识符的恒等关系写成idf（两者都是开放关系）。(iv) 对于关系组合，我们按图解顺序写;。(v) 如果R是一个开关系，我们写R0为限制R的封闭项和封闭值。(vi) 设R是一个闭关系。我们定义R（R的开扩张）为−−→−−→当M[V/x]RN[V/x]为−−→从Γ到空上下文的任何替换V /x注意闭关系的偏序集和开关系的偏序集在包含下都形成一个完备格因此，当我们使用单调函数、最小前定点和最大后定点定义一个开关系时，我们不需要证明结果关系的重命名条件--它是自动的。定义3.2设R和S是开关系。我们定义R[S]（S在R中的子项）为由项对Δ R构成的开关系，−− →−−→J JM[V/x]，N[W/x]：B，对于每一对项Γ∈M，N：B和子项对，−−→−−→函数ΓV/xΔ和ΓW/xΔ使得MJRNJ和V对于每个（x：A）∈ Γ，定义3.3设R是一个开关系。(i) 定义R^（对R的可实现的定义）以满足操作相关性当nθ=φ（henceI=J）时，若mθ{Mi}i∈I，dφ{Nj}j∈J，MiRNi，对于每个i∈I。(ii) 我们以同样的方式定义Rfinn，除了我必须是有限的。(For L0，这个硬币和R^在一起。(iii) 我们定义R是一种新的方法，因此不需要对θ m进行定义。命题3.4（i）上面给出的所有运算都是单调的。(ii)开关系的完备格在二元运算− [ − ]下形成有序幺半群，单位由idf给出。XP.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85930^（三）id[id]=id（1）欧欧R [S ]=（R[S]）（2）（R;RJ）[S;SJ] =（R[S]）;（RJ[SJ]）（3）（Ri）[S]=（Ri[S]）（4）i∈I i ∈I（R[S]）（5）R[id]=R（6）R0=R（7）S 中文（简体）中文（繁体）R^=RidfanddRidf=（9）idfRR^（十）（11）第11章：你是我的女人i^d=id（12）(iv) 如果R和S是互反的开关系，则R[S]=（R[S]）（13）R=R（14）证据（11）从R上的重命名假设得出。（iv）由prop.1.1得出。其余的都是微不足道的。Q定义3.5设S是一个开关系。(i) 当idf≠ S且S[S]≠ S时，S是置换的。(ii) 当S^≠ S时，S是相容的。(iii) 当Sfinn≠ S时，S是有限相容的。(ForL0，这与兼容性一致。）第3.6节（在第3.6节中无效） 7）设R是一个开关系。(i) 如果R是相容的，那么它是自反的。(ii) 存在唯一的开关系S使得S= R <$S，并且它是包含R的最小相容开关系。我们写RC，R的相容闭包，为在Prop中描述的开放关系。3.6㈡.命题3.7[5]设f是格A上的单调内函数，令x ∈ A。(i) （强归纳法）设f有最小预动点a。 则f（x <$a）<$a ≤ aa≤x。(ii) （强共归纳）设f有最大后定点b。 则b ≤ f（x ≠ 094P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85b）b意味着x≤ b。P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85954应用相似性定义4.1封闭关系R尊重值，当• V R VJ：A→B蕴含VW R VJW：B，对于每个闭值W：A• ⟨ˆı,V⟩R⟨ˆıJ, VJ⟩:Σi∈IAiimpliesˆı=ˆıJandVRVJ:Aˆı在[8，13]中，研究了应用模拟的三种变体，对应于下，上和凸幂域。在这里，我们介绍了第四个变种称为定义4.2设R是一个闭关系。(i) 我们说，R是一个较低的模拟时，它尊重的价值，和M R MJ和M<$V意味着MJ<$VJ对于某个VJ使得V R VJ。(ii) 我们说，R是一个上模拟时，它尊重的价值，和M R MJ并且M<$QV蕴含MJ<$QVJ，其中<$VJ∈ VJ。V∈ V。V R VJ.(iii) 我们说R是一个smash simulation，当它尊重值时，并且M R MJ和M <$QV蕴涵MJ<$QVJ，其中<$VJ∈ VJ。 V ∈ V，V R VJ和V ∈ V。<$VJ∈ VJ。V R VJ.(iv) 我们说R是一个凸模拟（又称部分互模拟[2]），当它既是一个下模拟又是一个上模拟（因此也是一个粉碎模拟）。op(v) 我们说R是下/上/smash/凸运算，当R是一个下/上/粉碎/凸模拟。我们将下/上/粉碎/凸相似性定义为下/上/粉碎/凸模拟的最大闭合关系。我们可以通过结合模拟和操作模拟来定义一系列封闭关系。以下两个示例适用于我们的目的。定义4.3（i）下双相似性是最大的封闭关系，它既是下模拟又是下操作模拟。(ii)细化相似性是最大的封闭关系，它既是下模拟又是上操作模拟。所有这些关系显然都是前序关系。我们的目的是证明它们的开扩张（也是预序）是预同余。5Howe5.1该方法设R是一个闭关系，它是一个预序。在这一节中，我们回顾豪它集中于找到满足以下条件的开放关系。96P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85我000定义5.1设R是一个闭的预序，S是一个开关系。 S是在R上如何合适，当• S是自反的、代换的和有限相容的• S;R-硫代氨基甲酸酯• 如果θ{Mi}i∈ISN，则存在s{MJ}i∈I，则对于i∈I和d，我我θ{MJ}i∈IR<$N。 我很抱歉，亲爱的。对偶地，当S是自反的、置换的和有限相容的时，S在R上是op-Howe-适合的，并且R;SR;S^定义5.1是有意义的，因为下面的定理。命题5.2设S是一个开关系，它在闭前序R上是Howe-suitable或op-Howe-suitable。(i) RS(ii) 如果S0<$R（例如，如果（S<$）0<$R），则R<$= S = S<$。(iii) 如果R尊重价值，那么S 0也尊重价值，因此S0也尊重价值。证据(i) R=id;RS;RS(ii) 通过（8）。(iii) Supposejuvenile，VS0juvenileJUVENILE， VJ. 这个值是VJJ，它等于VS0Vj和Vd，V j R，VJR， VJR。因为Rr es pectsvalu es，所以Vsvj=Vs VJ，并 且 v v j =VSVJ。 这个等式成立，因为S是自反的和有限相容的。Q命题5.3（Howe模拟定理）（i）设S是闭预序R上Howe-适合的开关系。如果R是下/上/粉碎/凸模拟，那么S 0也是，因此S也是。（ii）对偶地，设S是一个在R上Howe-suitable的开关系。如果R是下/上/smash/凸运算模拟，则S 0也是，因此S也是。证据（i）假设R是一个较低的模拟。我们必须证明MS0N和M<$V意味着MJ<$VJ对于某个VJ使得VS0VJ。我们用MV进行归纳。设M=（λx.MJ）W.然后我们有MJ[W/x]<$V，并且存在P和WJ使得λx.MJSP和WSWJ和PWJRN。从λx.MJSP，存在MJj使得MJSMJ J和λx.M JRP。由于MJSMJJ和WSWJ，我们得到MJ[W/x]SMJJ[WJ/x]，因此，通过归纳假设，存在VJJ使得MJ[WJ/x]<$VJJ，因此（λx.MJ）WJ<$VJJ。我们有（λx.MJ）WJRPWJRPWJ（因为R考虑值），R是一个较低的模拟，所以存在VJ使得N<$VJ和VJRVJ。因此VSVJ。其他情况类似，但更容易。P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85970上模拟和粉碎模拟的结果被证明是类似的，凸模拟的结果是即时的。Q5.2豪Howe命题5.4设R是闭关系。则存在唯一关系S使得S=S^;R^，其中R^ 是 唯 一 的。 通常，在S中，该表达式是唯一的，使得S=Rε;Sε，其中Rε是唯一的。证据 如果S和SJ是两个这样的，我们证明了MSN通过N上的归纳法蕴涵MSjN。 Q作为一个唯一的定点，R·可以被归纳地或余归纳地定义 这里是归纳定义，明确地写 出 来 ： R· 是 最 小 关 系 S ， 使 得 that ， ifMiSMJ 对 于 所 有 i∈I ， 并 且dθ{MJ}i∈IR<$N，thenθ{Mi}i∈ISN。我我命题5.5设R是闭前序。(i) R·在R上是Howe-suitable的，并且R§在R上是op-Howe-suitable的。(ii) R·和R§是相容的。证据这可以从R·的归纳定义或共归纳定义中得到证明。这是归纳的版本。（ii）是平凡的，并且R·的Howe-适合性的所有要求除了替代性紧随其后。对于替代性，我们必须证明，如果M R·N：B和V（x）R·VJ（x），对于每个（x：A）∈−−→·−−J→r则M[V/x]R N[V /x]。我们对M R·N进行归纳（使用归纳定义），分别处理M是标识符和不是标识符的情况Q现在，如果我们写R表示较低的相似性，那么，根据Prop.5.3（i），R·0是较低的模拟，因此包含在R中，所以根据Prop.5.2（ii），R·0等于R·，这是相容的。所以R是兼容的。根据同样的论点，上相似、smash相似和凸相似都是相容的。对偶地，我们可以利用op-Howe扩张（直接）证明下、上、smash和凸反相似的开扩张是相容的。接下来，我们处理较低的双相似性和细化相似性，遵循[7，13]。命题5.6（i）如果R是L上的开预序，则RC相容。(ii) 如果R是L0上的闭前序，则R·=RC=R§此外，R·是R上唯一的Howe-suitable关系，R§是R上唯一的op-Howe-suitable关系。(iii) 若R是L0上的闭等价关系，则R·R是对称的.98P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85我我我vS. （（S;R）S证据(i) 这是从Prop1.1开始的。(ii) R·<$R <$C，因为R·是相容的，包含R<$。R·<$R<$C通过R·的归纳定义，使用（i）。第二个方程与第一个方程是对偶的。如果S是H-可持续的R，则S=S^;R，S=R·bypropop。五、四、(iii) 一般来说，R§=Rop·op，所以这是由（ii）得出的。Q因此，如果R是L0上的细化相似性，则R·R既是一个较低的模拟，作为R§，上运算模拟。所以它包含在R中，我们得到R=R·，R是兼容的。对于较低的双相似性也是如此。然而，这种方法不适用于L1，所以我们转向无限豪6Howe现在我们来看看关键的构造：R的前向扩张，记为R→，以及R的后向扩张，记为R←。定义6.1设R是一个闭序。我们定义（R→，R←）为最大的一对开放关系（S，T），• 如果M=θ{Mi}i∈ISN，则对于所有i∈ I，R∈ S{MJ}i∈I都满足MiSMJ我我且θ{MJ}i∈IR<$N，且MT<$N• 若NTM=θ{Mi}i∈I，则R∈S{MJ}i∈I满足NR∈θ{MJ}i∈I且我我对所有i ∈ I，MJT M i，且N S<$M。简而言之，（R→，R←）是ν（S，T）. （（S^;R<$）<$T<$，（R<$;T^）<$S<$）在两种特殊情况下，我们可以简化这个定义。命题6.2（i）如果R是L0上的闭预序，则R→=R·且R←=R§.(ii) 若R是一个闭等价关系，则R←=R→op，且R→是S中的最大运算，使得如果M=θ{Mi}i∈ISN，则R→的最大运算xs{MJ}i∈I，使得对所有i∈I和θ{MJ}i∈IR<$N，MiSMJ，且NS<$M. 简而言之，R→是我我联系我们证据 在两种情况下，使用（i）中的Prop.5.6（iii）进行Q）的。P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）8599一般来说，使用Prop.第3.7（ii）条，它表面上证明100P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85ˆˆ^ˆ ˆˆˆˆS（SR→;R）R→（15）S（TR←）R→（16）T（R;TR<$）R<$（17）T（SR→）R→（18）当（15）在我们的所有例子中，（17）命题6.3设R是闭项上的预序。(i)R→=R←(ii) R→是Howe-适合于R的，R←是op-Howe-适合于R的。(iii) R→R←是相容的。证据(i) R→R←，所以R→ R←。 根据同样的论证，R←R→。(ii) 我们首先证明（R，R）是好的，这意味着R→和R←是自反的。证明（15）R=id;R=id;R RHS。（16）是平凡的。接下来我们证明（R→;R<$，R<$;R←）是好的。 为了证明（15），R→;R（R→;R）;R=R→;id;RR→;R;R RHS。 为了证明（16），R→;RR←;R=（id;R←）;（R;id）（R;R←）;（R;R←） RHS。然后我们证明（R→finn，R←finn）是好的。为了证明（15），R→finnR→（R→finnR→;R）<$R→为了证明（16），R→finnR <$finnR<$finn（R<$finnR<$）R→为了证明R→和R<$可替换，我们证明了（R→[R→]，R<$[R<$]）是好的。为了证明（15），R→[R→]（R→;R→）[R→;id]（R（（RR→[R→];R→f;R→R→[R→];R→R→这是RHS的一部分。为了证明（16），R→ [R→] R←[R←]（R←[R←]）(iii) 很容易证明（R→<$R<$，R→ <$R<$）是好的。下面详细证明了一个更强的结果（Prop.7.6）。P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85101^Q为了说明我们如何使用它，让R是细化相似性。 然后是prop。5.3，R→ R是下模拟，R←R是上模拟，但它们0 0是相同的，因此包含在R中。 通过提案5.2（二）R=R→=R<$=R→R<$所以R是兼容的。7非良好基础的7.1适应良好的基础帐户现在我们来看看L2，在L2中，语法这个术语是非良基的。类型的语法与L1的语法相同（因此存在可数和类型）。为了定义术语语法，我们可能会试图使图1中的所有规则都是共归纳的，但这将给我们“无限值”，如i 0，i 1，i 2，.。. 不应该存在的错误4. 因此，我们需要确保值是归纳给出的，而项是共归纳给出的。x ∈val（X）（Γ≠vA）（x：A）∈ΓM∈X（Γ，x：A<$B）λx，M∈val（X）（Γ∈vA→B）V∈val（X）（ΓvA）V∈val（X）（Γ<$v<$i∈Iˆı∈IAi）图三. val（X）的值归纳定义，一个由值序列将valseq写为值序列的集合rvB，将termseq写为项序列的集合rB。对于任何termseq-索引集X，我们通过图3中的规则归纳地定义valseq-索引集val（X）。然后我们在图4中共归纳地定义一个项序列索引集P。最后，我们写• 对于M∈P（Γ<$A），Γ <$M：A• 对于V∈val（P）（ΓvA），ΓvV：A重命名和替换的定义是共归纳的，如[10]。图2和前面一样定义了操作语义，应用相似性的各种概念也和第4节一样定义。我们使用无限豪六、至于prop。 5.5，列出了豪扩张的性质，为了使其成立，我们定义R·为最大定点νS。（S;R）。最小的固定点甚至不会是反应性的。[4]在具有求和类型和非良基语法的λ演算中，这确实是一个项，但在按值调用求值策略下，它会发散。102P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85^Q？∈P（Γnat）V∈val（P）（r∈vA）M∈P（r，x：A<$B）设V为x。M∈P（Γ ∈ B）V∈val（P）（Γ ∈vA）returnV∈P（ΓvA）M∈P（Γ<$A）N∈P（Γ，x：A<$B）M到X。N∈P（Γ ∈ B）V∈P（ΓvA→B）W∈P（ΓvA）VW∈P（ΓB）V∈val（P）（Γ<$v <$i∈IAi）Mi∈P（Γ，x：Ai<$B）（<$i∈I）当{（i，x）.Mi}i∈I∈P（Γ∈B）时，见图4。项-P的共归纳定义，一个由项序列索引的集合7.2根据上下文定义7.1偏序集A上的闭包算子是A上的单调内函数f，使得对所有x∈A，x≤fx=f（f x）。使得fx≤x（即fx=x）的元素x称为f-闭的。根据标准序理论，相容关系是开关系R映射到包含它的最小相容关系μ S的内函数的闭元。（R S）。后一种关系可以被认为是R在所有良基上下文下的闭包（可能有可数个洞，每个洞出现可数次）。但我们想知道，在所有情况下，关系都是封闭的。所以我们按以下步骤进行。定义7.2设R是一个关系。它在约束环境R C下的闭包是relionνS。（RS^）。提议7.3（i）-C是闭包算子。(ii) RC是反应性和兼容性的。证据(i) RRR^，soRRC. AndRCC=RC <$R<$C C=R<$R^C<$R <$C <$R<$CC所以RCC通过简单的共归纳法而生成RC(ii) id=i^dRi^d，soidRC. 我们可以找到拉姆贝克引理。绑定上下文之所以如此命名，是因为它们将标识符绑定在插入的项中。 一种更一般的上下文被称为替代上下文，它可以P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85103我我0n−1用给定值代替插入项中的标识符。在替换上下文下关闭R的第一个建议是关系式：Q=νS。（R[S]S^）（19）在这种关系中，一对项位于证明树的根处，其中某些节点是兼容性节点。MiQMJ （i∈I）θ{Mi}i∈IQθ{MJ}i∈I其中α是arityI的项构造函数，其他节点是替换节点V0QVJ···Vn−1QVJM[V0/x0，. ，V n−1/x1] Q M J [VJ/x0，. ，V J/x1]0n− 1其中，M，M，J在上下文x0：A0，. ，xn−1：A n−1（相同类型的项或相同类型的值）（19）的问题在于它是普遍关系。相反，我们需要约束证明树，使得沿着远离根的分支移动，只有有限多个连续的替换节点，因此最终会碰到兼容性节点。我们用下面的方式来精确地说明这一点。定义 7.4设 R是一 个关 系。它 在置 换上 下文R SC 下的 闭包 是 关 系 νS 。 μT 。（R[T]S^）。提案7.5（一）(ii) - SC是闭包算子。(iii) RSC[RSC]RSC证据(i) 我们推理RC=RR^C= R [id f] R ^CR[R^C]ΔR[R[μT. （R[T]<$R^C）]<$R^C]<$R^C=R[μT. （R[T]<$R^C）]<$R^C=μT。（R[T]<$R^C）他是RCVS。μT。 （R[T]S^）。(ii) 显然，RRCRSC。我们注意到RSC=μT。（R[T]RSC）（20）104P.B. Levy/Electronic Notes in Theoretical Computer Science 164（2006）85k，k为了显示RSCSCRSC，它通过简单的共归纳来显示RSCSCμT. （R[T]RSCSC）然后我们用T j把RHS放回原处。 SinceteLHSsμT。（RSC[T]<$R<$SCSC），根据Prop.3.7（i），它表明，RSC[TJRSCSC]RSCSCTJ（21）很明显，R_S_C_S_C_CRSC[TJ<$RSCSC]<$TJ这相当于说，RSC包含在如下定义的关系Q中。两个计算Δ ΣcM，MJ：B与Q相关，任意上下文态射J与TJ相关的ΔBARGORSCSC，计算rck<$M，kJ<$MJ：B与TJ相关，对于值也是如此Sinc e RSCisμT. （R[T]RSC），它可以通过将I/N映射到R[Q]RSCQR[Q]Q由下式给出：R[Q][TJ<$RSCSC]<$R[Q[TJ<$RSCSC]]<$R[TJ]<$R[TJ]<$R<$SCSC=TJ对于RSC Q，我们有这样的RSC[TJRSCSC]TJ。这是一个很好的机会RSC[TJRSCSC] =（RSCidf）[TJRSCSC]=RSC[TJRSCSC]RRSC[RSC[RSC=R<$SCSC<$TJ<$$>（R[TJ]<$R<$SCSC）=TJ<$（R[TJ]<$R<$SCSC）=TJ<$TJ=TJ(iii)RSC[RSC]RSC[RSCSC]RSCSC=RSCSC=RSCQ关系R在置换上下文下是闭的，当RSC≠ R时。通过Prop。 7.5、每一个这样的关系在语境下都是封闭的、相容的、互反的和替代的。