Clojure.core.logicでレイトン教授の問題を解く

 Alloy Analyzerについて教えてもらった時, Alloyなら, なぞなぞを解けるという話になって, でもそれってPrologでもほとんど同じことができるんじゃないかと思ったのですが, とりあえず, 以下のページにAlloyのなぞなぞSolverの実装があります.

レイトン教授で始める Alloy Analyzer入門 - まあ、そんなもんでしょう。

 Prologで同じ問題を解いてみようと思ったのですが, ほとんど書いたことのないPrologで一からやるより, 身近なClojureでやってみたほうが簡単だろうと思って, Clojure.core.logicを使って, 上記のページの問題を1問解いてみました.

clojure.core.logic - GitHub

 Clojure.core.logicは, Clojureの論理プログラミング用のライブラリで, 主な使い方は, 以下のページに載っています.

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

 解いたのは, レイトン教授の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は記述できるようです.