重写逻辑（Rewriting Logic）

原文来源：维基百科-重写逻辑

重写逻辑解析

分类：计算机逻辑

重写逻辑 是一种能够对多数编程语言及系统进行标准化描述的计算机逻辑体系。该逻辑体系可以将目标逻辑的抽象语法转化为代数结构，并通过重写规则来表达目标逻辑中的推理机制。1

在重写逻辑中，其语法与结构化公理均由用户自行设定，这一特性使得该逻辑体系具备高度的简洁性与广泛适用性。

1992年，José Meseguer 在其发表的论文《作为统一并发模型的条件重写逻辑》中首次引入了重写逻辑这一概念。2

基本公理

重写逻辑体系中最为基础的公理形式表现为 t→t' 这类的重写规则。对于此类规则，存在两种不同的解释路径，即计算性解释与逻辑性解释。这两种解释路径分别对应于重写逻辑在实际应用中的两个重要方向，即语义结构与逻辑结构。3

计算性解读

将t与t'视为系统碎片所处的两种状态，而将重写过程理解为状态之间的转换机制，这种转换方式类似于Petri网中的变迁过程。

语义框架

重写逻辑作为一种形式化工具，能够用于表述计算系统以及编程语言的特性。该逻辑体系专门构建用于描述动态变化过程，具备对系统状态迁移进行完整推理的能力。系统中所