クヌース・ベンディックス完備化アルゴリズム
クヌース・ベンディックス完備化アルゴリズムのベースとなる考え方は以下のように表現できる。
合流性:
発散する危険対を見付け出し、危険対を合流させる書き換え規則を追加することで、危険対を収束させる。
停止性:
対象となる項は何らかの規則で順序化されているものとし、書き換え規則は項順序の大きいものから小さいものに簡約していく。対象となる項の集合が有限な場合、項順序には必ず下限があるので、項順序の大きいものから小さいものに簡約していく書き換え規則が存在すれば、書き換えシステムは必ず停止する。
単純化したクヌース・ベンディックス完備化アルゴリズムは以下の通りである。R は書き換え規則の有限集合、E は等式の有限集合、> は停止性を保証する項順序を表す。また、危険対 ( p , q ) {\displaystyle \left(p,q\right)} は E 中の等式 p = q {\displaystyle p=q} として表現される。E の初期値は対象となる等式、R の初期値は空である。
このアルゴリズムの結果は、(1)停止して結果が R に求まる、(2)停止しない、(3)完備化失敗として終了、の3通りがある。
例えば危険対を合流させる規則の追加により新たな危険対が発生し続ける場合など、規則が有限にならない場合、このアルゴリズムは停止しない。つまり、正確には半アルゴリズム(semi-algorithm)である。