クヌース・ベンディックス完備化アルゴリズム
完備化アルゴリズムでは、適当な項順序による向き付けを決めないと書き換え規則が作れない。そのため { f ( x , y ) = f ( y , x ) } {\displaystyle \left\{f(x,y)=f(y,x)\right\}} のように左右の項の向き付けができない等式が現れると完備化が失敗する。失敗無し完備化(unfailing completion、あるいはcompletion without failure)は、このような等式を両方向に使える可能性のある書き換え規則と見なし、適当な代入で停止性が保証される向き付けが得られた場合のみ、この等式を向き付けられた書き換え規則として簡約を行うやり方である。例えば、 x = 2 , y = 1 {\displaystyle x=2,y=1} の場合、 ( f ( 2 , 1 ) > f ( 1 , 2 ) ) {\displaystyle \left(f(2,1)>f(1,2)\right)} のように引数の辞書式順序を用い、等式 { f ( 2 , 1 ) = f ( 1 , 2 ) } {\displaystyle \left\{f(2,1)=f(1,2)\right\}} を f ( 2 , 1 ) → f ( 1 , 2 ) {\displaystyle f(2,1)\to f(1,2)} のように向き付けを行い簡約を行う。
クヌース・ベンディックス完備化アルゴリズムは等式の有限集合をそれと等価な完備性のある項書き換えシステムに変換する。等式の有限集合とは、例えば以下の E g r o u p {\displaystyle E_{group}} ようなものである。これは群の公理である単位元の存在、逆元の存在、結合法則を表す。
E g r o u p = { 0 + a = a ( − a ) + a = 0 ( a + b ) + c = a + ( b + c ) {\displaystyle E_{group}={\begin{cases}0+a=a\\(-a)+a=0\\(a+b)+c=a+(b+c)\end{cases}}}
これらより 0 + a → a {\displaystyle 0+a\to a} , a + 0 → a {\displaystyle a+0\to a} , ( − a ) + a → 0 , . . . {\displaystyle (-a)+a\to 0,...} のような項書き換えの規則 R g r o u p {\displaystyle R_{group}} を作成する。特定の等式 u = v {\displaystyle u=v} が成立するかどうかを調べるためには、u, v それぞれを規則で正規形に書き換え、一致するかを調べればよい。