演绎、策略与重写：Maude重写语言的策略语言设计和应用

理论计算机科学电子笔记174（2007）3-25www.elsevier.com/locate/entcs演绎、策略与重写StevenEkera，NarcisoMart′s-Olietb，Jos′eMeseguerc，anddAlberto Verdejoba计算机科学实验室，SRI International，Menlo Park，CA，USAbFacultaddeInforma'tica，UniversidadComplutensedeMadrid，西班牙c美国伊利诺伊大学香槟分校计算机科学系摘要自动化演绎方法不应该在程序上，而应该在声明上被指定为推理系统，无论实现细节如何都被证明是正确的。然后，实现给定推理系统的不同算法应该被指定为应用推理规则的策略。推理规则本身可以自然地指定为（可能是条件的）重写规则。使用高性能的重写语言实现和策略语言来指导重写计算，我们可以获得 以模块化的方式实现自动推理过程的推理规则和控制其应用的算法。本文介绍了Maude重写语言的策略语言的设计，它支持这种模块化分解：推理系统在系统模块中指定，策略在策略模块中指定。我们给出了一个集理论的语义，这种策略语言，提出了它的不同的组合子，说明它的主要思想与几个例子，并描述了一个recrusive原型在Maude和正在进行的C++实现。关键词：重写逻辑，莫德，重写策略，同余闭包。1引言自动扣除方法（例如同余闭包、分解等）应该被指定，而不是程序化的，作为低级算法（基于指针操作等），而是声明性地作为推理系统，其被证明是正确的，而不管实现细节。然后，实现给定推理系统的特定算法应该在高级别上指定为应用推理规则的策略例如，Shostak这允许推理规则本身和它们通过策略的控制之间的模块化分离。这样，我们就可以推理，例如，研究部分由西班牙MEC项目MIDAS（TIC 2003-1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.03.0174S. Eker等人/理论计算机科学电子笔记174（2007）3推理系统的关键正确性属性，同时留下关于如何以最佳方式应用推理规则的各种控制问题。这是一个更好的方式来指定一个推理系统比传统的算法描述演绎过程中的逻辑和控制方面合并和混淆在一起。这种抽象的方法不仅可以应用于孤立的例子，而且可以应用于非常广泛的自动推理方法。到目前为止，它通常是在抽象层次上指定许多逻辑推理系统的一种方式。我们不想以任何方式试图详尽无遗，这是不可能的，我们可以通过例子提到• 统一（Martelli Montanari [18]，Jouannaud Kirchner [15]）。• 同余闭包（Kapur [16]，Tiwari [2，25]）。• Nelson-Oppen组合决策程序（Tiwari [25]，Conchon Krstic [12]，Nieuwenhuis，Oliveras Tinelli [22]）。• Knuth-Benidians完备化（Bachmair Dershowitz [1]，Lescanne [17]）。• 归纳定理证明和其他Maude工具（Cl avel，Dura′ n &Meseguer[11，8]）。重写逻辑是一个简单的逻辑框架，其中逻辑或任何演绎过程的推理规则可以很容易地表达为条件重写规则[21，19]。例如，一个规则，用于定向存在于推理系统中的等式orient（K，E<${t<$c}，R）（K，E，R<${t→c}）对应于条件重写规则如果t>c定向：（K，E<${t<$c}，R）−→（K，E，R<${t→c}）如果t>C使用高性能重写语言实现和策略语言来指导重写计算，可以直接实现推理规则和策略之间的上述高级区分，从而提供了一种将高级规范忠实地表示为可执行原型甚至实现的方式。重写逻辑的一个有趣的特征是，由于它的响应能力[5，10]，策略本身也可以通过在元级别重写规则的方式以声明的方式指定。 也就是说，通过重写规则，引导我们感兴趣的系统的推理规则如何在“对象级”应用。这种反应方法通过反应推理技术支持关于元级特征的推理[3]。Maude语言[6，7]保持了重写规则和执行它们的策略之间的模块化区别：Maude系统模块是没有策略信息的重写理论。一般来说，描述推理系统的相同重写理论可以用不同的策略来执行，每个策略都可能具有特定的优势，这取决于手头的目的因此，在莫德斯特拉-S. Eker等人/理论计算机科学电子笔记174（2007）35gies可以通过其META-LEVEL模块中的元级规则来定义。以这种方式定义不同的策略语言有很大的自由，然后可以用来为任何感兴趣的对象理论指定和执行策略。所讨论的策略语言的语义用于确保所有允许的计算都是对象理论中的正确演绎然而，务实的考虑是很重要的指导策略语言的设计，可以很好地处理相关的应用程序。因此，我们承担了为Maude提供基本策略语言的项目[20]。为了使语言更容易使用，我们在对象级别而不是元级别上提供它。我们的策略语言允许定义策略表达式，这些表达式控制术语的重写方式。我们从自己之前在Maude设计策略语言的经验中受益匪浅，也从其他语言（如ELAN [4]和ELAGO [27]）的经验中受益匪浅。我们的设计基于系统模块中的重写规则和策略表达式之间的严格分离，这些规则在单独的策略模块中指定。因此，在我们的建议中，不可能在系统模块的重写规则中使用策略表达式：它们只能在单独的策略模块中指定。事实上，这种分离使得定义不同的策略模块以不同的方式控制单个系统模块的重写成为可能。一个策略被描述为一个操作，当应用于一个给定的术语时，产生一组术语作为结果，假设该过程通常是不确定的。基本策略包括将规则（由相应的规则标签标识）应用于给定的术语，并允许规则中的变量在其应用之前通过替换来实例化。对于可能包含重写条件的条件规则，也可以通过策略来控制重写条件。基本策略通过几种组合子组合在一起，包括：正则表达式构造（连接，联合和迭代），if-then-else，控制给定项的子项重写方式的组合子，以及递归[20]。作为本文的一个新贡献，我们发展了通用策略的概念（例如，回溯、映射等），它们不适用于单一的重写理论，而是适用于满足某些参数要求的广泛的重写理论。为了验证我们的策略语言设计，我们主要集中在自动推理和编程语言语义应用。除了[20]中给出的简短示例外，该语言已成功用于实现环境演算的操作语义[23]，并行函数编程语言Eden的两级操作语义[14]和基本完成算法[26]。此外，作为本文的进一步贡献，我们在这里应用策略语言的同余闭包算法。我们的第一个原型实现以通常的反射方式在元级别定义语言，同时为了方便起见，将用户界面保持在对象级别与品质 在实验验证了我们的语言设计并达到成熟的语言设计之后，我们目前正在C++级别上开发我们的策略语言的直接实现，Maude系统本身就是在C++级别上实现的。6S. Eker等人/理论计算机科学电子笔记174（2007）3∪我JK实现，使语言成为Maude的一个稳定的新功能，并允许更有效的执行。本文的第三个贡献是在这种正在进行的实施中使用的主要设计思想2 重写逻辑与莫德重写理论[21]（E，E，R）由签名E、方程组E和规则组R一个系统或逻辑的静态部分通过等式在重写逻辑的等式子逻辑（成员资格等式逻辑）E.系统动力学（转换或推理）通过可能的条件规则R来指定，这些规则R将表示系统部分的项重写为其他项。Maude [6，7]是重写逻辑的一个有效实现。莫德语法是用户可定义的，并且运算符可以具有等式属性，如结合性（asq），交换性（asq）和恒等式（id：），因此可以对这些等式公理进行模重写。具有标签l的重写规则的一般形式如下：l：t → tJ，如果 （i=i（wj：sj）n（pk→ qk）其中t，tJ，ui，vi，wj，pk和qk是项，sj是排序标识符。为了将这样的规则应用于主题项u，我们必须找到u的子项，它是t模理论的方程公理的实例（例如，结合性、交换性、恒等式）。但是在用θ（tJ）替换θ（t）重写u之前，必须检查规则的条件。这意味着检查等式iθ（ui）= θ（vi）是否成立，成员数jθ（wj）：sj，说明每个项θ（wj）都有sort sj，成立，并且对于每个k，我们可以重写通过零步、一步或多步将每项θ（pk）变为θ（qk）（qk）的替换实例通常是可以具有额外变量的模式）。 假设方程E是Church-Rosser和终止的，检查方程和成员是一个可判定的问题。相反，检查重写条件需要执行广度优先搜索。由于通常这样的搜索过程可能不会终止，因此是否可以利用条件规则执行单个重写步骤可能是不可判定的。Maude系统模块指定重写理论。Maude语法与定义重写理论的相应数学符号非常接近，几乎是不言自明的。要记住的一般要点是，每一项：排序、子排序、运算、等式、规则等，是用一个明显的关键字声明的：sort，subsort，op，eq（或条件方程的ceq），rl（或条件规则的crl）等，每个声明都以空格和句号结束。事实上，重写理论（E，E A，R）是用关键字sort、subsort和op指定的签名E，用关键字eq指定的E中的方程，用关键字asort、subsort和id：指定的A中的方程公理，用关键字rl指定的R中的规则来定义的。另一个要点是使用了“mix-fix”用户可定义的语法，参数位置由下划线指定;例如：if then else fi。S. Eker等人/理论计算机科学电子笔记174（2007）37此外，条件中的方程的具体语法有三种变体，即：普通方程t=t' ;匹配方程t：= t '，其中需要匹配模式t ;以及形式为t的缩写布尔方程，其中t是布尔项，表示方程t = true。例如，下面的系统模块SORTING指定了一个重写理论，其表达式是数组，表示为索引值对的集合，具有测量数组长度的等式定义的长度函数，并且具有单个不连续的重写规则开关，用于切换两个数组位置处的值mod SORTING保护NAT。排序PairPairSet。子排序Pair Pair. opempty：->PairSet。op：PairSet PairSet -> PairSet [ascurrentid：empty]。操作长度：PairSet -> Nat.VARSIJVW：NAT.varPS：PairSet.eq长度（空）= 0。等式length（（I，V）PS）= length（PS）+1。rl [开关]：（J，V）（I，W）=>（J，W）（I，V）。恩德姆3Maude战略语言在本节中，我们将描述策略语言的组合子及其语义。我们有一个简单的集合论语义的重写理论R =（E，E，R）的战略，由一个功能@：Strat×T（X）−→ P（T（X）），它有一个明显的功能扩展，@：Strat× P（T（X））−→ P（T（X）），其中，如果s ∈ Strat且U <$T<$（X），则有s @ U= t∈Us @ t。3.1空闲和故障最简单的策略是常量空闲和失败。 第一个总是成功，但不修改它所应用的项t，即idle @ t= {t}，而第二个总是失败，即fail @ t={t }。3.2基本策略基本策略包括将规则（由相应的规则标签标识）应用于给定术语。在这种情况下，规则被应用于满足其条件的项中的任何地方，而对替换实例化没有进一步的约束。在条件规则的情况下，默认的广度优先搜索策略用于检查条件中的重写因此，如果l是规则标签，t是术语，则l@t的语义是t重写的术语集合8S. Eker等人/理论计算机科学电子笔记174（2007）3在一个步骤中，在任何匹配并满足规则条件的地方使用带有标签l一个稍微更一般的变体允许规则中的变量在其应用之前通过替换进行实例化，即变量到术语的映射，以便用户对规则的应用方式有更多的控制替换|<变量| 替代BasicStrat| 标签Strat无约束的情况L也可以表示为L[none]，其中none表示单位元（空）替换。对于条件规则，重写条件可以通过策略表达式来控制。和前面一样，如果替换为空，则可以省略StratList| 中文（简体）BasicStrat形式L[S]{E1. En}表示基本策略，其在给定状态项中的任何地方应用规则L，其中变量借助于替换S并使用E1，. . .，En作为策略表达式来检查L条件下的重写。出现在规则L的条件中的重写条件片段的数目必须正好是n，表达式才有意义。3.3顶部最常见的情况是允许在给定术语中的任何地方应用规则，如上所述，但我们也提供了一个操作来限制规则仅应用于术语的顶部，因为在一些示例中，如结构化操作语义，唯一有趣或允许的重写步骤发生在顶部。Strattop（BE）仅在给定状态项的顶部应用基本策略BE。 然而，请注意，由于可能存在多个匹配，即使在顶部应用规则也是不确定的，因为匹配是以运算符的等式属性为模进行的，例如结合性，交换性或恒等式。3.4测试测试被看作是检查状态属性的策略，因此测试是如果为真，则策略成功，如果为假，则策略失败。在第一种情况下，国家不是S. Eker等人/理论计算机科学电子笔记174（2007）39∪≥变了也就是说，对于T是一个测试，t是一个项，如果T在t上成功，T@t将求值为{t}，如果它失败，则求值为{t}，因此T在其输入上充当过滤器由于匹配是应用规则时发生的基本步骤之一，测试给定状态项的某些属性的策略基于匹配。 在应用规则时，我们区分了在任何地方匹配和只在给定术语的顶部EqCondition|Term|Term| 平衡条件（EqCondition）测试设备条件|match [s.t. 设备条件|xmatch模式转换器[s.t.设备条件Strat阿马奇山 C是一个测试，当应用于给定的状态tT'时，如果T'的子项与模式T匹配（即，匹配在状态项中的任何地方都是允许的），然后条件C满足在匹配中获得的变量的替换，否则失败。 匹配T s.t. C对应于仅在顶部匹配。 当条件C简单地为真时，它可以被省略。xmatch T s.t. C在顶部执行匹配，但扩展[7]模T的顶部运算符的属性。3.5正则表达式可以组合基本策略，以便将策略应用于执行路径。我们考虑的第一个策略组合子是典型的正则表达式构造：连接、联合和迭代。Strat| 斯特拉特河|ESTRAT ESTRATUNION|Strat|迭代+迭代（1次或多次）连接运算符是结合的，而联合运算符是结合和交换的。 这种并集的交换性在寻找解的方式上提供了一种如果E， EJ是策略表达式，t是项，则（E;EJ）@ t = EJ@（E @ t），（E|EJ）@t=（E @ t）（EJ@t），且E+@t=i1Ei@t，其中E1= E且En=（E;En−1），n >1。当然，E*=空闲|E+。例如，一个形式为E;P的策略（其中P是一个检验）将过滤掉E中所有不满足检验P的结果。10S. Eker等人/理论计算机科学电子笔记174（2007）33.6If-then-else及其衍生策略我们的下一个策略组合子是一个典型的if-then-else，但是被推广， 第一个论点也是一种策略。 我们借鉴了马格德堡的这个想法[27]，但它也出现在ELAN [4，例5.2]中。Strat Strat策略表达式E？E也就是说，根据定义，这个组合子满足以下方程：（E？EJ：EJJ）@ t=if（E @ t ）then EJ@（E @ t）else EJJ@ t fi.请注意，如上所述，一般来说，第一个参数是一个策略表达式，而不仅仅是一个测试。 由于测试是一种策略，我们有特殊的情况，P吗？ E“：E”用于测试P，其中评估符合典型的布尔情况区分：当测试P为真时评估E“，当测试为假时评估E”，考虑到当假时测试qua策略失败。使用if-then-else组合子，我们可以将许多其他有用的策略组合子定义为派生运算。E或 EE或E ' = E？空闲：E'not（E）反转了E的求值结果，因此当E不正确时，not（E）失败，反之亦然。不是（E）= E？失败：空闲not（E）的一个有趣的用法是下面的“规范化”（或“重复直到结束”）操作E！：艾薇！=E*;非（E）try（E）在给定的状态下对E求值;如果成功，则给出相应的结果，但如果失败，则返回初始状态try（E）= E？空闲：空闲测试（E）的评估检查E的成功/失败结果，但它不会改变给定的初始状态。测试（E）=否（E）？失败：空闲注意test（E）= not（not（E））。3.7重写子项对于前面的组合子，我们不能强制将策略应用于给定初始项的特定子项。特别地，（a/x）匹配组合子中的替换作用域仅是对应的条件。我们可以有S. Eker等人/理论计算机科学电子笔记174（2007）311T' = f（. g（. ...）... ...）−→ f（... g（. .）。...）匹配替换T=g（. T1 Tn.）−→ g（. .........................）E1子项的EnFig. 1. xmatchrew组合子的行为。对给定状态的不同子项通过（A/X）matchrew组合子重写的方式的更多控制。TermStratList| TermStratListStrat [设备条件]通过公司简介|火柴头图案 [ S.T. 设备条件 ]由公司简介|xmatchrew模式[s.t. [设备条件]通过公司简介当策略表达式amatchrew T s.t. C乘T1，使用E1，...，Tn使用En被应用于状态项T'，首先是满足T的T'的变形，并且选择满足C。然后，项T1，. . .，Tn（其必须是T的不相交子项），被适当地实例化，如策略表达式E1，，En，respecti vel y. 将结果合并在T中，并将结果合并在T如图1所示。策略表达式E1，，En可以利用实例化在匹配中，因此要注意从状态项中提取的信息（参见4.1节中的示例）。matchrew版本以相同的方式工作，但只在顶部执行匹配，而xmatchrew则在顶部执行匹配。在所有情况下，当条件为真时，它可以被省略。在ELAN和Rupgo [4，27]中使用的同余算子是matchrew组合子的特殊情况，如[20]所示3.8递归递归是通过给策略表达式命名并在策略表达式本身或其他相关策略中使用此名称来实现的。这是在策略模块中完成的（见第3.9节）。具体例子将在第4节中给出。12S. Eker等人/理论计算机科学电子笔记174（2007）33.9策略模块和命令在Maude系统模型M中，用户可以在一个或多个策略模型上编写来定义M的策略。这种战略模式有以下形式：斯摩德·斯特拉特在保护M包括STRAT1。...包括STRATj。E1：T11. T1m@K1。sd E1（P11，.，P1m）：= Exp1....stratEn：. Tnp @ Kn. sd En（Pn1，.，Pnp）：=Expn.csd En（Qn 1，.，Qnp）：=Expn'ifC. endsd其中M是其重写被控制的系统模块，STRAT1，. . . 、STRATp是导入的策略子模块，E1，.. . ，En是标识符，Exp1，...，Expn是策略表达式（在M提供的标签语言上），标识符可以出现在其中，因此允许（相互）递归定义。基本思想是这些策略声明为策略表达式E提供了有用的缩写，然后用户可以在（策略重写）命令srew T using E中使用该缩写，该命令使用策略表达式E重写项T。一个策略识别器可以有数据参数，这些参数是用sample中定义的syntax构建的术语。 当一个策略定义器被定义时（使用关键字strat），其参数的类型（如果有的话）在符号bols：和@之间指定。在此基础上，分析了该策略的条款类型，也可以具体应用。策略定义（以关键字sd引入）将策略表达式（在符号的右侧：=）与策略标识符（在左侧），使用模式作为参数，用于捕获调用策略时传递的值。这些策略定义可以是有条件的（带有关键字csd）。同一个策略标识符可能有几个定义，但它们应该指参数的不相交情况，这是由于模式中使用了不同的构造函数或使用了不同的条件策略模块可以是参数化的。至于其他参数化的Maude模[7]，一个具体参数必须满足的要求在一个理论中具体化，在这种情况下称为策略理论。在策略理论中，可以声明术语（排序和运算符）和策略标识符的语法。例如，下面的策略理论需要一个sortState，两个从State到Bool的运算符，以及一个策略标识符，它不带参数地扩展，并且适用于State项。BT-ELEMS正在保护BOOL。排序状态。op isOk：State -> Bool。op isSolution：State -> Bool.stratexpand @ State。S. Eker等人/理论计算机科学电子笔记174（2007）313结束一个参数化的策略模块，比如STRAT，可以有几个策略理论P1，. . ，Pn作为形式参数。它的头将用语法STRAT{X1：：P1，.，Xn：：Pn}。参数化的策略模块然后可以用作为策略模块S1，.，Sn，分别满足相应战略理论P1，...， Pn. 正如Maude在实例化任何其他类型的参数化模块[7]时所做的那样，每个形式参数Pi与其对应的实际参数Si的绑定由一个视图指定，即由一个理论解释指定，该理论解释将参数理论Pi中的排序映射到策略模块Si中的排序，同样，将运算符映射到运算符或项，将策略标识符映射到策略表达式。在4.3节中，我们展示了一个参数化策略模块的完整示例4一些示例在本节中，我们将展示一些示例来说明策略语言的使用4.1黑板第一个例子是一个简单的游戏。我们有一块黑板，上面写着几个自然数。一个合法的步骤是在黑板上选择两个数字，去掉它们，然后写出它们的算术平均值。 游戏的目标是得到最大的可能的数字写在黑板上在 端在Maude的游戏规范也很简单。mod BLACKBOARD正在保护NAT。排序黑板。子排序Nat Blackboard [黑板].varsMN：Nat.rl[play]：MN=>（M+ N）<$2。恩德姆玩家可以随机选择数字，也可以遵循一些策略。可能的策略包括总是取两个最大的数字，或两个最小的数字，或取最大的和最小的。下面的EXT-BLACKBOARD模块扩展了BLACKBOARD模块的操作，以获得黑板中的最大和最小数字，并删除黑板中的元素mod EXT-BLACKBOARD是包括NAT。包括黑板。操作最 大值 最 小值：Blackboard-> Nat.OP remove：Nat Blackboard ->Blackboard. varsMNXY：Nat.var B：黑板。eqmax（N）= N。等式max（NB）=如果N> max（B）则N elsemax（B）fi。14S. Eker等人/理论计算机科学电子笔记174（2007）3≤−−∧−Y：= 2而YNX：=Y当X>1V[X1]> V[X]时，V[X1]和V[X]X：=X1Y：=Y+1图二. 插入排序。eq min（N）= N。eq min（N B）=if N srew 2000 202 200 10 50 使用 Maxmin .结果 NzNat： 178莫德>srew 2000 202 200 10 50 使用最大 .结果 NzNat： 77莫德>srew 2000 202 200 10 50 使用闵闵 .结果 NzNat：10574.2插入排序在本节中，我们将介绍一种实现插入排序算法的策略。该算法的命令式伪代码如图2所示（用于对数组V [1. N]）。 该算法保留两个索引，一个指向要插入到已排序元素之间的下一个元素，另一个指向要插入的元素。首先，我们定义一个模块SORTING（见第2节），它将数组指定为对的集合，并定义一个规则来切换数组中两个位置的值下面的策略模块定义了sort和insert中的策略，S. Eker等人/理论计算机科学电子笔记174（2007）315−重写排序PairSet的项，并以递归方式表示算法中的循环。这两种策略都有一个自然数作为数据参数。它们表示算法使用的索引。表达式X1表示为sd（X，1），其中sd是NAT模块中预定义的对称差分运算。请注意，内部循环中的合取被分为两个条件， 最后一个策略定义是有条件的，条件X> 1。smod administration-SORT-STRAT是保护排序。varPS：PairSet.varsXYVW：Nat.stratinsort：Nat @ PairSet.sd insort（Y）：= try（match PSs.t. Y =长度（PS）;插入物（Y）;insort（Y+1））。stratinsert：Nat @PairSet。sd插入（1）：=空闲。csd insert（X）：= try（amatch（sd（X，1），V）（X，W）s.t. V > W;switch[J-sd（X，1）;I-X];insert（sd（X，1）如果X> 1.endsmMaude>srew（1，18）（2，14）（3，11）（4，15）（5，12）使用insort（2）。结果PairSet：（1，11）（2，12）（3，14）（4，15）（5，18）有时，一个策略需要记住一些关于它已经做了什么的信息，以便知道它下一步要做什么。 在上面的插入排序策略中，这些信息被保存在insort和insert策略的参数中。但是，取决于这些信息必须被修改的方式，有时这种在[20]中，我们展示了一种使用这种“基于内存”的方法实现插入排序算法的不同方法4.3回溯在本节中，我们展示了一个参数策略，用于使用回溯来解决问题。它要求（部分）解决方案表示为排序状态的项，并且有谓词isOk，以检查部分解决方案是否可扩展为完整解决方案，以及isSolution，以检查我们是否已经有解决方案。它还假设扩展部分解决方案的策略扩展。这些参数要求在3.9节所示的策略理论BT-ELEMS中收集。有了这些成分，我们就可以定义一个通用的策略解决方案，它定义了一个问题如何通过回溯来解决smod BT-STRAT{X：： BT-ELEMS}是var S：X$State.stratsolve @ X$State.sd解算：=（match S s.t. isSolution（S））？空闲：（expand;匹配S s.t. isOk（S）; solve）。16S. Eker等人/理论计算机科学电子笔记174（2007）3×endsm这个策略首先检查它是否已经得到了一个解。 如果是这样，它完成了。 否则，它应用策略expand，检查扩展是否正常， 并递归地继续。我们可以用这个策略找到一条走出迷宫的路。 迷宫的建造为88网格，其中一些单元格具有不能跨越的壁。 该条目在左上位置[1，1]，要找到的出口在右下位置[8，8]。解决方案表示为位置列表，指示要遵循的路径;如果列表在出口处结束，则为解决方案;部分解决方案满足 如果谓词的最终位置在没有墙的网格上，则谓词为Ok，并且列表不包含重复。下面的模块LABYRINTH定义了这些元素，在这里我们使用预定义的模块LIST，它是关于理论TRIV参数化的。fmod POSITIONS正在保护NAT。排序位置op [_，_]：Nat Nat-> Pos.endfm从TRIV到POSITIONS的视图位置排序为Elt到Pos。恩代夫mod LABYRINTH包含LIST{Pos}。op包含：List{Pos} Pos -> Bool。ops isSolution isOk：List{Pos} -> Bool.下一个操作：列表{位置} ->位置。操作墙：->列表{位置}。varsXY：Nat.var P Q：位置var L：List{Pos}.eq wall = * 墙已被省略 *。equisSolution（L [8，8]）= true。eq isSolution（L）= false[owise]。eq包含（nil，P）=false。eq包含（Q L，P）= if P == Q then true else包含（L，P）fi. eqisOk（L [X，Y]）= X>=1 and Y>=1 and X =8 and Y =8而不是（包含（墙，[X，Y]））和（包含（L，[X，Y]））。crl [extend]：如果next（L）=> P，则L => L P。rl [next]：next（L [X，Y]）=> [X +1，Y]。rl[next]：next（L[X，Y]）=>[X，Y+1]。rl [next]：next（L [X，Y]）=>[sd（X，1），Y]。rl [next]：next（L [X，Y]）=>[X，sd（Y，1）]。恩德姆一个非空的列表是通过重写规则extend来扩展的，该规则附加了与最后一个位置相邻的任何位置。此规则必须应用于表示当前部分解决方案的列表的顶部，并使用S. Eker等人/理论计算机科学电子笔记174（2007）317解决条件。这正是下面的战略扩展的具体内容。smod LABYRINTH-STRAT是保护迷宫stratexpand @List{Pos}.sd expand：= top（extend{next}）.endsm下面的视图指出了源理论、目标策略模块以及源理论中每个排序、操作符或策略标识符的映射。未提及的元素获得标识映射，如isOk和isSolution操作。sview LABYRINTH-BT-ELEM从BT-ELEMS到 LABYRINTH-STRAT是将State排序为List{Pos}。恩德SVsmod LABYRINTH-BT-STRAT是包括BT-STRAT{LABYRINTH-BT-ELEM}。endsm4.4抽象同余闭包同余闭包是与有限组基本方程相关的文字问题的判定过程由于它可以用来回答等式和不等式合取的可满足性，它也为不可解释函数符号的理论提供了一个判定过程我们给出了Tiwari给出的同余闭包的抽象公式，它允许对其正确性进行高级证明[25，2]。然后，我们将展示如何推理规则有自然和非常直接的表示重写规则，可以在Maude中执行。继Tiwari之后，我们还展示了Shostak [ 24 ]和Downey-Sethi-Tarjan [ 13 ]的同余闭包算法如何在我们的策略语言中被指定为策略。通过这种方式，我们获得原型，这些算法在莫德在一个直截了当的方式。请注意，由于同余闭包的正确性仅取决于推断规则的正确性[25，2]，并且策略语言仅允许在受控重写理论中正确的重写，因此这些算法的分析可以简化为控制和效率问题：它们永远不会执行不正确的推断。当然，它们仍然可以在完整性方面进行分析Tiwari18S. Eker等人/理论计算机科学电子笔记174（2007）3常数，E是一组方程，R是一组定向方程。扩展（K，E[t]，R）（K{c}，E[c]，R{t→c}）Simpli fication（K，E[t]，R<${t→c}）（K，E[c]，R<${t→c}）定向（K<${c}，E<${t<$c}，R）（K<${c}，E，R<${t→c}）距离（K，E{tt}，R）（K，E，R）Ded（K，E，R{t→c，t →d}（K，E<${c<$d}，R<${t→d}）Collapse（K，E，R）{s[t] →d，t →c}（K，E，R<${s[c] →d，t→c}如果t→c是D-规则如果t>c如果s/t它们在Maude中作为重写规则的表示非常紧密地遵循上述抽象公式，除了常数集K被表示为 作为计数器来生成新的常量。一些辅助功能，假设在推理规则和有一个简单的等式定义，使用。为简洁起见，省略了这些辅助定义crl[Ext]：K，Eu=v，R>=>K+1，Eu如果subterm（u）=>t*u[t]/\isOpConstants？(t)* t-> c是D规则/\c：= c（K）* 新常量/\u '：=subst（u，t，c）.crl[Sim]：K，Eu=v，Rt->c>=>K，Eu如果subterm（u）=>t/\u '：=subst（u，t，c）.crl[Ori]：K，Et=c，R>=>K，E，Rt->c>如果t> c.rl[Del]：K，Et=t，R>=> .crl[Ded]：K，E，Rt->ct->d>=>K，E，Rc->dt->d>S. Eker等人/理论计算机科学电子笔记174（2007）319如果c>d。crl[Col]：K，E，Ru->dt->c>20S. Eker等人/理论计算机科学电子笔记174（2007）3=>K，E，Ru如果subterm（u）=>t/\ t=/= u* 真子项/\u '：= subst（u，t，c）.ShostakTiwari等人' Shostak和Downey-Sethi-Tarjan算法[ 25，2 ]的具体化然而，由于这个公式依赖于对正则表达式的一般理解，而不是将正则表达式作为策略的精确语义，因此给出的正则表达式规范在某种意义上是模糊的。模糊性的根源在于缺乏一个符号来区分策略E，它重复地应用E零次，一次或多次，和策略E！=E;而不是（E），它重复地将E他们对Shostak和Downey-Sethi-Tarjan算法的规范，以及他们在我们的策略语言中相应的更精确的规范如下：• ShostakShos=（（SimExt）（DelOri）（ColDed））sd Shos 1：=（test（Sim|Ext）;Sim！;Ext！ ; try（Del|Ori）;（测试（Col |Ded）; try（Col）;Ded！）！.sd Shos：= matchrew S：State byS：使用Shos 1的状态;（match S：State orelse Shos）.• Downney-Sethi-Tarjan算法[13]：DST=（（Col（Ded{}））（Sim（DelOri）））sd start：=（Ext; Sim！）！奥利！ .sd DST 1：=（测试（Col |Ded）; try（Col）;try（Ded））！;（西姆！;（Del|Ori））！ .sdDST = matchrew S：状态S：使用DST 1的状态;（match S：State orelse DST）.例如，我们现在可以使用DST策略控制的抽象同余闭包规则来Maude> srew0，’f[’f[’a.S]] = ’f[’b.S], mtRlS使用start;DST。结果状态：S. Eker等人/理论计算机科学电子笔记174（2007）321<5，mtEqS，’b.Sc（0）-> c（1）c（2）-> c（4）c（3）-> c（4）’f[c(4)] -> c(4)5执行该语言的第一个建议是通过使用Maude元级特性实现的原型（第5.1节）。 这个原型相对容易开发，并且对于实验目的非常有用，以