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

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

……

ほほぅ……

……

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

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

カロタンは奇妙な癖のある種族です。男は常に真実を語り、女はいちどきに 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 {  } 

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

[追記] ミソは、カロタン親子の発言をどうモデル化するかです。
特に、「キビが男の子である」という事実と、「キビは（自分を）男の子と（あるいは女の子と）言った」という事実と、更にそれを言明する親の発言とを、ナイーブにAlloyの制約式にしてしまうと同列にモデル化できないわけです。
得てして高階論理で書きたくなるかもしれませんが、Alloyは一階論理しか扱えません（mr_konnさんが「向かない」と思ったのも、たぶんこの辺り）。

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