クヌース・ベンディックス完備化アルゴリズムの OCaml 実装
- OCaml 本体
- Dune（ビルド）
標準的な方法として Dune を使うことを推奨する。
dune build コマンドでライブラリをビルドできる。
dune buildOPAM にローカルソースのライブラリをとしてインストールする場合は opam install . を実行する。 アンインストールは opam remove コマンドで行う。
opam install .OPAM を介さずにインストールする場合はビルドの後に dune install を実行する。 この場合のアンインストールは dune uninstall コマンドを使う。
dune build dune installまた、対話環境の utop が使える場合は dune utop コマンドによってライブラリをトップレベルで即座に試せる。 対話環境の設定ファイル .ocamlinit により、項書き換え系と完備化モジュールを open するように定義されている。
dune utoputop で OPAM にインストールされたパッケージを読み込むには -require オプションを使う。
utop -require knuth_bendix例外的な方法として純正の OCaml コンパイラのみでビルドすることも可能である（ただし Dune による出力とは厳密には異なる）。 build_ocamlc.sh の手順に従うと ocamlc によるバイトコードライブラリをビルドできる。 build_ocamlopt.sh の手順に従うと ocamlopt によるネイティブコードライブラリをビルドできる。
標準のトップレベルでライブラリを使用する場合はバイトコードコンパイラで作られた knuth_bendix.cma と knuth_bendix.cmi を用意して #load ディレクティブで読み込む。
#load "knuth_bendix.cma";;項書き換え系モジュールと完備化モジュールの 2 つを使用する。
Knuth_bendix.Trs モジュールとして定義されている。
以下は当該モジュールを open した状態での説明であり、関数の属すモジュールは省略してある。
項は term 型によって表され木構造を成す。ノードは変数か関数のどちらかであり、関数のみが子ノードを持つことができる。
parseterm 関数を使って文字列から項を作れる。 小文字からはじまるシンボルは変数、大文字・数字・記号から始まるシンボルは関数と解釈される。
使用できる記号は +*!?-/^$%& である。
# parseterm "F(x, G(y, 0), +(H(z), 1))";; - : TermRewritingSystem.term = Function ("F", [Variable ("x", 0); Function ("G", [Variable ("y", 0); Function ("0", [])]); Function ("+", [Function ("H", [Variable ("z", 0)]); Function ("1", [])])])strterm 関数で項の文字列表現を得られる。 返される文字列は必ずしも再パース可能ではないことに注意されたし（parseterm によって作られた項なら問題ない）。
# strterm (Function ("F", [Variable ("x", 0); Variable ("y", 0)]));; - : string = "F(x, y)"printterm 関数は項の文字列表現を標準出力へ吐き出す。
# printterm (Function ("F", [Variable ("x", 0); Variable ("y", 0)]));; F(x, y) - : unit = ()var s : string -> termシンボル s の変数の項を返すconst s : string -> termシンボル s の無引数関数の項を返すfunc s ss : string -> string list -> term仮引数の変数のシンボルのリストが ss である、シンボル s の関数の項を返すcall s ts : string -> term list -> term引数の項のリストが ts である、シンボル s の関数の項を返すnest s n t : string -> int -> term -> term項 t にシンボルが s である 1 引数関数を n 回適用した項を返す
# let f4 = call "F" [nest "S" 4 (const "0")];; val f4 : TermRewritingSystem.term = Function ("F", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("0", [])])])])])]) # printterm f4;; F(S(S(S(S(0))))) - : unit = ()書き換え規則は項の組で表す。
parserule 関数によって文字列から規則を得る。 文字列は 項 -> 項 の形とする。
# parserule "F(x, y) -> G(y, x)";; - : TermRewritingSystem.rule = (Function ("F", [Variable ("x", 0); Variable ("y", 0)]), Function ("G", [Variable ("y", 0); Variable ("x", 0)]))strrule 関数で書き換え規則の文字列表現を得る。 printrule 関数は書き換え規則を標準出力する。
書き換え規則の集合は書き換え規則のリストで表す。 parserules 関数は規則の文字列のリストから規則の集合を返す。
# let rs = parserules ["A(0, y) -> y"; "A(S(x), y) -> S(A(x, y))"];; val rs : TermRewritingSystem.ruleset = [(Function ("A", [Function ("0", []); Variable ("y", 0)]), Variable ("y", 0)); (Function ("A", [Function ("S", [Variable ("x", 0)]); Variable ("y", 0)]), Function ("S", [Function ("A", [Variable ("x", 0); Variable ("y", 0)])]))]strrules 関数は書き換え規則の集合の文字列表現を得る。 printrules 関数は書き換え規則の集合を標準出力する。
# strrules rs;; - : string = "{ A(0, y) -> y\n A(S(x), y) -> S(A(x, y)) }" # printrules rs;; { A(0, y) -> y A(S(x), y) -> S(A(x, y)) } - : unit = ()linorm, lonorm 及び ponorm は書き換え規則の集合と項を与えると正規形を求める関数である。 それぞれ最左最内戦略、最左最外戦略、並列最外戦略に対応する。
以下は最左最内戦略で 7 番目のフィボナッチ数を評価した例である。
# let rs = parserules ["Add(0,y)->y"; "Add(S(x),y)->S(Add(x, y))"; "Fib(0)->0"; "Fib(S(0))->S(0)"; "Fib(S(S(x)))->Add(Fib(x),Fib(S(x)))"];; val rs : TermRewritingSystem.ruleset = [(Function ("Add", [Function ("0", []); Variable ("y", 0)]), Variable ("y", 0)); (Function ("Add", [Function ("S", [Variable ("x", 0)]); Variable ("y", 0)]), Function ("S", [Function ("Add", [Variable ("x", 0); Variable ("y", 0)])])); (Function ("Fib", [Function ("0", [])]), Function ("0", [])); (Function ("Fib", [Function ("S", [Function ("0", [])])]), Function ("S", [Function ("0", [])])); (Function ("Fib", [Function ("S", [Function ("S", [Variable ("x", 0)])])]), Function ("Add", [Function ("Fib", [Variable ("x", 0)]); Function ("Fib", [Function ("S", [Variable ("x", 0)])])]))] # printrules rs;; { Add(0, y) -> y Add(S(x), y) -> S(Add(x, y)) Fib(0) -> 0 Fib(S(0)) -> S(0) Fib(S(S(x))) -> Add(Fib(x), Fib(S(x))) } - : unit = () # let t = call "Fib" [nest "S" 7 (const "0")];; val t : TermRewritingSystem.term = Function ("Fib", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("0", [])])])])])])])])]) # let nf = linorm rs t;; val nf : TermRewritingSystem.term = Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("S", [Function ("0", [])])])])])])])])])])])])])]) # printterm nf;; S(S(S(S(S(S(S(S(S(S(S(S(S(0))))))))))))) - : unit = ()等式は規則と同じく項の組で表す。
parseeq 関数によって文字列から等式を得る。 文字列は 項 = 項 の形とする。
# parseeq "F(G(x)) = G(F(x))";; - : TermRewritingSystem.equation = (Function ("F", [Function ("G", [Variable ("x", 0)])]), Function ("G", [Function ("F", [Variable ("x", 0)])]))streq 関数で等式の文字列表現を得る。 printeq 関数は等式を標準出力する。
等式の集合は等式のリストで表す。 parseeqs 関数は等式の文字列のリストから等式の集合を返す。
# let eqs = parseeqs ["A = B"; "B = C"];; val eqs : TermRewritingSystem.equationset = [(Function ("A", []), Function ("B", [])); (Function ("B", []), Function ("C", []))]streqs 関数は等式の集合の文字列表現を得る。 printeqs 関数は等式の集合を標準出力する。
# streqs eqs;; - : string = "{ A = B\n B = C }" # printeqs eqs;; { A = B B = C } - : unit = ()Knuth_bendix.Kbc モジュールとして定義されている。
以下は当該モジュールを open した状態での説明であり、関数の属すモジュールは省略してある。
完備化のために停止性を保証する簡約化順序を与える必要がある。
関数のシンボルと整数値の組のリスト（優先順位を表すリスト）によってシンボル上の大小関係を定義する。
# let prece = [("F", 2);("G", 3);("H", 1)];; val prece : (string * int) list = [("F", 2); ("G", 3); ("H", 1)]kbc と kbcf が完備化を行う関数である。 kbc は優先順位を表すリストと等式集合を引数にとり、辞書式経路順序によって完備化を行う。 kbcf は簡約化順序を示す順序関数と等式集合を引数にとって完備化を行う。
kbcv と kbcfv はそれぞれの関数の途中経過を標準出力するバージョンである（重複等式の削除など一部の冗長な処理も追加で行われる）。
完備化に失敗すると例外が投げられる。 アルゴリズムが停止しない可能性もある。
以下はグラス置き換えパズル（酒・ウィスキー・ビール）の問題を完備化した例である。
2 つのグラス列が与えられ、等式に従ったグラス交換でもう一方と同じ列を作れるかどうかという問題である。
# let precedence = [("B", 3);("S", 2);("W", 1)];; val precedence : (string * int) list = [("B", 3); ("S", 2); ("W", 1)] # let eqs = parseeqs ["W(x)=S(W(x))"; "W(S(x))=B(x)"; "B(x)=B(B(x))"];; val eqs : TermRewritingSystem.equationset = [(Function ("W", [Variable ("x", 0)]), Function ("S", [Function ("W", [Variable ("x", 0)])])); (Function ("W", [Function ("S", [Variable ("x", 0)])]), Function ("B", [Variable ("x", 0)])); (Function ("B", [Variable ("x", 0)]), Function ("B", [Function ("B", [Variable ("x", 0)])]))] # let rs = kbc precedence eqs;; val rs : TermRewritingSystem.ruleset = [(Function ("W", [Function ("W", [Function ("W", [Variable ("x", 0)])])]), Function ("W", [Function ("W", [Variable ("x", 0)])])); (Function ("W", [Function ("W", [Function ("S", [Variable ("x", 0)])])]), Function ("W", [Function ("S", [Variable ("x", 0)])])); (Function ("B", [Variable ("x", 0)]), Function ("W", [Function ("S", [Variable ("x", 0)])])); (Function ("S", [Function ("W", [Variable ("x", 0)])]), Function ("W", [Variable ("x", 0)]))] # printrules rs;; { W(W(W(x))) -> W(W(x)) W(W(S(x))) -> W(S(x)) B(x) -> W(S(x)) S(W(x)) -> W(x) } - : unit = ()得られた書き換え規則を使って、例えば SBW と SSB の列を評価すると異なる正規形が求まる。 正規形が異なるのでグラス交換で SBW と SSB を行き来することができないと証明される。
# let t1 = parseterm "S(B(W(END)))";; val t1 : TermRewritingSystem.term = Function ("S", [Function ("B", [Function ("W", [Function ("END", [])])])]) # let t2 = parseterm "S(S(B(END)))";; val t2 : TermRewritingSystem.term = Function ("S", [Function ("S", [Function ("B", [Function ("END", [])])])]) # linorm rs t1;; - : TermRewritingSystem.term = Function ("W", [Function ("W", [Function ("END", [])])]) # linorm rs t2;; - : TermRewritingSystem.term = Function ("W", [Function ("S", [Function ("END", [])])])群の公理を完備化した例を示す。 kbcv 関数を使って途中経過もすべて出力している。
# let precedence = [("I", 3); ("G", 2); ("E", 1)];; val precedence : (string * int) list = [("I", 3); ("G", 2); ("E", 1)] # let eqs = parseeqs ["G(E,x)=x"; "G(I(x),x)=E"; "G(G(x,y),z)=G(x,G(y,z))"];; val eqs : TermRewritingSystem.equationset = [(Function ("G", [Function ("E", []); Variable ("x", 0)]), Variable ("x", 0)); (Function ("G", [Function ("I", [Variable ("x", 0)]); Variable ("x", 0)]), Function ("E", [])); (Function ("G", [Function ("G", [Variable ("x", 0); Variable ("y", 0)]); Variable ("z", 0)]), Function ("G", [Variable ("x", 0); Function ("G", [Variable ("y", 0); Variable ("z", 0)])]))] # kbcv precedence eqs;; ================ Input ================== { G(E, x) = x G(I(x), x) = E G(G(x, y), z) = G(x, G(y, z)) } ================ Step 1 ================= { G(I(x), x) = E G(G(x, y), z) = G(x, G(y, z)) } { G(E, x) -> x } ================ Step 2 ================= { G(G(x, y), z) = G(x, G(y, z)) } { G(I(x), x) -> E G(E, x) -> x } ================ Step 3 ================= { z = G(I(x_1), G(x_1, z)) } { G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 4 ================= { G(I(I(x)), z_1) = G(x, z_1) G(I(G(x, y)), G(x, G(y, z_1))) = z_1 G(I(I(x)), E) = x G(I(E), x) = x } { G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 5 ================= { G(I(I(x)), z_1) = G(x, z_1) G(I(G(x, y)), G(x, G(y, z_1))) = z_1 G(I(I(x)), E) = x G(I(I(E)), x) = x } { G(I(E), x) -> x G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 6 ================= { G(I(G(x, y)), G(x, G(y, z_1))) = z_1 G(x, E) = x z = G(x, G(I(x), z)) E = G(x, I(x)) } { G(I(I(x)), z_1) -> G(x, z_1) G(I(E), x) -> x G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 7 ================= { G(I(G(x, y)), G(x, G(y, z_1))) = z_1 z = G(x, G(I(x), z)) E = G(x, I(x)) x_1 = I(I(x_1)) E = I(E) } { G(x, E) -> x G(I(I(x)), z_1) -> G(x, z_1) G(I(E), x) -> x G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 8 ================= { G(I(G(x, y)), G(x, G(y, z_1))) = z_1 z = G(x, G(I(x), z)) E = G(x, I(x)) x_1 = I(I(x_1)) } { I(E) -> E G(x, E) -> x G(I(I(x)), z_1) -> G(x, z_1) G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 9 ================= { G(I(G(x, y)), G(x, G(y, z_1))) = z_1 z = G(x, G(I(x), z)) E = G(x, I(x)) } { I(I(x_1)) -> x_1 I(E) -> E G(x, E) -> x G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 10 ================= { G(I(G(x, y)), G(x, G(y, z_1))) = z_1 z = G(x, G(I(x), z)) G(x_1, G(y, I(G(x_1, y)))) = E } { G(x, I(x)) -> E I(I(x_1)) -> x_1 I(E) -> E G(x, E) -> x G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 11 ================= { G(I(G(x, y)), G(x, G(y, z_1))) = z_1 G(x_1, G(y, I(G(x_1, y)))) = E G(x_1, G(y, G(I(G(x_1, y)), z))) = z } { G(x, G(I(x), z)) -> z G(x, I(x)) -> E I(I(x_1)) -> x_1 I(E) -> E G(x, E) -> x G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 12 ================= { G(I(G(x, y)), G(x, G(y, z_1))) = z_1 G(x_1, G(y, G(I(G(x_1, y)), z))) = z x = G(y, I(G(I(x), y))) I(x_1) = G(y, I(G(x_1, y))) G(x, G(y_1, G(y, I(G(x, G(y_1, y)))))) = E } { G(x_1, G(y, I(G(x_1, y)))) -> E G(x, G(I(x), z)) -> z G(x, I(x)) -> E I(I(x_1)) -> x_1 I(E) -> E G(x, E) -> x G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 13 ================= { G(I(G(x, y)), G(x, G(y, z_1))) = z_1 G(x_1, G(y, G(I(G(x_1, y)), z))) = z G(x, G(y_1, G(y, I(G(x, G(y_1, y)))))) = E G(I(G(x, y_1)), x) = I(y_1) G(y, G(I(G(x_1, y)), x_1)) = E G(x, I(x_1)) = I(G(x_1, I(x))) G(I(y), I(x_1)) = I(G(x_1, y)) G(x, G(y_1, I(G(x_1, G(x, y_1))))) = I(x_1) G(z, I(G(x, G(y_1, z)))) = I(G(x, y_1)) G(I(x_1), z) = G(y, G(I(G(x_1, y)), z)) } { G(y, I(G(x_1, y))) -> I(x_1) G(x, G(I(x), z)) -> z G(x, I(x)) -> E I(I(x_1)) -> x_1 I(E) -> E G(x, E) -> x G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ================ Step 14 ================= { G(I(G(x, y)), G(x, G(y, z_1))) = z_1 G(x_1, G(y, G(I(G(x_1, y)), z))) = z G(x, G(y_1, G(y, I(G(x, G(y_1, y)))))) = E G(I(G(x, y_1)), x) = I(y_1) G(y, G(I(G(x_1, y)), x_1)) = E G(I(y), I(x_1)) = I(G(x_1, y)) G(x, G(y_1, I(G(x_1, G(x, y_1))))) = I(x_1) G(z, I(G(x, G(y_1, z)))) = I(G(x, y_1)) G(I(x_1), z) = G(y, G(I(G(x_1, y)), z)) I(G(x_1, G(x_1, I(x_2)))) = G(x_2, G(I(x_1), I(x_1))) I(G(x_2, G(y, I(x)))) = G(x, I(G(x_2, y))) } { I(G(x_1, I(x))) -> G(x, I(x_1)) G(y, I(G(x_1, y))) -> I(x_1) G(x, G(I(x), z)) -> z G(x, I(x)) -> E I(I(x_1)) -> x_1 I(E) -> E G(x, E) -> x G(I(x_1), G(x_1, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } ============== Complete 15 =============== { I(G(x, y)) -> G(I(y), I(x)) G(x, G(I(x), z)) -> z G(x, I(x)) -> E I(I(x)) -> x I(E) -> E G(x, E) -> x G(I(x), G(x, z)) -> z G(G(x, y), z) -> G(x, G(y, z)) G(I(x), x) -> E G(E, x) -> x } - : TermRewritingSystem.ruleset = [(Function ("I", [Function ("G", [Variable ("x", 0); Variable ("y", 0)])]), Function ("G", [Function ("I", [Variable ("y", 0)]); Function ("I", [Variable ("x", 0)])])); (Function ("G", [Variable ("x", 0); Function ("G", [Function ("I", [Variable ("x", 0)]); Variable ("z", 0)])]), Variable ("z", 0)); (Function ("G", [Variable ("x", 0); Function ("I", [Variable ("x", 0)])]), Function ("E", [])); (Function ("I", [Function ("I", [Variable ("x", 0)])]), Variable ("x", 0)); (Function ("I", [Function ("E", [])]), Function ("E", [])); (Function ("G", [Variable ("x", 0); Function ("E", [])]), Variable ("x", 0)); (Function ("G", [Function ("I", [Variable ("x", 0)]); Function ("G", [Variable ("x", 0); Variable ("z", 0)])]), Variable ("z", 0)); (Function ("G", [Function ("G", [Variable ("x", 0); Variable ("y", 0)]); Variable ("z", 0)]), Function ("G", [Variable ("x", 0); Function ("G", [Variable ("y", 0); Variable ("z", 0)])])); (Function ("G", [Function ("I", [Variable ("x", 0)]); Variable ("x", 0)]), Function ("E", [])); (Function ("G", [Function ("E", []); Variable ("x", 0)]), Variable ("x", 0))]