問題
どこかの国の非実在学園での話と思ってちょーだい。
この学園には四種類の人間が通っているそうです。男の子、女の子、男の娘、男装の麗人だそうで。自由な校風なんですね。
自由なのは結構なんですが、時偶あるのが、かわいい女の子だ！と思ったら実は男の娘でしたと云う悲劇で、人によっては美味しいシチュエーションなんでしょうが、少なくともぼくは女の子のほうがいいです。野郎は野郎なので……。ただ、学ラン着てる女の子とか倒錯してていいかんじだなあ、と思うので、男装の麗人はうぇるかむですね！わいわい。
と云う訳で、何とかして性別を判定したいんですが、はて……。
ところで、いかに自由な校風と云えど、一つだけ校則があるそうです。曰く、「嘘吐きは須く嘘を吐き、正直者はみな真実のみを喋るべし」。この法則は受け答えだけでなく、日常の所作や言動にも適用されるそうで、従って男の子や女の子は常に真実を、男の娘や男装の麗人は常に嘘だけを喋ることになります。
これを使って何とかして女性だけを見付けられないでしょうか？あとしつこい男は嫌われるので、イエス・ノーで答えられる質問一つだけで見分けられると良いんだけど……と云うのが問題。
解説
この問題の原典は、『スマリヤンの決定不能の論理パズル―ゲーデルの定理と様相理論』の第五章で出て来る金星人と火星人のパズルです。原典では「金星人の女性は常に真実、男性は常に嘘を喋り、火星人はその逆」と云う設定です。そのまま使ってもよかったんですが、今っぽいサブカルネタを採り入れた方がウケるだろうと云う編集部のテコ入れによって男の娘パズルに姿を変えました。純粋に政治判断であって、ぼくが男の娘が好きってわけじゃないです。理解は出来ますが、やっぱりね……。寧ろ男装女子のほうが好きです！わいわい。
閑話休題。そのまま論理的に解いても良いのですが、今回はAlloy Analyzerを使います。
Alloy Analyzer と云うのは有界モデル検査器とよばれるものの一種で、仕様を記述するとそれを満たす有限モデルを列挙・可視化してくれるようなツールです。ソフトウェアの仕様や抽象化の漏れ・矛盾が無いかを確認するツールですね。
何やらようわかりませんが、こいつの裏では SAT ソルバが動いているので、リッチな SAT ソルバのフロントエンドと思っておけば間違いないです。
と云う訳で、早速 Alloy で記述してみたのが以下です*1。
module otokonoko
enum 男か女 {男, 女}
enum 真理値 {真, 偽}
sig 質問 {
評価: 人間 -> one 真理値
}
abstract sig 人間 {
性別: 男か女,
服装: 男か女,
回答: 質問 -> one 真理値
} {
all q : 質問 |
性別 = 服装 <=> 回答[q] = q.評価[this]
}
one sig 男の子 extends 人間 {} {
性別 in 男 and 服装 in 男
}
one sig 男の娘 extends 人間 {} {
性別 in 男 and 服装 in 女
}
one sig 女の子 extends 人間 {} {
性別 in 女 and 服装 in 女
}
one sig 男装の麗人 extends 人間 {} {
性別 in 女 and 服装 in 男
}
pred 女性発見器(何か: 質問) {
all 誰か: 人間 | 誰か.性別 in 女 <=> 誰か.回答[何か] = 真
}
run 女性発見器これを実行すると以下のようなモデルが得られます*2。
何だかごちゃごちゃして判りづらいですね。と云う訳で「質問」で射影して、要らないものを消してみます。
図を見てみると、確かに性別が女性のときだけ「はい」、男性は「いいえ」と答えるようになっていますね。よかった！
では、どんな質問なのか？「評価」関係を基に見てみると……
| 性別 | 服装 | 質問の値 | 答え |
|---|---|---|---|
| 男 | 男 | 偽 | 偽 |
| 男 | 女 | 真 | 偽 |
| 女 | 男 | 偽 | 真 |
| 女 | 女 | 真 | 真 |
と云う関係にあるみたいです。よくよく見てみると、性別関係なく、服装が女性であるときだけ質問は真になっているので、求める質問は「あなたは女性の服を着てますか？」が答えと云うことになります。よかったね*3！
舞台裏
なんでこんなことを考えていたのかと云うと、社内発表で Alloy について喋ろうと思ってたんですが、Alloy のメインの用途と云っても過言ではない*4、論理パズルソルバとしての例が資料に欠けてることに気付いたわけなんですよ。
最初は有名な Kalotan パズルをやろうと思ったんですが、抽象化をどうしていいかわからずに「Kalotan パズルはAlloy に向いてない」などと安易に口走ったところ、bonotake さんの鉄槌を喰らってしまったので、これを参考にしつつ、何か知ってるパズルを解いてみようとしたのでした。
こういう、質問を探し出す"メタパズル"をどう解けばいいかなあ……と云うのを悩んでいると、ぼのたけさんから助言を頂いたので、それを参考にしつつ頑張ってみました。てへ ('-'*
この記事で Alloy に興味を持った方は、
- 作者: Daniel Jackson,中島震,今井健男,酒井政裕,遠藤侑介,片岡欣夫
- 出版社/メーカー: オーム社
- 発売日: 2011/07/15
- メディア: 単行本（ソフトカバー）
- 購入: 8人 クリック: 274回
- この商品を含むブログ (35件) を見る
を読むとAlloy の興味深く楽しい世界を知ることが出来るかと思います。僕もこれで勉強しています。
ウェブでも、id:m-hiyama さんや id:bonotake さん、さかいさんなどが Alloy の記事を書かれているので、参考にすると良いかと。
オマケ
ところで、世の中には「男の娘にしか興味ないんじゃい！」と云う末期の方々もいらっしゃると聞き及びましたので、その方々の為に「男の娘発見器」のソースも載せておきます。
さっきのの末尾にこれを追加して実行すれば、求めるものが手に入りますよ*5。
pred アッ男の娘だ(誰か: 人間) {
誰か.性別 in 男 and 誰か.服装 in 女
}
pred 男の娘発見器(何か: 質問) {
all 誰か: 人間 | アッ男の娘だ [誰か] <=> 誰か.回答[何か] = 真
}
run 男の娘発見器これがどのような質問なのかは、自分でモデル生成して考えてみてください。
それでは、enjoy!
