うそつきのパズル その１ - 教えて！アロイ人！

うそつきのパズル

ブルーバックスのパズル本は論理パズルの良書が多く楽しませてくれます。今回はその内の一冊史上最強の論理パズルからの問題を取り上げてみます。

黒猫と白猫

リナ、カナ、ハルナのうち二人は黒猫を飼っています。また二人は白猫を飼っています。黒猫も白猫も飼っていない者はいません。
黒猫を飼っている者は必ずウソをつきますが、黒猫を飼っていない者が真実を述べるとは限りません。
リナ「カナは白猫を飼っています」
カナ「ハルナは白猫を飼っています」
さて、誰が何を飼っているのでしょう？

という問題です。よくある「うそつき」の典型的な問題ですが「真実を述べるとは限らない」のあたりがちょっと目新しいかもしれません。

これをAlloyにかけていきましょう。

人とネコに関する状況の記述

まず、白猫と黒猫を飼っている人、というものを定義します。

abstract sig Owner {
  black : lone BlackCat,
  white : lone WhiteCat
}

loneは「BlackCatの数は0か1」という条件を意味しています。

one sig リナ, カナ, ハルナ extends Owner {}
sig うそつき in Owner {}

1行めで３人のオーナーの定義をしてから、２行目でOwnerの中に（何人か分からないが）うそつきがいる、という定義をしています。

sig BlackCat {}
sig WhiteCat {}

この２行は、黒猫と白猫の定義ですが、名前など特に付けず「そんなのがいる」程度の定義になっています。

人とネコの間に成り立つべき関係（事実）を定義する

factに続いて、問題文を見ながら条件を追加していきます。
黒猫は２匹、白猫は２匹

 #Owner.black = 2
 #Owner.white = 2

＃Owner.blackは、全てのオーナーのblackを寄せ集めたものの要素数を表します。つまり、全部の黒猫の数が2であることをこれで示しています。パズルの趣旨としてはネコの数が問われているわけではないのですが、パズルの本質とはあまり関係がないので、ここでは一人が黒猫を複数飼うことは考えていません。白猫についても同様です。

 all a : Owner | #a.(black + white) > 0

