高阶函数语义的重要方面和环境互模拟的复杂条件

可在www.sciencedirect.com在线获取理论计算机科学电子笔记276（2011）215-235www.elsevier.com/locate/entcs从应用到环境互模拟1Vasileios Koutavas Vasileios Koutavas2，5爱尔兰都柏林三一学院Paul Blain Levy保罗·布莱恩·利维3，6英国伯明翰大学角井英次郎4日本东北大学摘要我们通过一系列的例子阐明了高阶函数语义的重要方面，这些函数在局部状态、异常、名称和类型抽象的存在下是常见的，这些例子增加了斯塔克最重要的是，我们表明，任何这些语言功能引起的现象，某些行为的高阶函数只能通过提供给他们的参数，内部调用的功能再次观察。其他的例子显示了观察者需要累积从程序接收到的值并生成新的名称。这为在环境互模拟的定义中函数的复杂条件的必要性提供了证据，环境互模拟在这些方面都偏离了应用互模拟。关键词：环境互模拟，应用互模拟，局部状态，存在类型。1介绍应用互模拟[1]提供了一种关系语义，它优雅地编码了高阶函数的可拓性。它已被证明是健全的和完整的相对于上下文等价的纯lambda演算[1，8]，对象1初步报告见《达格斯图尔研讨会论文集》10351 [13]。2电子邮件：Vasileios. scss.tcd.ie3电子邮件：P.B. cs.bham.ac.uk4电子邮件：sumii@ecei.tohoku.ac.jp[5]由SFI项目SFI 06 IN.1 1898支持6由EPSRC高级研究金EP/E056091/1支助。1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.09.023216诉Koutavas等人/理论计算机科学电子笔记276（2011）215微积分[7]和具有I/O的语言[33]。然而，最近几种具有高阶函数的语言（有状态和纯）的互模拟语义是基于环境互模拟[31，32，27，15，5，14，16]，这是一种具有明显更复杂条件的定义。尽管它适用于许多高阶语言，环境互模拟的额外复杂性还没有得到充分的证明。我们在这篇论文中提出的问题（我们在论文中回答）是这种复杂性是否是必要的。应用互模拟和环境互模拟都通过将相关函数应用于参数来测试相关函数，并要求两个应用程序等价终止并给出相关结果。然而，环境互模拟有两种偏离应用互模拟的方式，每一种方式都在它可以进行的测试中给予上下文• 值的累积：在应用互模拟中，上下文可能只调用它刚刚从相关程序接收到的相关函数在环境互模拟中，它积累了它收到的函数，因此它可以随时调用它们，可能是多次。• 资源型参数：在应用互模拟中，上下文提供一个单独的封闭值，相关函数将被应用于但在环境双模拟中，它提供了一个单独的开放值，由库存中的相应函数关闭，因此相关函数适用于不同的参数。在有状态的语言（或有名称的语言）中，第一个devi- ation的必要性是相当合理的。累积是必要的，因为函数在第二次应用时可能返回不同的值。但足智多谋的论点的必要性似乎更值得怀疑。在一个有异常和多态的语言中更是如此。Mason和Talcott [22]在他们对具有一般存储的语言的关系理论的研究中提出了一个相关的他们给出了一个不等价的例子，表明对手需要在每个功能应用之前分配到全球位置[22，Sec.3]。因此，他们认为有必要将应用互模拟的定义扩展到有效语言：“[Applicative] bisimulation provides an alternative approach to equivalence anddeserves互模拟关系的定义假设外延是一致的。由于记忆效应的存在使这一点不再成立，因此需要对基本定义进行一些修改，以便将Abramsky和Howe的方法扩展到本文中提出的计算语言。我们计划研究这种方法。在本文中，我们研究了两个版本的环境互模拟，一个没有积累，一个没有足智多谋的参数。我们强调互模拟，而不需要足智多谋的论点，因为它更微妙。我们的例子表明，这些互模拟是不健全的语言，使用状态，异常，名称和多态性的数组。通过这种方式，我们确定了所有这些语言中高阶函数行为的共同点，诉Koutavas等人/理论计算机科学电子笔记276（2011）215217证明环境互模拟定义的复杂性。我们相信，我们关于异常和多态性的例子是文献中第一个使这些语言中有缺陷的互模拟无效的例子。然而，我们关于国家和名称的例子并不是同类中的第一个;斯塔克给出了体现相同原则的例子。24此外，在本文中，我们研究了环境互模拟定义中的规定，即在互模拟的每一步都创建新的名称，而不是在开始时只生成任意数量的名称。对于确定性语言，我们认为这是不必要的。然而，在非决定论的我们给出了新的例子，表明这种规定的必要性，环境互模拟是健全的必须测试，在可数非决定论的存在下，并在较低的双相似性，在存在甚至有限的非决定论。我们相信，在每一步的名称生成是不必要的可能测试，并在有限的非确定性的存在，必须测试。我们从研究一种纯语言开始（第二节）。2），为此，我们定义了应用和环境互模拟。然后，我们研究一种具有一般状态的语言（第二节）。3）。在这种情况下，我们定义了环境互模拟的两个有缺陷的版本，并提出了简单的例子，表明它们在上下文等价方面的不合理性然后，我们提出了类似的例子，一个语言的例外（第二节）。4.1），names（Sec. 4.2）和存在类型（第二节）。4.3）。最后，我们给出了一些例子，展示了在上述情况下固定名称集互模拟的不合理性（第二节）。5）。2纯语言2.1语言λ为了理解在引言中讨论的应用互模拟的两个偏差，我们首先回顾了纯环境中的应用和环境互模拟。我们选择了一个带有递归的按值调用λ-演算，我们称之为λ，它将作为我们在本文后面研究的语言的基础。λ的类型由下式给出：A，B，C：：=0 |A + A|1 |A×A|A→A |X|recX.一我们使用“细粒度按值调用”的语法V：：= x|输入V|INRV| ⟨⟩ |V，V|λx.M|反射率fλx.M|foldVM：：= returnV|M到X。M| VV|将V匹配为{}| 将V匹配为{inlx. M，INRx。M}|将V匹配为。 M| 将V匹配为x，y，M|匹配V作为折叠x。 M218诉Koutavas等人/理论计算机科学电子笔记276（2011）215defdefdefdef=►∈我们有类型判断，其中，对于值，我们有类型判断，其中， 不同的封闭类型标识符的列表，A是一个封闭类型，定义在通常的感应器我们写Γv −→V：−→A表示Γv Vi：Ai，对于所有i<|−→A|.我们将bool = 1 + 1与true和false进行相应的定义，将diverge =（rec fλx。fx）把M写成x。 N作为M; N当x不出现在N中时。然后，我们像往常一样定义M BV，因为M：B和M V：B。2.2终极模式匹配值得注意的是，任何闭合值都由标记和函数组成。标签构成了一个最终的模式[18]，函数构成了模式的填充。例如，我们将价值inlλx.M，inr最后的模式是inl−，inrinl−，和填充λx.M，λy.N。为了使这一点更精确，我们为每个类型A定义一个最终模式p的集合ulpatt（A），每个模式都配备了一个函数类型列表H（p）。这些集合被定义为通过归纳：• −A→B∈ulpatt（A→B）和H（−A→B）=A→B• ε ∈ulpatt（1）且H（ε）=ε• 若p∈ulpatt（A）ANDNDPJ∈ulpatt（AJ）tehen<$p，pj<$∈ulpatt（A×AJ）andndH（pj<$p，PJ<$）d=efH（p）·H（PJ）• 如果p∈ulpatt（A）t∈n，则p∈ulpatt（A+AJ）且ndH（inlp）d=efH（p）• 若p∈ulpatt（AJ）t∈ninrp∈ulpatt（A+AJ）anddH（inrp）d=efH（p）• 若p∈ulpatt（A [rec X. A/X]）则foldp∈ulpatt（rec X. A）和H（foldp）H（p）。defGivenp∈ulpatt（A），和值列表Γv−→V：H（p），我们定义一个值Γvp[−→V]：A以明显的方式。独特的分解是即时的：定理2.1对于任意闭值vV：A，存在唯一的pulpatt（A）和唯一的d个值列表<$v −W→：H（p）使得V=p[−W→]。2.3应用互模拟我们现在定义我们的应用互模拟。为了方便以后对这个定义的扩展，我们可以把它作为一组元组，我们称之为相关元组。一个亲戚是一个由f组成的元组（−A−→−−→B;−→V;−V→J）• 函数types−A−→−→B的列表• 函数列表v−→V：−A−→−−→B• f函数列表v −V→J：−A−→−−→B。诉Koutavas等人/理论计算机科学电子笔记276（2011）215219R−→−→−→R相关者的这三个区域代表了文本中已知的公共信息（对于这种语言，这只是一个类型列表）和两种情况，−→V和-V→J，我们不能联系。应用互模拟的条件是，当我们将相应的函数应用于同一个闭值时，应用是等价终止的，并且结果值具有相同的最终模式，具有双相似填充。定义2.2一组 亲属 是当（−A−→−→B;−→V;−V→J）∈R时的应用互模拟意味着对于ny，• 索引i <|−A−→−−→B|• 和闭合值ΔVU：Ai，v−→如果ViU<$Bip[−W→]，则存在填充函数WJ：H（p）suc h，ViJU<$Bip[−W→J]andnd （H（p）;−W→;−W→J）∈R当ViJU≠Bip[−W→J]时，a b o v e条件的逆成立。定义2.3当存在应用互模拟R使得• 若M<$Ap[−W→]，则存在MJ<$Ap[−W→J]且d（H（p）;W;WJ）包含在R中，• 当MJ<$Ap[−W→J]时，a b o v e条件的逆成立。正 如 我 们 在 引 言 中 所 讨 论 的 ， 定 义 式 2.2 是 非 累 加 的 ： 最 终 关 系 式 （ H（p）;−W→;−W→J）d不包含起始关系式（−A−→−→B;−→V;−V→J）中的函数。更重要的是，这个定义是不合理的，因为它适用于将函数转换为相同的封闭参数。2.4环境互模拟我们定义了纯语言λ的环境互模拟，以说明它与应用互模拟的区别。在接下来的部分中，我们将把这个定义应用于一种有状态的语言定义2.4当（−A−→−−→B;−→V;VJ）∈R时，一组相关者是环境互模拟，这意味着对于一个ny• 索引i <|−A−→−−→B|• andopenv aluef−−：−A−−→−−→BvU：Ai，v−→如果ViU[−V−/→f]<$Bip[−W→]，则存在填充函数WJ：H（p）suc h，ViJU[−V−J/→f]<$Bip[−W→J]annd （−A−→−−→B·H（p）;−→V·W−→;−V→J·−W→J）∈R220诉Koutavas等人/理论计算机科学电子笔记276（2011）215−→−→−→−→当ViJU[V−−J/→f]<$Bip[−W→J]时，a b o v e条件的逆成立。定义2.5当存在环境互模拟R使得• 若M<$Ap[−W→]，则存在MJ<$Ap[−W→J]且d（H（p）;W;WJ）包含在R中，• 当MJ<$Ap[−W→J]时，a b o v e条件的逆成立。与应用互模拟一样，环境互模拟的条件要求函数Vi和ViJ的应用，在原始的relatee中相关，等终止，并且它们的结果值具有与双相似填充然而，在环境互模拟中，提供给Vi和ViJ的each的辐角是通过分别用来自原始源的库存的函数V和VJ闭合相同的openv值−f−：−A−→−→BvU：Ai来构造的。亲戚这就是足智多谋的论证原则。此外，还证明了typ是−A−→−−→B·H（p）与最终值−→V·−W→和V−→J·−W→J的连接relatee对值的累积进行编码。3状态的环境互模拟我们给出了一种有状态的语言和这种语言的环境互模拟的定义然后，我们给出了两个更简单的版本的互模拟，一个没有足智多谋的参数，一个没有积累，并证明他们的不健全的上下文对等。3.1语言λs我们在语言λ中添加了生成新位置的功能，这些位置可以被分配和读取。而不是将位置视为值（如第二节中的名称）。4.2），我们使用语法M：：= ·· ·|l：=V. M|把l读作x。 M|新l−−：−=−→V 。M因此，位置既不能存储也不能返回。 类型判断现在是Δ;ΓM：A和Δ;ΓvV：A，其中Δ是不同的封闭类型的列表，地点对于一个状态s，我们写Δ; Γ v s：Δ j表示dom（s）= dom（Δ j）和Δ; Γ v s（i）：Δ j（i）。评估采用Δ，s，M<$A Θ，t，V的形式，Δ;ΔM：A，状态Δ;ΔS：Δ，位置列表Θ，扩展Δ，值Θ;ΔV：A，以及状态Θ;θt：Θ。−−−−→术语new l：= V的操作语义。 M使用gensym操作以生成新的位置，我们称之为私有的，因为该术语的上下文无法直接访问它们。gensym操作的特定选择使得语义不被考虑。 因此，在不失一般性的情况下，我们假设， 是一个可数无限的位置集，与原义范围不相交。 我们将这些位置称为公共位置，并在下面的部分中将其用作域诉Koutavas等人/理论计算机科学电子笔记276（2011）215221øø）=的∈∈−→►∈我们关系中的公共状态;即语境直接进入的状态。3.2状态的环境互模拟我们将位置上下文写为Δpub Δpriv，其中Δpub是公共位置上下文，Δpriv是私有位置上下文，域分别是公共和私有位置的集合。 同样地，我们将状态写为spubspriv，我们称spub为公共状态，spriv为私有状态。请注意，每个状态都可以唯一地分解为公共状态和私有当上下文调用函数时，除了参数和结果之外，公共状态还提供函数与其上下文之间的额外通信。 它本质上是函数的另一个参数，当函数返回时，它是另一个最终需要模式匹配的结果。 注意，这不是私有状态的情况，因为上下文不能访问它。因此，对于公共位置上下文Δpub，我们写乌尔帕特（Δ酒吧def（l：C）∈Δpubl›→ulpatt（C）对于pulpatt（Δpub），我们定义H（p）为H（p（l））在（l：C）Δ pub上的级联。然后，对于nyΔ;Γv−W→：H（p），我们定义Δ;Γvp[−W→]：Δpub，明显的方式。作为示例，设l1和l2是公共位置，Δpubd=efl1：bool×bool，l2：1+（bool→bool）则公共状态Δ pub; λv l1›→ λ vtrue，falseλ v，l2›→ inr λx。把l1读作ny，zn。 returny：Δ pub有最终模式pd=efl1→ftrue，ffalse，l1<$→inr−。再次，我们有独特的分解：定理3.1(i) F或任何值Δ;vV：A，re是唯一的p∈ulpatt（A）且Δ;v−W→：H（p）故V = p [W]。(ii) 对于任何公共状态Δ;vspub：Δpub，存在唯一的pulpatt（Δpub），Δ;v −W→：H（p）使得spub=p[−W→]。λs的环境互模拟定义在关系元上，关系元是形式为（Δpub，−A−→−→B;Δpriv，spriv，−→V;ΔJpriv，sJpriv，V−→J）的元组，由以下组成：• 公共位置上下文Δpub• 函数types−A−→−→B的列表• 私有位置上下文Δpriv222诉Koutavas等人/理论计算机科学电子笔记276（2011）215• f函数列表ΔJv−→J−→Δ;ΔV：A→B。pubprivøøøøø ø øøø和• a private state ΔpubΔpriv;pubspriv：Δpriv• 函数列表ΔpubΔpriv;Δv−→V：−A−→−−→B• 私有位置上下文ΔJpriv• a private state Δpub ΔJpriv;vsJpriv：ΔJpriv在应用性设置中，相关者被组织在三个区域中（由分隔符分隔），代表公共信息和我们想要关联的两种情况。在这里，公共信息除了函数的类型之外，还包含公共状态的类型。其他两个区域包含可以在函数中使用λs的环境互模拟的定义遵循与λ（定义2.4）相同的结构，只是在应用程序之前添加了一个公共状态的创建，最终在最后进行模式匹配定义3.2当（Δpub，−A−→−→B;Δpriv，spriv，−→V;ΔJpriv，sJpriv，V−→J）∈R时，一个相关者集合R是一个环境互模拟意味着对于任何• 索引i <|−A−→−−→B|• 公共位置上下文Θpub扩展Δpub• publicstate<$pub;f−−：−A−−→−−→B公共状态：<$pub• 和v值Θpub;−f−：−A−−→−−→B<$vU：Ai，如果ΘpubΔpriv，spub[−V−/→f]spriv，ViU[V−/→f]<$Biθpubθpriv，q[−→T]tpriv，p[W−→]则存在• 私有位置上下文• afillingΘpubθJpriv;v−→TJ：H（q）• private state <$PUB<$jpriv;privatetJpriv：<$Jpriv• afillingΘpubθJpriv;v−W→J：H（p）使得Θpub<$ΔJpriv，spub[−V−J/→f]<$sJpriv，ViJU[−V−J/→f]<$Bi Θ pub<$θJpriv，q[−→TJ]<$tJp r iv，p[−W→J]（Θpub，−A−→−−→B·H（q）·H（p）;Θpriv，tpriv，−→V·−→T·−W→;ΘJpriv，tJpriv，V−→J·−→TJ·−W→J）∈R（1）诉Koutavas等人/理论计算机科学电子笔记276（2011）215223ø ø øø此外，当ΘpubΔJpriv，spub[−V−J/→f]sJpriv，ViJU[−V−J/→f]<$BiΘpubΘJpriv，q[−→TJ]tJpriv，p[−W→J]定义3.3当存在环境互模拟R使得• 如果则存在ε，ε，M<$AΘpriv，tpriv，p[−W→]· 私有位置上下文· private state ΘJpriv;privatetJpriv：ΘJpriv· afillingΘJpriv;v−W→J：H（p）使得ε，ε，MJ<$AΘJpriv，tJpriv，p[−W→J]且（ε，H（p）;Θpriv，tpriv，-W→;ΘJpriv，tJpriv，-W→J）包含在R中，• 上述条件的逆成立，ε，ε，MJ<$AΘJpriv，tJpriv，p[−W→J]Def. 3.2包含了引言中讨论的适用互模拟的两种偏离;具体而言：(i)f−−的使用：−A−−→−→B−vU：AiandstatespubΘ pu b;f−−：−A−−→−−→Bv spub：Θ pubenc o destheresourcefulargummentsprinciple.(ii)types−A−→−−→B·H（q）·H（p）与值−→V·−→T·−W→的连接和-V→J·-→TJ·-W→J在最终关系enc ode值的累积中。放弃这些原则中的每一个都会导致两种不同版本的Def. 3.2：(i)如果我们要求Θ pub; θv U：A i和Θ pub; Av spub：Θpub，我们说R是一个闭宗量互模拟(ii)如果我们替换（1）by（Θpub， H（q）·H（p）;θpriv，tpriv，−→T·W−→;ΘJpriv，tJpriv，−→TJ·W−→J）∈R我们说R是无累积互模拟。这也导致了封闭表达式的两个相应的关系版本。显然，如果MJ：A是环境双相似的，那么它们也是闭宗量和无累积双相似的。3.3机智的论点和积累为了证明足智多谋的论点的必要性，我们需要证明封闭论点互模拟是不可靠的。下面的例子可以实现这一点。例3.4（有资源的参数）考虑M1和M1J型224诉Koutavas等人/理论计算机科学电子笔记276（2011）2151Σøø（1→ 1）→bool：M1d=efreturnV1MJd=efnewflag：=true. returnVJ1 1哪里V1d=efλf：1→1。返回trueVJd=efλf：1→1。读取标志为{真的。 flag：= false; f返回false;flag：= true;return true false。返回false当flag = false时，函数V1J返回与V1不同的值，这仅是应用程序范围内的情况。以下上下文区分M1和M1J：C1d=ef新记录：=true。 [1]g。g（λx. g（λy. 返回y）到z。 int n = n; return n）;读取记录为x。returnx项C1[M1]返回true，而C1[M1J]返回false。这篇文章显然是足智多谋的：提供给g的外部参数包含了g本身。然而，下面的相关者集合是一个封闭的参数互模拟，用标志›→真将V1与V1J联系起来。 为了证明这一点，它表面上表明，在V1和V1J中的应用程序在具有相关专用部分的商店中等同终止这是因为f和公共状态是由封闭的值，因此应用程序不依赖于，也不改变，在《The Dogs》 因此，M1和M1J是闭宗量双相似的，闭宗量互模拟对于λs是不合理的。Δpu b，（（1→1）→bool·A−−→−→B）;Δpriv，spriv，（V1·−→T）;（flag：bool·ΔJpriv），（flag <$→true·sprivθ），（V1J·−→Tθ）|θ：Δpriv→ ΔJpriv是一个双射重命名，ΔpubΔpriv;Δ pv−→T：−A−→−−→B，ΔpubΔpriv;Δ pvspriv：ΔprivΔ pQ我们现在提供一个例子，说明在状态互模拟中累积是必要的。因此，无积累互模拟是不合理的。例3.5（累加）考虑类型1→bool的M2和M2J：M2d=efreturnV2MJd=efnewflag：=true. returnVJ2 2..诉Koutavas等人/理论计算机科学电子笔记276（2011）2152252..Σ..ΣΣ‡--哪里V2d=efλ。返回trueVJd=efλ。将flag读为{true。flag：=false;返回true错误。返回false函数V2j在第一次应用时返回true，而在第二次应用时返回false而V2总是返回true。下面的上下文区分M2和M2J：C2d=ef[·]tof. f项C2[M2]返回真，而C2[M2J]返回假.然而，我们可以证明，下面的一组相关者是一个非累积的互模拟，因此M2和M2J是无累积双相似的。所以没有-累积互模拟对于λs是不可靠的。Δpub， 1→bool;ε，ε，V2;flag：bool，flag›→true，V2JΔpub，−A−→−−→B;Δpriv，spriv，−→T;（flag：bool·ΔJpriv），（flag›→false·sJprivθ），−→Tθ|θ：Δpriv→ ΔJpriv是一个双射重命名，Δpub<$Δpriv;Δ pv−→T：−A−→−−→B， Δpub<$Δ priv;Δ pvspriv：Δpriv<$Q4其他语言扩展4.1例外我们在λ语言中添加了生成新异常的功能，这些异常可能会被引发和捕获。下面[4]我们的语法采用以下形式：M：：= ·· ·|新E。 M|升高e|M{\displaystyleX}。 M，−c−a−t−c−h−e−。−M−→e}Toevalu ateM到x P，−c−a−t−c−h−e−。−M−→e，我们首先对M进行求值，如果返回V，我们就对P[V/x]进行求值。 如果相反它引发了一个异常e，那么在−→e中出现的这个异常e，我们继续对Me求值，否则e保持被引发。我们定义了两个大步骤关系，分别用于返回和提升：• Δ，M=A， Θ，V = Δ;M =M：A，例外情况是Θ延伸Δ和Θ; M=V：A。• Δ，MAΘ，e用于项Δ; ΔM：A，例外Θ扩展Δ和例外e出现在Θ。最终模式匹配和环境互模拟及其两个缺陷变体的定义见第二节。3.2.226诉Koutavas等人/理论计算机科学电子笔记276（2011）2153444例4.1（资源型参数）考虑类型为（1→1）→ 1的M3，M3JM3d=ef新e。returnV3MJd=efnewe.returnVJ3 3哪里V3d=efλf。提高eVJd=efλf。 f{tox. 举e，接住e。返回页首这些术语是根据上下文来C3d=ef[·]tog. g（λx. g（λy. returny））C3[M3]会引发异常，而C3[M3j]会返回异常. 然而，术语M3和M3J是闭参数双相似的，因为V3和V3J对同一闭参数的应用将具有相同的行为;这样的参数将不能抛出异常e。Q例4.2（累加）设M4和M4J（1→（1→ 1）→bool）是项：类型（1→ 1）×M4d=ef新e。 返回λ。 提高e，λ。returnV4MJd=efnewe. 返回λ。 提高e，λ。returnVj哪里V4d=efλf。 f{tox. 返回true，捕获e。返回falseVJd=efλf。 f{tox. 返回true，捕获e。返回true一个独特的背景是C4d=ef[·]tof，g. g到h. h f所以C4[M4]返回false，C4[M4J]返回true。 注意，C4使用累加：它使用在应用g之前获得的函数f作为h的参数，作为应用g的结果获得。 项M4和M4J是非累积双相似的，因为当非累积上下文通过应用g获得h时，它已经丢弃了函数f。由于无累积互模拟使用资源丰富的参数，为了证明上述术语无累积互相似，我们需要以下事实：对于任何Δ;y：（1→ 1）→bool|M：B，其中Δ不包含e，如果Δ·e，M [V4/y]的值为Θ·e，W，则存在Θ;y：（1→ 1）→bool|V：B，使得诉Koutavas等人/理论计算机科学电子笔记276（2011）215227defW=V[V4/y]和Δ·e，M [V4J/y]的计算结果为Θ·e，V [V4J/y]，如果它引发异常，情况也是如此 这一点通过对大步关系的归纳得到了证明。Q4.2名字我们为λ添加了生成新名称的工具，这些名称是值，并且可以用于相等，类似于nu演算[25，28]。我们的语法变成了A：：=···| 名称V：：=··· | MM：：=··· | 新x。M| V=V与以前对具有第一类名的语言的环境互模拟的工作不同（例如[31，15，5]），这里我们没有将相关对象中的名称关联起来。相反，通过最终的模式匹配，相关函数向其上下文显示的私有名称被重命名为相同的公共名称。例如值vm0，m1 n0，n1，n2;n=2，m= 0，n=1，n=2，inlλx. returnn0，n1搜索结果（2）：（name×name）×（name×（name×（（1→（name×name））+1）有终极模式p=m2，m0，m3，m2，inl−（3）为了从算法上获得（3），我们从左到右扫描（2），将第一次遇到的私有名称转换为公有名称，将函数替换为-并保留公有名称和标记。我们在n1之前遇到n2，因此它们分别转换为m2和m3。我们从（3）中恢复（2），• 在新的命名方案下填充孔，即。λx。returnn=0，m=3• 按出现顺序排列的已转换私有名称的列表，即n2，n1。一旦我们重新定义了Thm。3.1沿着这些路线，环境双向模拟的概念及其两个有缺陷的变体被定义为第3.1节。3.2.例4.3（有资源的参数）设M5和M5J（name→bool）→boolbeM5d=efnewn. returnV5V5d=efλf. fn型MJd=ef返回VJVJd=efλf。新的;新的fn5 5 5它们的区别在于C5d=ef[·]tog. g（λn. g（λm. m=n））228诉Koutavas等人/理论计算机科学电子笔记276（2011）215ΣΣ66677显然，C5[M5]evaluatotrue，而C5[M5J]evalua tofalse。另一方面，M5和M5J是闭参数双相似的，因为闭参数不可能知道n。特别是，当应用于它时，它不能存储n以备将来使用，因为该语言不允许存储名称。Q例4.4（累加）下面是类型1 →名称的项：M6d=efnewn. returnV6V6d=efλ。返回;返回MJd=efreturnVJVJd=efλ。新的;新的返回;返回这些术语仅通过将函数累积在其孔中并应用两次的上下文来区分，例如：C6d=ef[·]tog. g=x。 我的天x=yC6[M6]返回真，但C6[M6J]返回假.M6和M6J之间的关系如何没有-累积双相似，因为只应用一次（即使是资源丰富的参数）他们的行为是一样的。Q4.3多态性我们将多态性添加到λ中，因此类型和术语的语法变为A：：=···|十.A|十.AV：：= ··· | Λ X.M| recf Λ X.M|阿维尼翁，VM：：=··· | VA|将V匹配为<$X，x<$。 M使用[19]中发展的终极模式匹配定理，我们再次将足智多谋的论点和积累的原则以及两个有缺陷的版本结合起来，制定环境互模拟。下面的例子说明了这些原则的必要性。例4.5（Resourceful参数）考虑以下类型为X的存在包。（X→（1 +X））→bool：M7d=ef返回值1，V7dMJd=ef返回布尔值， VJd诉Koutavas等人/理论计算机科学电子笔记276（2011）2152297Σ88哪里V7d=efλf。 f到{inl。返回false，inr 返回true}VJd=efλf。 ffalseto{inl} 返回falseinrtrue。 返回falseinr假。 f为真{inl}。 返回trueinr true。返回trueinrfalse。 返回false这些是根据上下文C7d=ef[·]至X，g。g（λy：X. g（λz：X. 返回inr y）到{true. 返回inr y，错误。returninl}）C7[M7]项为真，而C7[M7J]项为假. ButM7和M7J关闭-参数双相似，因为V7和V7J的封闭参数具有多态类型X→（1 + X），并且只有三个这样的函数：常数函数λx。返回inl λ x和λx。发散，函数λx. 返回inr x. 显然，V7和V7j在应用于这些参数时的行为是相同的.Q请注意，具有存在量化参数类型X的函数（例如下面的示例中的那些）必须提供资源参数，因为上下文不能构造X类型的闭合值。因此，人们可能会认为，对于这种语言，一个较弱的足智多谋的概念可能是合理的。然而，前面的例子证明了不仅需要一个资源丰富的参数，而且需要一个在λ下使用资源（来自库存的值）的参数，就像我们迄今为止学习的其他语言一样例4.6（累加）累加是必要的，因为上下文可能会接收旧函数的新参数。例如，考虑术语M8和X型的M 8 j。（1 → X）×（X → bool）：M8d=ef返回1，V8V8d=efλ。 返回λ x，λx. 返回真值MJd=ef返回1， VJV8d=efλ。 返回λ x，λx. 返回错误这些是根据上下文C8d=ef[·]至X，f，g。 f从x到x。G x显然，C8[M8]返回真，而C8[M8j]返回假. 如何使用M8和M8J是无累积双相似的，因为当上下文接收到这两个函数230诉Koutavas等人/理论计算机科学电子笔记276（2011）215它不能区分右边的函数，因为它还没有一个值来应用它们。Q5新名字环境互模拟定义中的另一个问题是上下文在互模拟的每一步添加公共名称的每-我们可以在定义3.2中固定Δpub，给出Δpub-互模拟的概念，然后要求项; M，MJ：A是Δpub-对所有Δpub的双相似。对于到目前为止我们所考虑的确定性语言，我们相信这是一个合理的修改。然而，在存在非决定论的情况下，没有单一的答案;它取决于非决定论的种类和我们考虑的语境对等在这里，我们研究的扩展语言的名称从SEC。4.2有限的和可数的非决定论。我们相信，上述限制对于may测试是合理的在这里，我们给出两个例子，说明在可数非决定论存在的情况下，这对于必须检验是不合理的，在甚至有限非决定论存在的情况下，这对于较低的双相似性是不合理的在本节中，我们将nat= recX。1 + X和命名= recx。1 +姓名×X。我们使用常用的构造函数zero和succ来表示nat，empty和cons来表示namespace。我们使用以下函数：• ;boolmember：（name× name）→bool告诉我们它的第一个参数是否出现在第二个参数• ;navdistnames：namespace→nat返回参数中的非重复名称的数量• ;navmkfreshlist：nat→namespace创建一个长度等于 其论点• ;navmin：nat×nat→nat是最小函数。5.1可数不确定性与必测我们从Sec扩展语言。4.2同时使用二进制和可数（不稳定）不确定性选择-当然，前者是多余的。我们的语法现在M：：=··· | M或M| 选择x。M其中x的类型为nat。bigstep语义以标准方式给出[23]。首先，我们归纳地定义一个关系Δ，M<$A Θ，V，这意味着Δ，M可以求值为Θ，V。然后，我们共归纳地定义一个谓词Δ，M<$A，意味着Δ，M可以发散。为了合理地推理可能检验（收敛的可能性）和必须检验（发散的不可能性），一组相关者R需要是凸环境互模拟，即如果C和CJ是R相关配置，则一个可能执行的任何收敛步骤或发散可以被另一个模仿。诉Koutavas等人/理论计算机科学电子笔记276（2011）2152319如果我们不要求发散被模仿，那么R仅仅是一个较低的环境互模拟[34，20]，这只适用于五月测试例5.1（生成）我们考虑项M9和M9JTd=efrecX. name→1 +X：型M9d=ef选择w。V9发动机，空发动机MJd=efM9或VJ空9 9哪里V9d=efrec（f：（nat×namespace）→T）λ（c，lst）. 返回foldλn。成员n，lstto{true. 返回inl值，false。将c作为{零. 返回到下一页，succyy. 好的，我先走了。 返回inr g}}VJd=efrec（f：namespace→T）λlst. 返回λn。membern，lstto{真的 返回到下一页，错误。 f（cons n，lstn）到g. 返回inr g}在这里，M9和M9J返回一个函数，否则为inl_nl。项M9赋予上下文一个它可以记住的任意有限数量w的不同名称; M9J有额外的可能性，可以赋予无限的记忆。这两个术语是根据上下文来C9d=ef[·]tof.（rec（h：T → 1）λ（fold y）. 新的;新的 我的意思是在这里。 返回顶部，因尔湾 Hg}）f显然C9[M9J]是可分裂的，而C9[M9]则是不可分裂的. 但是对于一个n固定的名字列表Δpub，很明显M9和M9J是凸Δpub-双相似的。该示例表明，为了使环境互模拟在必须测试中是合理的，可数非决定论的存在，我们不能免除上下文在每一步产生新名称Q232诉Koutavas等人/理论计算机科学电子笔记276（2011）215105.2作为同余的下互模拟例5.2（生成）设M10和M1J0 是以下类型姓名→自然：M10d=ef选择w。返回V10M1J0 d=ef返回VJ或M10哪里V10d=efλlst。最小值distnames（lst），wV1J0 d=efλlst。distnames（lst）项M10选择一个数w（或发散），并返回一个可以在列表中计数到w个不同名称的函数;M1J0有额外的可能性返回一个可以在列表中计数无限数量的不同名称的函数设C10是以下类型1 →nat的上下文：C10d=ef[·]tof.返回λ。选择k。mkfreshlist（k）到lst。第一NowC10[M1J0]may返回一个函数，当a应用于整数时，may返回一个自然数，而C10[M10]不能这样做因此，任何可想象的较低的二进制化（或evenlowersimulation）的概念必须区分C10[M1j0]和C10[M10]，因此，如果它是一个同余，则M1j0和M10。每一个经典，在名称Δpub中，M1J0和M10是较低的（事实上，甚