概要

Knuth-Bendixの完備化アルゴリズムを実装したツールを作ってみました。いくつかの簡単な問題に対して使ってみながら紹介します。

github.com

なお、Knuth-Bendixの完備化アルゴリズムの詳細自体については、こちらのページが分かりやすいです。

www.nue.ie.niigata-u.ac.jp

インストールの仕方

Linux/Windowsのそれぞれ用に、実行可能バイナリをビルドしました。こちらからダウンロードできます。

Releases · moratori/clover · GitHub

Common Lisp（と、roswell）の実行環境がある場合は、リポジトリをクローンしてコードを取得しても大丈夫です。

実行してみる（その１）

実行権限を確認して、ダブルクリックなりで起動します。コードを取得しroswell経由で実行する場合は以下の通り、起動スクリプトを叩いてください。

$ ./roswell/clover.ros

実行するとREPLに入るので、そこに完備化したい等式を入力していきます。例えば、群の公理を示す以下の3つの等式を入力します。

\begin{align} plus(ZERO, x)& = x\\ plus(plus(x,y),z)& = plus(x, plus(y,z))\\ plus(i(x),x)& = ZERO \end{align}

(NIL)>>> :def-axiom group
input . to finish definition
axiom[1]>>> plus(ZERO,x) = x
axiom[2]>>> plus(plus(x,y),z) = plus(x, plus(y,z))
axiom[3]>>> plus(i(x),x) = ZERO
axiom[4]>>> .
Detected that a set of equations has been inputted.
Do you want to execute completion algorithm?  (yes or no) yes

The completion process was successful:
i(plus(y,x))=>plus(i(x),i(y))
i(i(x))=>x
i(ZERO)=>ZERO
plus(x,ZERO)=>x
plus(x,i(x))=>ZERO
plus(x,plus(i(x),y))=>y
plus(i(x),plus(x,y))=>y
plus(ZERO,x)=>x
plus(plus(x,y),z)=>plus(x,plus(y,z))
plus(i(x),x)=>ZERO
(group)>>>

完備化が成功し、10個の項書き換え規則が出力されたことが分かります。この状態で証明したい等式、例えば $plus(plus(x,y),plus(z,w)) = plus(x, plus(y, plus(z, w)))$ を入力してみます。

すると、想定通り証明することができます。

(group)>>> plus(plus(x,y),plus(z,w)) = plus(x, plus(y, plus(z, w)))
The equation can be PROVED under the axiom group

irreducible form under the group:
plus(x,plus(y,plus(z,w))) = plus(x,plus(y,plus(z,w)))

(group)>>>

先ほどの項書き換え規則の下で両辺の既約形が同じになった為、等式が成り立つことが分かります。

実行してみる（その２）

続いて別の問題として、以下リンクに記載のある「グラス置き換えパズル」を解いてみようと思います。

http://www.nue.ie.niigata-u.ac.jp/toyama/lab-intro/TRS-intro/index.html#glass

グラスの列の置き換えを、以下の等式で表してみます。列は $cons$ を用いたリストで表すこととしてます。

\begin{align} cons(S, cons(W, x))& = cons(W, x)\\ cons(x, cons(S, cons(W, y)))& = cons(x, cons(W, y))\\ cons(W, cons(B, x))& = cons(S, x)\\ cons(x, cons(W, cons(B, y)))& = cons(x, cons(S, y)) \end{align}

上2つは、列 $SW$ が列 $W$ と等しいことを示しています。

1つは、列の先頭に $SW$ が存在した場合、１つは、列の途中又は最後に存在した場合を示しています。下2つも同様です。

この等式を完備化してみますと、3つの書き換え規則に変換されます。

(NIL)>>> :def-axiom glass
input . to finish definition
axiom[1]>>> cons(S, cons(W, x)) = cons(W, x)
axiom[2]>>> cons(x, cons(S, cons(W, y))) = cons(x, cons(W, y))
axiom[3]>>> cons(W, cons(B, x)) = cons(S, x)
axiom[4]>>> cons(x, cons(W, cons(B, y))) = cons(x, cons(S, y))
axiom[5]>>> .
Detected that a set of equations has been inputted.
Do you want to execute completion algorithm?  (yes or no) yes

The completion process was successful:
cons(S,cons(S,x))=>cons(S,x)
cons(S,cons(W,x))=>cons(W,x)
cons(W,cons(B,x))=>cons(S,x)
(glass)>>>

この状態で、次の2つの等式 $[S,S,W,B] = [W,B,W,B]$ と $[S,S,S,W] \neq [W,B,W,B]$ を証明してみます。

(glass)>>> [S,S,W,B] = [W,B,W,B]
The equation can be PROVED under the axiom glass

irreducible form under the glass:
cons(S,NIL) = cons(S,NIL)

(glass)>>> [S,S,S,W] != [W,B,W,B]
The equation can be PROVED under the axiom glass

irreducible form under the glass:
cons(W,NIL) ≠ cons(S,NIL)

想定通り証明することができました。