この１行で定義しているのはどのオーナーを一人選んでも、そのオーナーが飼っている黒猫と白猫の数(#)は0より多いこと、つまり「黒猫も白猫も飼っていない人はいない」ことを指しています。

 no disj a, b : Owner | a.black = b.black
 no disj a, b : Owner | a.white = b.white

これは問題文には出てきていないのですが、同じ黒猫を複数のオーナーが共有してしまっては困るので、それを禁止するためのものです。つまり「二人の異なるオーナー（これをa,bとする）を選んだとき、aの黒猫とbの黒猫が同じであることはない」ということを語っています。白猫についても同様です。

 no c : BlackCat | not c in Owner.black
 no c : WhiteCat | not c in Owner.white

そしてこの２行もパズルの本文に語られていませんが、どの黒猫を一つ選んでも、それが誰かの飼い黒猫でない、ということはない」、つまり、どの黒猫もだれかに所有されている、ということを示しています。白猫も同様。

うそつきの定義

いよいよ「うそつき」についての記述をします。

all a : Owner | a.black != none <=> a in うそつき

これが意味するのは「すべてのオーナー（これをaとすると）について、aが飼っている黒猫がnoneでない、つまりaが黒猫を飼っている「ならば」aはうそつきの集団に含まれる」ということになります。
ここで、見慣れない記号「<=>」が出てきました。この記号は「両含意」という、とても便利なものなのですが、Alloyの本をみてもあまり強く触れられておらず、「サラッ」と流されていることが多いので、ちょっとここで語ってみます。

「含意」

ただし、「両含意」の前に、どうしても「含意」について学ぶ必要があります。
これを呼んでいる人の多くは、おそらく高校で一度は論理学の初歩を習っているはずです。「ド・モルガンの定理」が出てきて、ベン図を書いたりしていたやつです。その中で「ならば」という記号があったのを覚えているでしょうか。A→B（AならばB）というやつです。

• 人間ならば、死ぬ

という、「前者が成り立っているなら、後者は必ず成り立つ。前者が成り立っているのに後者が成り立っていないのはおかしい」と言えるような関係が「含意」です。
このAならばBという言葉の（ならば）にあたる関係を「含意」と呼び、Alloyでは（=>）という記号で表します。
この「含意」は一見分かりやすいのですが、使用にあたって重大な注意点があります。「前者が成り立っていない場合については特に何も言っていない」ということです。
例えば、お母さんが子供に
「勉強したら、おやつをたべていいよ」
と言った場合、当然「勉強しなければおやつはダメ」という意味を含むわけですが、論理学で言うところの「ならば」は、勉強をしなかった場合は「おやつは食べても食べなくてもいい」という意味になります。
「そんな理不尽な」と思うかもしれませんが、これが論理学の厳密さなので気をつけてください。
そんな訳なので、「黒猫を飼っているなら、うそつき」という文をAlloyに伝えるには、通常の「含意」ではまずいわけです。「含意」で書いてしまうと「黒猫を飼っているならうそつきだけど、飼っていない人はうそつきかもしれないし、うそつきでないかもしれない」という意味になってしまうからです。

両含意

ここで登場するのが「両含意」です。
おやつのケースで言うと、結局お母さんが言いたかったのは

1. 勉強したならば、おやつをたべていい
2. 勉強しないならば、おやつを食べてはいけない

という、二つのことなわけです。これを二つの条件を並べて書いてもいいのですが、二つ目の条件をよく見てください。
「勉強しないならば、おやつを食べてはいけない」
ところで「対偶」って覚えていますか？うっすらと思い出しませんか？「AならばB」が成り立つなら「BでないならばAでない」も必ず成り立つ、という関係を「対偶」と呼んでいませんでしたっけ？
この「勉強しないならば、おやつを食べてはいけない」の対偶は「おやつをたべていいならば、勉強した」となりますが、これは、一つ目の「勉強したならば、おやつをたべていい」の左右をひっくり返したものになっています。
つまり、お母さんが言っていたのは

1. 勉強した => おやつをたべていい（前半）
2. 勉強した <= おやつをたべていい（後半の対偶）

という意味なのです。
この両方をひっくるめた表現が

勉強した  <=> おやつをたべていい

というもので、ここで出てきた、右向きの「ならば」と左向きの「ならば」を足した記号が「両含意」という訳なのです。

これで分かるように、日常会話で使われる「ならば」の多くは「含意（=>）」ではなく「両含意（<=>）」の方になります。長くなってしまいましたが、「うそつきの定義」で両含意の記号を使っているのはそういう理由なのです。
ちなみに、両含意は（<=>）という記号を使う変わりに、iffという単語を使って

all a : Owner | a.black != none iff a in うそつき

と書くこともできます。ネット上のサンプルもこう書いているものが多いようです。が、僕は（<=>）という表現のほうが「両含意」という言葉の意味をよく表していて好きです。

発言の記述

最後に、リナとカナの発言を記述します。

リナが言っているのは「カナが白猫を飼っている」と言うことなので、リナがうそつきなら、カナは白猫を飼っていないことになります。リナがうそつきでない（黒猫を飼っていない）場合は、真実をいうとは限らない（ウソであるとも限らない）訳ですから、うそつきでない場合は何も語っていないのと同じなわけですから、何でもいいわけです。ということで、

リナ in うそつき => カナ.white = none

と書くことができます。リナがうそつきなら、カナは白猫を飼っていない。リナがうそつきでないなら、カナは白猫を飼っていても飼っていなくてもかまわない。これは図らずも「含意」で見た「理不尽な方」と同じになっていますから、「=>」を使って記述できます。

カナについても同様です。カナがうそつきなら、ハルナは白猫を飼っていないし、そうでないなら、ハルナは白猫を飼っているか飼っていないかわからないのです。

 カナ in うそつき => ハルナ.white = none

両含意を（iff）と書くことができるのと同じように、含意も(implies）という単語を使って

 カナ in うそつき implies ハルナ.white = none

と書いてもかまいません。が、僕は（=>）のほうがしっくりきますね。ただ「iff」や「implies」といった表現も覚えておかないと、人が書いたAlloyのソースを読むことができませんので、押さえておきましょう。

最後に

pred show {}
run show

「以上を満たすものを見せてちょうだい！！」という命令をこのように記述します。

実行結果

カナとハルナがうそつきで黒猫を飼っており、白猫はカナとリナが飼っている（カナは両方飼っている）ということが明らかになりました。

全ソース

abstract sig Owner {
  black : lone BlackCat,
  white : lone WhiteCat
}

one sig リナ, カナ, ハルナ extends Owner {}
sig うそつき in Owner {}

sig BlackCat {}
sig WhiteCat {}

fact {
  #Owner.black = 2
  #Owner.white = 2
  all a : Owner | #a.(black + white) > 0
  no disj a, b : Owner | a.black = b.black
  no disj a, b : Owner | a.white = b.white
  no c : BlackCat | not c in Owner.black
  no c : WhiteCat | not c in Owner.white
}

fact {
  all a : Owner | a.black != none <=> a in うそつき
}

fact {
  リナ in うそつき => カナ.white = none
  カナ in うそつき => ハルナ.white = none
}

pred show {}
run show

（文責：片山 功士）

今日： - 人
昨日： - 人
トータル： - 人