今日、twitterで @mr_konn さんがこのような発言をなされました。
……
ほほぅ……
……
というのはウソですが、これくらいの論理パズルが向かないってことはないだろー。
と思い、解いてみました。
ちなみに、カロタンパズルはこんなの（こちらから引用）。
カロタンは奇妙な癖のある種族です。男は常に真実を語り、女はいちどきに 2 つの真実は言わない、あるいは、いちどきに 2 つの嘘は言わないというものです。
ある人類学者(彼をウォルフと呼びましょう)が彼らの研究を始めました。ウォル フはまだ、カロタンの言葉を知りません。ある日、カロタンのカップル(異性)と その子どものキビと出会いました。ウォルフはキビに「きみは男の子？」とたず ねました。キビはカロタン語で答えたので、ウォルフには分りませんでした。
ウォルフは両親(英語を知っている)に説明を求めました。ひとりが、「キビは、 自分は男の子だといっている」と言いもうひとりが、「キビは女の子。キビは嘘 をついた」と付け加えました。
この両親の性別とキビの性別をあててください。
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のモデル上で統一的に扱えるようにしているのです。[/追記]
