Alloy Analyzerについて教えてもらった時, Alloyなら, なぞなぞを解けるという話になって, でもそれってPrologでもほとんど同じことができるんじゃないかと思ったのですが, とりあえず, 以下のページにAlloyのなぞなぞSolverの実装があります.
Prologで同じ問題を解いてみようと思ったのですが, ほとんど書いたことのないPrologで一からやるより, 身近なClojureでやってみたほうが簡単だろうと思って, Clojure.core.logicを使って, 上記のページの問題を1問解いてみました.
Clojure.core.logicは, Clojureの論理プログラミング用のライブラリで, 主な使い方は, 以下のページに載っています.
解いたのは, レイトン教授のNo.50の問題で,
牛が5頭(それぞれa~eとする)いて, うち, 3頭は, ウソしか言わない種であり, 残りの2頭は, ホントのことしか言わない種であるそうです. このとき, 各牛は, 次のように発言しています.
a : dはウソをついている.
b : cはウソをついている.
c : aはウソをついていない.
d : eはウソをついている.
e : bはウソをついている.
さて, このとき, 嘘をついているのは誰でしょうという問題.
というわけで, 小学生の頃よくやった推理算ですが, 元の記事では, この問題をAlloyを使ってコンピュータに考えさせようという話でした.
core.logicで書くとAlloyで書いた場合よりも少し冗長になっている気がしました(マクロを駆使すれば解決できるのでしょうが/また, 書きなれていないことも原因かもしれません).
core.logicのオペレータは非常にシンプルで, ==, conde, fresh, consoが主でした. それぞれ, 同値であるという述語, 条件分岐, 変数の束縛, リストの構築を表す述語(?)です.run*でUnificationを実行し, 各変数のmost general unifier(最も一般化された単一子, 要するに述語を満たすような最も抽象的な値)を求めます. 結果は, 束縛した変数に対応する値のリストとして返されます. 答えの候補が複数ある場合は, 一つの変数に対して, リストが返ってきます. run*の次のシンボルのベクタが, 求めたい変数のリストで, その後ろのS式が, 制約条件となります.
問題の発言を述語にするのは, 簡単で, 「aがdはウソをついている」 という発言は, 「a = "正直"かつb = "嘘つき"」または, 「a = "嘘つき"かつb = "正直"」といった感じで, 発言者について場合分けすれば, きれいに分解できます. もっともAlloyのコードでは, 逆のパターンの記述はする必要がないようですが.
5頭のうち, 2頭が正直であるという条件の制約の定義は手間取りました. もう少し, 上手い書き方があるような気がするのですが... 以下のソースコードのhonest-cows-inという関数がそれに相当します. しかし, このような書き方が適切なのかよくわかっていません.
以下がソースコード.
(use 'clojure.core.logic)
(defn honest-cows-in [ls n]
(fresh [xs]
(conde
[(== ls []) (== n 0)]
[(conso 'honest xs ls)
(honest-cows-in xs (dec n))]
[(conso 'liar xs ls)
(honest-cows-in xs n)])))
(defn layton50 []
(run* [a b c d e]
(fresh [ls]
(conso a [b c d e] ls)
(honest-cows-in ls 2))
;; A said D is a liar. (A is honest and D is liar) or (A is liar and D is honest).
(conde [(== a 'honest) (== d 'liar)] [(== a 'liar) (== d 'honest)])
;; B said C is a liar.
(conde [(== b 'honest) (== c 'liar)] [(== b 'liar) (== c 'honest)])
;; C said A is honest.
(conde [(== c 'honest) (== a 'honest)] [(== c 'liar) (== a 'liar)])
;; D said E is a liar.
(conde [(== d 'honest) (== e 'liar)] [(== d 'liar) (== e 'honest)])
;; E said B is a liar.
(conde [(== e 'honest) (== b 'liar)] [(== e 'liar) (== b 'honest)])))
実行してみると,
user> (layton50)
([liar honest liar honest liar])
それぞれ, run*で束縛した[a b c d e]という各牛のパラメータで, aとc, eが嘘つきだということが判明しました. というわけで, 答えは出ましたが, 正解かどうかは知りません. 少なくとも, clojure.core.logicでなぞなぞSolverは記述できるようです.