クヌース・ベンディックス完備化アルゴリズム（クヌース・ベンディックスかんびかアルゴリズム、英: Knuth?Bendix completion algorithm）、あるいはクヌース・ベンディックス完備化手続きは、等式の有限集合をそれと等価な完備性のある項書き換えシステムに変換するアルゴリズムである。このアルゴリズムは普遍代数（en）での語の問題（word problem）（en）を解くための手法としてクヌースとベンディックスから提案された[1]。アルゴリズムは必ず成功するとは限らないが、成功した場合は停止性と合流性のある項書き換えシステムを生成することができる。そのベースとなる考え方は多くの分野で応用することができる。
背景

一般に、項書き換えシステムは項の書き換え（簡約、reduction）が必ず停止するとは限らず、また書き換えの際に複数の書き換え規則を適用できる場合は最終的な結果が一意になるとは限らない。

無限の簡約の列が存在しないことを停止性、複数の書き換え規則を適用可能な場合にその後の簡約の流れが合流することを合流性と言う。停止性と合流性を両方もっていれば、システムは完備（completion）と言う。

完備性があるシステムは、最終的な結果が必ず求まり、その結果は簡約の順序によらず一意になる。

以下では、a から b への簡約を a → b {\displaystyle a\to b} 、a を簡約していってこれ以上簡約できなくなった最も単純な形（正規形、英: normal form）を a ↓ {\displaystyle a\downarrow } と表記する。
危険対

ある要素に対し2つの書き換え規則を適用可能な場合がありうる。2つの規則の条件に重なりがあるとき、それらの規則で簡約した異なる結果のペアを危険対（英: critical pair）と呼ぶ。危険対が存在する場合、どの書き換え規則を適用するかにより簡約の結果が変わる可能性がある。

例えば、以下の項書き換え規則を考える。 ρ 1   :   f ( g ( x , y ) , z ) → g ( x , z ) {\displaystyle \rho _{1}\ :\ f(g(x,y),z)\rightarrow g(x,z)} ρ 2   :   g ( x , y ) → x {\displaystyle \rho _{2}\ :\ g(x,y)\rightarrow x}

項 f ( g ( x , x ) , x ) {\displaystyle f\left(g(x,x),x\right)} を考える。 ρ1 を適用すると項 g ( x , x ) {\displaystyle g\left(x,x\right)} が得られ、ρ2 を適用すると項 f ( x , x ) {\displaystyle f\left(x,x\right)} が得られる。このときの危険対は、 ( g ( x , x ) , f ( x , x ) ) {\displaystyle \left(g(x,x),f(x,x)\right)} である。
クヌース・ベンディックスの合流条件

危険対の要素をそれぞれ簡約化して正規形を求めたとき、両者が一致する場合を"収束する"、一致しない場合を"発散する"という。危険対について、以下の定理が成立する。クヌース・ベンディックスの合流条件 停止性を満たす項書き換えシステム R が合流性（つまり完備性）をもつための 必要十分条件は R の全ての危険対が収束することである。

書き換え規則が有限であれば危険対も有限であり、項書き換えシステムが停止性をみたす場合は危険対の各要素の正規形も有限の簡約ステップで求めることができる。つまり、停止性を満たす項書き換えシステムの合流性は以下の有限のステップで分かる。
システムの危険対を全て求める。

危険対 ( 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 } であれば、システムは合流性を持つ。

アルゴリズム

クヌース・ベンディックス完備化アルゴリズムは等式の有限集合をそれと等価な完備性のある項書き換えシステムに変換する。等式の有限集合とは、例えば以下の 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 それぞれを規則で正規形に書き換え、一致するかを調べればよい。

クヌース・ベンディックス完備化アルゴリズムのベースとなる考え方は以下のように表現できる。

合流性：
発散する危険対を見付け出し、危険対を合流させる書き換え規則を追加することで、危険対を収束させる。

停止性：
対象となる項は何らかの規則で順序化されているものとし、書き換え規則は項順序の大きいものから小さいものに簡約していく。対象となる項の集合が有限な場合、項順序には必ず下限があるので、項順序の大きいものから小さいものに簡約していく書き換え規則が存在すれば、書き換えシステムは必ず停止する。

単純化したクヌース・ベンディックス完備化アルゴリズムは以下の通りである。R は書き換え規則の有限集合、E は等式の有限集合、＞ は停止性を保証する項順序を表す。