クヌース・ベンディックス完備化アルゴリズム
一般に、項書き換えシステムは項の書き換え(簡約、reduction)が必ず停止するとは限らず、また書き換えの際に複数の書き換え規則を適用できる場合は最終的な結果が一意になるとは限らない。
無限の簡約の列が存在しないことを停止性、複数の書き換え規則を適用可能な場合にその後の簡約の流れが合流することを合流性と言う。停止性と合流性を両方もっていれば、システムは完備(completion)と言う。
完備性があるシステムは、最終的な結果が必ず求まり、その結果は簡約の順序によらず一意になる。
以下では、a から b への簡約を a → b {\displaystyle a\to b} 、a を簡約していってこれ以上簡約できなくなった最も単純な形(正規形、英: normal form)を a ↓ {\displaystyle a\downarrow } と表記する。