合流性
一般的な算術の規則は項書き換え系と見なすことができる。次のような式があるとする。
(11 + 9) × (2 + 4).
この式を書き換える方法は2種類ある。最初の括弧の中を単純化するか、2番目の括弧の中を単純化するかである。最初の括弧の中を先に項書き換えで単純化すると、次のようになる。
20 × (2 + 4) = 20 × 6 = 120.
2番目の括弧の中を先に単純化すると、次のようになる。
(11 + 9) × 6 = 20 × 6 = 120.
算術式は複数の方法で書き換え可能で、どの方法でも最終的な結果正規形は同じになる。つまり、算術規則からなる項書き換え系は合流性を持つ。
これを項書き換えの流れとして表現すると以下のようになる。
一般的な項書き換えシステムを考えると、特定の項を書き換え可能な規則や書き換え可能な部分が複数あるため、書き換えの流れは1通りとは限らない。合流性とは、同じ項から始まる相異なるかも知れない書き換えの流れから二つの項を取り出した時、常に両項を同じ形に書き換えることが可能である事、即ち任意の項 a を簡約化していって項 b, c を得たならば、必ず b, c から合流できる項 d が存在することである。
より形式的には、抽象書換え系 ⟨ A , → ⟩ {\displaystyle \left\langle A,\to \right\rangle } について、a から b への簡約化 (reduction) を a → b、簡約化の有限のステップを a → ∗ b {\displaystyle a{\overset {*}{{}\to {}}}b} と表現した場合、合流性の定義は以下のようになる。
∀ a , b , c ∈ A , ∃ d ∈ A , a → ∗ b and a → ∗ c {\displaystyle \forall a,b,c\in A,\,\exists d\in A,\,a{\overset {*}{{}\to {}}}b\quad {\text{and}}\quad a{\overset {*}{{}\to {}}}c} ⟹ b → ∗ d and c → ∗ d {\displaystyle \implies b{\overset {*}{{}\to {}}}d\quad {\text{and}}\quad c{\overset {*}{{}\to {}}}d}