重写演算的命令式版本Rogue到基础系统MicroRogue的演进

理论计算机科学电子笔记117（2005）69-87www.elsevier.com/locate/entcs从Rogue到MicroRogue放大图片作者：James C. Brodman，JonathanHseu，Bill Kinnersley部计算机科学与工程，华盛顿大学在圣路易斯。圣路易斯美国密苏里州路易斯市，网址：http://cl.cse.wustl.edu/摘要重写演算是结合λ -演算和项重写思想而提出的一个基础系统。重写是显式的，在这个意义上，规则必须显式地应用于术语以转换它们。本文从重写演算的命令式版本Rogue开始。然后，它展示了Rogue本身如何通过一个更基础的系统MicroRogue方便地实现。 MicroRogue使用一组全局一阶规则重写术语。可以在作用域中启用、禁用和动态添加规则，可以推送和弹出规则。MicroRogue还提供了指定评估顺序的机制。使用这些原语，Rogue解释器可以在不到40行的MicroRogue代码中实现保留字：重写微积分，动态规则，求值顺序1介绍重写演算已经被提出作为结合λ演算和项重写的中心思想的基础系统[6，7]。重写是显式的，在这个意义上，规则必须显式地应用于术语以转换它们。这不同于传统的项重写方法，在传统的项重写方法中，项通过重写规则的给定全局集合中的任何一个在其任何子表达式处不确定地经受变换（参见例如，[4，9]）。事实上，重写演算开发的最初动机之一是为实现传统项重写的系统提供操作语义[6，7]。本文的出发点是重写演算的命令式版本，称为Rogue。Rogue已被用于实现决策过程[12]，以及其他符号程序，包括证明检查器、类型1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.06.02870A. Stump等人理论计算机科学电子笔记117（2005）69检查器，以及用于词法分析器和解析器生成的标准自动操作算法。在这些应用程序中，代码比标准语言中的实现更简洁。简洁是有价值的，不仅仅是出于美学原因：最小化可信计算基础对于安全应用是重要的（参见，例如，[2，3]）。这项工作的主要关注点是显示如何流氓本身可以简洁地实现在一个更简单的重写系统，称为MicroRogue。MicroRogue类似于术语重写的传统实现，因为它使用全局规则集重写术语。 然而，这些规则仅适用于术语的顶层。规则是有序的：如果有多个规则适用，则使用排序中最大的规则。甚至不像传统的术语重写，规则可以动态地启用和禁用。受Visser工作的启发，我们还允许动态添加新规则[13]。规则被添加到作用域中，可以推送和弹出。最后，MicroRogue提供了指定评估顺序的机制。使用MicroRogue的原语，Rogue解释器可以在少于40行（非注释，非空白）的MicroRogue代码中实现。从实用的角度来看，这是有吸引力的，因为它使Rogue的开发比在工业非符号语言（如C++）中更容易。从更理论的角度来看，从Rogue到MicroRogue的转变是由于观察到重写演算的操作语义的定义包含几个基本上是简单重写规则的子句。这表明，用于实现Rogue或重写演算的元语言应该基于某种重写。这似乎有些奇怪，因为这些已经被认为是基础重写语言！MicroRogue通过提供一小部分重写原语来解决这种紧张关系，这些原语足以实现Rogue的操作语义。本 文 的 其 余 部 分 组 织 如 下 。 第2 节 描 述 Rogue 。 第 3 节 讨 论 了 导 致MicroRogue从Rogue发展的力量。第4节定义了MicroRogue，第5节介绍了Rogue在MicroRogue中的实现。2流氓T：：=cxnullT1.T2T1@T2T1，T2T1→T2T1T2T1|T2<$T1.T2：= T3<$α x.TFig. 1. Rogue的语法Rogue编程语言本质上是非类型化的A. Stump等人理论计算机科学电子笔记117（2005）6971重写微积分[6，7]。 重写演算中的关键思想是使重写规则的应用显式化，并使重写规则（实际上是重写规则集）作为第一类数据传递成为Rogue固定了一个特定的模式匹配算法和评估策略，重写演算的定义在很大程度上将其作为可定制的参数。重写演算中的流氓差异在于添加了一个显式的作用域运算符来声明变量，并添加了可变表达式属性和递归定义1。递归定义只是为了方便，因为重写演算没有它们已经是图灵完备图1给出了Rogue的语法。操作员按从最紧到松的顺序排列。所有二元运算符都是右结合的，除了“@”和“。“，它们是左关联的。 我们把α x.E写成x ^E，当x是一个变量或变量时，允许x（y）作为x@y常数2.1流氓基础知识Rogue的操作语义的正式定义现在，我们通过一些基本的例子来介绍这种语言。表达式通常按最左、最内的顺序计算，除了计算不在箭头表达式的以下是基本规则应用于术语的三个一步评估1. （a-> b）@ a=> b2. (f(a)->g（b））@ f（a）=> g（b）3. (f(a)->g（b））@ f（c）=> null前两个应用程序成功，因为正在应用的规则的左侧与规则所应用的术语相同。第三个应用程序失败（为null），因为f（a）与f（c）不相同。 注意如如上所述，f（a）只是f@a的替代符号。 现在考虑在对具有变量的规则的应用进行一步评估1. （ x^ x-> x）@ a=> a2. （x^y^ x，y-> y，x） @（a，b）=>（b，a）3. （x^ f（x，x）-> g（x，x））@ f（c，c）=> g（c，c）4. （x^ f（x，x）-> g（x，x））@ f（c，d）=> null前三个规则成功，因为应用的规则的左侧都匹配目标术语。例如，f（x，x）用替换[c/x]（“replace x by c”）匹配f（c，c）1显式作用域运算符是新的，仍在开发中（参见[1]）。72A. Stump等人理论计算机科学电子笔记117（2005）69operator声明x是可用于实例化的变量。但是模式f（x，x）和目标f（c，d）没有匹配的替换，因为模式需要相同的子表达式，但是c和d在语法上是不同的。以下是演示逗号使用的评估：1.（x^（a ->b），（x -> x））@ a=>（a-> b）@a，（x^x-> x）@a=>b，a2. （（a->b），（c->d））@ a=>（a -> b）@a，（c -> d）@a =>b，null=> b我们将逗号表达式从左边（但在Rogue中，不是从右边）分布在应用程序上。因此，在第一个例子中，我们将两个规则都应用于a，并将结果收集在逗号表达式中。如第二个例子所示，如果其中一个规则（c-> d）不匹配，那么结果是（b，null），这就减少到只有b。bar算子本质上是重写演算的第一个算子[7]。条形表达式的应用程序通过应用与目标匹配的第一个（从左到右）规则进行评估1.（x^f（x）-> x|x-> a）@ f（b）=> B2.（x^f（x）-> x|x-> x）@ g（d）=> g（d）Rogue还有一个懒惰箭头（=>），这对于元编程和反射非常有用它允许对未求值的表达式进行操作（我们在这里包括算术运算，我们在正式的演示中省略了这些运算，但它们可以很容易地被包括在内）：1.（x^y^x为oh-> 年）的@（null，3）===>（x^y^x为oh-> 年）的@3=>numb2. （x^y^x，y=>f（x），y+y）@（null，3）===>f（null），3 +3=> f（null），6在第一个例子中，（null，3）首先被简化为3，这与模式（x，y）不匹配。因此，整个应用程序减少到null。但是在第二个例子中，因为应用了一个惰性箭头表达式，所以我们没有reduce（null，3）。然后，这个未求值的表达式匹配模式（x，y），并且求值成功地继续。2.2编程示例本节给出了一些在Rogue中编程时有用的示例首先，我们有if-then-else和if的定义。 这些都是使用懒惰箭头（lazy arrow，简写为IARROW）来定义的，因为if部分必须在其他部分之前进行计算。如果a的值为非null，则if（a，b）的值为b所做的任何事情，否则为null。A. Stump等人理论计算机科学电子笔记117（2005）6973ite：=x^y^z^x，y，z=>（null->z| q^q ->y）@ x if：=x^y^x，y => ite（x，y，null）我们还可以定义布尔运算和等式;这些定义允许合取和析取分别具有任意数量的合取和析取。此外，如果在从左到右的所有合取词的评估中发现评估为假的合取词，则不评估该合取词右侧的合取词。例如，and（null，（a：= b））计算为null，而不会导致a被设置为b。和：= p^q^ p，q => ite（和（p），和（q），null）|p-> p;; not：= p^null -> 1;;或 ：= p^q^p，q => ite（或（p），1或（q））|p-> p;;eq：= x^x，x -> 1;;另外两个定义证明非常有用。第一个是模式匹配的let语句。有了这个定义，如果不存在使模式x匹配目标表达式y的替换σ，则let（x，y，z）的计算结果为null;否则，它的计算结果为σ（z）。let：= x^y^z^x，y，z=>（x -> z）@y;;例如，令（x^f（x），f（3），x+4）的计算结果为7。最后的定义是一个我们称为apply（也称为map）的函数，它将一个函数应用于逗号树的每个元素。所以apply（x^x -> x+10）@（（1，2），（ 3，4）） 的 计算 结果为（（11，1,2），（13 ，14））。apply：= F^ F-> x^y^（x，y -> apply（F）@x，apply（F）@ y|null-> null |f（x）;2.3更丰富的例子我们考虑一个更复杂的例子，取自前面提到的决策过程的应用领域[12]。图2给出了union-find数据结构的find函数的Rogue代码[8，Chapter 22]。发现函数应该跟随使用findp属性存储的find指针，从元素x开始，直到它到达没有find指针的节点。后一个节点作为x的等价类的规范表示，并由find返回。如果x有一个find指针，它被修改为指向这个top节点。图中的Rogue代码接受元素x。然后，根据x的如果它递归调用find（x.findp），那么它随后修改x.findp回想一下，属性赋值的计算结果是被赋值的任何值，所以x.findp：= top的计算结果是top。 在另一种情况下，当x.findp为null时，代码首先设置74A. Stump等人理论计算机科学电子笔记117（2005）69find：= x^ x-> ite（x.findp，let（top^top，find（x.findp），（x.findp：=top）），null（x.rank：= 0），x）;图二. 使用路径压缩查找的x这是为了联合的代码（未显示）的利益。通过将null应用于该属性赋值，我们会导致值（0）丢失，因为null应用于任何东西都是null。所以我们得到（null，x）作为if-then-else的else部分，它的值为x。3关于MicroRogue本节解释了在实施和使用Rogue过程中产生的各种力量，这些力量将我们引向MicroRogue。MicroRogue的大部分功能直接来自于同时满足这些设计力量的尝试。3.1Rogue操作语义的重写Rogue和重写演算的定义包含了许多条款，看起来非常像传统的术语重写规则。例如，我们有以下规则：（r1，r2）@t=n（r1@t），（r2@t）null@t=nullx，null=xnull，x=x这些可以很自然地被视为术语重写规则，这表明一个好的实现Rogue或重写演算的元语言即使重写演算中的重写规则不直接映射到标准项重写中的重写规则（例如，重写演算中允许非正则规则），也是如此。由于重写演算本身是作为实现重写系统的基础而提出的，因此在某种意义上，描述它的元语言涉及重写似乎有点自相矛盾。也就是说，基础（重写微积分）似乎取决于它打算作为基础（项重写）的东西。为了解决这一紧张局势，我们寻求容纳：A. Stump等人理论计算机科学电子笔记117（2005）6975Force1启用Rogue的操作语义，使用重写规则来编写，例如（r1，r2）@t=（r 1@t），（r 2@t）。3.2定义和可变属性简单的定义，比如ite和上面的其他基本例子，看起来也像简单的重写规则。在评估过程中，无论何时遇到定义符号，都应由于定义是在Rogue程序的主体中添加的，Rogue的操作语义的定义查找表达式E1的属性E2的值也可以被认为是将E1.E2重写为其值。自然，由于属性可以动态设置，因此必须能够动态添加和修改规则，以使用规则实现属性分配。这些考虑导致了MicroRogue的另一种设计力量：Force2使用动态规则支持定义和可变属性。3.3评估顺序如果我们要在更基础的语言中实现Rogue罗格应用程序M@N必须仔细评估，因为如果M评估为懒惰箭头表达式，或以懒惰箭头表达式开头的bar表达式，则不应评估N此外，我们需要能够指定在某些位置没有评估发生;即，在箭头表达式的右侧。这导致：Force3启用对评估顺序的细粒度控制。3.4可回溯状态在实现一阶理论的无量化器公式的命令式决策过程时，重要的是能够根据命令回溯决策过程的所有状态[12，5]。这是因为这些决策过程与命题SAT求解器集成在一起，后者对目标的原子子公式的布尔赋值空间执行回溯搜索。SAT求解器可能决定从某些特定的分配中部分退出，在这种情况下，决策过程也必须回溯其状态以保持与SAT求解器同步。因此，至少对于这些类型的应用程序，具有以下内容非常有用：76A. Stump等人理论计算机科学电子笔记117（2005）69不：：=Eβ阳性T1→T2T1→T2 公司简介关闭 不别这样！T1;T2 T2型 α x.T超推POP-ENDCORE已完成POS：：=. - 是的NumListNumList ：：=N N. NumList图三. MicroRogue的语法Force 4启用对动态添加或修改的规则的回溯。4MicroRogueMicroRogue旨在满足前一节的设计要求，作为一种基础重写语言，适合实现Rogue和其他更高级的重写语言。MicroRogue表达式T的集合在图3中定义，其构造按照从最紧密绑定到最松散绑定的顺序给出。这些运算符都是非结合的，除了双引号和波浪号双引号，它们都是右结合的。假设兴趣的基本表达式E的集合这些可以使用一些运算符在常量和变量符号上构建。我们利用一组位置Pos，它们只是自然数的有限序列。它们用于控制不同形式的表达式的求值顺序。箭头表达式用于规则。他们要么是匿名的-mous（T1→T2）或named（i：T1→T2，其中i取自某个名称集合）。变量的作用域是用α表达式声明的，就像在Rogue中一样。分号和波浪号分别用于右和左排序。在每一种排序中，子项按从左到右的顺序进行评估。在右排序（在左排序（“左;”）中，它的计算结果是左子项的计算结果。如上所述，我们有一些构造来打开和关闭规则。我们现在转向构造T！MicroRogue的操作语义定义了在计算MicroRogue表达式期间如何更新某种状态。 这种状态有两个部分。有一组全局规则可用于表达式的顶级重写。还有一个单一的MicroRogue表达式称为holdexpression。hold表达式可以在适当的位置重写其子表达式。这就是MicroRogue允许控制评估顺序的方式两者A. Stump等人理论计算机科学电子笔记117（2005）6977全局规则集和hold表达式使用bang构造进行修改。当T！ 如果T是一个规则，则T被添加到全局规则集。 当T！使用T作为位置进行计算，则hold表达式 H被修改如下。 写H|T↓表示T确实是有效的位置为H。 如果H|T↓，hold表达式修改为H [Q] T，其中Q是H|T求值为（遵循标准符号，例如，第3章 [4]）。另一个操作设置hold表达式：whenever我们试图找到一个适用于表达式X的全局规则，hold表达式被设置为X。计算DONE会导致hold表达式被标记为规范化。这是有用的，例如，以防止同余性规则被不必要地应用到一个已经被充分评估的术语。然而，为了适应动态添加的规则，表达式被标记为仅针对全局规则集的某些核心前缀进行规范化。动态规则仍然可以用于重写已经相对于核心规则规范化的表达式。规则的核心前缀通过计算特殊表达式ENDCORE来表示。如果一个项被标记为规范化，并且应用于它的排序中的第一个规则是在ENDCORE求值之前添加的规则集中，那么该项将被重写为自身。否则，重写将继续进行。图4和图5给出了正式的评估规则。出于排版的原因，规则的名称及其附带条件写在上面规矩的可导出的对象是序列R：：H：：T=RJ：：HJ：：TJ，显示起始规则列表R、保持表达式H和当前MicroRogue要重写的表达式T;以及T的结果规则列表、保持表达式和结果TJ。规则列表是带注释的规则i：l→的列表。r，其中i是规则的唯一标识符，并且？为+或−，指示规则是启用还是禁用。 规则在添加时初始启用。的每个列表中的规则都是按照它们被添加到该列表的时间（完全）排序的。作用域在规则列表中使用分隔符分隔。当一个POP被求值时，所有自上一个未弹出的PUSH后添加的规则都将被删除。表达式E被（done）规则标记为规范化的，写En;我们在其他规则中省略了这个符号。我们将规则列表R应用于表达式T的结果写为R（T），其定义如下。设l→r是R的第一个（从右到左）使l匹配T的使能规则。如果T是未标记的，或者该规则不在R中任何（（由ENDCORE添加）的左侧，则我们定义R（T）为σ（r），其中σ是l和T的匹配替换。否则，或者根本没有匹配规则，我们定义R（T）就是T。图4和图5的规则用于评估MicroRogue表达式，该表达式从空规则列表和空保持表达式开始。规则很78A. Stump等人理论计算机科学电子笔记117（2005）69122121（右起）R：：H：：T1=R1：：H1：：TJR：：H：：T1; T2 =R2：：H2：：TJR1：：H1：：T2 =R2：：H2：：TJ（左起）R：：H：：T1=R1：：H1：：TJR1：：H1：：T2 =R2：：H2：：TJR：：H：：T1; T2 =R2：：H2：：TJ（上）R，i：l→？r，RJ：：H：：ONi=0R，i：l→+r，RJ：：H：：null（o）R，i：l→？r，RJ：：H：：OFFi=<$R，i：l→−r，RJ：：H：：null（add-rule 1）ifreshR：：H：：l → r！ = R，i：l →+r：：H：：i（add-rule2）R：：H：：i：l → r！ =R，i：l→+r：：H：：i见图4。 MicroRogue的操作语义（第一部分）通过自底向上地将它们作为逻辑程序应用而直接可执行。左手边是输入，右手边是输出。规则的应用是非确定性的，除了在副条件中指出的，规则（basic-1）和（basic-2）仅在没有其他规则的情况下使用A. Stump等人理论计算机科学电子笔记117（2005）6979（推）R：：H：：推=R：：H：：null(pop)n/∈RJRRJ：：H：：POP=R：：H：：null（subexpr） H|P↓，HJH [Q] PR：：H：：H|P =RJ：：H1：：QR：H：P！=RJ：：HJ：：HJ（已完成）R：：H：：完成=完成R：：H：：Hn（端核）R：：H：：ENDCORE=CNR（：：H：：H（基本-1）TR（T），无其他规则适用R：：H：：T=R：：T：：T（基本-2）T/T/TjR（T），无其他规则适用R：：T：：TJ=RJ：：HJ：：QR：：H：：T=RJ：：HJ：：Q图五. MicroRogue的操作语义（第二部分）80A. Stump等人理论计算机科学电子笔记117（2005）69apply.请注意，下面，我们将发现它方便地评估一系列MicroRogue表达式。在第一个表达式之后，每个后续表达式都将根据规则列表进行评估，并保持由前一个表达式评估产生的表达式。这些规则没有提到作用域运算符α。要使用这些规则计算某个表达式，所有形式为α x的子表达式。T首先被重写为[xJ/x] T，其中xJ是一个新变量。 在评估过程中没有引入新的变量。5Rogue在MicroRogue本节解释了如何使用MicroRogue来给出Rogue的一个非常简洁的实现。值得注意的实现技术用于处理以下两个问题：• 相互作用同余规则和减少规则：简化规则（如（r1，r2）@t= t（r1@t，r2@t））的左侧与同余规则重叠，例如，应用程序通过以下方式进行评估：以某种方式计算它的子表达式。我们在MicroRogue中处理这种重叠如下。同余规则被赋予比归约规则更高的优先级，只需稍后将其添加到全局规则集即可。一旦全等规则重写了子表达式，它就使用OFF禁用自己。要做到这一点，它需要知道它的唯一标识符，这可以通过以下方式实现：只需在添加规则时为其命名即可。然后，全等规则指示应当进一步重写作为应用的可能重写版本的保持表达式这就给了归约规则一个重写的机会，然后归约规则负责再次启用同余规则，使用ON。如果不减少规则适用时，我们可以在归约规则之后包含一个总括规则，全等法则再次出现。或者，我们可以在hold表达式的递归计算之后重新打开同余规则• 显式规则应用：显式规则应用（l→r）@t的评估在MicroRogue中大致如下实现。我们首先动态地添加一个catch-all规则，该规则表示任何内容都重写为null。然后我们动态地添加规则l → r。我们必须以这样一种方式添加这些规则，即它们每个最多使用一次，然后它们都将被删除.这可以通过下面描述的方式来实现。最后，我们请求重写显式应用程序的目标表达式。我们动态添加的两个规则之一将适用。然后，这两个规则都将被删除，重写将在结果上继续（null或用σ（l）代替σ（r）。A. Stump等人理论计算机科学电子笔记117（2005）6981图6将Rogue定义为一系列MicroRogue表达式，每个表达式以“;;"结尾。为了便于参考，每个MicroRogue表达式都进行了编号去掉数字后，图6的代码是正在开发的原型MicroRogue解释器的有效输入用一块合成糖，其中T1：= T2代表T1->T2！ ， 以 及i：T1： = T2 对 于i：T1-> T2！ . Welet ：=bindmore比除α以外的所有其他算子都要宽松。请注意，Micro-Rogue的：=运算符的语义除了表达式25之外，每个num-图6中的一个格式化的表达式导致一个规则被添加到MicroRogue的全局规则集。同余规则被命名，这样它们就可以被打开和打开。归约规则不需要名字。我们从简单的部分开始，一次一段地浏览图6中的定义。由于空间的原因，我们省略了对属性规则的解释（表达式4、5、22、23和24）。5.1箭头表达式图6的表达式6和7给出了Rogue的两种箭头表达式的一致性规则6.x^y^ x->y：=.0！完成 ;;7.x^y^ x=>y：= .0！;DONE;;这些规则规定，任何一种箭头表达式都要重写为“.0！ 完成“。如图5中的（basic-1）和（basic-2）规则所定义的，当我们试图为目标表达式找到匹配规则时，目标表达式将成为新的hold表达式。在这里，将始终使用规则（basic-2）因为箭头表达式E被重写为“.0！“行”与“行”是不同的。 所以，（basic-2）说我们应该递归地计算“ . 0 ！;DONE这样做首先会导致要使用的（右序列）规则。（subexpr）规则用于重写箭头表达式的左侧，然后使用（done）规则以将保持表达式标记为标准化。重写后的保持表达式将作为计算原始箭头表达式的结果5.2逗号表达式图6的表达式2、10、11和13是与评估相关的表达式逗号表达式。注意，条形表达式的处理类似于表达式3、8、9和14。82A. Stump等人理论计算机科学电子笔记117（2005）691.x^y^x@y：=ONAPP1; ONAPP2; DONE;;2.x^y^x，y：=ON COMMA1; DONE;;3.x^y^x| y：= ON BAR 1; DONE;;4.x^y^x.y：= null;;5.DOT 1：x^y^x.y：= .0！1！;OFF DOT 1; .！~;ONDOT 1;;6.x^y^ x->y：=.0！完成 ;;7.x^y^ x=>y：= .0！;DONE;;8.x^x| null：= ON BAR1; x;;9.x^null| x：= ON BAR 1; x;;10. x^ x，null：=ON COMMA1;x;;11. x^ null，x：=ON COMMA1;x;;12. x^ null@x：=ONAPP 1; ONAPP 2;null;;13. COMMA1：x^y^x，y：=.0！1！关闭COMMA 1;。！;;14. BAR 1：x^y^x| y：=.0！1！OFF BAR 1;. ！的 情况。15. l^r^r2^t^（l->r| r2）@ t：=PUSH; x^x ->（POP; ON APP1; ON APP2; r2@x）！;l->（POP; ON APP 1; ON APP 2;r）！;t;;16. r1^r2^t^（r1，r2）@ t：= ON APP 1; ON APP 2; r1@t，r2@t;;十七岁（l=>r）@t;18. APP2：x^y^x@y：= ON APP1;.1！;关闭APP 1;关闭APP 2;。！的情况。19. l^r^r2^t^（l=>r| r2）@ t：=PUSH; x^x->（POP; ON APP1; r2@x）！;l->（POP; ON APP1;r）！;t;;20. l^r^t^x^（l=>r）@t：=PUSH; x->（POP; ON APP1;null）！;l->（POP; ON APP1;r）！;t;;21. APP1：x^y^x@y ：=.0！;关闭APP 1;。！的情况。22. x^y^set（x，y）：=ON SETRULE 1;ON SETRULE 2;（x：=y）;y;;23. SETRULE 2：x^y^set（x，y）：=.1.1！ ; OFFSETRULE 2;. ！;;24. SETRULE 1：x^y^z^set（x.y，z）：= .1.0.0！0.0.1！ ;关闭SETRULE 1;.！的情况。25. ENDCORE;;见图6。 在MicroRogueA. Stump等人理论计算机科学电子笔记117（2005）69832.x^y^x，y ：= ON COMMA1; DONE;;10. x^ x，null：=ON COMMA1;x;;11. x^ null，x：=ON COMMA1;x;;13. COMMA1：x^y^x，y：=.0！1！关闭COMMA 1;。！的情况。这里我们有一个归约规则（10和11）和一个同余规则（括号中13的部分）之间的相互作用。如上所述，我们的策略是，全等规则在导致子表达式被重写后将自身变为无效。后者是通过“.0！1！”, which对，递归计算。在重写子表达式之后，同余规则将自身关闭，代码为OFFCOMMA1，其中COMMA1只是同余规则的名称 在全等规则禁用自身之后，它请求递归地计算hold表达式（“。！“）. 此时，hold表达式保存逗号表达式，并递归计算其子表达式。然后，这个逗号表达式将通过使用规则（11）、（10）或（2）中的一个来计算，并按此顺序进行尝试。 每个规则首先打开全等规则，然后返回表达式。表达式2只是一个用于确保全等规则重新打开的通用规则。5.3应用图6中最复杂的功能相关的规则子集是用于处理应用程序的规则。表达式1、12、15、16、17、18、19、20和21都与应用有关。我们在这里只关注处理箭头表达式的应用。不过，首先要注意，正如我们之前所希望的，逗号表达式的应用是由一个简单的规则（表达式16）处理的，只需添加一些代码来打开一些暂时禁用的规则：16. r1^r2^t^（r1，r2）@ t：= ON APP 1; ON APP 2; r1@t，r2@t;;让我们考虑用于处理箭头表达式的应用的表达式1.x^y^x@y：= ON APP1; ON APP2; DONE;;17. l^r^t^（l->r）@ t：= ON APP2;（l=>r）@ t;;十八岁 APP2：x^y^x@y ：= 0NAPP1; 一个！;关闭APP 1;关闭APP 2;。！的情况。20. l^r^t^x^（l=>r）@t：=PUSH; x->（POP; ON APP1;null）！;l->（POP; ON APP1;r）！;t;;21岁 APP1：x^y^x@y：=. 0分！ ;OFFAPP1;. ！的情况。84A. Stump等人理论计算机科学电子笔记117（2005）69我们使用上面描述的技术来控制同余规则和归约规则之间的交互。然而，由于必须分阶段评估应用程序x@y，因此情况很复杂。第一我们必须查看x的计算结果是否为惰性箭头（=>）表达式（或条形表达式以惰性箭头开始如果x的计算结果是一个惰性箭头表达式，我们不计算y，而是立即使用适当的归约规则。如果x的计算结果是一个急切箭头表达式（->），那么我们必须在应用适当的归约规则之前计算y我们通过对应用程序x@y使用两个同余规则来解决这个额外的复杂性。第一个是表达式21，它指定x应该递归计算（“.0！“），则应禁用该同余规则（OFF APP 1），并且最终应继续对x@y（“）的更新版本进行评估。 ！“）. 如果x的计算结果是一个惰性箭头表达式，那么表达式20添加的我们在下面考虑这个规则是如何工作的。让我们首先考虑一下，如果x没有被计算为一个懒惰箭头表达式，那么计算是如何进行的。 下一个可以匹配的规则（同样，省略考虑以惰性箭头表达式开始的bar表达式）是应用程序的第二个全等规则，它是表达式18中括号中的部分。在处理原始应用程序x@y时，我们需要评估Y。全等规则用“.1！”, but微妙之处：我们必须在此时重新启用第一个同余规则，因为新考虑的表达式的递归计算应该在启用所有规则的情况下开始。因此，表达式18的同余规则首先将规则APP 1重新打开全等规则（APP1和APP2）被禁用，并且评估继续（“.！”) on the此时，如果没有应用归约规则，则将使用表达式1的所有规则，并且表达式将被标记为规范化的。另一方面，如果应用程序现在是（l->r）@t形式，则表达式规则17将被应用这个规则只返回（l=>r）@t，因为如果目标表达式已经被求值，则惰性箭头和急切箭头以相同的方式被求值;并且重新打开同余规则APP 2。我们这样做是为了维护不变式，即当应用规则时，该规则在规则列表中出现的时间比这些同余规则之一（APP 1和APP 2）晚，则所有较早的同余规则都被启用。最后，我们来到表达式20的规则，用于评估形式为（l=>r）@ t的应用。我们在这里使用第5节开头提到的第二种技术来处理显式规则应用。再次考虑表达式20：A. Stump等人理论计算机科学电子笔记117（2005）698520. l^r^t^x^（l=>r）@t：=PUSH; x->（POP; ON APP1;null）！;l->（POP; ON APP1;r）！;t;;这意味着对申请的评估将按以下方式进行。我们首先为动态添加的规则推送一个新的作用域，然后添加两个规则。第一条规则匹配任何东西，因为它的左边x只是一个变量。第二个匹配l，即我们试图应用明确地指向目标t。最后，我们要求递归地计算t。如果t与l匹配，则会执行代码（POP;ONAPP 1;r）。我们弹出包含（仅）我们在这里添加的两个动态规则的范围然后我们重新启用同余规则APP1，然后返回σ（r），其中σ是匹配替换。如果l和t不存在这样的匹配替换，那么我们动态添加的第一个规则（左侧x）适用。我们再次弹出这两个规则的作用域，重新启用APP1，然后返回null。5.4执行MicroRogue的当前原型解释器能够以合理的效率评估Rogue程序。例如，在少量（62行）的Rogue代码中，可以编写一个程序，该程序使用正则表达式将词法规范转换为非确定性有限自动机。MicroRogue解释器使用Rogue操作语义的图6Java 1.4的词法规范可以在16秒内转换为具有423个状态的自动机，在1.2GHz Pentium 3（Mobile）上使用略低于4M的内存和512K缓存。运行时间有点慢，但内存使用量相当适中。为了达到当前的性能水平，MicroRogue解释器使用了几种高级实现技术。这些使实现复杂化，尽管如此，目前C++的实现大约只有2000行（非注释，非空白）。首先，重写规则的全局集合被索引，当前仅使用简单的路径索引方案（如在例如，[11，第5节]）。第二，很自然地会发现一些规则，如图6中的一些规则，其右侧以“结尾。！”, indicating重写应该在当前保持表达式上继续。微流氓解释器在计算这些表达式时使用尾部递归，以避免分配堆栈帧。目前，尾递 归 必 须 在 MicroRogue 代 码 中 通 过 写 “CONTINUE“ 而 不 是 “ 来 显 式 指示。！“. 此优化允许计算86A. Stump等人理论计算机科学电子笔记117（2005）69而不会耗尽堆栈内存。表达式是引用计数的，但我们并不坚持将相同的表达式映射到相同的内部表示。这将为每次创建表达式保存在哈希表中的查找。为了减少内存使用，表达式在内部实现为没有任何虚方法的C++类。这节省了4个字节，否则需要指向vtable结构。复合表达式每个需要三个4字节的字：一个用于左孩子，一个用于右孩子，一个用于保存引用计数和一些标记。一个标记用于将不包含变量的术语标记为闭合的;在替换期间不需要遍历它们。替换被急切地执行，因为懒惰替换的初步实验显示性能略有下降。MicroRogue的部分编译器也已经实现（在Rogue中）。MicroRogue规则被简单地编译成C++代码，否则将由解释器为它们执行。此编译目前仅限于顶级规则。不编译由其他规则动态添加的规则。然后将生成的部分编译版本的MicroRogue程序静态链接到MicroRogue解释器中。应用于MicroRogue中Rogue的定义，这种部分编译减少了约20%的代表性Rogue程序的解释运行时间。6结论与未来工作我们已经看到了Rogue是如何在MicroRogue中定义的，Rogue是基础重写演算的命令式版本MicroRogueMicroRogue是一个成功的简单重写语言，适合于实现像重写微积分这样的语言。在MicroRogue中的Rogue实现以及MicroRogue的C++实现当然不会比直接在C++中实现的Rogue解释器复杂得多，并且可能稍微不那么复杂。在MicroRogue中实现Rogue比直接实现Rogue更容易体验Rogue的操作语义。然而，MicroRogue作为一个基础系统还不令人满意作为基础，我们可能想建立元理论性质，如：A. Stump等人理论计算机科学电子笔记117（2005）6987一个系统的各种特征的独立性;与其他类型的基本系统的连接，如某种逻辑; 以 及 动 机 良 好 的 指称 语 义 学 。 因 此 ， 需 要 进 一 步 的 工 作来 将MicroRogue或类似的精神开发成真正的基础重写语言。提高业绩仍然是今后工作的另一个重要方面。鸣谢：感谢匿名审稿人对论文前一稿提出的非常有帮助的建议，并感谢Horatiu Cirstea，Ger-mainFaur′e，ClaudeKirchner，LuigiLiquori，BenjaminWack等。PROTHEO团队的成员就重写微积分进行了许多精彩的讨论。引用[1] A. 是的。