クヌース・ベンディックス完備化アルゴリズム
危険対の要素をそれぞれ簡約化して正規形を求めたとき、両者が一致する場合を"収束する"、一致しない場合を"発散する"という。危険対について、以下の定理が成立する。
書き換え規則が有限であれば危険対も有限であり、項書き換えシステムが停止性をみたす場合は危険対の各要素の正規形も有限の簡約ステップで求めることができる。つまり、停止性を満たす項書き換えシステムの合流性は以下の有限のステップで分かる。
システムの危険対を全て求める。
危険対 ( p , q ) {\displaystyle \left(p,q\right)} について正規形 ( p ↓ , q ↓ ) {\displaystyle \left(p\downarrow ,q\downarrow \right)} を求める。
p ↓= q ↓ {\displaystyle p\downarrow =q\downarrow } であるかどうかを調べる。
全ての ( p , q ) {\displaystyle \left(p,q\right)} について p ↓= q ↓ {\displaystyle p\downarrow =q\downarrow } であれば、システムは合流性を持つ。