合流性
これを図で表現したものが図1である。実線は全称記号、点線は存在記号を意味し、* は簡約化の有限のステップを表す。
書き換え系が合流性を満たすとき、以下が成り立つ。
項 a の正規形は高々1個しか存在しない。
等式 a = b が成立するならば、適当な項 c が存在して a → ∗ c {\displaystyle a{\overset {*}{{}\to {}}}c} かつ b → ∗ c {\displaystyle b{\overset {*}{{}\to {}}}c} である。
なお、正規形が高々一個である事を指して「書き換え順序によらず、結果が一意に定まる」と言われることがあるが、そもそも正規形に辿り着くことが可能かどうか(つまりその順序での書き換えの「結果」と呼べるものが存在するかどうか)は書き換え順序によって変化する事があるため、厳密にはミスリーディングである。常に一意な結果があると言うには「結果」の定義に加え強正規化性等の性質が追加で必要になる。
強合流性(Strong confluence)は局所合流性を強くした性質である。要素 a ∈ A が強合流性を持つとは、 c ← a → b {\displaystyle c\,\leftarrow \,a\,\rightarrow \,b} となる任意の b, c ∈ A について c → = d ← ∗ b {\displaystyle c\,{\overset {=}{{}\to {}}}d\,{\overset {*}{{}\leftarrow {}}}b} となるような d が存在することである。ここで c → = d {\displaystyle c\,{\overset {=}{{}\to {}}}d} とは、 c → d {\displaystyle c\,{{}\to {}}d} か c = d {\displaystyle c\,=d} のいずれかが成立することを表す。これを図で表現したものが図4である。