合流性
要素 a ∈ A が 局所合流性(Local confluence)を持つとは、 c ← a → b {\displaystyle c\,\leftarrow \,a\,\rightarrow \,b} となる任意の b, c ∈ A について c → ∗ d ← ∗ b {\displaystyle c\,{\overset {*}{{}\to {}}}d\,{\overset {*}{{}\leftarrow {}}}b} となるような d が存在することである。これを図で表現したものが図2である。
局所合流性は、弱合流性(Weak confluence)あるいは弱チャーチ・ロッサー性(Weak Church-Rosser property)と呼ばれることもある。
局所合流性は合流性より弱い性質で、全ての要素が局所合流性を持つ場合でも、例えば書き換え規則にループが含まれる場合など、システム全体の合流性が成立するとは限らない。
ただし、システムが停止性と局所合流性とを持つ場合、システムは合流性を持つ(ニューマンの補助定理、Newman's lemma)。
チャーチ・ロッサー性(Church-Rosser property)とは、抽象書き換え系 ⟨ A , → ⟩ {\displaystyle \left\langle A,\to \right\rangle } の任意の a , b ∈ A {\displaystyle a,\,b\in \,A} について a ↔ ∗ b {\displaystyle a{\overset {*}{{}\leftrightarrow {}}}b} ならば a → ∗ c and b → ∗ c {\displaystyle a\,{\overset {*}{{}\to {}}}c\quad {\text{and}}\quad b\,{\overset {*}{{}\to {}}}c} となるような c が存在することである。ここで a ↔ ∗ b {\displaystyle a{\overset {*}{{}\leftrightarrow {}}}b} は a と b それぞれの方向に有限ステップで簡約できることを表す。
チャーチ・ロッサー性は合流性と等価である。チャーチ・ロッサー性はラムダ計算でのベータ簡約の合流性を示すチャーチ・ロッサーの定理で用いられた。