core logicで論理プログラミングとかやってみた。

(このエントリは Clojure Contrib Library Advent Calendar 22日目の記事です。)

core logicについて

論理プログラミング言語とは?

• つまり Prolog です。!

論理プログラミングは3つの要素でできています。

• 1階述語論理の公理の集合
• 質問(query)
• 定理証明器(theorem proper)

ここで、定理証明器とは、質問について証明や反証明するため、公理を元に 演繹 を行なうシステムのことです。演繹を行うことを論理プログラミングでは実行することになります。

環境構築

Leiningenでプロジェクトを作成し、project.cljに

(defproject prolog-clojure "1.0.0-SNAPSHOT"
  :description "prolog clojure"
  :dependencies [[org.clojure/clojure "1.3.0"]
                 [org.clojure/core.logic "0.8.5"]])

と記述。そして

lein deps

で完了。最版は0.8.5。

Core logic の基本的な文法について

基本的な形はこのようになります。

(run* [logic-variable]
   &logic-expressions)

これは、logic-expressionsに述語論理式を書きます。実行するときに、証明器が論理式を満足する、値を論理変数に与えます。

論理式について

論理式は、論理変数と、値の制約によって成りたっています。

論理変数

論理変数とは、曖昧な値を持つ変数のことです。つまり、いくつかの値を持てる変数のことです。

制約

制約とは、値や論理変数に制限を与えるものです。例を上げると。

 (run* [q]
   (membero q [1 2 3])
   (membero q [2 3 4]))

日本語に翻訳するとすれば、

(membero q [1 2 3]) ->「qは[1 2 3]の一員である。」
(membero q [2 3 4]) ->「qは[2 3 4]の一員である。」

ここから得られる、qの可能性はなんでしょうか? それは、qという論理変数は2か3のメンバーであるということです。そして証明器は、(2 3)を返します。

もう一つ例を上げでみましょう。

(run* [x]
    (membero 7 [1 3 5 x]))

これは、「7は、[1 3 5 x]のメンバーの一員である」なので、xは7です。

flesh

fleshとは,letのようなものです。つまり、fleshでレキシカルな論理変数を作ることができます。

 (fresh [a b c] &logic-expressions)

これで、&logic-expressions以下に論理変数a b cが導入されました。
ちなみに freshとは、oxfordでは"not previously known or used; new or different:"と書いてました。なるほど。

単一化(ユニフィケーション , unify, ==)について

単一化は、一言で言えば、2つの論理変数(の集合)の内容を同一化するものです。core.logicでは、==で行ないます。

一番単純な例はコレです。

(run* [x]
    (== x "x"))

これでは、ただの束縛と変りません。
では次の例を上げてみましょうか。

(run* [x]
    (fresh [t]
        (== [x 1] [t t])))

さて、[x 1]と[t t]を全く同一しましょう。これは、x と t、 t と 1が一緒になるので、結局、xに1になります。 単一化は対称的であるので 例は次の様に逆に書いても同じです。

(run* [x]
    (== "x" x))

(run* [x]
    (fresh [t]
        (== [t t] [x 1])))

また、単一化できない例も存在します。そのときは、失敗になります。

(run* [x]
   (== [x 10] [x 11]))

これは、(== [x 10] [x 11])でunifyが失敗します。

差分リスト

さてcore.logicで独自のデータ構造を表現してみましょう。今回は差分リストというものをやります。差分リストとは、2つのリストの差でリストを表現するというものです。

たとえば

• [(1 2 3 4) (3 4)] -> (1 2)を表す
• [(1 2) (1 2)] -> 空を表す
• [(1 2 3 4 . x) x] -> (1 2 3 4)を表わす。
• [(1 2 3 4) (4 x)] -> (1 2 3)を表わす。

となります。実際には差分リストは

• [(&values . x) x]

という形を使う場合が多いです。

さて、この様に表現したとして、差分リストの連結を表現しましょう。

(defne append-d [a b c]
  ([[?x  ?y] [?y  ?z] [?x  ?z]]))

さて、連結しましょう。

(run* [z]
    (fresh [x y a b]
        (== a (lcons 1 (lcons 2 (lcons 3 x))))
        (== b (lcons 4 (lcons 5 (lcons 6 y))))
        (append-d [a x] [b y] z))))
;; -> ([(1 2 3 4 5 6 . _0) _0])

なんで、こんなへんてこな、差分リストを使うのかといえば、差分リストの2のリストが束縛されてない変数であれば、一定時間で連結できるらしいです。

