战略重写：基于规则的编程和声明性功能的挑战

理论计算机科学电子笔记124（2005）3-9www.elsevier.com/locate/entcs战略重写克劳德·基什内尔1洛丽亚·因里亚615，rueduJardinBotaniquee54600Villers-l`es-Nancy，France摘要这是一份立场文件，为第四届重写和方案编制中的减少战略国际研讨会期间组织的圆桌会议做准备。我概述了我认为是战略改写的重要挑战。保留字：重写，规则语言，策略，策略1什么和如何声明式编程在许多领域都是非常可取的，它允许我们描述我们想要做什么，而不是如何做。它不仅允许更好地理解编程的内容，而且允许通过描述其属性并搜索或检查其证明来使程序和系统更安全。这是典型的基于规则的编程（无论是在其代数形式或. .由于声明性功能的扩展以及我们想要表达对自身的巧妙控制，这些控制的描述本身就变成了声明性的，因此本身也受到Meta控制的影响。1电子邮件：Claude. loria.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.0174C. Kirchner/Electronic Notes in Theoretical Computer Science 124（2005）32我们要编什么程序？事实上，第一个当然，计算机是今天的大型编程工地。但这不是它，因为我们也想编程分子，细胞和复杂的有机体。在所有情况下，即使一些实现细节不同，我们也面临着同样的编程挑战，应该指定并可能执行什么和如何。3基于规则的语言基于规则的编程之所以特别有吸引力，首先是它能够使用模式匹配来区分我们想要采取行动的配置;其次，它能够执行特定于这种区分的动作。因此，对基本作用的理解是局部的，而且通常是容易的。当然，全局图像，即一组规则的动作的语义要详细得多，并且取决于对规则的触发的控制。因为这种控制本身可以用声明的方式来描述，所以在重写社区中，它被称为策略。但是，人们也谈到计划或战术和战术，以编程证明搜索在许多定理证明器。由于程序员倾向于以更抽象的方式建模，编程对象变得更符号化，因此需要进行模式匹配。因此，典型的对象是术语、图形、命题或子句、约束、。. .4ELAN体验当我们在90年代初开始设计和实现ELAN语言时，首先使用从乳胶文件到ELAN文件的几乎恒等函数来建模推理过程，即能够以非常接近数学语法的语法来但是，使这样一个模型可执行立即面临的挑战，描述推理规则应用程序的策略对于一个给定的重写系统，我们定义一个策略只是C. Kirchner/Electronic Notes in Theoretical Computer Science 124（2005）35所有重写的推导这个集合可以非常精细，甚至是非递归的。这里有趣的是设计和研究形式主义来描述感兴趣的策略。考虑到ELAN策略的设计，我们使用适当的重写逻辑的证明项或作为适当的重写演算项将其形式化第一种方法是完全声明性的，并没有精确地描述这个集合。前者的声明性较低，但为我们提供了一种构建预期派生的建设性方法。我们把由规则系统和策略组成的一对称为语言中引入的第一个策略除了标准的策略，如首先是dk，dc（不知道也不在乎），然后是更详细的语义ELAN策略的语义一个更功能的语义学[4]最终导致重写演算的出现，研究和应用[7，8]2。敏捷性作为实验时，许多应用程序开发的ELAN编码，这些策略组合子是非常有用的，并允许开发简洁的模型3。但它们在建模时的敏捷性也有局限性，例如在解决CSP [5]时的智能回溯，或者简单的广度优先搜索，或者概率选择。使用[1]中为ELAN开发的扩展策略语言或使用响应方法[18]可以实现一些可扩展性。但总的来说，人们希望有一个完整的策略语言，具有清晰和简单的语义和良好的实用效率。5战略挑战ELAN的经验是富有成效的和鼓舞人心的（见ELAN[22]4或新的Maude策略语言[20]），它的设计和使用提供了许多关于建模策略所需的反馈2 另见重写微积分网页;www.loria.fr/~faure/TheRhoCalculusHomePage。3实例、应用和贡献可在ELAN网页上查阅elan.loria.fr4 www.stratego-language.org/Stratego/StrategoHistory6C. Kirchner/Electronic Notes in Theoretical Computer Science 124（2005）3以下是我目前所看到的挑战，各种困难，在研究战略规划以及实施和传播。企业战略当然，第一个挑战是有更好的方法来指定策略，记住我们希望对它们进行证明，评估和分享。从现有的策略语言中，我们应该找到描述策略的最合适的方法和构建策略的最佳组合子。该问题的一个典型例子是建立一种策略语言来方便地建模概率算法以及它们的性质和证明工具。一个不同但相关的问题在于描述概率证明方法。从迄今为止所取得的成就来看，重写演算是我认为目前最有希望在适当的细节级别上统一表达策略的框架，特别是因为它为我们提供了lambda演算的可能类型化扩展，具有匹配（模）功能，显式非确定性，以及精细表达策略所需的详细例外和控制机制。这还需要做很多工作。策略重写一旦我们通过对允许的推导增加一些限制来改变重写关系，我们就必须重新考虑生成关系的相关证明工具。通常的性质，如连续性、终止性、定义的完备性等等，都不能再像以前那样加以检验了，因为这种关系已经发生了深刻的变化。因此，我们需要为策略引导重写提供新的证明工具。几年来，在这个方向上已经取得了第一个结果[19，17，12，13]，但主要是重写系统生成的重写关系的每个先前已知的结果现在应该被推广到处理策略控制的重写系统。当然，策略重写系统的计算能力相对于重写系统的计算能力而改变。因此，这就为标准问题的可判定性和复杂性打开了大门，如可达性、终止性、连续性等，用于特定的战略重写系统。静态分析，特别是通过类型系统，模型检查或抽象解释是有希望的，以保证适当的健全程序的属性。C. Kirchner/Electronic Notes in Theoretical Computer Science 124（2005）37战略评价一个普遍的看法是，通过使策略明确，我们获得了清晰度和表达能力，但有可能导致评估效率降低。这在第一个近似值中肯定是正确的。但是，使控制显式允许我们执行切割机分析，以简化或优化控制，并生成高效的代码。例如，在[1，13]中描述了策略的简化。代码生成也可以受益于这些部分评估，我们仍然处于理解如何适应战略重写的开始。共享战略一个巨大的任务是编写策略，这是非常重要的。当然，分享这些工作和知识是一项根本的利益和挑战。这方面的第一项工作涉及PVS和Coq证明搜索编程环境之间的策略共享[16]。一般来说，我们希望尽可能地将策略与它们所应用的数据和基本动作断开连接，建立一种类似于TOM的方法，其中模式匹配和重写能力独立于它们所锚定的语言[21]5。战略应用和转让战略成果和技术向实际应用的深度转化是一项重要任务。当然，一个主流是定理证明（即。证明搜索规范）和验证，因为每个证明者或验证者都以巧妙的策略为中心，无论是隐式的还是显式的。在这方面，我们使用ELAN或TOM执行模型检查的经验表明，战略编程至少可以与专用模型检查器一样有效[9，6]，但使用更抽象的模型描述。对战略方案拟订的应用仍处于初级阶段。事实上，正如在ELAN、Maude、MongoGo或Rogue中进行的经验所表明的那样，从战略编程的角度来看，编写算法的方式是非常不同的。这就意味着，既要开展关于使用这种范式的编程方法的研究，又要大力教授这种编程方法，而目前的情况并非如此。这可能会迅速改变，因为方法的根本利益，因为它在什么和如何之间有很强的区别，而且因为5 另见tom.loria.fr。8C. Kirchner/Electronic Notes in Theoretical Computer Science 124（2005）3基于XML的应用正变得非常流行。这意味着符号和特别是术语结构是无所不在的，并且规则库编程成为必须。像JavaScript这样的编程语言并没有利用策略的显式使用：策略编程在这里有很大的展示和发展的机会。另一个应用领域是生产或业务规则意义上的基于规则的系统[14]。这里的基本要素之一是策略，特别是在规则激活中[10]。由于这也成为一种非常流行的方式来理解和建模公司，市场，生态，工业或经济过程的组织和分析，战略规划也将在这里发挥主要作用。正如我在开始时提到的，模拟和编程生物实体是本世纪的主要挑战之一。由于策略编程提供了声明性和策略性的使用，特别是允许并发的自然规范，它可能是模拟生物系统等复杂系统的最佳编程范式之一。在这方面，使用Maude[11]的第一次经验看起来很有希望，应该在不久的将来从更加战略导向的角度进行开发致谢：非常感谢Protheo团队过去和现在的所有成员，以及LuigiLiquori和Pierre-Etienne Moreau对本文初稿的评论引用[1] P. Borova n sky'.Lecon t r o ntroledelareec riture：etudetimpl antationd' u n f o r m e d e s t a t eg i es。Th`esedeDoctoratd' U niversit'e，U niversit'e H en ri Poi n c ar'e- N an n c y 1，法国，1998年10月。TR LORIA 98-T-326[2] P. Borova n sky'，H. Cir st ea，H. 杜博伊斯，C。 K irchn er，H. Kir chn er，P. - E. 莫雷阿乌，Q。-H. 恩古伊恩，C. Ringeissen和M.维特克ELANV 3.6用户手册。 Loria，Nancy（法国），第五版，2004年2月。[3] P. Borovansky，C. Kirchner，H. Kirchner和P. - E. 莫罗 从重写逻辑的观点来看。TheoreticalComputer Science，2（285）：155[4] P. Borova n sky'，C. Kirchner，H. Kirchner和C. 我给他打电话。 用ELAN中的语法规则重写：一种功能语义学。International Journal of Foundations of Computer Science，12（1）：69-98，February 2001.[5] C.卡斯特罗使用重写规则和策略构建约束满足问题求解器。Fundamenta Informaticae，34：263[6] H. Cirstea。使用重写和策略的身份验证协议。第三届国际声明性语言实践研讨会，计算机科学讲义1990卷，第138-153页[7] H. Cirstea和C.基什内尔重写演算-第一部分和第二部分。Logic Journal of the Interest Group inPure and Applied Logics，9（3）：427C. Kirchner/Electronic Notes in Theoretical Computer Science 124（2005）39[8] H.奇尔斯泰阿角基什内尔湖Liquori和B.变态 重写演算中的重写策略。 芽孢杆菌中Gramlich和S.卢卡斯，编辑，电子笔记理论计算机科学，第86卷。Elsevier，2003年。[9] H. Cirstea，P. E. Moreau和A.雷列斯Java中基于规则的编程，用于协议验证。 在N. Mart′s-Oliet，editor，ProceedingingsFifthInternationalWorkshoponRewritingLogicanditsApplications，WRLA 2004，Barcelona，Spain，March 27Elsevier，2004年。[10] H. Dubois和H. 基什内尔 基于约束和策略的规则编程。 在K. Apt，A. A. C. Kakas，E. Monfroy和F. Rossi，editors，New Trends in Constraints，Papersfrom the Joint ERCIM/Computlog-Net Workshop ， Cyprus ， October 25-27 ， 1999 ，Volume 1865 ofLecture Notes in Arti Ficial Intelligence，pages 274Springer-Verlag，2000.[11] S. Eker，M. Knapp，K. Laderoute，P. Lincoln，J. Meseguer，and K. 桑梅兹 途径 逻辑：对生物信号的符号分析。在太平洋生物计算研讨会论文集，第400-412页[12] O. 菲索尔岛 格内迪格， 和 H. 基什内尔 Cariboo ： 一个 感应 基于 证明 用战略来终止的工具。第四届声明式编程原则和实践国际会议论文集，第62-73页Press.[13] O.菲索尔岛Gnaedig和H.基什内尔基于规则的语言中策略的简化和终止。第五届声明式编程原则和实践国际会议（PPDP），瑞典乌普萨拉，2003年8月。Press.[14] C. 福吉Rete：一个快速的多模式/多对象模式匹配算法。Arti ficial Intelligence，19（1）：17[15] C. Kirchner，H. Kirchner，and M. 维特克 使用计算系统设计CLP。 在P. Van Hentenryck和S. Saraswat，编辑，约束编程的原理和实践。麻省理工学院出版社，1995年。[16] F. 基 什 内 尔 走 向 共 同 的 战 术 语 言 ： coq 和 pvs 的 案 例 。 硕 士 论 文 ， Universitée DénisDiderot，Paris，France，S ept em ber r 2003。[17] H.基什内尔和我。格奈迪格战略下的终止和规范化-ELAN中的证明。 在Proceedigs of the ThirdInternational Workshop on Rewriting Logic and its Applications中，第36卷Electronic NotesIn Theoretical Computer Science ， Kanazawa ， JAPAN ， 2000 年 9 月 。 Elsevier SciencePublishers B.诉（北荷兰）。[18] H. Kirchner和P. - E.莫罗Elan的一个相应扩展。In J. Meseguer，editor，Proceedings of thefirst international workshop on rewriting logic ， volume 4 ， Asilomar （ California ） ，September 1996.理论计算机科学电子笔记。[19] S. 卢 卡 斯 通 过 重 写 来 终 止 上 下 文 相 关 的 重 写 。 在 Proceedings of the 23rd InternationalColloquium on Automata，Languages and Programming，Volume 1099 ofLecture Notes inComputer Science，pages 122Springer-Verlag，1996.[20] N. 天啊-哦，撒谎，J。 Meseguer和A。 我来了。这两个是一个非常有趣的故事。InN. Mart′s-Oliet，editor，ProceedingingsFifthInterna t i o n at i o n a tion a t i o na ti n g l W o r ks h o p o n R e w r i t i n g i c a n d i t s Applications，WRLA 2004，Barcelona，Spain，2004年3月27日至4月4日Elsevier，2004年。[21] P. - E.莫罗角，澳-地Ringeissen和M.维特克一个用于多种目标语言的模式匹配编译器。InG.Hedin，编辑，计算机构造国际会议-CC[22] E.维瑟Replego：一种基于重写策略的程序转换语言。系统描述：以. Middeldorp，编辑，重写技术和应用（RTASpringer-Verlag，2001年5月。[23] M. 维特克 ELAN：一种用于编程语言原型的逻辑框架. 1994年10月1日，联合国开发计划署（开发计划署）通过了一项名为《联合国开发计划署，联合国开发计划署