寻址项重写系统：共享与循环数据的编程语义定义

理论计算机科学电子笔记127（2005）57-82www.elsevier.com/locate/entcs术语重写系统：语义学、语用学与语义学扩展抽象丹·道格尔伍斯特理工学院，伍斯特，MA，美国皮埃尔·莱斯坎纳法国里昂E'coleNormaleSup'erieure，路易吉·利科里INRIA Sophia Antipolis，法国Fr'ed 'eri cLangINRIA Rhone-Alpes，法国摘要我们提出了一种称为寻址项重写系统的形式主义，它可以用来定义编程语言的操作语义，特别是那些涉及共享，递归计算和循环数据结构。因此，寻址术语重写系统非常适合描述基于对象的语言，例如称为λ Obja的语言家族，涉及函数和基于对象的特征。保留字： 项重写系统，图重写，λ演算，对象演算。1介绍1.1地址演算与共享语义懒惰函数式语言（以及计算机代数、定理证明器等）的高效实现。需要某种共享机制来避免多个1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.12.04258D. Doughnut等人理论计算机科学电子笔记127（2005）57一无环图一BB对应的寻址项a aBBB循环图对应寻址项图1. 共享和循环使用计算一个参数。 在符号演算中对这种共享进行建模的一种自然方式是从项的树表示传递到有向图。这种术语图可以被认为是抽象语法树和内存中的具体表示之间的程序表达式的表示，并且术语图重写提供了对共享敏感的函数编程的正式操作语义。 关于项图的理论和应用有大量的研究;例如，参见[9，31，28，6]的一般处理，以及[33，32，4，3，1]的λ-演算和实现的应用。在本文中，我们注释的条款，作为树，与全球地址的精神[14，3 0，8]。L'evy[2 3]andMaranget[25]preveiouslyintransodl ocaladd resse s;从操作语义的角度来看，全局地址更好地描述了计算机或抽象机器中发生的事情。术语图重写和寻址项重写的形式主义基本上是相似的，但我们认为寻址项设置有几个优点。我们的意图是定义一个尽可能接近实际实现的演算，并且我们术语中的地址确实对应于内存引用。在某种程度上，我们试图在理论和实现之间建立一座桥梁，我们更喜欢这种直接性，而不是术语图处理中固有的隐式编码。使用显式全局地址，我们可以跟踪可用于实现微积分的共享。共享公共地址的子项表示相同的子图，如图1（左）所示，其中a和b表示地址。在[12]中，在寻址项重写的背景下研究了寻址项，作为经典一阶项重写的扩展在寻址项重写中，我们可以同时重写共享相同地址的所有子项，模仿实现中会发生的情况。我们还使用一个特殊的后指针来处理循环图[30]来丰富共享。循环在函数式语言中用于表示有限的数据结构，（在某些实现中）用于表示递归代码;它们在命令式面向对象语言的上下文中也很有趣，其中存储中的循环可以通过使用self（或this）的命令式更新来创建。 循环表示的概念通过寻址项是相当自然的：有限图中的循环路径是完全的。BD. Doughnut等人理论计算机科学电子笔记127（2005）5759由一个前缀路径确定，该路径以一个“跳转”到前缀路径的某个节点（用一个后指针表示）结束包含显式间接节点是这里的一个关键创新。间接节点允许我们对术语图重写的所谓折叠规则（将术语重写为其适当子术语之一的规则）进行更现实的处理。更详细的讨论见第2节。1.2可寻址TRS描述基于对象框架的适用性近年来，大量的研究旨在为面向对象编程语言提供严格的基础。在许多情况下，这项工作采取了“对象演算”的形式这种结石可以从两个方面来理解。一方面，形式系统是语言语义的具体化，可以用作分类语言设计选择的框架，为研究类型系统提供设置，或支持指称语义。或者，我们可以将对象演算视为一种中间语言，用户代码（以高级面向对象语言）可以被翻译成这种语言，并且可以从中导出实现（以机器语言）。功能操作语义学的几种处理方法存在于文献[21，5，19，26]中。Addressed Term Rewriting Systems（最初由惰性函数式编程语言[27，29]的实现激发）是用于建模面向对象语言的λObJa框架[24]的基础[24]中的结果展示了如何使用寻址项重写系统来建模λObJa这里我们揭示了λObJa的重写语义下的基于图的机制。据我们所知，在分析基于对象的编程的上下文中，很少探讨术语图重写λObJa的新颖之处在于它为编程语言的函数式和面向对象方面提供了一种同构的方法，在这个意义上，这两种语义是以相同的方式使用寻址项来处理的，而在允许的代数结构中只有最小的牺牲。事实上，所使用的寻址术语最初是为了描述函数式编程语言的共享行为而引入的[30，8]。一个有用的方法来了解λObJ一个框架是通过类比图归约作为函数式编程的实现演算。将λObJa与函数式程序设计（FP）和面向对象程序设计（OOP）的实现技术相比较，给出了以下对应关系。λObJa60D. Doughnut等人理论计算机科学电子笔记127（2005）57范式λObJa片段Powered by纯FPλObJa（L）种atr纯FP+OOPλObJa（L+C+F）种atr1.3论文大纲第二节详细介绍了寻址项重写系统的框架第3节通过介绍构成λObJa核心的重写规则的三个模块，使有地址的项重写系统工作。 为了教学方便我们分两步进行：首先，我们提出了演算λObJσ，中间在Fisher，Honsell和Mitchell [15]的演算λObJ之间，然后我们放大到我们的λObJa。第4节给出了一个在λObJa框架中运行的基于对象的示例。第5节讨论了λObJ和λObJa之间的关系。第6节结束。由于篇幅有限，这里并没有给出所有的证明这篇论文的较长版本包含完整的证明和大量关于对象框架的函数和基于对象的命令式示例，可以在技术报告和手稿中找到[22，12]。2解决术语重写系统在本节中，我们将介绍寻址项重写系统，简称ATRS。经典的术语重写[10，20，7]不能简单地表达共享和突变的问题。微积分在描述内存管理时，经常引入一些特殊的数据结构来对内存进行建模，称为堆或存储，以及访问和更新操作。然而，这些结构的使用需要限制演算到特定的策略。寻址项重写（以及项图重写）的目的是提供一个计算的数学模型，该模型反映内存使用情况，并且足够鲁棒以独立于重写策略。共享计算。考虑约简平方（x）→乘以（x，x）。为了共享子术语，在术语中插入地 址 ， 使 它 们 成 为 寻 址 术 语 .例 如 ， 如 果 我 们 要 计 算 square （ square（2）），我们将地址a，b，c附加到各个子项。这就产生了平方a（平方b（2c）），然后可以按如下方式减少：D. Doughnut等人理论计算机科学电子笔记127（2005）5761正方形a（正方形b（2c））~乘以a（正方形b（2c），正方形b（2c））乘以a（乘以b（2c， 2c），乘以b（2c， 2c））~乘以a（4b， 4b）~16a，其中共享计算的关键点是共享一个公共地址的所有项同时被约简。对象结构的共享。重要的是不仅要共享计算，而且要共享结构。实际上，对象通常是接收多个指针的结构。作为一个例子，如果我们共享由b寻址的共同结构。这可以很容易地形式化因为地址是一等公民。 参见第4节。自行车.循环在函数式编程中是必不可少的，当我们处理有限的数据结构时，就像在懒惰的函数式编程语言中一样。循环也用于在递归函数的代码中节省空间。此外，在对象编程语言的上下文中，循环可以用来表达可以通过递归代码的惰性计算引入内存的循环2.1地址条款寻址项是由运算符符号标记并用地址装饰的一阶项。它们满足格式良好的约束，确保每个寻址项表示存储的一个连接部分。此外，每个节点的标签设置其后继节点的数量。 抽象地说，寻址项表示项图，作为图的最大树展开，在任何路径中没有重复的地址。直观地表示节点在内存中的位置。因此，出现在不同路径上的相同子树可以具有相同的地址，这对应于两个出现被共享的事实。定义分为两个阶段：第一阶段定义基本的归纳术语结构，称为preterms，而第二阶段只是将preterms限制为格式良好的preterms或寻址术语。定义2.1[早产儿](i) 设是一个项签名，·是一个零元的特殊符号（一个常数）。 设A是由a，b，c，.. . X是一组变量，用X，Y，Z，.表示。 一个可寻址的preterm t over n是一个变量X，或者·a，其中a是一个地址，或者62D. Doughnut等人理论计算机科学电子笔记127（2005）57Δ=形式Fa（t1，...， tn）其中F ∈ N（标号）有元n≥0，a是一个地址，并且每个ti是一个寻址的早产儿（归纳）。(ii) 所处理的早产儿t的位置，用loc（t）表示，定义为：.禄亚ΔaΔF（t1，.，tn）=loc（·）=a，它不是由变量定义的。(iii) 出现在pretermt中的变量和地址的集合分别用var（t）和addr（t）表示，并以明显的方式定义早产儿的定义使用了一个特殊的符号·，称为后指针，用于表示周期[30]。在一个地址项中的一个后指针·a必须是这样的，a是从根路径上出现的一个地址返回到后指针节点。它只是指示在哪个地址必须分支（或指向回）沿着无限路径继续一个基本的操作，我们必须有解决（前）条款是展开，允许看到，按需，什么是超越了一个后指针。因此，解折叠可以被看作是一个懒惰的操作符，它在循环图中更深地遍历一步它伴随着它的对偶，称为折叠，允许给出循环的最小表示然而，请注意，折叠和展开操作在实际实现中没有操作意义（因此没有操作成本），但它们是必不可少的，以便正确地表示所寻址的项之间的变换。定义2.2[折叠和展开]折页. 设t为早产儿，a为地址。 我们将fold（a）（t）定义为 位于t中a处的早产儿的折叠如下：fold（a）（X）=X折叠（a）（·b）Δ·b.Σfold（a）Fa（t，.（t）Δ·a.1nn=.Σ折叠Fb（t，.（t）ΔFbfold（a）（t），.、折（a）（t）如果a/b1n=1n展开。设s和t是前置项，使得loc（s）是a（因此定义），并且a在t中不出现，除非作为·a的地址。我们定义unfold（s）（t）D. Doughnut等人理论计算机科学电子笔记127（2005）5763Δ=ΔΔ作为·a在t中由s展开如下：展开（x）=X ⎧如果一个 女人展开（s）（·b）Δ·b否则.展开ΣΔb（t，...（t）B.JJJΔ 其中sfold（b）（s）F1m=Ft1，. ，tm=tJ J1=展开（s）（t1）...tJ Jm=展开（s）（tm）我们现在开始正式定义寻址项，也称为可接受的前项，或简称为项，当没有歧义时。如前所述，寻址项是表示项图的前置项。in-term的概念有助于定义所述术语。称呼语的定义分两步：第一步是悬垂的定义术语，即通常意义上的实际寻址术语的子术语。同时，我们定义了一个悬挂项的概念，比如说s，在一个给定的地址，比如说a，在一个悬挂项，比如说t。当悬挂项t（i. e.“out”-项）是已知的对于悬空项t，其入项由函数t@表示，读作展开因此，有两个概念需要区分：一方面是通常的有充分根据的“子项”概念换句话说，尽管项不是其本身的适当子项，但由于循环，项可能是其本身的适当内项或项是其内项之一的内项。函数ti@在构造过程中也被用来检查同一项的所有部分是否一致，主要是检查共享同一地址的所有入项是否都是相同的悬挂项。悬挂项可能具有不指向任何地方的后指针，因为在项中不存在具有相同地址的节点。 后者都是挂 着 的 背景音。 F或在stan ce中，（λx. y）[·b/y]c有一个悬挂的bak-p，而hile（λx. y）[·c/y]chanone. 定义的转换步骤将寻址项限制为不具有悬挂的悬挂项后指针以下定义同时提供了两个概念：• 那些悬置的条件。64D. Doughnut等人理论计算机科学电子笔记127（2005）57• 函数t@从addr（t）到dangling in-terms。t@a返回t在地址a处的输入项。定义2.3[悬挂寻址项]悬挂寻址项的集合DT（DT）是满足以下性质的最小集合变量 XDT（X）和X@没有任何定义。反指针。 ·a∈DT（π）和·a@aπ·a.表情对于 t1∈DT（π），.，tn∈DT（t）使得：b∈addr（ti ）<$addr（tj）<$ti@b<$tj@b，对于a，一个地址使得：a∈addr（ti）<$ti@a <$·a，并且对于元数n的F ∈ N，• tFa（t1，.，tn）∈DT（n）.• t@at。• b∈addr（ti）\{a}<$t@b<$founder（t）（ti@b）.可接受的寻址项是指所有·a都指向t中的某个东西，使得该项存在一个完整的（可能无限的）展开。我们可以用t @函数观察到这一点的唯一方法是通过检查没有•a可以定义2.4[寻址项]如果a∈addr（t）<$t@a<$·a，则悬挂寻址项t是可容许的。一个可接受的悬挂寻址项将被简单地表示为一个寻址项。命题2.5（项内可容许性）如果t是可容许项，且a∈addr（t），则(i) t@a是可接受的，并且(ii) <$b ∈ addr（t @ a），我们有（t @ a）@ b <$t @ b。2.2解决术语重写一个定址词项的缩减必须返回一个定址词项（而不仅仅是一个preterm）。换句话说，计算模型（这里称为项重写）必须考虑地址给出的共享信息，并且必须定义为保持所寻址项之间的可容许性的最小重写关系。因此，计算必须同时发生在所寻址的项中的几个位置处，即在位于同一地址的位置处。在实际实现中，项的这种同时更新对应于存储器中的位置的更新。在ATRS中，重写规则是一对开放寻址项（即，例如，包含变量）。解决术语重写的方法D. Doughnut等人理论计算机科学电子笔记127（2005）5765=.=在所寻址的项上进行重写与通常的项重写的方式没有太大的不同;概念上有四个步骤。(i) 在t中找到一个redex，i。e. 匹配规则左侧的项内。直观地说，寻址项匹配与经典项匹配相同，除了有一种新的变量，称为地址，只能用地址代替。(ii) 创建新的地址，i. e.在当前寻址项T中未使用的地址，其将对应于出现在右手侧但不出现在左手侧的位置（即，e. 新的位置）。(iii) 将规则右侧让我们把这个新的地址项称为u。(iv) 对于所有在t和u中都出现的a，重写步骤的结果，比如tJ，将有tJ@au@a，否则tJ将等于t。我们给出匹配和替换的形式定义，然后精确地定义重写定义2.6[替代、匹配、统一](i) 从地址到地址的映射称为地址替换。从变量到寻址项的映射称为变量子项。 一对地址替换α和变量替换σ称为置换，记为<$α; σ<$。(ii) 设<$α;σ<$是一个代换，p是一个项，使得addr（p）≠dom（α），var（p）≠dom（σ）.将<$α;σ<$应用于p，记为<$α;σ<$（p），归纳定义如下：α;σα（·a）Δ·α（a）Δα;σΣΔα; σ<$Fa（p，. ，p）Fα（a）（q、...、Q）和q折叠（α（a.Σσα;σα（p）1m=1m i=））i(iii) 我们说一个项t匹配一个项p，如果存在一个替换项<$α;σ<$使得σα;σα（p）≤t。(iv) 我们说两项t和u统一，如果存在一个代换<$α;σ<$和一个定址项v，使得v<$$>α;σ<$（t）<$$>α;σ<$（u）。我们现在定义替换。替换函数按条件操作给定一个项，它将在给定位置的一些项更改为具有相同地址的其他不同于经典的术语重写（例如，见[10]页。252)执行替换的位置简单地由地址而不是项中的路径给出。Δ66D. Doughnut等人理论计算机科学电子笔记127（2005）57Δ=定义2.7[替换]设t，u为寻址项。由u在t中生成的替换，表示为repl（u）（t），定义如下：repl（u）（X）=X⎧如果a∈addr（u），则返回u@arepl（u）（·a）Δ.Σ但在其他方面，⎧如果a∈addr（u），则返回u@arepl（u）Fa（t，.，不）Δ1m=⎪⎩F a .Σrepl（u）（t1），. ，repl（u）（tm）否则命题2.8（替换可接受性）如果t和u是寻址项，则repl（u）（t）是寻址项。我们现在定义Redex和重写的概念。定义2.9[寻址重写规则]在k上的寻址重写规则是在k上的一对寻址项（l，r），写作l~r，使得loc（l）<$loc（r）和var（r）<$var（l）。此外，如果在addr（l）中有地址a，b和addr（r）使得l@a和l@b是unifiable，那么r@a和r@b必须用相同的unifier来unifiable。条件loc（l）loc（r）表示l和r具有相同的顶地址，因此l和r不是变量;条件var（r）var（l）确保没有创建变量。定义2.10[Redex]项t是规则l~r的Redex，如果t匹配l。一个项t有一个redex，如果存在一个地址a ∈ addr（t）使得t@a是一个redex。请注意，一般来说，我们不会对地址中的线性施加限制（即，e.相同的地址可以出现两次），或者L和R的非循环性。然而，λObJa在地址上是线性的除了重定向指针之外，ATRS还创建新节点。新的重命名确保这些新节点地址尚未使用。定义2.11[新鲜更名](i) 我们用dom（λ）和rng（λ）表示函数λ的通常定义域和值域.(ii) 重命名是一种单射地址替换。(iii) 设t是一个项，它具有寻址重写规则l~r的redex。如果dom（αfresh）=D. Doughnut等人理论计算机科学电子笔记127（2005）5767Δaddr（r）\addr（l）i.e. 重命名对每个新引入的地址进行重命名以避免捕获，并且rng（αfresh）Δaddr（t）=Δ i，i。e.所选择的地址不存在于T中。提案2.12（替代品可受理性）假设一个可接受的条件t，其具有针对所寻址的重写规则l ~ r的redex。然后(i) 对于l ~ r关于t存在一个新的重命名α fresh。(ii) α<$αfresh;σ<$（r）是可容许的。在这一点上，我们已经给出了指定重写所需的所有定义定义2.13[改写]设t是一项，我们想在a处通过规则l~r约简它。按以下步骤操作：(i) 确保t@a是redex。令σα; σα（l）=t@ a.(ii) 计算αfresh，l~r关于t的新重命名。(iii) 计算uααfresh;σ（r）。(iv) 在地址a处用规则l~r重写t的结果s是repl（u）（t）。 我们写约简t~s，将定理2.14（重写闭包）设R是一个寻址项重写系统，t是一个寻址项. 如果t ~ u在R中，那么u也是一个寻址项。2.3非循环无突变ATRS在本小节中，我们考虑ATRS的一个特殊子类，即不涉及循环和突变的ATRS。我们表明，这一类特殊的ATRS是健全的模拟长期重写系统。定义2.15[无环性和无突变性]• 如果一个被寻址项没有出现·，则它被称为非循环项。• 一个ATRS规则l~r称为非循环的，如果l和r是非循环的.• 如果一个ATRS的所有规则都是非循环的，那么它就被称为• 一个ATRS规则l~r被称为无变异的，如果a∈（addr（l）<$addr（r））\{loc（l）}<$l @ a <$r @ a.• 如果一个ATRS的所有规则都是无变异的，那么它就被称为无变异的68D. Doughnut等人理论计算机科学电子笔记127（2005）57Δφa（X）=XΔ下面的定义旨在建立ATRS和术语重写系统之间的关系。我们定义了从寻址项到代数项的映射，以及从寻址项到代数上下文的映射。定义2.16[映射]• 一个ATRS到TRS的映射是一个从非循环预项到有限项的同态φ，使得对于某个函数集{Fφ|其中每个Fφ是一个投影或一个构造函数：φ（X）=Xφ（Fa（t，.，t））ΔF（φ（t），...，φ（t））1n=φ1n• 给定一个ATRS到TRS的映射φ和一个地址a，我们将φa定义为：- 从寻址的前置项到多孔上下文的映射，使得地址a处的所有子项（如果有的话）被写为Q的孔替换。更正式地说，Δ⎧如果一个人φ（Fb（t，.，t ））Δ将1n=Fφ（φa（t1），.，φa（tn）），否则• 给定一个包含零个或多个洞的上下文C，我们将C[t]写为用t填充C中的所有洞所获得的项。• 给定一个ATRS到TRS的映射φ，我们定义了从Ad-dressed termssubstitution到terms substitution的映射φs，如下所示：⎧φ（σ（X））若X∈dom（σ）φs（σ）（X）=X否则定理2.17（TRS模拟）设S ={li~ri|i = 1.. n}是非循环无突变ATRS，并且t是非循环项。若t~u在S中，则系统φ（S）={φ（li）~φ（ri）}中的φ（t）~ +φ（u）|i = 1.. n}3通过ATRS建模基于对象的框架：λObJa本节的目的是描述框架λObJa的顶层规则，该框架是基于前一节中介绍的ATRS的框架。该框架是由一组规则安排在模块中描述。这三个模块分别称为L、C和F。D. Doughnut等人理论计算机科学电子笔记127（2005）5769WM，N：：= λx.M|MN|X|C|⟨⟩ |M←m = N|M m（代码）U，V ：：= M [s] |UV|.Σ乌木|U←m = V|选择O，m，U（评估背景）O：：= |O←m = Vs：：= U/x; s |id（替换）图2. λObjσ的解L是函数模，本质上是微积分λσa[8]。这模块本身定义了基于λ演算和弱归约的纯函数式编程语言的核心C是公共对象模块，包含了所有定义为λObJa的对象演算的所有实例所共有的所有规则。它包含对象的实例化和方法的调用规则。F是函数更新的模块，包含实现对象更新所需的规则，也改变了对象标识。规则集L+C+F是函数对象演算的λObJa的实例我们分两步来做：(i) 首先，我们提出了函数演算λObJσ，介于Fisher，Honsell和Mitchell[15]的演算λObJ和我们的演算λObJa之间。(ii) 然后，我们在整个λObJa上按比例放大，作为λObJσ的保守扩展，在这个意义上，对于非循环的无突变项，λObJa中的计算和λObJσ中的计算返回相同的范式。由于一个λObja-项通过擦除地址和间接性而产生一个λObjσ-项，这种保守性的一个共同推论是地址无关性，即：e.内存中的程序布局不能预测计算的最终结果。这是一个关于实现的非正式推理如何被转换成λObJa并被正式证明的例子。3.1λObJσ的λλObJσ不使用地址（参见图2中的语法）。的语法λObJσ如图3所示;读者会注意到，70D. Doughnut等人理论计算机科学电子笔记127（2005）57替代品的基础知识（MN）[s]~（M[s]N[s]）（App）.Σ（λx.M）[s]U~M[U/x;s]（Bw）x[U/y;s]~x[s]x/y（RVar）x[U/x;s]~U（FVar）M<$m=N方法调用[s]~（NO）（Mm）[s]~（M[s]m）（SP）（Om）~Sel（O，m，O）（SA）Sel（U_O←m=U_O，m，V）~（U_V）（SU）Sel（O<$n=U<$，m，V）~Sel（O，m，V）m/n（NE）图3. λObjσ的规则是λObJa的项，不含地址、间接和对象恒等式，并且规则适当地包含在λObJa的模L+C+F的规则中。第一类表达式是程序代码。定义代码的术语没有地址，因为代码不包含环境，在计算过程中受到任何变化的影响（记住，地址意味着告诉计算引擎计算结构的哪些部分可以或必须同时改变 第二类和第三类定义动态实体或内部结构：求值上下文和对象的内部结构（或简单的对象结构）。最后一类定义了替代，也称为环境，即。例如， 绑定到变量的术语列表，这些术语将在代码中分布和增加。D. Doughnut等人理论计算机科学电子笔记127（2005）5771Sel O，M，U=M，N：：= λx.M|MN|X|C| ⟨ ⟩ |M←m = N|M m代码U，V：：= M [s] a|（紫外线）a|Eval.背景（乌吉亚）a|U←m=V|[[O||a.|a.Σ|[美国|一|·aO：：=a|O←m = V|·对象结构s：：= U/x; s |id替换3.2λObJa的λ图4. λObja的λ图4总结了λObJa的语法。对于λObJσ项，定义代码没有地址（替换也是如此）。相反，计算上下文中的术语和对象结构具有显式地址。记法。“与传统的列表表示法类似，我们采用以下别名：M[ ]aΔM[id]aM [U/x;.] ; U/x] aΔ M [U/x;.] ;U/x;id]a1 1n n=1 1n n在下文中，我们将考察λObJa的所有四种句法类型。代码类别。代码项，写为M和N，提供以下结构：• 纯λ-项，由抽象、应用、变量和常量构成。这允许定义高阶函数。• 对象，由空对象和函数更新操作符←构造。 第4节给出了更新操作符的非正式语义。在功能设置中，该操作符可以理解为扩展操作符以及覆盖操作符，因为覆盖被处理为扩展的特定情况。• 方法调用（ ）。72D. Doughnut等人理论计算机科学电子笔记127（2005）57模块L（MN）[s]a~（M[s]bN[s]c）a（App）. （λx.M）[s]bU<$a~M[U/x;s]a（Bw）x [U/x; s] a~[U |a（FVar）x[U/y;s]a~x[s]ax/y（RVar）（[U |bV）a~（U V）a（AppRed）[（λx.M）[s] b|a~（λx.M）[s] a（LCop）模块C⟨⟩ [s] a~[[⟨ ⟩b||a（无）（M<$m）[s]a~（M[s]b<$m）a（SP）（[[O||b<$m）a~ Sela（O，m，[[O||b）（SA）（[U|b<$m）a~（U<$m）a（SRed ）Sela（ O<$m = U<$b ，m，V）~（U V）a（SU）Sela（O<$n = U<$b，m，V）~Sela（O，m，V）m/n （NE）模块FM<$m=N<$[s]a~[O||b<$m = V a~[[O <$m = V c||a（FC）美国|b<$m = V a~ VU<$m = Va（FRed）图5. 模L、C和F评估上下文。这些术语，写为U和V，模拟抽象机器。评估上下文包含计算操作结果所需的临时结构的抽象。它们被赋予地址，因为它们表示动态实例化的数据结构;它们总是表示一个封闭的D. Doughnut等人理论计算机科学电子笔记127（2005）5773在一个环境的分布下。有以下评价背景：• 闭包的形式为M[s]a，是一对代码和一个环境。粗略地说，s是代码M中自由变量的绑定列表。• 项（UV）a、（U<$m）a和<$U<$m=V<$a是与相应的代码构造函数相关联的求值上下文。这些求值上下文的直接子项本身就是求值上下文，而不是代码。• 对象，格式为[[O||a，表示内部对象结构为O且对象标识为a的被求值对象。换句话说，地址a扮演对象结构O的入口点或句柄的角色，如图6所示。• 项Sela（O，m，U）是与方法查找相关联的求值上下文i. 例如，扫描对象结构O以找到方法m，并将其应用于对象U。它是一个辅助操作符，在向对象发送消息时调用。• 术语[U]|a表示从地址a到所寻址项U的根的间接。运营商[|a没有任何指称意义。它的引入是为了使右手边与左手边保持在同一地址。事实上，在某些情况下，这是必须执行的。e. G.规则（FVAR）。这说明了实施者所熟知的现象。规矩（AppRed）、（LCop）和（FRed）删除这些间接。• 形式为·a的反向引用表示一个反向指针，用于表示第2节中解释的循环。内部对象。λObJa的关键选择是使用内部对象（写为O）来建模内存中的对象结构。它们是持久结构，只能通过对象的地址访问，在[[ O]中用a表示||a，并且永远不会被销毁或修改（当然，最终会被实现中的垃圾收集器删除）。由于我们的演算本质上是基于委托的，对象被实现为（字段/方法的）链表，但可以设想更有效的数组结构。同样，循环的潜在存在意味着对象结构可以包含后指针·a.对一个程序的评价，我。例如，代码项M总是在空环境中开始，i. 例如，作为闭包M[ ]a。注3.1[λObJa的基于ATRS的预项]λObJa的具体语法图4中的“早产”在两个方面与早产定义一致：74D. Doughnut等人理论计算机科学电子笔记127（2005）57(i) 签名中的符号也可以是fix（如e）。例如，在一个实施例中，（））、括号（如e. 例如，在一个实施例中，（||）、mix fix（如[ ]），甚至是“不可见”（如应用程序的传统做法，由并置表示）。在这些情况下，我们选择将地址写在方括号和圆括号之外。(ii) 我们将使用λObJasort-specific变量名。例如，我们写（UV）a而不是应用a（X，Y），M[s]a而不是闭包a（X，Y）（用U代替X，等等）。实际上，我们将不指定λObJa函数符号的名称，例如上面提到的apply和closure。据我所知，并非所有早产儿都有这种情况。，因为这是一个简单的，在这一过程中，在这种情况下，preterm（[[preterm]a||b.m）a[[||b是不一致的，因为位置a既被标记为“。的.abce b早产（[||（中文）||也是不一致的，因为位置b在位置a和e都有它的后继者，这是不可能的。.abca b bbd一个术语图。相反，早产儿（[||（中文）||表示具有分别位于地址a、b、c和d的四个节点的法律术语图。此外，地址a和b处的节点，分别标记为[1]和[2]。||、在相应的图中共享，因为它们具有多个实例在任期内。这些是第2.1节定义的良构约束所捕获的区别。图5定义了λObJa作为计算引擎的规则。注3.2[关于新地址]我们假设所有出现在右边而不是左边的地址都是新的。这是一个可靠的解释，它依赖于新地址的正式定义和寻址项重写（见第2节），这确保了地址冲突不会发生。归约规则的非正式含义在[24]中定义，而更完整的解释在[11]中给出。4工作中的ATRS：λObJa在这里，我们提出了一些例子来帮助理解框架。我们首先给出一个例子，展示一个函数对象在接收到消息m时用字段n扩展自己[17]。1观察到使用此项的计算会导致方法未找到错误，因为被调用的方法m不属于对象[[a]||b，因此将被适当的声音类型系统或运行时异常拒绝。D. Doughnut等人理论计算机科学电子笔记127（2005）5775Δ=⟩||例4.1[一个“self-in”扩展的对象selfext = λ self ← add n = λself. n = λs。1个小时。“我的天，N从空替换开始，MΔ（self ext_add_n）在λ O b_j a中的约化如下：M[]a~n（n=N）a（1）~（[e ||d←add n = N [] c<$b<$add n）a（2）~（[[e←add n=N[]cfb加n）a（3）⟩||⇐“我的天，O~Sela（O，add n，[[O||（b）（4）~（（λself. n = λs。1）[] c[[O||b）a（5）~λself<$n= λs。1[ [O||b/self]a(6)~{\displaystyle {\frac{f}}[[O||b/self]h←n=(λs. 1）[O||b/self]g⟩a(7)~[ [O||h ← n =（λ s .|h←n=(λs. 1）[O||b/self]g⟩a(8)~[[O||b←n=(λs. 1）[O||b/self]g⟩a(9)~[[λ0←n=（λself. 1）[O||b/self]gha(10)在（1）中，执行两个步骤以使用规则（SP）和（FP）在扩展内分布环境。在（2）中，空对象被赋予对象结构和对象标识（NO）。在（3）中，这个新对象是功能扩展的（FC），因此它共享前一个对象的结构，但具有新的对象身份。在（4）和（5）中，两个步骤（SA）（SU）执行方法add n的查找。 在（6）中，我们应用（Bw）。 在（7）中，环境是功能扩展（FP）。在（8）中，（FVar）替换self通过它所引用的对象，设置从h到b的间接。（9）在第（9）款中，删除部分（FRed）。步骤（10）是另一个功能扩展（FC）。在最后一项约简中没有redex，即。e. 它是正常的形式。结构的共享出现在上面的例子中，因为e。G. [[O||b在推导的某些项中出现了几次。4.1图6中的对象表示76D. Doughnut等人理论计算机科学电子笔记127（2005）57本节中的示例体现了关于语言设计和实现的某些选择（例如重要的是要强调，这些选择是