NQueensの問題

さて、 Prologといえば、なんかパズルを解かせることがおおいですね。ここでは、NQueensの問題を解いてみましょう。

safe-queensがゲームのルールに合うようにqueenを探してきてくれます。

(defne safe-queens [q others]
  ([_ ()])
  ([[x1 y1] [[x2 y2] . t]]
     (!= x1 x2)
     (!= y1 y2)
     (project [x1 x2 y1 y2]
       (!= (- x2 x1) (- y2 y1))
       (!= (- x1 y2) (- x2 y1)))
     (safe-queens [x1 y1] t)))
 
(defne nqueen-solves [l n]
  ([() _])
  ([[[x y] . t] _]
     (nqueen-solves t n)
     (membero x (range n))
     (safe-queens [x y] t)))
 
(defn queens [n]
  (run* [q]
    (== q (map vector (repeatedly lvar) (range n)))
    (nqueen-solves q n)))

(defn -main []
  (prn (queens 4)))

ちなみに結果はこんな感じになりました。

(([3 0] [1 1] [6 2] [2 3] [5 4] [7 5] [4 6] [0 7]) 
 ([4 0] [1 1] [3 2] [6 3] [2 4] [7 5] [5 6] [0 7])
 ([2 0] [4 1] [1 2] [7 3] [5 4] [3 5] [6 6] [0 7]) 
 ([2 0] [5 1] [3 2] [1 3] [7 4] [4 5] [6 6] [0 7])
 ([4 0] [6 1] [0 2] [2 3] [7 4] [5 5] [3 6] [1 7]) 
 ([5 0] [3 1] [1 2] [7 3] [4 4] [6 5] [0 6] [2 7])
 ([3 0] [5 1] [7 2] [2 3] [0 4] [6 5] [4 6] [1 7]) 
 ([4 0] [2 1] [7 2] [3 3] [6 4] [0 5] [5 6] [1 7])
 ([2 0] [5 1] [7 2] [0 3] [3 4] [6 5] [4 6] [1 7]) 
 ([4 0] [6 1] [3 2] [0 3] [2 4] [7 5] [5 6] [1 7])
 ([3 0] [0 1] [4 2] [7 3] [5 4] [2 5] [6 6] [1 7]) 
 ([2 0] [5 1] [3 2] [0 3] [7 4] [4 5] [6 6] [1 7])
 ([3 0] [6 1] [4 2] [2 3] [0 4] [5 5] [7 6] [1 7]) 
 ([5 0] [2 1] [6 2] [1 3] [7 4] [4 5] [0 6] [3 7])
 ([1 0] [6 1] [2 2] [5 3] [7 4] [4 5] [0 6] [3 7])
 ([5 0] [3 1] [6 2] [0 3] [7 4] [1 5] [4 6] [2 7])
 ([0 0] [6 1] [3 2] [5 3] [7 4] [1 5] [4 6] [2 7])
 ([5 0] [7 1] [1 2] [3 3] [0 4] [6 5] [4 6] [2 7])
 ([5 0] [1 1] [6 2] [0 3] [3 4] [7 5] [4 6] [2 7])
 ([3 0] [6 1] [0 2] [7 3] [4 4] [1 5] [5 6] [2 7])
 ([4 0] [7 1] [3 2] [0 3] [6 4] [1 5] [5 6] [2 7])
 ([3 0] [7 1] [0 2] [4 3] [6 4] [1 5] [5 6] [2 7])
 ([1 0] [6 1] [4 2] [7 3] [0 4] [3 5] [5 6] [2 7])
 ([0 0] [6 1] [4 2] [7 3] [1 4] [3 5] [5 6] [2 7])
 ([1 0] [4 1] [6 2] [3 3] [0 4] [7 5] [5 6] [2 7])
 ([3 0] [1 1] [6 2] [4 3] [0 4] [7 5] [5 6] [2 7])

...
...
...
総数で解が92個あるはず!
..
...

答えは多分あっているはず!

最後に

core.logicはClojureの言語の上ので気軽にできる論理プログラミング言語だと思います。
すごく楽しいライブラリだと思います。

まだまだ、加筆修正するかもしれません。

参考文献的ななにか。

core logicのgithubのソース

core logic の githubのwiki

あとこれ"A Core Logic Primer"

t2ruさんのブログ

twitterで@halcat0x15aさんが、教えてくださいました

あと、CTMCPとか。