合流性

合流性指重写系统中不同的重写路径终将归一的性质.

$\lambda$ 演算作为重写系统是满足合流性的, 这一定理叫做 Church–Rosser 定理.

1定义

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

2性质

在定义 1.1 中, 对 $a{\to }^{\ast }b$ (即一串单步重写 $a=a_1\to \cdots \to a_n=b$) 的长度做归纳, 就可以得到一个等价的描述:

引理 2.1. 重写系统 $E$ 合流, 等价于当对于任何 $a,b,c\in E$ 有 $b\leftarrow a{\to }^{\ast }c$, 都存在 $d$ 使得 $b{\to }^{\ast }d{\leftarrow }^{\ast }c$.

但是需要注意的是, 不能再将另一侧 $a{\to }^{\ast }c$ 也改进为 $a\to c$. 考虑有两个生成元的幺半群$$E=⟨u,v\mid uvv=vuu⟩.$$在 $E$ 上定义重写关系: 对任意元素 $a$ 有 $a\to au$, $a\to av$. 此时对于任何 $b\leftarrow a\to c$, 唯一非平凡的情况是 $b=au,c=av$. 因此, 有如下重写关系:$$aauavauvavuauvvavuu$$但是这个系统没有合流性, 例如 $uu{\leftarrow }^{\ast }e{\to }^{\ast }vv$, 但是不存在 $d$ 使得 $uu{\to }^{\ast }d{\leftarrow }^{\ast }vv$.

另一方面, 如果已经知道重写系统有停机性, 即任何链 $a\to a_1\to a_2\to \cdots$ 都必然在有限步停止, 那么的确可以做此改进.

术语翻译

合流性 • 英文 confluence