Lispでも論理プログラミングがしたい！
core.logicはClojureの準標準ライブラリ群であるClojure Contribに含まれる、論理プログラミングのためのライブラリです。
この記事では、core.logicを使ったClojureにおける論理プログラミングを紹介します。
core.logic
このライブラリはClojureで制約論理プログラミングとProlog-likeな関係プログラミングを可能にします。
Lispの論理プログラミングライブラリといっても、処理系毎に様々なライブラリが存在します。
core.logicはSchemeの論理プログラミングライブラリであるminiKanren、そしてその拡張であるcKanrenに基づき実装されています。
append
Prologの述語append/3は結合、差分、組み合わせと複数の意味を持ち、論理プログラミングの例としてよく取り上げられます。
core.logicによるappendの例をみてみましょう。
(defne append [x y z]
([() y y])
([[h . t] _ [h . t']] (append t y t')))
Prologのコードとよく似ていることがわかりますね？
append([], L, L).
append([H|T1], L, [H|T2]) :- append(T1, L, T2).
REPLで実行してみましょう。
user> (run* [q]
(append [1 2] [3 4] q))
((1 2 3 4))
user> (run* [q]
(append [1 2] q [1 2 3 4]))
((3 4))
user> (run* [q]
(fresh [a b]
(== q [a b])
(append a b [1 2 3 4])))
([() [1 2 3 4]]
[(1) (2 3 4)]
[(1 2) (3 4)]
[(1 2 3) (4)]
[(1 2 3 4) ()])
このように、Prologとは少し違った質問の仕方をします。
これらのコードについて詳しくみていきましょう。
core.logicの基本
core.logicを使って論理プログラミングを行う上で、幾つかの重要な制御構造が存在します。
run
run*は1つの論理変数とその論理変数に対する制約を与え、制約を充す値の全てをリストで返します。
しかし、制約を充す値が多く存在する、または無限に存在する場合はプログラムが応答しなくなるでしょう。
そこで、runを使用することで探索を制限することができます。
user> (run 2 [q]
(fresh [a b]
(== q [a b])
(append a b [1 2 3 4])))
([() [1 2 3 4]] [(1) (2 3 4)])
fresh
Prologは論理変数に大文字を使用し、質問の結果に使用した論理変数とその値が表示されます。
core.logicではfresh用いて論理変数を明示的に宣言する必要があります。
(defne number [char int]
([\1 1]) ([\2 2]) ([\3 3])
([\4 4]) ([\5 5]) ([\6 6])
([\7 7]) ([\8 8]) ([\9 9])
([\0 0]))
user> (run* [q]
(fresh [c]
(number c q)))
(1 2 3 4 5 6 7 8 9 0)
user> (run* [q]
(fresh [i]
(number q i)))
(\1 \2 \3 \4 \5 \6 \7 \8 \9 \0)
Prologとは違い、ゴールの内側のみ有効な変数を定義することが可能です。
値が未確定な論理変数は、各結果ごとに _0, _1, _2 と表示されます。
project
projectは論理変数の値を取り出し、ゴールに適用します。
主にClojureの関数を適用するときに使用します。
(defna factorial [m n]
([0 1])
([1 1])
([_ _] (fresh [x y]
(project [m] (== x (dec m)))
(factorial x y)
(project [m y] (== n (* m y))))))
user> (run 1 [q] (factorial 5 q))
(120)
もし、論理変数に値が束縛されていない場合は、論理変数がそのまま渡されます。
user> (run 1 [q] (factorial q 5))
ClassCastException clojure.core.logic.LVar cannot be cast to java.lang.Number clojure.lang.Numbers.dec (Numbers.java:118)
探索の制御
core.logicにはPrologのcutに相当するものは存在しません。
そのかわり、3つの制御構造が存在します。
conde
condeは複数の節をとります。
節の各ゴールが全て真になるように値を推論します。
user> (run* [q]
(conde [(== q :foo)]
[(== q :bar)]))
(:foo :bar)
conda
condaはSoft cutと呼ばれるもので、上部の節が成功した後、その後の節は無視されます。
user> (run* [q]
(conda [(conde [(== q :foo)]
[(== q :bar)])]
[(== q :baz)]))
(:foo :bar)
condu
conduはCommitted choiceと呼ばれ、節の最初の成功を結果とします。
user> (run* [q]
(condu [(conde [(== q :foo)]
[(== q :bar)])]
[(== q :baz)]))
(:foo)
これらconde, conda, conduによってパターンマッチや述語定義の制御構造が定義されます。
| 制御構造 | 論理和 | Soft cut | Committed Choice |
|---|---|---|---|
| 条件分岐 | conde | conda | condu |
| パターンマッチ | matche | matcha | matchu |
| 述語定義 | defne | defna | defnu |
これらの制御構造が扱えれば、大抵の述語を定義することが可能でしょう。
データベース
clojure.core.logic.pldbを使うことで関係データベースを扱えます。
db-relにより関係を定義し、dbによってデータベースを構築します。
(db-rel language p)
(db-rel jvm p)
(db-rel logic p)
(db-rel library p p')
(def facts
(db [language 'Java]
[language 'Prolog]
[language 'Clojure]
[language 'Scheme]
[jvm 'Java]
[jvm 'Clojure]
[logic 'Prolog]
[logic 'core.logic]
[logic 'miniKanren]
[library 'Clojure 'core.logic]
[library 'Scheme 'miniKanren]))
定義した関係は他の述語と同じ様に使えます。
user> (with-db facts
(run* [q]
(fresh [a b]
(language a)
(jvm a)
(logic b)
(library a b)
(== q [a b]))))
([Clojure core.logic])
速度
core.logicの実行速度はProlog処理系と比べると遅いです。
フィボナッチ数を求めるプログラムで速度を比較してみます。
core.logic
(defna fib [n r]
([0 1])
([1 1])
([_ _] (fresh [x x' y y']
(project [n] (== x (dec n)))
(project [n] (== x' (- n 2)))
(fib x y)
(fib x' y')
(project [y y'] (== r (+ y y'))))))
user> (time (run* [q] (fib 25 q)))
"Elapsed time: 6165.90255 msecs"
(121393)
SWI-Prolog
fib(0, 1).
fib(1, 1).
fib(M, N) :-
X1 is M - 1,
X2 is M - 2,
fib(X1, Y1),
fib(X2, Y2),
N is Y1 + Y2.
?- time(fib(25, N)).
% 364,176 inferences, 3.614 CPU in 3.626 seconds (100% CPU, 100780 Lips)
N = 121393 .
この速度はTablingによって改善できます。
Tabling
Tablingは述語をメモ化するための機能です。
先ほどのフィボナッチ数の例に適用します。
(defn fib' [n r]
((tabled [n r]
(matchu [n r]
([0 1])
([1 1])
([_ _] (fresh [x x' y y']
(project [n] (== x (dec n)))
(project [n] (== x' (- n 2)))
(fib' x y)
(fib' x' y')
(project [y y'] (== r (+ y y')))))))
n r))
user> (time (run 1 [q] (fib' 25 q)))
"Elapsed time: 59.461846 msecs"
(121393)
このように、Tablingが有効な計算では著しい速度の改善が認められます。
DCG
Prologには限定節文法(Definite Clause Grammar)と呼ばれる構文解析のための機能があり、core.logicにもclojure.core.logic.dcgとしてDCGが実験的に実装されています。
(def-->e tuple [q]
([[[:fst a] [:snd b]]] [a] [b]))
この構文は以下の述語と同等の意味を持ちます。
(defne tuple' [q x y]
([[[:fst a] [:snd b]] [a b . c] c]))
user> (run* [q]
(fresh [a b]
(== q [a b])
(tuple a '[foo bar baz] b)))
([[[:fst foo] [:snd bar]] (baz)])
user> (run* [q]
(fresh [a b]
(== q [a b])
(tuple' a '[foo bar baz] b)))
([[[:fst foo] [:snd bar]] (baz)])
この構文は述語定義のシンタックスシュガーであり、暗黙的に2つの引数を取っています。
さらに、この構文の中で呼び出される関数にも暗黙的に2の値が渡されるため、通常の関数を呼ぶためには!dcgを使う必要があります。
この構文を用いて、数式の解析、計算をする例を作ります。
(def-->e number [n]
([_] [n] (!dcg (project [n] (== (number? n) true)))))
(def-->e term [t]
([_] (fresh [x y]
(number x) '[*] (term y)
(!dcg (project [x y] (== t (* y x))))))
([_] (fresh [x y]
(number x) '[/] (term y)
(!dcg (project [x y] (== t (/ y x))))))
([_] (number t)))
(def-->e expr [e]
([_] (fresh [x y]
(term x) '[+] (expr y)
(!dcg (project [x y] (== e (+ y x))))))
([_] (fresh [x y]
(term x) '[-] (expr y)
(!dcg (project [x y] (== e (- y x))))))
([_] (term e)))
(defn eval' [e]
(run* [q]
(expr q (reverse e) [])))
同じ優先度の演算が並んだ場合の計算順序を正しくするため、入力を反転し、オペランドの位置も反転させています。
user> (eval' '[2 + 3 * 5 - 7])
(10)
user> (eval' '[2 - 4 + 8 * 16 / 32])
(2)
freshはこの構文の中で特別扱いされているため、通常の制御構造と変わりなく呼び出すことが可能です。
ClojureScript
ClojureScriptはClojureのコードをJavaScriptへ変換するコンパイラです。
core.logicにはClojureScript版のライブラリも存在し、論理プログラミングがJavaScript上で可能です。
まとめ
core.logicには基本的な論理プログラミングの機能だけでなく、TablingやDCGなどの実用的な機能も兼ね備えています。
ライブラリとして実装され、JVMやJavaScript上で動作するので、サーバーやデスクトップ、Web上で動作するプログラムに簡単に組込むことが可能です。
また、Clojureで論理プログラミングを簡素な構文で実現するために、多くの機能がマクロによって定義されています。
それ故に、エラーが追い辛く、Clojureの他のマクロと組合せ難いという欠点があります。