双相似性的名称和值调用的λμ演算实现

可在www.sciencedirect.com在线获取理论计算机科学电子笔记308（2014）49-64www.elsevier.com/locate/entcs按名调用和按值调用λμ-演算的Dariusz Biernacki1弗罗茨瓦夫大学计算机科学研究所弗罗克劳谢尔盖·朗格莱2洛里亚Universit'edeLorraineNancy，France摘要我们提出了第一个声音和完全的双相似性的调用的名称和调用的值无类型λμ演算，定义在应用风格。 我们给出等价的例子来说明我们的关系如何可以特别是，我们证明了David和Py关键词：语境对等，应用互模拟，连续，控制算子1介绍上下文等价[13]被认为是基于λ演算的语言中最自然的行为当在任何上下文中对两个术语进行评估时，如果外部对象服务器无法区分它们，则这两个术语是等效的（有漏洞的术语）。然而，对上下文的量化使得证明两个给定程序的等价性变得很麻烦。因此，人们寻求语境对等的其他表征，如共归纳定义的双相似性。已经提出了几种双相似性，例如，应用双相似性[1]，通过将项还原为值（如果可能）来关联项，然后通过将这些值应用于任意参数来比较这些值想法是1电子邮件：dabi@cs.uni.wroc.pl2电子邮件：serguei. univ-lorraine.frhttp://dx.doi.org/10.1016/j.entcs.2014.10.0041571-0661/© 2014 Elsevier B. V.保留所有权利。50D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）49对于环境双相似性[18]也是一样的，除了值是用从环境构建的参数来测试的，这代表了观察者关于测试项的知识。最后，范式双相似性[11]（最初称为开放双相似性[17]）将开放项减少为范式，然后比较它们的子项。应用和环境的双相似性仍然包含一些数量上的论点，通常与上下文等价一致。相比之下，范式双相似性更容易使用，因为它的定义不包含对参数的任何量化，但它通常是不完整的，即，存在不是标准形式双相似的等价项本文讨论了无类型λμ演算的行为理论[15]。λμ-演算提供了经典自然演绎的计算解释，从而将Curry-Howard对应从直觉逻辑扩展到经典逻辑。在操作上，演算的归约规则不仅表示函数应用，而且还表示对当前求值上下文的捕获因此，当考虑在无类型的设置，演算运算器提供了一种方法，以流产的控制运算符，如调用/cc已知的方案编程语言的语义，它可以被视为一个密切相关的替代Felleisen和Hieb到目前为止，还没有对按值调用或按名称调用λμ演算提出上下文等价的刻画Lassen定义了按名称调用弱头归约[10]、头归约[12]以及与Støvring一起定义的按值调用弱头归约[19]的规范形式双相似性，这些规范形式双相似性是不完整的。然而，对于头约简的Λμ-演算[5]和存储的λμ-演算[19]，在按值调用弱头约简下，范式双相似性是完全的Lassen还在[10]中定义了按名称调用弱头约简的不完全应用双相似性。应用性双相似性的定义也被提出用于按值调用类型的μPCF [14]，但由此产生的关系既不合理也不完整。在这项工作中，我们提出了λμ-演算的上下文等价的第一个特征，用于按名称调用和按值调用的弱头约简语义。我们定义的应用双相似性比Lassen的范式双相似性更难用来尽管我们定义的两个应用性双相似性是根据相同的原则建立的，但我们在按值调用中获得的关系然而，我们提供的反例表明，简化按值调用的情况，使其与按名称调用的情况相匹配，会导致不合理的定义。本文的结构如下。我们首先在第二节讨论了按名称调用（call-by-name，简称CBN）λμ演算的行为理论。我们提出了一个上下文等价的概念（在2.2节），它观察顶级名称，然后我们用应用性双相似性来描述它（2.3节）。特别是，我们比较我们的定义与拉森的工作，我们证明了大卫和Py的反例使用我们的关系。然后，我们将在D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）4951∅第3款.我们提出了一个应用性双相似性的定义（3.2节），它与上下文等价一致。我们还提供了反例，表明不能天真地将定义简单化以匹配按名称呼叫的定义。虽然我们得到的关系比按名称调用的关系更难使用，但我们仍然可以证明一些有趣的项的等价性，正如我们在第3.3节中所证明的那样。我们在第4节结束。随附的研究报告[3]包含了本文缺少的证据，并且还讨论了按名称呼叫的环境双相似性。2按名调用λμ-演算2.1语法和语义λμ-演算[15]扩展了λ-演算的命名项和μ构造函数，μ构造函数将名称绑定到项中。我们假设一组变量X，范围为x，y等，和一个不同的名称集合A，由a，b等组成。术语（T）和命名术语（U）由以下语法定义：条款：t：：= x| λx.t| TT|μ a.u命名术语：u：：=[a]t值（V），在v的范围内，是形式为λx.t的项。λ-抽象λx.t在t中约束x，μ-抽象μa.t在t中约束a。我们将项等同于它们的绑定变量和名称的α-转换，并且我们假设绑定名称是两两不同的，以及不同于自由名称。我们分别把t和u的自由变量集写成fv（t）和fv（u），把它们的自由名集写成fn（t）和fn（u）。一个项t或命名项u称为闭项，如果分别满足fv（t）=0或fv（u）= 0。请注意，封闭（命名）术语可能包含自由名称。封闭项、封闭值和命名项的集合分别为T0、V0和U0。在任何讨论或证明中，我们说一个变量或一个名字是新鲜的，如果它没有出现在所考虑的任何项中。我们区分了几种由外向内表示的上下文，如下所示：上下文：C：：= Q| C t| tC | λx。C | μa. C命名上下文：C：：= [a] CCBN评估上下文：E：：= Q|E t命名求值上下文：E：：=[a]E（命名的）求值上下文的语法反映了所选择的归约策略，这里是按名称调用。上下文只能用术语t填充，以产生常规术语C[t]，E[t]或命名术语C[t]，E[t];t的自由名称和自由变量可以在此过程中捕获52D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）49E⎧⎨⟨⟩/E([b]t)⟨/⟩=defEE我们写t0{t1/x}和u0{t1/x}，用于通常的避免捕获的变量项替换。我们定义了名称的命名上下文的避免捕获替换，写为tE/a和uE/a，如下所示。请注意，μ绑定情况下的边条件总是可以使用α转换来满足。xE/ad=efx（λx.t）ΔE/aΔd=efλx.tΔE/aΔ（t0t1）/a=t0/at1/a（μb.u）<$E/a<$d=efμb.u<$E/a<$ifb∈/fn（E）<${a}def[b]tE/a，如果a=b一E[t我们通过以下规则归纳地定义CBN约化关系→n（βn）[a]（λx.t0）t1→n[a]t0{t1/x}（μ）[a]μb.u→nu<$[a]Q/b<$（app）[a]t0t1→nu<$[a]Qt1/b<$if[b]t0→nuandb∈/fn（[a]t0t1）减少仅根据指定的术语定义。规则（βn）是通常的按名称调用β-归约。在规则（μ）中，当前的延续（由a表示）被捕获并替换为u中的b。在应用程序中（cf. rule（app）），我们通过引入表示顶层的新名称b来减少函数位置中的项t0。然后我们用[a]Qt1代替[b]t0约简的结果u中的b。我们也可以用顶层求值上下文来表示归约，如下所示。引理2.1u→NUJI<$u=E[（λx.t0）t1]且UJ=E[t0{t1/x}]，或u=E[μa.UJJ]且uJ= uJJ<$E/a<$.在以下意义上，减少也与评价环境相容。引理2.2如果u → nuJ，则u ∈ E/a ∈ → nuJ ∈ E/a ∈。对于→n的传递闭包和恢复闭包，我们将ite→nn定义为，并将演算的求值关系定义如下。定义2.3如果u→nuJ且uJ不能进一步减少，则W e r i t e u n u j。如果unuJ，则uJ是一个命名值。如果u允许一个无限约化序列，则我们可以是一个潜规则，writenun。例如，设Ωd=ef（λx.xx）（λx.xx）;则[a]Ω<$n对所有a。2.2语境对等与λ演算一样，λμ演算中的上下文等价也是根据收敛性来定义的。然而，与以前的定义不同[10，12]，我们首先在命名术语上定义上下文等价，然后将其扩展到任何术语。定义2.4两个闭项u0，u1是上下文等价的，记为u0<$cu1，如果对于所有闭上下文C和名称a，存在b，v0和v1使得C[μa.u0]<$n[b]v0 i <$C[μa.u1]<$n[b]v1。D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）4953注意，我们只能在上下文中插入项，因此我们用μ-抽象来前缀u0和u1定义2.4并不像它可能的那样通用，因为我们要求得到的命名值具有相同的顶级名称b;更一般的定义可以简单地说我们的定义比一般的定义严格，因为在某些情况下，上下文不能区分顶级名称，正如我们在下一个例子中看到的那样例2.5设Θd=ef（λx.λ y.y（x xy））（λx.λ y.y（x xy））是图灵的CBN固定点合并器，设v d = ef λx.λ y .x。 因此，当λx=f [ a ]时，μc = f [ a ]时，μc = f [ a]. [b]λ y。Θv和u1d=ef[b]λ y。Θv由定义2.4区分，如果b，但我们表明他们是与一般上下文等价相关。为此，我们证明E[μc.u0]<$ni <$E[μc.u1]<$n对所有E和c成立，然后我们可以得出u0和u1与David和Py的上下文引理[ 4 ]一般等价设E为[d]Et的形式，对于某个d，E，t。 则E [μa.u0]<$n[b] λy。Θv和E [μa.u1]<$n[b] λy。Θv，E [μb.u0]<$n [a] λx.μc. E [λy. Θv]和E [μb.u1]<$n[d] λy。Θv，并且最终对于c∈/{a，b}，E [μc.u0]<$nu0和E[μc.u1]<$nu1。 E=[d]Q的情形很容易证明。我们选择定义2.4，因为它比一般等价给出了更多关于项的行为的信息。此外，只有非常特殊的项u0和u1与一般等价有关，而与定义2.4无关。这些项就像黑洞一样：它们（在某些上下文C中）约化为值[a]v0和[b]v1，其中a/=b永远不会评估它们的参数。实际上，如果E = [c] Qt0. t n，则E [μa. [a] v0] →nE [v0E/a]，E [μa. [b]v1] n[b] v1E/a。假设在计算E[v0<$E/a<$]时，我们计算ti 然后，通过用Ω替换ti，我们获得上下文EJ，使得EJ [μa. [a] v0]n（因为Ω将被评估）和EJ [μa]。[b] v1]n，这与u0和u1一般等价的事实相矛盾（它们由EJ [μa. C]）。我们把定义2.4推广到任何闭项 t0，t1，说如果对任何新的a[a]t0<$c[a]t1 ，则t0<$ct1。扩展的其他版本也是可能的，例如将“for any a”替换为我们也可以使用开放扩展的概念来定义开放项上的上下文等价，它将封闭（命名）项上的任何关系扩展到开放（命名）项。如果σ用闭项替换了fv（t）（或fv（u））中的变量，则我们称替换σ闭合t（或u定义2.6设R是闭（命名）项上的关系两项t0和t1在R的邻延拓中，记为t0R <$t1，如果对于闭t0和t1的置换σ或所有置换σ，都有0σRt1σ（对于u0R<$u1也是如此）.2.3应用双相似性我们提出了一个应用互模拟的概念，它通过将它们应用于随机封闭参数来测试值。与上下文等价一样，我们在将其扩展到常规术语之前，给出命名术语的54D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）49定义2.7闭命名项上的关系R是应用互模拟，如果u0Ru1意味着• 若u0→NUJ0，则存在UJ1，满足u1→n≠UJ1和UJ0RUJ1;• 如果u0=[a]λx. t0，则存在t1su c h，使得u1→ <$n[a]λx. t1且对所有t，我们有[a]t0<$[a] Qt/a<${t/x} R[a] t1<$[a] Q t/a<${t/x};• 关于u1应用性互相似性（Applicativebissimilarity）是最大的应用性互模拟。对于正则项，如果对任意a∈/fn（t0，t1），[a]t0R[a]t1，则记为t0 Rt 1. 定义2.7的第一项对命名项进行互模拟游戏，没有命名的值。如果u0是一个命名值[a]λx.t0，则u1必须减少到一个命名的值[a]λx.t1，我们通过将它们应用到参数t来比较这些值。然而，上下文不能通过简单地将它们应用于t来与[a]λx.t0和[a]λx.t1交互，因为语法不允许（[a]λx.t0）t。因此，我们必须首先用μa来表示它们。 因此，我们考虑命名项[a]（μa. [a] λx.t0）t和[a]（μa. [a]λx.t1）t，它们分别约简为[a] （ λx.t0<$[a]Qt/a<$ ） t 和 [a] （ λx.t1<$[a]Qt/a<$ ） t ， 然 后 约 简 为[a]t0<$[a]Qt/a<${t/x}和[a]t1<$[a]Qt/a<${t/x};我们得到定义2.7的值的子句中的项。注2.8当考虑[a]（μa. [a] λx.t0）t和[a]（μa. [a]λx.t1）t，我们使用相同的顶级名称a作为命名值[a]λx.t0和[a]λx.t1之一。我们可以使用一个新的名字b来代替;重复使用相同的名字会使互模拟证明更容易（我们不必引入不必要的新名字）。我们也可以定义一个大的互模拟版本，在那里我们只考虑对一个值的评估。定义2.9闭命名项上的关系R是一个大步长应用双模拟，如果u0Ru1意味着• 若u0→n[a]λx. t0，则存在t1su c h，使得u1→ <$n[a]λx. t1且对所有t，我们有[a]t0<$[a] Qt/a<${t/x} R[a] t1<$[a] Q t/a<${t/x};• u1的对称条件。引理2.10如果R是一个大步长的应用互模拟，则R是一个大步长的应用互模拟。作为第一个属性，我们证明了减少（因此，评估）包括在双相似性。引理2.11我们有→n。是的。 通过显示{（u，uJ）|u→ <$nuj}<${（u，u）}是一个大步长的二进制化。Q我们给出一个基本的例子来说明如何应用互模拟例2.12对于所有闭v和a，b∈/fn（v）3，我们假设[a]v∈[n]，[a]λx.μb. [a]vbyswingthat{（[a]v，[a]λx.μb. [a]v）|b∈/fn（v）}函数是一个应用程序3 注意，如果a∈fn（v），结果仍然成立。D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）4955˜˜˜˜˜˜˜˜˜互模拟如果v = λx.t，则对于所有tJ，我们有[a] t{tJ/x}<$[a] μb。[a] v tJ，b是因为[a]μb。[a]vtJ→n[a]t{tJ/x}（和by引理2.11）。2.4可靠性和完备性现在我们证明了，与c重合。我们首先使用Howe的方法[8，7]证明一个应用双相似是一个同余，Howe的方法与[10]一样，我们需要稍微修改λμ演算的证明。在这里我们只简述了该方法的应用，所有细节可以在[3，附录A.1]中找到该方法的原理是证明一个关系称为Howe豪闭包的定义xRxt0Rt1λx。t0R<$λx.t1t0Rt1tJ0RtJ1t0tJ0Rt1tJ1u0Ru1μa.u0Rμa.u1t0R t1[a]t0R[a]t1QRQt0Rt1E0RE1t0E0/a Rt1E1/aE0R E1t0Rt1E0t0RE1t1u0Ru1E0RE1u0E0/a Ru1E1/aE0RE1[a]E0R[a]E1在相容精化的原始定义中，如果两个项具有相同的外部语言构造函数，则它们通过R由R.在λμ-演算中，相容精化被扩展到（命名的）求值上下文，并且我们允许用相关的命名上下文替换名称给定两个关系式R1和R2，我们将它们的合成记为R1R2t0R1R2t2成立，如果存在t1使得t0R1t1和t1R2t2.我们现在可以定义豪定义2.13豪≈◦⊆ ≈·≈· ≈◦⊆ ≈·≈˜·⊆ ≈·Howe闭包是在开放（命名）项和（命名）评价上下文上定义的。因为它包含相容的修饰，所以它是一个同余。为了证明它是一个互模拟，我们需要一个更强的结果，称为伪模拟引理，在这里我们不是用相同的参数来测试指定的值，而是用由π·相关的参数tJ0，tJ1来测试。引理2.14设（·）c·仅限于闭项，且设u0（·）cu1。• 如果u0→nuj0，则theNu1→nuj1，UJ0（n·）cuj1.56D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）49• 如果u0=[a]λx. t0，thenu1→n[a]λx.t1和f或a l ltJ0（·）ctJ1，我们有[a] t0<$[a]Qt'0/a<${tJ0/x}（·）c[a] t1<$[a]Qt1'/a<${tJ1/x}。有了这个结果，我们可以证明（ε·）c是互模拟，因此包含在ε中。因为它也包含了by定义，所以我们有=（·）c，这意味着是一个同余。因此，他的声音w.r.t.到了2000年。定理2.15为了简化完备性的证明（反向包含），我们考虑上下文等价的另一种定义，其中我们仅使用命名的评估上下文来测试术语。通过这样做，我们证明了一个上下文引理的过程中。4.定义2.16设u0，u1为闭项。我们写u0cu1，如果对于所有闭上下文E和名字a，存在b，v0，v1，使得E[μa.u0]<$n [b]v0 iE[μa.u1]n[b]v1..定理2.17.第一个包含是通过定义，第二个包含是通过证明，一个大步骤的应用互模拟。2.5与Lassen工作的比较在[10]中，拉森还提出了应用双相似性的定义，他证明了声音，但他承认这是不完整的。我们在这里讨论这两种方法之间的差异。拉森定义了一个互模拟的概念，只适用于正则项，而不适用于命名项。定义如下。定义2.18闭项上的关系R是拉森应用互模拟，如果t0Rt1意味着：• 对所有的a，i f [a]t0→nn[b]λx. TJ0，t当存在TJ1，使得[a]t1→ <$n[b]λx. tJ1，且对于所有t，我们有vetJ0<$[b]Qt/b<${t/x}Rt1J<$[b]Qt/b<${t/x};•t1上的对称条件。拉森这比我们的定义更具限制性，在我们的定义中，我们只将这些项与顶级名称b进行比较（或者，如注释2.8中所讨论的，我们可以对某个新名称c进行比较-[c]t0[c]Qt/b{t/x}和[c]t1[c]Qt/b{t/x}）。为了说明这种差异，我们考虑[ 10 ]中拉森例2.19设t0d=ef（λx.λ y.xx）（λx.λ y.xx），t1d=efμa. [a]λ y.μc. [a]t0（与c a）。根据拉森的定义，这些术语不是双相似的。对于所有b，我们4我们不能直接使用David和PyD. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）4957⇓∈⇓h ave[b]t0→n[b]λ y。t0和[b]t1→n[b]λ y.μc. [b]t0. 根据Lassen的定义，必须将t0和μc联系起来。[b] t0t对于任何t，这意味着比较[d] t0和[d] μc。[b]t0t for所有D。 但这两项不等价，如果d b。Lassen在[ 10 ]中证明这些项在上下文上是等价的，我们确实可以证明它们与我们的定义是（大步）双相似的：我们只需要比较[b] t0和[b] μaJ。[b] t0t（或[c] t0和[c] μaJ）。[c]t0t for some freshc）for anyt，两项的值都是[b]λx.t0（或[c]λx.t0），因此是等价的。正如我们在定义中所做的那样，通过比较主要命名的术语，我们可以跟踪顶层发生了什么，特别是顶层和子术语之间的任何联系 在例2.19中，我们可以看到，必须记住b代表μc中的最高水平。[b]t0t，因此没有意义比较[d] t0和[d] μc。[b]t0t对于任何d b，正如我们必须与拉森的定义有关我们认为，比较命名的条款是必不可少的，以获得完整的w.r.t.上下文等价;注意λμp演算[19]的声音和完全范式双相似性也是在命名项上定义2.6大卫和派在[4]中，David和Pygi给出了一个反例，说明了在CBN λμ -演算中Bohm定理是不成立的他们证明，他们的条款是上下文等价的使用上下文引理。在这里，我们稍微简化了他们的反例，并使用应用双相似性证明等价性。注意，这些项不能被证明与渴望范式双相似性（的CBN变体）等价[10，19]。例2.20设0d=efλx.λ y. y， 1d=efλx.λ y.x，ndtad=efμc. [a]0。然后我们就λx.μa. [a] x μb。[a] x t a0 <$λx.μa. [a] x μb。[a]x ta15.证据[概要]这里我们只给出主要思想，完整的等价性证明可以在[3，附录A.2]中找到第一，λx.μa. [a] x μb。[a] xta0与λx.μa不是正规型双相似的。[a] x μb。[a]xta 1，因为这两项的子项不是标准形式双相似的（0不等于1）。为了证明应用双相似性，设c是一个新名字，t是一个闭项。 我们想关联[c] μa。[a] tμb。[a] tt a0和[c] μa。[a] tμb。[a] tt a1，分别约为[c] tμb。[c] t t c0（1）和[c]tμb。[c]t tc 1（2）。设d/fn（t）;我们根据[d]t的行为区分几种情况。有趣的情况是，当[d] t n[d] λy.tJ;则μb。[c] t t c0或μb。[c]t tc 1分别在（1）和（2）中作为参数传递给λy.tJ如果tJ执行其参数（即，如果tJ对于某个E简化为E[y]），则（1）简化为[c]t tc 0（3），（2）简化为[c]t tc 1（4）。但是我们知道[d]tn[d]λy.tJ，并且tJ执行它的参数，所以当计算（3）和（4）时，tc将被减少，因此（3）和（4）将计算为[c]0。在其他情况下（例如，[d]t<$n[e]λy.tJ，其中e d），最终（1）和（2）中的任一个到达类似于上面执行tc的情况的点，或者它们发散。[5] David和Py在他们的工作中考虑的项是λx.μa。[a] xμb。[a]（xta0）ta和λx.μa. [a] xμb。[a]（xta 1）ta.然而，附加的论点ta在我们给出的证明中不会起作用，所以我们省略了它。58D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）49在所有情况下，它们都是适用性双相似的。Q3按值调用λμ演算3.1语义与语境对等在本节中，我们使用CBV从左到右求值，它在CBV求值上下文的语法中编码：E：：= Q|E t|v ECBV归约关系→v由以下规则定义（βv）[a]（λx.t）v→v[a]t{v/x}（μ）[a]μb.u→vu<$[a]Q/b<$（app）[a]t0t1→vu<$[a]Qt1/b<$if[b]t0→vuandb∈/fn（[a]t0t1）（appv）[a]v t→vu<$[a]vQ/b<$如果[b]t→vu且b∈/fn（[a]vt）使用规则（appv），我们将参数归约为值，以便能够应用CBVβ-归约（规则（βv））。规则（μ）和（app）不变。我们也可以用顶层命名的求值上下文来表示归约，如引理2.1所示。此外，CBV约简与CBV约束文本兼容，如在引理2.2中。Wewrie→v表示→v的自反和传递闭包，W e r i e → v表示CBV求值，W er i e → v表示CBV发散。我们使用与CBN中相同的上下文对等定义。定义3.1设u0，u1是闭的命名项。我们写u0<$cu1，如果对于所有闭上下文C和名称a，存在b，v0和v1，使得C[μa.u0]<$v[b]v0 i <$C[μa.u1]<$v[b]v1。然而，与CBN不同的是，这个定义（我们要求结果值具有相同的顶级名称）与我 们 简 单 地 说 “C [ μa.u 0 ] v i C [ μa.u 1 ] v” 的 一 般 定 义 一 致 事 实 上 ， 如 果C[μa.u0]<$v[b]v0和C[μa.u1]<$v[c]v1，与cb，那么我们可以很容易地区分它们，因为[b]μb。C[μa. u0]Ω→Ωv[a] v0<$[b] Q Ω/b<$Ω<$v，和[b] μb。C [μa.u1]Ω <$v [c] v1<$[b] Q Ω/b<$。我们将cbc推广到任何封闭项，如CBN中。与CBN相比，CBV中开放扩展的定义略有变化：我们通过仅用封闭值替换其变量来封闭开放项，而不是任何封闭项。3.2应用双相似性在给出它的完整定义之前，我们解释了应用双相似性矩阵应该如何比较两个命名值[a]λx.t0和[a]λx.t1。下面的推理解释并证明了定义3.4中的条款。特别是，我们提供了反例来表明我们不能简化这个定义。D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）4959在CBVλ-演算中（也有带分隔的控制[2]），通过将值应用于任意值参数来测试值。遵循这个原则，很自然地提出了CBVλμ-演算的以下子句[a]对于所有v，我们有[a]t0<$[a]Qv/a<${v/x}<$[a]t1<$[a]Qv/a<${v/x}。与定义2.7一样，我们实际上比较[a]（μa）。[a] λx.t0）v与[a]（μa. [a]λx.t1）v，其简化为第（1）条中的项。 然而，这样的子句会产生一个不合理的应用性双相似性;它会涉及上下文不等价的术语，就像下一个例子中的术语一样例3.2设v0d=efλx.μb. [a]wx，v1d=efλx.wxx，withwd=efλ y.λ z.zy. 该方法具有（[a]v0）λ[a]Qv/aλ=[a]（λx.μb. [a]w xv）v→<$v[a]w vv和（[a]v1）<$[a]Qv/a<$=[a]（λx.wxx）v→<$v[a]w vv。因为它们归约为相同的项，所以（[a]v0）<$[a]Qv/a<$在上下文上等价于（[a]v1）<$[a]Qv/a<$，并且使用子句（1）会导致我们得出结论，[a]v0和[a]v1也是等价的。然而，[a]v0和[a]v1可以用td=ef来区分μd。[d] λy.μc.[d]wJ，其中wJd=efλx.μc. [d]xwJJ和wJJd=efλx.λy.λz. Ω。事实上，我们可以检查，（[a]v0）<$[a]Qt/a<$→ <$vλ z。Ωand（[a]v1）<$[a]Qt/a<$→v<$Ω。 这种差异来自于这样一个事实，即在（[a] v1）[a] Qt/a中，t被减少到一个值一次，在这个过程中捕获[a] v1Q，而t被减少到（[a] v0）[a] Qt/a中的一个值两次，每次它捕获不同的上下文。[a] v0和[a] v1由上下文[a]（μa）区分。Q）t，因此它们在上下文上不等价。例3.2表明我们应该用形式为[ a ] Qt而不是[ a] Qv的上下文来比较[a] λx.t0和[a]λx.t1。因此，我们应该比较u0d=ef[a]（λx. t0<$[a]Qt/a<$）t其中u1d=ef[a]（λx. t1[a]Qt/a）t. 不过，我们可以限制一下测试项t的选择，基于它的优点。设b∈/fn（t）;如果[b]tdi-当u> 0时，u0和u1也发散，并且我们得不到关于[a] λx，t0和[a]λx的信息。把自己的想法说出来。如果[b]t→v[c]v，其中b/=c，则thenu0→v[c]v<$[a]λx.t0<$[a]Qt/a<$Q/b<$，u1也是如此。值[a] λx.t0和[a] λx.t1被[b] t捕获，在这个过程中t和两个指定值之间没有相互作用（[a] λx.t0和[a] λx.t1不适用于任何值）;同样，我们没有获得关于[a]λx的任何新的知识。t0和[a]λx.t1。最后，如果[b]t→v[b]v，则u0→λv[b]（λx. t0<$[a]Qt/a <$）v<$[a]λx.t0<$[a]Qt/a<$Q/b<$，与u1类似;inthis在这种情况下，一个值确实被传递给[a]λx.t0和[a]λx.t1，我们可以比较它们各自的行为。因此，在t和测试的v之间发生相互作用i[b]t→v[b]v，并且相互作用的结果（在β-约化之后）是下面的子句中的两项[b]F或所有t，b，v都满足[b]t→n[b]v且b∈/fn（t），weve[a]t0<$[a]Qt/a<${v<$[a]λx.t0<$[a]Qt/a<$Q/b<$/x}<$[a]t1<$[a]Qt/a<${v<$[a]λx.t1<$[a]Qt/a<$Q/b<$/x}。不幸的是，第（2）条不足以获得声音双相似性。下一个例子表明需要一个额外的子句60D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）49例3.3设v0d=efλx.μb. [a]（λ y.λ z. wy）x和v1d=efw其中wd=efλx. wJ（xλy. y），且wJd=efλy.yλ z. Ω。 我们首先证明[a]v0和[a]v1通过子句（2）是相关的。设t满足[b]t∈v[b]v，其中b∈/fn（t）。然后wehave（[a]v0）<$[a]Qt/a<$→<$v[a]wJ（v<$[a]v0<$[a]Qt/a<$Q/b<$λx.x）and（[a]v1）<$[a]Qt/a<$→ <$v[a]wJ（v<$[a]v1Q/b<$λx.x）.We可以通过证明关系{（u<$[a]E[v0<$[a]E[Qt]/a<$Q]/b<$，u<$[a]E[v1Q]/b<$），证明两个结果项在上下文上是等价的。|[b]t<$v[b]v，b∈/fn（t）}是根据定义3.4并通过使用定理3.9（参见[3，附录B.1]）的应用互模拟。因为（[a]v0）<$[a]Qt/a<$和（[a]v1）<$[a]Qt/a<$在上下文上是等价的，所以仅使用子句（2）将导致我们得出结论，[a]v0和[a]v1也是等价的。然而，这两个命名的值可以用上下文[a]（λx.xx）μa来区分。Q，因为在一种情况下，有ve（[a]v0）<$[a]（λx.xx）Q/a<$→ <$vλ z。Ω，在另一个（[a]v1）<$[a]（λx.xx）Q/a<$→<$v Ω。 如例3.2所示，当评估（[a]v0）<$[a]（λx.x x）Q/a<$，v0的主体被评估两次，每次捕获两个不同的上下文。相比之下，v1不包含任何控制对象，所以当它的主体被求值两次时，我们得到的结果是一样的例3.3表明，我们必须比较两个值[a]λx.t0和[a]λx.t1，同时用形式为[a]vQ的上下文测试它们，即， 考虑[a] v λx.t0<$[a] vQ/a<$和[a] v λx.t1<$[a] vQ/a<$。如果v =λx.t ， 则 这 些 项 在 一 个 β 约 化 步 骤 中 约 化 为 [a] t{λx.t0<$[a] v Q/a<$/x} 和 [a]t{λx.t1<$[a] v Q/a<$/x}。考虑到这一点和第（2）条，我们得到以下适用互模拟的定义。定义3.4闭命名项上的关系R是应用互模拟，如果u0Ru1意味着• 如果u0→VUJ0，则存在UJ1，such，使得u1→v∈UJ1，UJ0RUJ1;• 若u0=[a]λx.t0，则存在t1su c h，使得u1→uv[a]λx. t1，and：(i) 对于所有的t，b，v，使得[b]t→n[b]v和b∈/fn（t），wehave[a]t0<$[a]Qt/a<${ v<$[a]λx.t0<$[a]Qt/a<$Q/b<$/x}R[a]t1<$[a]Qt/a<${v<$[a]λx.t1<$[a]Qt/a<$Q/b<$/x};(ii) 对于所有v=λx.t，我们有[a]t{λx.t0<$[a]vQ/a<$/x} R[a]t{λx.t1<$[a]vQ/a<$/x};• 关于u1应用性互相似性（Applicativebissimilarity）是最大的应用性互模拟。通过使用新的顶级名称a，该定义扩展到CBN中的常规术语t0，t1。注意，子句（ii）暗示互模拟R是同余w.r.t.（正则）值;事实上，如果v0Rv1，则[a]v0R[a]v1对于一个新的a，所以我们有[a]t{v0/x}R[a]t{v1/x}对于所有的t（根据子句（ii））。这一性质简化了Howe方法的同余证明与CBN一样，我们可以定义一个大的互模拟版本（我们使用评估而不是约D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）4961简），并且互相似性包含约简。62D. Biernacki，S.Lenglet/Electronic Notes in Theoretical Computer Science 308（2014）49关于我们引理3.5我们有→v。CBV的应用互模拟比CBN的应用互模拟更难使用，我们可以通过再次考虑例2.12中的项来看到。例3.6设v=λx.t，a，b∈/fn（v），则[a]v<$[a]λx.μb。[a]v.To对 于 子 句 （ i ） ， 我 们 考 虑 tJb 使 得 对于b ∈ / fn（t j）， [b]tJ→v[b]vJ; 我们必 须 将[a]t{vJv[a]vQ/bv/x}与[a]μb进行比较。[a]vtJ.But[a]μb。[a]vtJ→v[a]vtJ→<$v[a]t{vJ<$[a]vQ/b<$/x}，因此我们可以得出引理3.5。对于子句（ii），我们必须将[a] tJv/y和[a] tJλx.μb联系起来。[a] vJv/y为所有vJ=λy.tJ.我们继续对tJ进行案例分析;最有趣的案例是tJ=E[yvJJ]。在这种情况下，weh ave[a]tJ{λx.μb. [a]vJv/y}→v[a]vJv→v[a]tJ{v/y}，因此我们可以由引理3.5得出结论。为了处理所有可能的情况，我们在[3，Ap penvelopeB.1]中证明了{（u{v/y}，u{λx.μb. [a]t0/y}）|[a]t0→αv u{v/y}}互模拟是一种应用互模拟。在下一个例子中，我们给出了两个可以证明与应用双相似性等价但与渴望范式双相似性不等价的项[19]。例3.7设u0d=ef[b]λx y。Ω，vd=efλ y.μa. [b]λx。y，andu1d=ef[b] λxy。Θvvy，其中Θvd=ef（λxy.y（λz.xxyz））（λxy.y（λz.xxyz））是图灵调用如果u0和u1是正规形双相似的，我们需要[c]Ω与[c]Θ vvy相关，但[c]Θ vvy与[b