クヌース・ベンディックス完備化アルゴリズム

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

背景

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

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

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

以下では、a から b への簡約を $a\to b$ 、a を簡約していってこれ以上簡約できなくなった最も単純な形（正規形、テンプレート:Lang-en-short）を $a\downarrow$ と表記する。

危険対

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

例えば、以下の項書き換え規則を考える。

${\rho }_1:f(g(x,y),z)\to g(x,z)$

${\rho }_2:g(x,y)\to x$

項 $f(g(x,x),x)$ を考える。 ρ₁ を適用すると項 $g(x,x)$ が得られ、ρ₂ を適用すると項 $f(x,x)$ が得られる。このときの危険対は、$(g(x,x),f(x,x))$ である。

クヌース・ベンディックスの合流条件

危険対の要素をそれぞれ簡約化して正規形を求めたとき、両者が一致する場合を"収束する"、一致しない場合を"発散する"という。危険対について、以下の定理が成立する。

クヌース・ベンディックスの合流条件
  停止性を満たす項書き換えシステム R が合流性（つまり完備性）をもつための
  必要十分条件は R の全ての危険対が収束することである。

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

1. システムの危険対を全て求める。
2. 危険対 $(p,q)$ について正規形 $(p\downarrow ,q\downarrow )$ を求める。
3. $p\downarrow =q\downarrow$ であるかどうかを調べる。
4. 全ての $(p,q)$ について $p\downarrow =q\downarrow$ であれば、システムは合流性を持つ。

アルゴリズム

クヌース・ベンディックス完備化アルゴリズムは等式の有限集合をそれと等価な完備性のある項書き換えシステムに変換する。等式の有限集合とは、例えば以下の $E_{group}$ ようなものである。これは群の公理である単位元の存在、逆元の存在、結合法則を表す。

