Lambda项的暂停符号及其实现：逻辑框架的显式替换

35网址：http://www.elsevier.nl/locate/entcs/volume67.html14页Lambda项的暂停符号及其在元语言实现GopalanNadathur1;2计算机科学与工程系明尼苏达大学Minneapolis，MN 55455，美国摘要近年来出现了许多元语言和逻辑框架，它们使用lambda演算的术语作为数据结构。一组常见的问题管理的适用性的一个代表性的lambda条款在实施这样的系统：-可转换性必须很容易识别，共享reduc- tion步骤，长期遍历和长期结构必须是可能的，比较和unication操作应有效地支持，它应该是可能的，以检查嵌入在抽象的条款。lambda演算的显式替换符号为实现这些要求提供了基础我们在这里讨论与使用这样一种符号有关的问题|Nadathur和Wilson悬记法|以这种身份。这种表示法已经在两个重要的实际系统中使用：NewJersey编译器的标准ML和Prolog的Teyjus实现。我们揭示了这种符号的理论性质，突出实用的考虑，在其使用中实现操作，如减少和union，并讨论其关系，其他明确的替代符号。关键词：逻辑框架，显式替换，悬记法1引言元语言和逻辑框架操纵各种符号对象，如公式、程序、证明和类型，其结构自然涉及绑定的概念已经发现Lambda术语在捕获此类对象的抽象语法方面是有用例如，假设我们希望表示公式8x（（px）_（qc）），其中p和q是谓词1 这项工作得到了美国国家科学基金会CCR-0096322的部分支持2 电子邮件地址：gopalan@cs.umn.edu2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。36C是常量，C是常量。注意到量化器扮演着确定作用域和作出谓词的双重角色，这个公式的基本结构可以用lambda项（all（xor（（p x）;（qc））来捕捉;在这个项中，all是表示泛量化的构造函数，或者是表示析取的构造函数。在这种表示中，绑定的显式处理使得公式上的几个逻辑运算的实现简单而透明地正确。因此，用t实例化由项（all P）表示的公式中的quantier的任务通过写项（P t）立即实现。实际的替换是通过对lambda项的-归约运算进行的，具有所有必要的重命名。类似地，对结合敏感的公式的结构分析可以通过增强的单阳离子操作来执行。例如，假设我们希望认识到给定的公式是在一个析取上具有单变量的公式，其中定量变量不出现在第二个析取中。这个属性可以通过尝试将表示它的术语与“模板”（所有（x或（（P x）; Q））统一起来来确定，其中P和Q是可实例化的变量。变量Q在这里不能被替换，以致第二个析取词依赖于quantier，因此只能与“正确”的项匹配。当然，这种高阶抽象语法的编程便利性必须由相关元语言或逻辑框架实现中的lambda术语的有效表示来补充。虽然lambda术语实现在函数式编程上下文中一直很受关注，但目前这些术语的内涵使用对适当的表示提出了新的限制。因此，lambda项的比较必须是可能的，因此它们的结构不能在编译过程中被牺牲。在更详细的层面上，lambda项之间的相等概念必须忽略用于绑定变量的特定名称由于这个原因，表示必须支持快速确定身份直到可转换性。 另一个重要的操作是要实现高效是-减少。由于我们稍后讨论的原因，相对于此操作，必须满足两个要求：应该可以惰性地执行由-收缩生成的替换，并且可以渗透这样的替换以及在抽象上下文中执行-收缩。最后，高阶union计算是许多元编程任务的核心，必须考虑元变量的处理和在其实现中重要的操作lambda项的适当内涵表示的一个很好的起点这种表示法消除了绑定变量的名称，从而简化了以重命名为模的身份检查。建立在de Bruijn方案上的显式替换符号[1，2，4，8，13]为满足其他几个提到的要求提供了基础。这些符号的具体特征是不同的，必须以具体的方式进行选择。37部署在元语言实现的上下文中。本文揭示了在这种情况下，从我们的经验，在实现语言Prolog的一些重要的问题。我们围绕Nadathur和Wilson的暂停符号进行讨论，据我们所知，这是唯一一个在两个实际实现任务中使用的符号[12，14]。然而，我们的一般性意见适用于其他计划，以及我们还比较了不同的符号在最后。2暂停符号由收缩不同的赎回权引起的替代行走的组合可以对效率产生重大影响。因此，假设我们希望实例化由（all（x（all（yP）表示的公式中的两个量化器，其中P表示未指定的公式，其中项t1 T2。假设deBruijn表示，这样的实例通过两个约束实现，实际上需要t2 和t1 被替换为P中的第一个和第二个自由变量，并且所有其他自由变量的索引被递减2。每一个替换都涉及到遍历同一个结构|P的结构|如果它们能一起完成，那就太好了。 研究表明，通过系统地利用这一思想，结构遍历在实践中可以大大减少，在某些情况下可以减少到原来的八分之一[9]。现在，以这种方式组合遍历的关键能力是暂时挂起由-收缩生成的替换。 在一个条件下，所有的赎回都可以在一个单一的术语，这种延迟的替代可以内置到减少程序通过特设设备。然而，在所考虑的情况下，两个量化实例化是只能增量地考虑的实例化，并且进一步地，需要在遇到引起第二redex的抽象之前处理中间结构因此，导致共享的结构在对归约过程的单个调用中并不都是可用的，并且在P上的替换的显式编码似乎是实现这种好处所必需的。通过使用环境，在函数式编程语言的实现中，替换被延迟，并且可能出现将这种环境简单地反映到术语结构中应该满足当前目的。然而，问题是，当lambda术语用于表示对象时，可能需要检查嵌入在抽象中的结构。例如，考虑确定在形式为（all R）的公式中实例化量化器所产生的项是否具有由模板（all（xor（（P x）; Q）捕获的形状的任务;我们假设R在这里表示未指定的项，并且P和Q是可实例化的变量。一个肯定的判定涉及在对应于一个量化器的抽象之下进行一个替换，然后检查嵌入的结构是否是一个析取。在进行这种计算时，有必要38考虑转换或de Bruijn表示中的等效重新编号，将其合并到环境模型中需要小心。还要注意的是，R的实际形式可能需要在捕获量化作用域的抽象中执行-收缩，以揭示其顶层逻辑结构。这种计算使环境的结构更加悬挂符号体现了对上述问题的解决方案。形式上，它包含一组称为术语、环境和环境术语的表达式，其语法由以下语法规则定义的类别h Ti、h E i和h ET i给出，其中h C i、h I i和h N i分别表示常数、正数和自然数：hTi： ： =hCij#hIij （ hTihTi ）j （ hTi ）j[[hTi;hNi;hNi;hEi]]hEi： ： =niljhETi ： ：hEijffhEi;hNi;hNi;hEigghET i：：=@hN i j（hT i; hN i）j hhhET i; hN i; hN i; hE iii.对de Bruijn项进行必要的添加以产生悬置项的是形式[[t; ol; nl; e]]的表达式，其中t是项，e是环境。 这样的项被称为悬置，表示项t，其中以由环境e确定的方式替换了项t的第一个变量，并且其剩余的绑定变量被重新编号以反映t过去出现在ol个抽象中但现在出现在nl个抽象中的事实。在最简单的形式中，环境的元素要么是由缩写生成的替换项，要么是表示在外部上下文中持久存在的抽象的虚拟条目然而，索引的重新编号可能必须在替换期间完成，并且为了对此进行编码，每个这样的环境元素由称为其索引的相关抽象级别进行注释。这样的suspension必须满足一定的良构性约束，这些约束在我们对其内容的非正式理解中具有自然基础：在形式[[t; i; j; e]]的表达式中，环境e的“长度”必须等于i，e中条目的索引必须是非递增的，并且它们必须以j为界。该符号还允许替换的组合：形式fe1;i;j;e2gg的表达式表示e1中包含的替换的组成 和e2 并且hhhet;i;j;e2i对应于通过在e2中的替换而修改的项e t。 i，j，环境的长度和所组成的环境中的项的索引必须满足某些约束，这些约束自然地产生于对简单环境的限制。由于篇幅有限，这里无法讨论这些方面，但[13]中有详细的论述通常的-收缩运算在悬记法中分两个阶段实现：生成和随后的置换渗透这个过程由重写规则的集合形式化地描述这些规则分为三类：产生悬浮的s规则，渗透替换的阅读规则和允许中间悬浮组合的合并规则。这些规则类别是3911 2 1 2 12112221122（s）（（t1）t2）！[[t1;1;0;（t2;0）：：nil]]Fig. 1. 的的统治(r1)[[c; ol; nl; e]]！ c，如果c是常数。(r2)[[#i; 0; nl; nil]]！#j，其中j = i +nl。（r3）[[#1; ol; nl;@l：：e]]！ #j，其中j = nl l。（r4）[[#1;ol;nl;（t;l）：：e]]！[[t;0;nl0;nil]]，其中nl0 =nlll.（r5）[[#i;o l;n l;et：：e]]！[[#i0;ol0;nl;e]];其中i0 =i1和o l0 =ol1，提供i>1。（r6）[[（t1 t2）;ol;nl;e]]！（[[t1;ol;nl;e]][[t2;ol;nl;e]]）。（r7）[[（t）;ol;nl;e]]！（[[t;ol0;nl0;@nl：：e]]），其中0 =ol+ 1和n l0 =nl+1。图二. 阅读规则（m1） [t;ol;nl; e]];ol;nl; e]]！[[t;ol0;nl0;ffe;nl;ol; egg]]，其中0 =ol+（ol： nl）和nl0 =nl+（nl： ol）。（m2） ffni l;n l;0;nilgg！ 尼湖（m3） ffni l;n l;ol;et：：egg！ffnil;nl0;ol0;egg，其中nl;oll，nl0 =nl1和o l0 =ol1。(m4)ffnil; 0; ol; egg！e.（m5） ffet：：e1;nl;ol;e2gg！ hhet;n l;ol;e2ii：：ffe1;nl;ol;e2gg. （m6）hhet; nl; 0; nilii！ et.(m7)hh@ n; nl; ol;@ l：：eii！ @ m，其中m = l+（nl：ol），条件是nl = n +1。（m8） hh@n; nl; ol;（t; l）：：eii！ （t; m），其中m = l+（nl：ol），条件是nl = n +1。（m9） hh（t;n l）;nl;ol;ett：：eii！ （[[t;ol;l0;et：：e]];m）其中l0 =ind（et）且m=10+（nl： 01）。（m10）hhet;nl;ol;et0 *eii！hhet;nl0;ol0;eii;其中nl0 =nl1和o l0 =ol1，提供了nl6 =ind（et）。图三. 合并规则40分别在图1、2和3从模拟约简的角度来看，合并规则实际上是然而，如果没有它们，就不可能组合替换和执行它们的行走。定义2.1一方面由读合并规则生成的悬置表达式上的（一步）归约关系，41RMRMRM另一个分别由RM和RMs表示。关于de Bruijn项的通常的-压缩关系记为。最后，我们用R表示关系R的自反传递闭包。读取和合并规则旨在暴露任何给定项下的de Bruijn项，我们希望它们总是成功地这样做。下面的命题，在[13]中证明，表明情况就是这样。命题2.2关系rm是强终止的，即所有这样的约化序列都是nite。形式为[[t;ol1;nl1;e1]];ol2;nl2;e2]];ol3;nl3;e3]]的项可以通过规则m1的两次使用而被“at-tened”成单个暂停。但这注意力可以通过两种方式来实现|byrstcomposinge1 和e2，然后将结果与e3进行比较，或者首先比较e2和e3，然后比较e1 结果|我们希望两种情况下的结果都一样。一些显式的替换演算通过包含一个组合替换的结合性规则来在我们的微积分中，这个性质是其他规则的结果：命 题 2.3 设 a 和 b 是 fffe1;nl1;ol2;e2gg;nl2+ （ nl1 ）：ol2）;ol3;e3gg和ffe1;nl1;ol2+（ol3：nl2）;ffe2;nl2;ol3;e3gg gg，分别 那么有一个环境r使得r和bR.我们想要一个更强的性质，即rm范式的存在性成立：这些形式对于任何给定的表达式都应该是唯一的。根据命题2.2，足以证明rm是局部相合的。 为了达到这个目的，我们需要考虑规则左边的非平凡重叠，并证明与这些重叠对应的临界对可以重写为一个共同的形式。相关的重叠是在m1和每个读取规则之间，m1和其自身之间以及m2和m4之间。其中唯一复杂的情况是重叠在m1和自身之间。然而，命题2.3确保了在这种情况下将简化为一个公共形式。因此，我们有命题2.4关系rm是局部连续的，因此是连续的。我们将描述的rm正规形式的一个表达式e在悬浮演算由je j。之间的对应关系约化关系的de Bruijn条款和悬浮条款，然后可以说如下。命题2.5设t是悬置演算中的一项。 如果tSr然后jt jj r j。 相反，如果j t js，然后t s。rms从这个命题还可以得出rms是连续的。42S（0）（（[[t;ol+1;nl+1;@nl：：e]]）t）！[[t;ol+1;nl;（t;nl）：：e]]3取消合并规则合并规则提供了一种用于组合替换的通用机制。然而，它们的强大之处在于对组合的细致处理，这对于实际实现来说有点麻烦。 出于这个原因，值得探索在更粗糙、更有效的派生规则中捕获它们的共同用途的可能性。我们观察到以下两种情况，这种方法可以有效地应用。第一种情况对应于由嵌套-赎回的收缩引起的替换的组合 作为说明，我们可以考虑项（#1#2）#3）t2））t3）的约简，其中t2 和t3 是任意的deBruijn项。在一个最左-最外的约化机制中，第一步是使用s规则来产生悬浮[[（#1#2）#3）t2）;1;0;（t3;0）：：nil]]：阅读规则现在将被使用几次来产生这个术语（（[（#1#2）#3））;2;1;@0：：（t3;0）：：nil]]）[[t2;1;0;（t3;0）：：nil]]）：在这个阶段，将再次使用 s规则，产生 项[（ （#1#2 ）#3））;2;1;@0：：（t3;0）：：nil]];1;0;（[[t2;1;0;（t3;0）：：nil]];0）：：nil]]：现在可以使用m1规则组合这两个环境，生成[[（#1 #2）#3））;2; 0;ff@0：：（t3;0）：：ni l;1;1;（[[t2;1;0;（t3;0）：：ni l]];0）：：ni lgg]]。使 用 其 他 合 并 规 则 ， 该 项 可 以 简 化 为 形 式 [[ （ #1#2 ）#3））;2;0;（[[t2;1;0;（t3;0）：：nil]];0）：：（t3;0）：：nil]]其优点是对其环境的“查找”是简单的。从第二次使用s规则开始到最终中止项结束的重写步骤序列可以被折叠成一个更“强大”的规则的使用：3s1 2 1 2这个规则可以被证明是悬浮演算的一个派生规则。使用它的优点是可以避免中间合并步骤刚刚考虑的例子实际上说明了通过合并实现的结构行走中的共享和约简中的共享之间的权衡。在第一次使用s规则之后，我们选择上面的方法来传播替换。我们可以选择重写内部的s-redex，[（#1#2）#3））;1;0;（t2;0）：：ni l]];1;0;（t3;0）：：ni l]]。在基于图的归约实现中，遵循本课程可确保3 这个规则有一个未说明的限制条件，它适用于使用我们的归约规则从de Bruijn导出的所有项：e中项的索引必须小于@nl的索引。430SR注意，为了完全实现这种共享的好处，有必要在（（#1 #2）#3）的结构上的单独因此，在两种不同的还原选择之间存在着一个两难的选择然而，只有当存在共享赎回的真实案例时，这种困境才是真实的我们的实验在实践中很少发现这种情况[9]，表明倾向于尝试结合结构遍历的方法。合并规则有用的第二种情况是，当索引需要在抽象上下文中替换的挂起中重新编号时。我们通过继续减少项（#1#2）#3）t2））t3）来说明这一点。使用我们离开o的地方的阅读规则（#1[t2;1;0;（t3;0）：：nil]];0;1;nil]]）[[#3;3;1;@0：：（[[t2;1;0;（t3;0）：：nil]];0）：：（t3;0）：：nil]]））：子项[t2;1;0;（t3;0）：：ni l]];0;1;ni l]]对应于两个悬置中的t2embedded，外部悬置表示内部悬置中自由变量的索引的“提升”，其插入抽象内部是必要的。 使用合并规则，所指示的子项可以被重写为[[t2;1;1;（t3;0）：：ni1]]，从而将不同的替换合并到一个环境中。合并规则的这种使用也可以反映为派生规则：（碰撞）[t;o l;nl;e]];0;nl0;nil]]！[[t;o l;nl+n l0;e]]。在实际的归约实现中，这条规则实际上可以被归纳为阅读规则R4的应用。碰撞规则的缺点是，它再次倾向于在结构遍历中共享，而不是在约简中共享。在这里，约简共享中的实际损失也是de Bruijn表示和实现约简中绑定变量的基于名称的表示之间的区别：使用bump规则，de Bruijn方案中的额外重新编号工作被包含到嵌入项的结构的已经必要的遍历中，但可能会损失约简共享。和以前一样，我们的观察是，在实践中，很少有真正的机会分享减少，这表明只要适用，就倾向于使用碰撞规则，并且使用de Bruijn方案减少的缺点也定义3.1我们用r 0表示由读数和碰撞规则定义的归约关系。 当还包括s和s规则时获得的r_d由r_0表示。下面的命题显示了我们导出的规则的连贯性。建议3.2R0r是连续的且强终止的。Fur-因此，对于任何项t，如果tr然后trms R. 相反，如果trms r，然后在S044s，rS.最后rS0秒are项s和s00rrm00rms是骗-Suent。将de Bruijn项还原为（头）正规形式可以进行只使用定义r0关系的规则。主要缺点不使用合并规则的原因是，一些分享结构的机会，真正的散步可能会错过。事实证明，在最左最外的归约实现中，实际上很少有这样的情况44可实例化变量、并发性和统一性挂起表达式的当前语法不允许可实例化或Meta变量。这些变量可以以两种形式之一引入。在第一种形式中，这些变量将被视为与普通lambda演算相同。特别是，它们的实例化必须尊重作用域的概念因此，如果X是在抽象绑定x1; ：;xn中出现的可实例化变量，则它不能被依赖于任何抽象的结构替换。这种逻辑视图实际上是模式识别应用程序所需要的视图。例如，项（all（xor（（P x）; Q）用作具有在析取上的泛量化的公式的识别器，该析取的右部分独立于量化，这正是因为Q不能被实例化为依赖于x的形式。将这种可实例化变量的视图构建到悬挂符号中很容易。在语法级别，我们简单地将术语的规则更改为hTi ：：=hVijhCij#hIi j（hTihTi） j（hTi） j[[hTi;hNi;hNi;hEi]]其中hV i表示这些变量的类别。为了说明这些变量不能被替换产生的事实，- 收缩，我们添加以下内容到我们的阅读规则：（r8）[[x; ol; nl; e]]！x，假设x是可实例化变量。这 个 规 则 类 似 于 读 取 常 量 的 规 则 。 因 此 ， 不 难 看 出 conuence 和termination属性自然地扩展到包含新变量的语法。还要注意的是，第3节中讨论的重写规则的较小集合可以将包含这些变量的项简化为范式。另一种可能性是将可实例化变量视为占位符，任何格式良好的术语都可以嫁接到占位符上。这种“可移植的”变量最初出现在模式匹配应用程序中。然而，这些应用程序的必要约束可以通过适当的预处理来建立因此，考虑模板（all（xor（（P x）; Q），在de Bruijn记法中将被写为（all（（or（P#1）Q）。 此项可以转换为（all（（或（[[P;0; 1; nil]];#1）[[Q;0; 1; nil]]）。通过这样4 事实上，如果削减是唯一有条件的行动，就不应该有这种情况。所有观察到的情况都源于对后文讨论的Meta变量的单一替换使得t和s45SS1m1m k1m将P和Q嵌入到悬浮物中，我们将它们从对外部抽象的依赖中隔离出来。这种观点也可以被纳入悬挂符号。术语的语法需要像以前一样完全修改。 然而，与先前的情况相反，不需要添加新的重写规则。其基本原理是，在可实例化变量的实例化本身已知之前，可实例化变量上的归约替换的效果是未知的。在这些变量已经被实例化的点处，与项的其他形式有关的重写规则支持计算约简的效果。我们记为byrm，r0，rm和r10先前看到减少关于扩大的SYN税的关系。而rm和r0 我必须仍然强烈地终止、并发属性更成问题。关系r0是，事实上，不是这样。因此，考虑项（X）t1））t2），其中X是一个可即时变量，而t1 和t2 是标准形式的术语。有三个不同的术语可作为这方面的“正常”形式：[X;1;0;（t1;0）：：ni1]];1;0;（t2;0）：：ni1]]，[X;2;1;@0：：（t2;0）：：nil]];1;0;（[[t1;1;0;（t2;0）：：nil]];0）：：nil]]，和[[X;2;0;（[[t1;1;0;（t2;0）：：ni 1]];0）：：（t2;0）：：ni 1]]。添加合并规则改变了图片：前两项然后减少到最后一项。事实上，可以证明以下命题：命题4.1假设一个包含可移植变量的项集合，关系rm和rms 两者都是一致的。证明这个命题的关键观察是命题2.3中描述的组成替换的结合性继续成立。对Meta变量的可移植解释的兴趣来自[5]中描述的利用这些变量的高阶union的新方法。（类型化的）lambda演算的通常过程[7]是基于将任何给定的单性问题简化为一组以下形式的方程：X1 * xn（Xt1 * tm）=x1 * *xn（@s1 ： ：sl）其中X是一个可实例化的变量，@是一个常量或变量x1; ：;xn中的一个。为了求解这样一个方程，w： w （@0 （Hw* *w） ：（Hw* *w ）），其中@0 是@或w; ：; w和H; ：; H中的一个是新的实例-1m1k能够变量，为X设定。这样的替换试图让头部的这两个术语是统一的，以匹配，而延迟决定有关的论点。事实上，替换项的参数被选择为不排除对原始项的参数的任何依赖性。例如，如果@0=@，对应于y，l=k，则这种替换将把唯一化问题简化为同时求解方程之一X1 * xn（Hit1 * tm）=x1 * xnsiS46对于1μL。注意，Hi 可以自由地“使用”密码ntst1; ：;tm 以一种被认为是必要的方式。上述变换涉及到一个复杂项的构造、多个-换算的收缩以及它们的替换项的计算 使用显式替换和“可移植”变量，可以考虑减少依赖信息渗透所涉及的影响。将w1一词 * *wmY其中Y是X的可移植变量，最初的方程可简化为：X1 ：： ：xn[[Y;m;0;（tm;0）：：： ：（t1）：：ni 1]]=x1 * *xn（@s1：sl）。注意，所考虑的X的替换只有在Y可以稍后被替换为可能包含变量w1; ：;wm的某个值时才有意义，即，Y必须是可移植的。现在，在这种减少之后，形式为（@H1）的项 ：Hl）可以被用于Y，使得方程被变换成以下形式的方程：X1 ： xn[[Hi;m;0;（tm;0）：（t1）：：ni 1]]=x1 * xnsi对于1μ L。明显地，可以避免涉及应用的复杂项的形成以及仅仅为了传递依赖性信息而进行的后续约简。上述讨论实际上表明了实现高阶union的不同方法之间的权衡。基于可移植变量的方法具有上述优点，但它也需要使用更完整，更复杂的环境合并规则集。一个内部的观察是，新的方法，uniation主要取决于（头）正常形式，不包含嵌套的悬浮在顶部水平的生成。一种可能性是，一个特殊的控制方案，减少了一套重写规则，将确保只有这样的形式产生。5与其他显式替换演算的比较显式替换符号有三个令人垂涎的属性：在包含可移植Meta变量的情况下的连续性，组成替换的能力其中，替换的可组合性对于元语言实现来说似乎是最重要的。不幸的是，大多数显式替换演算似乎不包括这个功能。特殊的结石也会牺牲其他特性。微积分保持了很强的正规化性[2]，但它不接受Meta变量。 s-演算允许Meta变量，并且即使有这种加法也是一致的[8]，但不提供强的归一化能力[6]。wso-演算单独both承认Meta变量并保持强的可正规化性[4]。两种演算允许替换的合成，- 微积分[1]和暂停符号。有几个相似之处-471221 211 22我们希望在一篇较长的论文中通过翻译函数来证明这两个演算之间的关系在这里，我们仅限于提及两个可能对低级实现任务有重要意义的差异。首先，在我们的演算中，似乎更容易分离出基于函数的重写规则，从而识别出更容易在实践中使用的子集，如第3节中所述。第二个区别涉及对环境中的项的索引的调整进行编码的方式。在我们的表示法中，这些不被显式地维护，而是从必须被代入的项的嵌入水平与环境中的项记录的嵌入水平之间的差异获得。因此，考虑形式为[[t;1;nl;（t;nl0）：：ni l]]的一个扩展项。这表示一个项，它是通过替换t2得到的 对于t1中的第一个自由变量 （以及修改其他自由变量的索引）。然而，t中自由变量的指数我一定是被（nl）弄得精疲力竭了。N10）进行这种替换。 在-演算中，自由变量的索引所需的因此，上面所示的暂停项可以表示为[[t;1;nl;（t;（nl实际上，在这一项中，只需要确定对t1中的自由变量的平差，就可以使用新、旧的边界条件。 其索引大于旧的EMBEDDING级别，并且封装这种调整的用于表示环境的设备简化了实际使用的符号。这种方法的缺点是，在抽象下移动替换时，环境中的每个术语都是受影响的。因此，在本发明中，从一个项如ke[[（t）;1;nl;（t;（nl nl0））：：nil]]，我们必须产生以下之一：形式（[[t;2;nl+1;@1：：（t;nln 10+1）：：n 1]]）。 相反，使用我们的符号，只需要向环境中添加一个“dummy”元素，并对整个术语的嵌入级别进行局部更改。微积分和悬挂符号都允许可移植的Meta变量。已知前一种演算不能保持强的归一化性[10]。对于暂停符号，这是一个开放的问题。我们猜想它确实保持了这个性质。6结论我们在本文中公开了悬挂符号，着眼于它在元语言实现中的使用。在这次讨论中提出的某些问题需要更全面的处理。在第4节中，我们考虑了利用我们的符号增加可移植的Meta变量来实现高阶union的可能性。 实际上，需要详细说明这一程序，并在执行层面与不使用这些变量的方法进行仔细比较。Meta变量的不同处理方法的好处可能取决于生成替换的方式，因此，实验还应考虑高阶单元的特殊情况，如所述48在[11]中。在另一个方向上，它是有趣的，以显示之间的联系，悬挂符号和微积分更完整，可能通过它们之间的翻译。最后，悬记法是否保持了强规范化性的问题需要解决。我们希望在本文的后续部分考虑其中的一些方面引用[1] M.阿巴迪湖Cardelli，P. L. Curien和J. - J·莱维。显式替换。Journal ofFunctional Programming，1（4）：375{416，1991.[2] Z. Benaissa，D. Briaud，P. Lescanne，and J. Rouyer-Degli.，一个演算的明确的替代，保持强规范化。Journal of Functional Programming，6（5）：699{722，1996.[3] N. 德布鲁因 Lambda演算符号与无名的假人，一个工具，自动公式操作，与应用程序的教会-罗瑟定理。Indag. 数学，34（5）：381{392，1972.[4] R.大卫和B。纪尧姆具有显式弱化和显式替换的A -演算. 出现在计算机科学中的数学结构，2000年。[5] G. Dowek，T. Hardin和C.基什内尔通过显式替换实现高阶单正离子。信息与计算，157：183{235，2000。[6] B.纪 尧 姆这 种 微 积 分 不 能 提 供 强 的 标 准 化 .Journalof FunctionalProgramming，10（4）：321{325，July2000.[7] G.休特类型演算的一个统一算法. 理论计算机科学，1：27{57，1975。[8] F. Kamareddine和A.用显式替换将保强规范化的-演算扩展为开项的连续演算。 Journal of Functional Programming，7（4）：395{420，1997.[9] C. Liang和G. Nadathur在lambda项的内涵表示中的折衷。In S. Tison，编辑，重写技术和应用，计算机科学讲义。Springer-Verlag，2002年7月。(To出现）。[10] 保罗-安德烈和梅利斯。类型化-带有显式替换的演算不能终止。In M.Dezani-Ciancaglini 和 G.Plotkin ， 编 辑 ， TypedLambdaCalculiandApplications，计算机科学讲义第902号，第328页。Springer，1995年。[11] D.米勒一种逻辑程序设计语言，具有抽象化、函数变量和简单的统一性。Journal of Logic and Computation，1（4）：497{ 536，1991.[12] G. Nadathur和D.J. Mitchell系统描述：Teyjus|一个基于编译器和抽象机的Prolog实现。In H. Ganzinger，编辑，Automated Deduction{CADE-16，编号1632，在Arti cial Intelligence的讲义中，第287页{291。Springer-Verlag，1999年7月。49[13] G. Nadathur和D.S.威尔逊lambda术语的符号：环境的一般化。 理论计算机科学，198（1-2）：49{98，1998.[14] Z.绍角，澳-地League和S. Monnier.实现类型化中间语言。在Proc.1998ACM SIGPLAN International Conference on Functional Programming中，第313页{323. ACM Press，September 1998.