[科普中国]-重写逻辑

重写逻辑是一种对绝大多数编程语言和系统进行规范描述的计算机逻辑。重写逻辑能把目标逻辑的抽象语法表示为代数结构。利用重写规则，目标逻辑的推理规则可以被描述出来。

重写逻辑中的语法和结构化公理都由用户自己定义，这使其变得极为简单且通用。

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等。

MaudeMaude是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是占有优势的。

国内研究国内有学者认为把“重写逻辑”提升到一个单独概念而与“项重写系统”相分别可能是没有必要的，其理由是：很多基于项重写的系统和语言都具有跟Maude相近的机制和能力1，但他们的作者并没有提到自己的软件是基于重写逻辑。从项重写的角度理解这些系统和语言（包括Maude）的运行机理是非常自然的。重写逻辑的提法反而让人感到困惑。所有项重写语言使用等式逻辑运行时本来就是单向的（所谓的重写逻辑！）
不过，上述考虑是基于Maude和其他语言（如Haskell以及Pure）中的规则被“计算性解读”的情形下；如果考虑Meseguer提出的“逻辑性解读”，非对称推理的重写和对称推理的等式确实不一样。考虑如下语句：

a=b；a=c；则可以得到 c=b a->b；a->c；得不到 c->b Maude在运行时并不会把c重写到b,但如果使用Maude的search命令（不变量检测）或LTL模型检测工具来分析上述语句时，Maude确实把等式和重写规则分别对待（如果是等式规则，search c => b是满足的，重写规则不满足； => 表示可达或可推理得到）。此外，Maude的开发者开发了一些附带工具用来检测等式规则和重写规则的其它性质。这包括终止性，合流性，而这些都是项重写系统研究课题中的内容。而Pure和Haskell等语言并不集成search命令或LTL模型检测工具。虽然程序员也可以自己开发这些不平凡的工具。
总体来说，Maude的语法虽然没有Haskell优雅，但功能设计上Maude比Haskell更偏向对项重写系统的分析。后者定位在一种通用（虽然是函数式，不是命令式）的编程语言。Maude使用reduce命令(可简写为red)完成Haskell那样的计算任务(规则的计算性解读)，使用search命令，LTL(连同red)checker，以及其他checker完成项重写系统的其它分析任务（规则的逻辑性解读）。
国内已经有学者把Maude用于模型检测和缺省逻辑研究。Maude一般不作为通用的编程语言，虽然它也可以完成简单的计算任务。但它用于实用计算的库太少了（数值计算，图形和网络编程）。

本词条内容贡献者为:

王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所