$E_{group}=\{\begin{array}{c}0+a=a\\ (-a)+a=0\\ (a+b)+c=a+(b+c)\end{array}$

これらより $0+a\to a$, $a+0\to a$, $(-a)+a\to 0,...$ のような項書き換えの規則 $R_{group}$ を作成する。特定の等式 $u=v$ が成立するかどうかを調べるためには、u, v それぞれを規則で正規形に書き換え、一致するかを調べればよい。

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

• 合流性：

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

• 停止性：

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

単純化したクヌース・ベンディックス完備化アルゴリズムは以下の通りである。R は書き換え規則の有限集合、E は等式の有限集合、＞ は停止性を保証する項順序を表す。また、危険対 $(p,q)$ は E 中の等式 $p=q$ として表現される。E の初期値は対象となる等式、R の初期値は空である。

E が空になるまで繰り返す。
    E から等式 $s=t$ を1つ選択し、取り除く。
    正規形 $s\downarrow$、 $t\downarrow$ を求める
    もし $s\downarrow \equiv ̸t\downarrow$ ならば、
        もし $s\downarrow >t\downarrow$ ならば
            $s\downarrow \to t\downarrow$ を R に追加する。
        もし $s\downarrow <t\downarrow$ ならば
            $t\downarrow \to s\downarrow$ を R に追加する。
        そうでなければ完備化失敗として終了
        新しい R から生成される全ての危険対を等式にして E に追加する。

このアルゴリズムの結果は、(1)停止して結果が R に求まる、(2)停止しない、(3)完備化失敗として終了、の3通りがある。

例えば危険対を合流させる規則の追加により新たな危険対が発生し続ける場合など、規則が有限にならない場合、このアルゴリズムは停止しない。つまり、正確には半アルゴリズム（テンプレート:Lang）である。また、等式の左右の項が順序化できない場合、書き換え規則を作成できず完備化は失敗する。

しかし、クヌース・ベンディックス完備化アルゴリズムが停止する場合、生成された項書き換えシステムが完備性を持っていることは証明されている。

なお、上記の手続きのままでは、規則の追加に伴って冗長な規則が増えていき、発散する危険対も多くなる。実際には、規則を追加していく際に以下のルールを用いて等式や書き換え規則の正規化を行い、冗長なものを取り除く。

• 等式の正規化（normalise equation）

E に等式 { s = t } があり、R で t が正規形 u に書き換えられるなら、等式 { s = u } に正規化

• 規則の正規化（normalise rule）

R に規則 { $s\to t$ } があり、R で t が正規形 u に書き換えられるなら、規則 { $s\to u$ } に正規化

• 規則の折り畳み（collapse rule）

R に規則 { $s\to t$ } があり、R で s が正規形 u に書き換えられるなら、規則を等式 { u = t } に変換

• 不要な等式の削除（remove useless equation）

E に等式 { s = s } があれば、削除する。

具体例

具体例として群の公理を完備化する。群の公理は以下の通り。

1. 0 + a = a

2. (-a) + a = 0

3. (a + b) + c = a + (b + c)

完備化アルゴリズムは以下のように行う。

4. ((-a) + a) + b … 2と3より生成

= 0 + b = b … 2、次に、１より

= (-a) + (a + b) … 3より

(-a) + (a + b) の方が式として大きいので、(-a) + (a + b) = b を追加。

5. (-0) + (0 + a) … 1と4より生成

= (-0) + a … 1より

= a … 4より

(-0) + a の方が式として大きいので、(-0) + a = a を追加。

6. (-(-a)) + ((-a) + a) … 2と4より生成

= (-(-a)) + 0 … 2より

= a … 4より

(-(-a)) + 0 の方が式として大きいので、(-(-a)) + 0 = a を追加。

このような作業を数十回繰り返し、冗長な物を取り除くと、最終的にこの式が残る。

0 + a = a

(-a) + a = 0

(a + b) + c = a + (b + c)

(-a) + (a + b) = b

a + 0 = a

a + (-a) = 0

a + ((-a) + b) = b

-0 = 0

-(-a) = a

-(b + a) = (-a) + (-b)

拡張

完備化アルゴリズムでは、適当な項順序による向き付けを決めないと書き換え規則が作れない。そのため $\{f(x,y)=f(y,x)\}$ のように左右の項の向き付けができない等式が現れると完備化が失敗する。失敗無し完備化（テンプレート:Lang、あるいはテンプレート:Lang）は、このような等式を両方向に使える可能性のある書き換え規則と見なし、適当な代入で停止性が保証される向き付けが得られた場合のみ、この等式を向き付けられた書き換え規則として簡約を行うやり方である。例えば、 $x=2,y=1$ の場合、$(f(2,1)>f(1,2))$ のように引数の辞書式順序を用い、等式 $\{f(2,1)=f(1,2)\}$ を $f(2,1)\to f(1,2)$ のように向き付けを行い簡約を行う。

他分野との関連

合流性を保証するための危険対や停止性を保証する項順序の考え方は、一般の簡約系でも有効であり、他分野でも同様の手続きが知られている。

グレブナー基底

グレブナー基底は、多変数多項式の簡約化を一意に行える多項式の集合であり、グレブナー基底を求めるブッフベルガーアルゴリズムは数式処理の分野での連立代数方程式の解法や、可換環論、代数幾何、微分方程式論、整数計画問題などに出てくる様々な数学的対象物を構成するための基礎となっている。

クヌース・ベンディックス完備化アルゴリズムでの危険対はブッフベルガーアルゴリズムでのS-多項式、項順序は単項式順序に対応する。

参考文献

• D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. in Computational Problems in Abstract Algebra (Proc. Conf., Oxford, 1967). J. Leech (ed.), Pergamon Press. pp.263–297. 1970.
• J. W. Klop. Term rewriting systems. in Handbook of logic in computer science (vol.2): background: computational structures, Oxford University Press. 1992
• 坂井 公. Knuth-Bendixの完備化手続きとその応用. コンピュータソフトウェア, 4(1), pp.2-22. 1987.
• 外山 芳人. 項書き換えシステム入門.(pdf) 信学技報, SS98-15, pp.31-38, 1998.
• 外山 芳人. 完備化による等式証明.(pdf) 人工知能学会誌, Vol.16, No.5, pp.668-674, 2001.

関連項目

• 項書き換え
• ラムダ計算
• 合流性
• グレブナー基底

外部リンク

• テンプレート:MathWorld
• 項書き換えシステム入門. 東北大学 電気通信研究所
• 書き換えと計算機.(pdf) Jacques Garrigue, 名古屋大学

テンプレート:Normdaten