重写逻辑

在数学、计算机科学和逻辑学中，重写逻辑是把目标逻辑的抽象语法替换为代数结构，通过用其他术语表示公式子项的各种实现方法。利用重写规则，目标逻辑的推理规则可以被描述出来。 重写逻辑中的结构化公理和语法都由用户自己定义，这使其变得极为简单且通用。在最基本的形式中，一种重写的规则可适用多个规则。因此，当与适当的算法结合时，重写系统被视为绝大多数编程语言和系统应用程序进行规范描述的计算机逻辑，许多定理证明和宣告式编程语言是基于重写的。

1992年，José Meseguer在《作为统一并发模型的条件重写逻辑》一文中首先提出重写逻辑这一概念。

基本公理

重写逻辑中的基本公理是形如 t→t'的重写规则。重写规则涵盖了计算性解读与逻辑性解读两种解读方式。这两种不同的解读方式能对应重写逻辑的两种应用价值：语义框架和逻辑框架。

计算性解读

把t、t'看作系统碎片的状态，把重写当作状态迁移（类似Petri网）。

语义框架

重写逻辑可以用来表达计算系统和编程语言。重写逻辑被设计成一种描述变化的逻辑，能对系统的迁移进行完备的推理。系统的基本变化用重写规则刻画。

逻辑性解读

把t、t'看作公式，t→t'表示t可以推导出t'。

逻辑框架

重写逻辑可以被用来表达其他逻辑（如等式逻辑、线性逻辑及霍尔逻辑等）。

与项重写系统

重写逻辑这一概念由José Meseguer等提出并定义，并作为他们自己开发的Maude的基础。 但计算机科学界一般把大部分相关知识体系归到“项重写系统”。 项重写和项重写系统的最早研究可以追溯到数理逻辑发展早期，如弗雷格，Herbrand，哥德尔等人的工作，虽然那时候并没有明确提出“项重写系统”这个概念。2003年，荷兰的klop等人出版了第一本研究项重写系统的专著《term rewriting systems》，系统阐述了项重写系统的历史起源和概念，主要内容，课题和应用。klop等的书中稍微提及重写逻辑，脚注为“实际上就是没有对称性的等式逻辑(equational logic without symmetry)”。 在列举基于项重写系统的软件系统时描述José Meseguer等开发的Maude为“可以按照等式逻辑和重写逻辑推理”，遵照了José Meseguer等自己对Maude的描述用词。20世纪80年代到90年代曾出现基于项重写系统的程序语言设计的热潮，其中Obj系列的项重写语言比较有名，而Maude是对Obj3的继承。基于项重写的程序语言的特点是匹配和替换(重写)，因此，函数式编程语言Haskell也属于这一类。而且，函数式编程语言的理论基础——lambda演算和组合逻辑——本身就被认为是典型的项重写系统。其它基于项重写的语言或系统包括：Isabella,Pure,Clean等。

Maude

Maude是José Meseguer等带领下开发的基于重写逻辑的软件。可以同时支持等式逻辑和重写逻辑推理。 Maude可以用关键字comm和assoc来指定模交换律和结合律的重写（rewriting modulo commutativity and associativity）。pure等语言同样可以使用 a+(b+c)=(a+b)+c的等式来指定“+”的结合律。不过，pure确实不能通过a+b=b+a来指定“+”的交换律，因为这样的等式会造成 a+b=b+a=a+b...无穷推理下去。这是因为a+b和b+a的匹配模式是一样的，而a+(b+c)和(a+b)+c的匹配模式不一样。后者不会造成无穷推理。而pure语言确实没有提供模交换律的重写。这一点上，Maude是占有优势的。

外部链接

• The Rewriting Home Page （页面存档备份，存于互联网档案馆）
• IFIP Working Group 1.6 （页面存档备份，存于互联网档案馆）
• 因斯布鲁克大学Researchers in rewriting （页面存档备份，存于互联网档案馆）
• Termination Portal
• Maude System （页面存档备份，存于互联网档案馆） — 通用术语重写系统的软件实现。

参见

• 临界对 (逻辑)
• 编译器
• Knuth-Bendix 完成算法
• L系统指定并行完成的重写。
• 计算机科学中的参考透明度
• Regulated rewriting
• Rho演算
• Interaction nets