bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

Alloyで知識論理を使わずに論理パズルを解く

うーん、命題を指標にするのかー。

と感心しつつ、自分も眠気覚ましに解いてみました。途中様相論理をものすごく使いたくなったけど、敢えて使わない方針で。ちょっと嘘くさいんだけど。

-- Aさん、Bさん
abstract sig Person {
  wears: some Hat, -- 被っている帽子と思われるものの「集合」
}
one sig A, B extends Person {}

-- 帽子(赤を被らない人は白、はここの定義で言えている)
abstract sig Hat {}
sig RedHat, WhiteHat extends Hat {}

fact Rules {
  -- 少なくとも一人は赤い帽子を被っている
  some p: Person | p.wears in RedHat
  -- 帽子の数は人数分
  #Hat = 2
}
-- (相手の帽子の色を)知っている
pred knows(p: Person) {
  p.wears in RedHat || p.wears in WhiteHat
}

様相論理を使わない代わりに、AさんとBさんが被ってる帽子 'wears' を集合にしてやりました。で、

  • どの帽子を被ってるのがわかっている ⇔ wears の集合が、赤の帽子か白の帽子かのどちらかに含まれる
  • どの帽子を被ってるのがわかっていない ⇔ wears の集合に、赤帽子も白帽子も含まれる

という勝手な解釈で。非決定性を扱うのにリストで表現するようなもんです(本当か?)
Alloyという言語は述語論理と集合論のミクスチャーなんで、そこいらへんうまく使い分けると便利。(逆に、初学者にはひたすら混乱の元になってる気もしなくもないですが)


で、モデルのインスタンスがあるかチェック…するんだけど、見た目的に面白くないので絵は省略。記述はたとえばこんな感じで。

pred show() {
  knows[B]
}
run show for 10

で、下記アサーションで反例なしです。

assert BsHatInRed {
  (knows[B] and not knows[A]) => B.wears in RedHat
}

check BsHatInRed for 8

んー、やっぱちょっと嘘くさいんですがね。きちんとした解は、元記事のさかいさんをご参考に。

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。