Maude1的按需评估：处理随需应变的策略注释

理论计算机科学电子笔记124（2005）25-39www.elsevier.com/locate/entcsMaude1的按需评估FranciscoDura'na桑蒂亚戈·埃斯科巴r b SalvadorL u casbaLCC，Uni v ersidaddeMa'laga，CampusdeTeatinos，Ma'laga，Spain.duran@lcc.uma.esBDSIC，UPV，Camino de Vera s/n，46022 Valencia，Spain. {sescobar，slucas}@dsic.upv.es摘要策略注释提供了一种简单的机制，可以在表达式的计算中引入一些惰性。作为一种热切的编程语言，Maude可以利用它们，事实上，它们是语言的一部分。Maude策略注释是与函数符号相关联的非负整数列表，这些符号指定了函数调用中参数（最终）计算的顺序。一个正的索引允许对参数进行求值，而“零”意味着必须尝试函数调用。已经提出了使用负索引来表达按需评估，其中该需求是尝试将参数项与重写规则的左侧相匹配。 在本文中，我们展示了如何提供莫德的能力，处理随需应变的策略注释。关键词：声明式编程，Maude，反射，需求，按需策略注释。1介绍处理有限对象是懒惰（函数式）语言的典型特征。虽然Maude[5，6]中的约简基本上是最内在的（或渴望的），但Maude能够通过使用策略注释[18]表现出类似的行为 Maude策略注释是与函数符号相关联的非负整数的列表，其指定在函数调用中（最终）评估参数的顺序：当考虑函数调用f（t1，.，tk），只有其索引在局部中呈现为正整数的参数1部分得到CICYT TIC 2001 -2705-C 03 -01和TIC 2001 -2705-C 03 -02、MCyT AccionIntegrada HU 2003-0003、Valenciana de Ciphéry Tecnolog 'ıa GR 03/025和欧盟-印度跨文化传播项目ALA/95/23/2003/077-054支持的工作。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.07.01326F. Durán等人/理论计算机科学电子笔记124（2005）25策略（i1···in）进行评估（遵循指定的顺序）。 如果找到0，则对整个项f（t1，...，k）的尝试。事实上，Maude给每个符号f一个策略注释（1 2···k 0），而没有明确的策略注释。例1.1考虑下面的模块LAZY-NAT和LIST-NAT，定义排序Nat和LNat，符号0和s定义自然数，符号nil（空列表）和_。 用于列表的构建。fmodLAZY-NAT是sort Nat。op 0：-> Nat.op s：Nat -> Nat [strat（0）] .op_+_：Nat Nat-> Nat.vars M N：Nat.等式0 + N = N。等式s（M）+N= s（M + N）。endfmfmod LIST-NAT是pr LAZY-NAT。排序LNat。子排序Nat LNat.op_._：Nat LNat -> LNat [strat（10）]。op nil：-> LNat.op nats：-> LNat.操作增加：LNat ->LNat。操作长度：LNat -> Nat。vars X Y：Nat.var XS YS：LNat .eq incr（X . XS）= s（X）。增量（XS）eq nats = 0。增加（nats）eq长度（nil）=0。eq长度（X . XS）= s（长度（XS））。endfm策略注释通常可以改善程序的终止行为（通过从任何表达式开始修剪所有无限重写序列在上面的例子中，符号s和_._的策略（0）和（10）是分别保证结果程序是终止的2（注意，这两种策略对于这种终止证明都是必要战略年鉴2规范的终止可以通过使用工具MU-TERM正式证明，见http://www.dsic。向上; es/$\sim$slu c a s/csr/t erm in ati on/m ute rm.F. Durán等人/理论计算机科学电子笔记124（2005）2527站还可以提高计算的效率（例如，通过减少尝试匹配的数量或避免无用或重复的减少）[11]。然而，局部策略中某些指标的缺失也会危及这些策略计算范式的能力。例如，表达式s（0）+ s（0）的求值为w.r.t. 使用Maude3的实施例1.1产生以下：Maude>（红色s（0）+s（0）.）结果Nat：s（0 + s（0））由于符号s的注释（0），0 + s（0）是不可能的，求值到此为止。关于计算的正确性和完整性，（仅）使用肯定注释的障碍在例如，[1，2，16，20，21]，并提出了一些解决方案：(i) 执行分层规范化：当评估由于策略注释引入的替换限制而停止时，在结果表达式的具体内部继续，直到达到范式（如果有的话）[17];(ii) 变换该程序以获得能够获得非常感兴趣的输出的不同程序（例如，[2][3][4][5](iii) 使用带有负索引的策略注释，这允许按需进行一些额外的评估，其中需求是尝试将参数项与重写规则的左侧匹配[20，21，1]。在[8]中，我们引入了两个新命令（norm和eval），使技术i和ii可用于Maude程序的执行。 在本文中，我们将展示我们如何将按需策略带入Maude。在进入细节之前，我们展示了负指数如何改善Maude策略注释。示例1.2（继续示例1.1）以下NATS-TO-BIN模块将自然数的二进制编码实现为0和1的列表（从最小有效位开始）。fmod NATS-TO-BIN是ex LAZY-NAT。pr列表-NAT。op 1：-> Nat.op natToBin：Nat -> LNat.3 2. 1个解释器[6]可在www.example.com上获得http://maude.cs.uiuc.edu。28F. Durán等人/理论计算机科学电子笔记124（2005）25op natToBin2：Nat Nat -> LNat.X：Nat.var XS YS：LNat. 等式natToBin2（0，0）= 0。eq natToBin2（0，M）= 0。natToBin（M）.等式natToBin2（s（0），0）=1。等式natToBin2（s（0），M）= 1。natToBin（M）.等式natToBin2（s（s（N）），M）= natToBin2（N，s（M））。等式natToBin（N）= natToBin2（N，0）。endfm表达式natToBin（s（0）+ s（0））的求值应产生2的二进制表示。然而，我们得到：Maude>（red natToBin（s（0）+ s（0））.）结果LNat：natToBin2（s（0 +s（0）），0）问题是当前的策略注释不允许在natToBin2（s（0 + s（0）），0）中计算子表达式0 + s（0），从而禁用了natToBin2的最后一个等式的应用。在[8]中引入的命令范数的使用并没有解决这个问题，因为它只是规范化了非约化的子表达式：Maude>（norm natToBin（s（0）+s（0））.）结果LNat：natToBin2（s（s（0）），0）正如我们下面所展示的，按需策略注释可以解决这个问题。事实上，对符号s使用策略（-1 0），声明它的第一个参数只能按需求值，允许恢复所需的行为，同时保持程序的终止（见下面的示例4.1和4.2）。在本文中，我们提供Maude处理按需策略注释的能力Maude的响应能力是构建这种语言扩展的关键Full Maude是用Maude 本身编写的Maude的扩展，它赋予Maude面向对象模块的符号和强大且可扩展的模块代数[5]。它的设计，以及它所给出的抽象层次，使它成为一个优秀的元级工具，用于测试和实验（核心）Maude中不存在的特性和功能[9，10，5]。我们利用Full Maude的可扩展性和可扩展性来允许使用red（Maude的常用评估命令）和norm（在[8]中引入）与Maude程序一起使用按需策略注释。F. Durán等人/理论计算机科学电子笔记124（2005）25292按需评估策略正如在引言中所解释的，Maude程序的局部策略中缺少某些索引可能会危及这些策略计算范式的能力。在[20，21，1]中，提出了负索引来指示应该仅“按需”评估的那些参数例如，例1.2中的项natToBin2（s（0 + s（0）），0）的子项0 + s（0）的求值由符号natToBin2的最后一个等式要求，即，通过它的左手边natToBin 2（s（s（N）），M）：natToBin2（s（0 + s（0）），0）中符号s的最外出现的参数由定义的函数sym-bol，_+_根，而左手边的对应运算符是s。因此，在能够应用该规则之前，我们必须进一步评估0 + s（0）。至于我们的运行示例，我们可以得出结论，（仅）具有肯定注释的评估要么进入无限推导-例如，对于项长度（NATS），对于符号S采用策略（10）-或者不提供预期的范式-例如，对于符号s，使用策略（0），参见例1.2-。然而，策略（-10）给出了符号s的适当局部策略，因为它使其参数仅“按需”被评估。然后，在用于s的策略（-10）下对表达式natToBin（s（0）+ s（0））的评估能够减少符号natToBin 2，并且将其从顶部位置移除，从而获得头部范式（参见下面的示例4.1）。这也允许使用结果表达式作为分层求值（带范数）的起点，从而得到范式（参见下面的示例4.2）。注意，这是在不进入非终止求值的情况下实现的.我们建议读者参考[12]，以获得有关在编程中使用按需策略注释的最新详细讨论。在本文中，我们遵循[1]中定义的计算模型来处理负注释。一个k元符号f∈ F的局部策略是{−k，.，-1，0，1，...，k}，在括号内给出。将局部策略f（f）与每个f∈F相关联的映射f称为E-策略映射[20]。为了计算表达式e，每个e中的符号根据E-策略图方便地注释。注释表达式的评估需要一个术语和与其顶部符号相关联的策略，然后通过顺序考虑这样一个策略的注释来继续进行[1]：如果提供了一个正参数索引，则评估跳转到该参数位置的子项;如果提供了一个负参数索引，则索引被消耗但不做任何事情;如果找到零，则我们尝试找到一个应用于这样一个术语的规则。如果没有规则可以应用，那么我们继续执行它们（所要求的）评估，30F. Durán等人/理论计算机科学电子笔记124（2005）25也就是说，我们试图减少位置中的一个子项（消费或当前）负指数。使用额外的策略列表将所有消耗的索引（正和负）与术语中的每个符号保持关联，以便可以搜索所需的位置。参见[1]以获得该过程的正式描述，以及与OBJ3[15]和CafeOBJ[20，21]等其他负注释框架相比，为什么内存列表是必要的详细信息在本文中，我们不考虑交流符号或规则的非线性左手边。此外，AC符号明确禁止使用策略注释（参见[13，14]），并且仅对线性左侧和基于构造器的程序（见[17，1]）。3反射和META-LEVEL模块Maude特别地，META-LEVEL对Term和Module进行了排序，使得项t和模块R的表示是，分别是排序Term的项t和排序Module的项R。项表示的基本情况由引用标识符的排序Qid的子排序Constant和Variable获得。常量是引用标识符，包含常量的名称及其类型，用点分隔，例如，’0.Nat类似地，变量包含它们的名称和类型，它们之间用冒号分隔，例如，’N:Nat然后，通过将运算符符号应用于项列表，子排序常量变量 TermList [ctorassistant] . op _[_]：Qid TermList -> Term [ctor] .例如，模块NATS-TO-BIN中的排序LNat的项natToBin 2（s（s（0）），0）元表示为META-LEVEL模块还包括元表示模块的声明。例如，功能模块可以表示为术语使用以下运算符对模块进行操作fmod_is_sorts_。endfm： Qid ImportList SortSetSubsortDeclSet OpDeclSet MaxAxSet EquationSet-> FModule [ctor].类似的声明允许我们表示我们在模块中可以找到的不同类型的声明。F. Durán等人/理论计算机科学电子笔记124（2005）2531模块META-LEVEL还提供了关键的元级函数，用于在元级重写和评估术语，即元应用、元重写、元归约等，以及通用解析和漂亮打印函数MetaParse和MetaPrettyPrint [7，5]。例如，函数MetaReduce取模R的表示和该模中项t操作MetaReduce：Module Term->[ResultPair]。op {_，_}：Term Type->ResultPair [ctor].MetaReduce返回术语t使用R中的方程，连同其相应的排序或种类。所有这些功能对于元编程非常有用，特别是在构建正式工具时。此外，Full Maude提供了一个强大的设置，其中提供了额外的设施，使添加新命令或重新定义以前的命令变得更简单，如本文所述。Full Maude的规范及其执行环境可以用作构建新功能的基础设施。4扩展Full Maude以处理按需策略注释我们提供了考虑按需注释的项的减少，作为Maude的通常评估命令red的重新定义（仅考虑积极注释）。例4.1考虑例4.2中替换的指定结果。1.2该运算符s的声明由另一个：op s：Nat-> Nat [strat（-1 0）].natToBin（s（0）+ s（0））的按需求值获得头部范式：Maude>（red natToBin（s（0）+ s（0））.）结果LNat：0.natToBin（s（0））至于Full Maude中的其他命令，我们可以通过定义其相应的元函数来定义使用新命令例如，通过适当地调用met- alevelMetaReduce函数来执行红色 为了向Maude提供按需评估，我们提供了一个新的元级操作MetaReduceOnDemand，它扩展了Maude的响应和元级功能，如第3节所述。操作MetaReduceOnDemand接受sortsModule的参数，32F. Durán等人/理论计算机科学电子笔记124（2005）25OpDeclSet和Term，并返回排序为ResultPair的项。它的参数分别表示发生归约的模块、该模块中的操作声明以及要归约的项。返回的结果与MetaReduce给出的结果相同（参见第3节）。请注意，（Core）Maude不能处理否定注释，因此，该函数采用有效的模块，即没有否定注释的模块，以及带有任何类型注释的操作声明集。重新定义的命令red必须根据是否存在否定注释在MetaReduce和MetaReduceOnDemand之间进行选择。基本上，MetaReduceOnDemand调用辅助函数procStrat，该函数实际上处理与术语顶部符号相关联的策略列表。var M：Module.var OPDS：OpDeclSet.var T T '：术语。op metaReduceOnDemand：模块OpDeclSet术语-> [ResultPair].op procStrat：Module OpDeclSet AnnTerm -> AnnTerm.ceq metaReduceOnDemand（M，OPDS，T）= {ifT '：= erase（procStrat（M，OPDS，annotate（M，OPDS，T）.为了将注释包含到Maude此外，我们还提供了两个函数：annotate和erase，用于在排序Term和AnnTerm之间移动。排序AnnVariable AnnTerm AnnTermList。子排序AnnVariable AnnTerm AnnTermList。op_{}：Variable-> AnnVariable。op _{_}：ConstantIntListNil ->AnnTerm。联系我们|_}[_]：Qid IntListNil IntListNil AnnTermList-> AnnTerm。op _，_：AnnTermList AnnTermList -> AnnTermList [ascurry].op annotate：Module OpDeclSet TermList-> AnnTermList.操作erase：AnnTermList -> TermList。函数procStrat在处理与要评估的术语的顶部符号相关联的策略列表时遵循第2当发现一个积极的指标时，这种论点的评价是强制的，F. Durán等人/理论计算机科学电子笔记124（2005）2533并且正索引从策略列表（右分量）移动到顶部符号的存储器列表（左分量）。例如，由arity大于0的符号作为根的注释项的等式如下。var N N' ： I n t .var NL NL'：IntListNil. varF：Qid.var ATL：AnnTermList.ceq proc Strat（M，OPDS，F{NL| N[ATL]）= procStrat（M，OPDS，F{NL @@ N |NL'}[procStratSel（M，OPDS，ATL，1，N）]）。当找到一个负索引时，该参数中的任何计算都不会启动，负索引将从策略列表（右组件）移动到内存列表（左组件）。ceq proc Strat（M，OPDS，F{NL| N[ATL]）= procStrat（M，OPDS，F{NL @@ N|NL<'}[ATL]），如果N 0.当找到索引0时，函数procStrat尝试使用元级函数metaApply将该术语与规则的左侧进行匹配。4如果匹配，则应用规则。如果没有获得匹配，则我们使用函数proc StratOD来确定是否存在任何所需的位置，该函数执行匹配算法以检测负注释下的哪些位置实际上是由某个规则所要求的（详细信息参见[1如果存在所需的位置，则开始对这样的位置进行评估，然后在评估完成后，我们将根据规则如果不存在所需位置，则从策略列表中删除当前索引0，并考虑策略列表的其余部分。varMA：ResultTriple？.ceq procStrat（M，OPDS，F{NL| 0 N L' } [ A T L ] ）=如果MA==失败则proc StratOD（M，OPDS，F{NL |0 NL '}[ATL]）else procStrat（M，OPDS，annotate（M，OPDS，getTerm（MA）fi如果MA：= MetaApply（moveEqsToRls（M），F[erase（ATL）]，4函数MetaApply只应用规则，因此在应用MetaApply34F. Durán等人/理论计算机科学电子笔记124（2005）25’on-demand, none,当执行函数procStratOD时，即当搜索所需位置时，[ 1 ]的计算模型指定必须遵循由策略中的位置顺序定义的搜索顺序，即如果（-1 -2 0）是符号的策略。，则第一个参数下的任何所需子项都将首先被选择，而不管第二个参数下的任何所需子项（详见[1]）。一旦实现了函数MetaReduceOnDemand ，我们需要重新定义FullMaude 的 部 分 ， 以 便 命 令 red 能 够 执 行 MetaReduce 或MetaReduceOnDemand。 不需要定义一个新的命令并扩展Full Maude来接受该命令，就像在[ 8 ]中对norm和eval命令所做的那样。我们只需要修改红色命令的处理方式。在Maude的当前版本中，输入/输出由预先定义的LOOP-MODE模块完成，该模块提供通用的读取-评估-打印循环。在Full Maude的情况下，循环的持久状态由维护系统数据库的Database类的单个对象给出。这个对象有一个属性db，用来保存实际的数据库，其中存储了所有输入的模块（一组记录），一个属性default，用来默认保存当前模块的标识符，以及属性input和output，用来简化由LOOP-MODE模块给出的读取-评估-打印循环与数据库的通信。使用面向对象模块中类的表示法，我们可以声明这样的类如下：数据库类|db：数据库，默认值：ModName，输入：TermList，输出：QidList。read-eval-print循环的状态由DatabaseClass 类的对象给出。在FullMaude 的 情 况 下 ， 读 取 - 评 估 - 打 印 循 环 的 处 理 在 模 块 DATABASE-HANDLING和FULL-MAUDE中定义。模块FULL-MAUDE包括初始化循环的规则（ruleinit），以及指定循环（系统的输入/输出）与数据库之间的通信的规则（rulesin andout）。根据数据库接收的输入类型，它的状态将被更改，或者将生成某些输出。要使用内置函数metaParse解析某些输入，Full Maude需要解析输入的签名的元表示。在Full Maude中，这样的语法由FULL-MAUDE-SIGN模块提供，我们可以在其中找到适当的声明，以便可以解析任何有效的输入，即模块，理论，视图和命令。因为我们不想改变语法FULL-MAUDE-SIGN，它用于解析输入，所以我们不需要改变FULL-MAUDEF. Durán等人/理论计算机科学电子笔记124（2005）2535module.模块DATABASE-HANDLING定义了数据库在新条目时的行为。与命令相关的行为由描述调用函数procCommand的转换的规则管理。例如，当收到红色命令时，定义该做什么的规则如下。rl [红色]：< O：X@数据库|db：DB，input：（'red_. [T])，output：nil， default： MN，Atts>=>< O：X@Database| db：DB，输入：nilTermList，输出：procCommand（'red_. [T]，MN，DB），默认值：MN，Atts >.当输入一个red命令时，对输入的解析返回一个形式为red_的项。[T]其中T是表示气泡的T类变量。解析的结果放在数据库对象的输入属性中。 函数procCommand指定当red_出现时该怎么做。[T]接收到的MN和DB变量的值分别为当前默认模块的名称和数据库的状态。 在命令red的原始情况下，procCommand使用适当的参数调用函数procRed，即default模块的名称，默认模块本身，表示命令参数的气泡，default模块中的变量和数据库。请注意，根据默认模块是否是内置模块，以及是否经过编译，procCommand将执行不同的操作，以便获得procRed的参数。在对命令red的重新定义中，procCommand调用了一个新的函数procReduceOnDemand来重新定义procRed。eq procCommand（'red_. [’bubble[T]], MN,=如果 MN inModNameSet内置然后procReduceOnDemand（MN，DUMMY（MN），elseif compiledUnit（MN，DB）then procReduceOnDemand（MN，getFlatUnit（MN，DB），否则procReduceOnDemand（MN，getFlatUnit（MN，evalModExp（MN，DB）），Fi菲函数procReduceOnDemand负责评估气泡36F. Durán等人/理论计算机科学电子笔记124（2005）25作 为 red 命 令 的 参 数 给 出 ， 调 用 函 数 metaReduce 或metaReduceOnDemand，然后准备结果（将传递到read-eval-print循环的 输 出 通 道 以 显 示 给 用 户 的 带 引 号 的 标 识 符 列 表 函 数procReduceOnDemand 检 测 模块 中 是 否 存在 否 定 注 释 5 （ 使 用 函 数noNegAnns），然后调用MetaReduceOnDemand或MetaReduce。如上所述，由 于 Core Maude 不 接 受 带 有 否 定 注 释 的 策 略 ， 因 此 函 数procReduceOnDemand必须调用带有模块的函数MetaReduceOnDemand，而不带这种否定注释（remNegAnns负责删除它们）和带有它们的运算符声明。最后，定义procReduceOnDemand的等式如下。op procReduceOnDemand： ModExp模块术语OpDeclSet数据库-> QidList.ceq procReduceOnDemand（MN，M，T，VDS，DB）*No negative annotation -> Use metallevel metaReduce=如果 RP？：：ResultPair then...else（'\r'错误：'\o'不正确'命令。'\n）fiif noNegAnns（getOps（M））.../\ TM：= solveBubbletRed（T，remNegAnns（M），B，VDS，DB）/\ RP？：= metaReduce（getModule（TM），getTerm（TM））。ceq procReduceOnDemand（MN，M，T，VDS，DB）*Negative annotations -> Use metallevel metaReduceOnDemand=如果 RP？：：结果对then...else（'\r'错误：'\o'不正确'命令。'\n）fiif not noNegAnns（getOps（M））.../\ TM：= solveBubbletRed（T，remNegAnns（M），B，VDS，DB）/\ RP？：= MetaReduceOnDemand（getModule（TM），getOps（M），getTerm（TM））。[5]当只提供肯定的注释时，“经典的”Maude评价是不被认可的。F. Durán等人/理论计算机科学电子笔记124（2005）25374.1使用按需策略注释将Full Maude扩展到分层规范化正如本文所解释的，我们的目标是为带有策略注释的程序提供适当的范式。然而，命令red的重新定义不能提供范式0。对于例1.2中的程序，注释1，因为在符号的策略列表中缺少注释2。（参见例4.1中的red命令的输出）。然而，正如在第1节中所解释的，这个具体的问题可以使用分层规范化或转换来解决在本节中，我们重新定义了[8]的命令范数，以执行由先前提出的按需评估给出的输出的分层归一化。例4.2考虑例4.1中的模块。命令范数的重新定义现在能够提供与表达式natToBin（s（0）+s（0））相关联的预期值。Maude>（norm natToBin（s（0）+ s（0））.）结果LNat：0 . 1命令规范的重新定义与[8]中给出的命令规范的实现几乎相同。这里我们没有给出细节，但基本上，我们的想法是保留元级函数metaNorm并 定 义 一 个 新 的 元 级 函 数 metaNormOnDemand ， 它 调 用MetaReduceOnDemand而不是MetaReduce来减少初始项。eq metaNormODRed（M，OPDS，T）= procStratOD（M，getTerm（metaReduceOnDemand（M，OPDS，T）），OPDS）。我们建议读者参考[8]以了解norm命令的实现细节请注意，还需要执行与第4节中所述类似的更改：• 我 们 重 新 定 义 了 proc Command 来 调 用 一 个新 的函 数 proc NormOnDemand，它重新定义了proc Norm，当norm_。[T] 已收到;• 函 数 proc NormOnDemand 根 据 是 否 存 在 否 定 注 释 （ 再 次 使 用 函 数noNegAnns）调用metaNorm或metaNormOnDemand。5结论我们使用Full Maude来为Maude提供执行按需评估的能力，这是一种更复杂的懒惰行为形式，适用于局域网。38F. Durán等人/理论计算机科学电子笔记124（2005）25像莫德这样的语言。我们利用了可扩展性和可伸缩性允许使用红色（Maude的常用评估命令）和标准（在[8]中介绍），Maude程序使用按需策略注释。完整的规范可在http://www.dsic.upv.es/users/elp/toolsMaude上获得。这些功能已集成到Full Maude中，使其在其编程环境中可用。FullMaude的规范（实现）的高水平使得这种方法与传统实现相比特别有吸引力（参见例如[3]）。Full Maude的灵活性和可扩展性使得扩展非常简单，并且在很短的时间内完成。然而，值得注意的是，我们的按需评估原型在效率上不能与具有否定注释的评估的其他实现（例如CafeOBJ6或OnDemandOBJ7）相比。这项工作的目标不是提供一个有竞争力的实现，而是为Maude这样的语言提供按需评估。请注意，On-DemandOBJ并不包括Maude的所有功能，并且CafeOBJ用于处理否定注释的计算模型有一些缺点（参见[1]）。事实上，将其视为按需战略的实施是不公平的，甚至不是原型。它应该被视为它的可执行规范，更接近它的数学定义（在[1]中给出）而不是它的实现。尽管可以按照类似的方法给出按需评估的更有效的可执行规范/实现，但我们相信，将按需评估直接实现到Maude中是可取的。最后，作为未来的工作，我们计划考虑是否可以用策略语言（如[19，4]）来表达按需评估策略。引用[1] M.阿尔蓬特角埃斯科瓦尔湾Gramlich和S.卢卡斯改进按需策略注释。In M. Baaz和A. Voronkov，editors ， Proc.9th Int. Conf. on Logic for Programming ， Arti Ficial Intelligence ， andReasoning，LPAR[2] M.阿尔蓬特角Escobar和S.卢卡斯 正确和完整的（积极的）战略注释的目标。Gadducci和U.Montanari，编辑，Proc.第四届重写逻辑及其应用国际研讨会，WRLAElsevier，2004年。6可在http://www.ldl.jaist.ac.jp/cafeobj上获得7可用 在http://www.dsic.upv.es/users/elp/ondemandOBJF. Durán等人/理论计算机科学电子笔记124（2005）2539[3] M.阿尔蓬特角Escobar和S.卢卡斯OnDemandOBJ：战略注解实验室。在J. - L. Giavitto和P. -E. Moreau ， editors ， Proc. of the 4th International Workshop on Rule-BasedProgramming，RULEElsevier，2003年。[4] P. Borova n sky'，C. Kirchner，H. Kirchner和C. 我给他打电话。 用ELAN中的数据表进行重写：一种功能语义学。国际计算机科学基础杂志，12：69 - 95，2001。[5] M. Clavel，F. 杜兰，S。 Eker，P. Lincoln，N. 我的天啊-我的天啊。梅塞格尤尔和J。你好。Maude：重写逻辑中的规范和编程。Theoretical Computer Science285（2）：187- 243，2002.[6] M. Clavel，F. 杜兰，S。 Eker，P. 林科林，N。 妈的-哦，J。 我是你，还有C。 Talcott.Maude 2.0 系 统 。 In R. Nieuwenhuis ， 编 辑 ， Proc. of14th International Conference onRewriting Techniques and Applications，RTA[7] M. Clavel，F. 杜兰，S。 Eker，P. 林科林，N。 妈的-哦，J。 我是你，还有C。 Talcott. 马友德2.0手册. 见http://maude.cs.uiuc.edu，2003年。[8] F. 杜兰，S。 Escob ar，andS. 陆克文。新一轮的采购要求，以满足客户的需求。在N. 妈的-哦，撒谎，撒谎，Proc。第五届国际软件工程师大会将于2004年举行，WRLA'04，ENTCS将于2004年[9] F. 杜兰和杰。 Mesegu er. 一个简单的模型可以在一个简单的框架中为Maud e。 我在C。KirchnerandH. Kirchner，编者，第二届重写逻辑及其应用国际研讨会论文集，WRLAElsevier，1998年。[10] F. 杜兰。 AReec tiveModuleAlgebrawithApplicationteMaudeLanguage. PhDthesis，Un iver sidaddeMalaga，Junne1999.[11] S.艾克用运算符评估策略重写术语。《理论计算机科学电子笔记》，第15卷，20页，1998年。InC. Kirchner和H. Kirchner，编者，第二届重写逻辑及其应用国际研讨会论文集，WRLAElsevier，1998年。[12] S. 埃 斯 科 瓦 尔 函 数 式 程 序 优 化 的 策 略 和 分 析 技 术 。 PhDThesis ，UniversidadPolit'ecnicadedeValencia，Oc tooberr2003.[13] M.C. F 费 雷 拉 和 A. L. 里 贝 罗 。 上 下 文 相 关 AC 重 写 。 在 Proc. of the 10th InternationalConference on Rewriting Techniques and Applications，RTA181. Springer，1999年。[14] J. Giesl 和 A. 米 德 尔 多 普 上 下 文 相 关 重 写 系 统 的 转 换 技 术 。 Journal of FunctionalProgramming，2004。[15] J.A. Goguen，T. Winkler，J. Meseguer，K. Futatsugi和J. - P. Jouannaud。在J.Goguen和G.Malcolm，编辑，软件工程与OBJ：行动中的代数规范。Kluwer，2000年。[16] S. 卢卡斯 按需重写的终止和OBJ程序的终止。 在 Proc. 第三届声明式编程的原则和实践国际会议，PPDP'01，第82-93页，ACM出版社，2001年。[17] S.卢卡斯上下文敏感的重写策略。信息与计算，178（1）：293- 343，2002。[18] S.卢卡斯带有策略注释的程序的语义。技术报告DSIC-II/08/03，DSIC，联合国开发计划署，2003年。[19] N. 天啊-哦，撒谎，J。 Meseguer，A. 你好。 这对马乌德来说是一个很长的时间。 InN. Mart's-Oliet，编辑，Proc. 第五届重写逻辑及其应用国际研讨会，WRLA' 0 4 ， E N T C S 将 于 2 0 0 4 年举 行 。[20] M. Nakamura和K.绪方有无按需标记的头部范式评价策略。在K。第三届重写逻辑及其应用国际研讨会论文集Elsevier，2001年。[21] K. Ogata和K.二次使用按需求值策略重写的操作语义。20