正规性 (重写系统)

关于其它含义, 请参见 “正规”.

在重写系统中, 正规性说的是该重写系统在不同程度上满足的 “停机性”.

1定义

定义 1.1. 重写系统中的表达式若不能被进一步重写, 那么它是一个正规形式.

定义 1.2. 若重写系统中任意表达式都能通过某个特定的顺序重写为正规形式, 那么该重写系统是弱正规的.

定义 1.3. 若重写系统中任意表达式都能通过任意顺序重写为正规形式, 那么该重写系统是强正规的. 强正规性又叫停机性.

如果固定一个重写策略 (即遇到多种可用的重写关系时, 每次都按照一个固定的规则选取重写关系), 那么正规性的强弱就没有区别.

强正规显然蕴含弱正规, 因此找到一个弱正规的反例就证明了该重写系统不停机.

术语翻译

正规性 • 英文 normalization

正规形式 • 英文 normal form