たけをの日記@天竺から帰ってきたよ このページをアンテナに追加 RSSフィード

2011-08-29

カロタンパズルをAlloyで解く

| 17:04 | カロタンパズルをAlloyで解くを含むブックマーク

今日、twitterで @mr_konn さんがこのような発言をなされました。

f:id:bonotake:20110829170024j:image

……

ほほぅ……

……

f:id:sangencyaya:20080905173143j:image

というのはウソですが、これくらいの論理パズルが向かないってことはないだろー。

と思い、解いてみました。

ちなみに、カロタンパズルはこんなの(こちらから引用)。

ロタンは奇妙な癖のある種族です。男は常に真実を語り、女はいちどきに 2 つの真実は言わない、あるいは、いちどきに 2 つの嘘は言わないというものです。

ある人類学者(彼をウォルフと呼びましょう)が彼らの研究を始めました。ウォル フはまだ、カロタンの言葉を知りません。ある日、カロタンのカップル(異性)と その子どものキビと出会いました。ウォルフはキビに「きみは男の子?」とたず ねました。キビはカロタン語で答えたので、ウォルフには分りませんでした。

ウォルフは両親(英語を知っている)に説明を求めました。ひとりが、「キビは、 自分は男の子だといっている」と言いもうひとりが、「キビは女の子。キビは嘘 をついた」と付け加えました。

この両親の性別とキビの性別をあててください。

で、Alloyのモデル。(Gistにも貼ってあります。)

abstract sig カロタン {
  性別: 男か女か,
  発言1: Prop,
  発言2: lone Prop
}
{
  // 男なら常に真実を語る
  性別 in 男性 => 発言1.真偽 in ホント and (some 発言2 =>発言2.真偽 in ホント)
  // 女はどっちかホントでどっちかがウソ
  else some 発言2 => 発言1.真偽 != 発言2.真偽
}
enum 男か女か { 男性, 女性 }

one sig キビ extends カロタン {}
{
  // 自分を男といったか、女といったかのどちらか
  発言1 in キビは男の子 + キビは女の子
  no 発言2
}
one sig 親A extends カロタン {}
{
  発言1 in キビは男の子と言っている
  no 発言2
}
one sig 親B extends カロタン {}
{
  発言1 in キビは女の子
  some 発言2
  発言2 in キビはウソをついている
}

fact 親の性別はたぶん別々 {
  親A.性別 != 親B.性別
}

/** 皆さんの発言(命題)*/
abstract sig Prop {
  真偽: ホントかウソか
}
enum ホントかウソか { ウソ, ホント }

one sig キビは男の子 extends Prop {}
{
  真偽 in ホント <=> キビ.性別 in 男性
}
one sig キビは女の子 extends Prop {}
{
 真偽 in ホント <=> キビ.性別 in 女性
}
one sig キビは男の子と言っている extends Prop {}
{
  真偽 in ホント <=> キビ.発言1 in キビは男の子
}
one sig キビはウソをついている extends Prop {}
{
  真偽 in ホント <=> キビ.発言1.@真偽 in ウソ
}

run {  } 

出てきた解のスナップショット

f:id:bonotake:20110829170023j:image

[追記] ミソは、カロタン親子の発言をどうモデル化するかです。

特に、「キビが男の子である」という事実と、「キビは(自分を)男の子と(あるいは女の子と)言った」という事実と、更にそれを言明する親の発言とを、ナイーブにAlloyの制約式にしてしまうと同列にモデル化できないわけです。

得てして高階論理で書きたくなるかもしれませんが、Alloyは一階論理しか扱えません(mr_konnさんが「向かない」と思ったのも、たぶんこの辺り)。

その解決策として、ここでは各発言(命題)を述語やファクトでなく、シグネチャでモデル化してます。こうすることで、各発言やその真偽みたいなものを、Alloyのモデル上で統一的に扱えるようにしているのです。[/追記]