重写系统

重写是一种将表达式的一部分替换为其它表达式的过程, 可以看作一种关系或者一组规则. 在此之上, 重写系统或抽象重写系统就可以看作是由一个表达式的集合和表达式到表达式之间的重写关系组成的结构, 以及类似的推广结构.

重写系统可以看作箭图或者有向图, 以表达式为顶点, 重写关系为边.

1记号

令表达式的集合为 $E$, 重写关系为 $(\to )\subset E\times E$ (这里意思是说 $\to$ 是一个二元关系).

定义 1.1 (自反传递闭包). 记 ${\to }^{\ast }$ 为 “将 $\to$ 应用任意自然数次” 的关系. 换言之,

•	(自反性) ${\to }^{\ast }$ 是一个自反关系.
•	对于 $a,b\in E$, 若 $a\to b$ 那么 $a{\to }^{\ast }b$.
•	(传递性) 对于 $a,b,c\in E$, 若 $a\to b$ 且 $b{\to }^{\ast }c$ 那么 $a{\to }^{\ast }c$.

定义 1.2 (对称传递闭包). 对于 $a,b\in E$, 若 $a{\to }^{\ast }b$ 或者 $b{\to }^{\ast }a$ 则 $a{\leftrightarrow }^{\ast }b$ 为 ${\to }^{\ast }$. 这对应 1.1 的对称版本.

引理 1.3. ${\leftrightarrow }^{\ast }$ 是一个等价关系.

2性质

正规性

主条目: 正规性 (重写系统)

定义 2.1 (正规形式). 对于重写系统 $E$ 和 $a,b\in E$, 若 $a{\to }^{\ast }b$ 当且仅当 $a=b$, 那么 $a$ 是一个正规形式.

合流性

主条目: 合流性

定义 2.2 (合流性). 若对于重写系统 $E$ 和任意 $a,b,c\in E$ 有 $b{\leftarrow }^{\ast }a{\to }^{\ast }c$, 都存在 $d$ 使得 $b{\to }^{\ast }d{\leftarrow }^{\ast }c$, 那么 $E$ 是合流的.

3例子

•	由整数和加减乘法作为生成元的表达式集合, 配上运算化简 (例如 $1+1\to 2$), 构成一个重写系统.
•	各种$\lambda$ 演算的变体都可以被视为一种重写系统.

4相关概念

•	计算规则可以看作范畴论视角下的重写.

术语翻译

重写 • 英文 rewriting • 俄文 переписывание