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

うそつきのパズル その２

黒猫白猫のパズルに続いて、うそつきの問題をもう一つ史上最強の論理パズルから引用してみます。

うそつき鳥、正直鳥

ここに２羽のカラス（AとB）がいます。それぞれミヤマガラスかワタリガラスです（ミヤマガラスはいないかもしれませんし、ワタリガラスはいないかもしれません）。一方の種（ミヤマガラスかワタリガラスかは不明）のカラスは常にウソをつき他方の種のカラスは常に真実を述べます。
Aが「私はミヤマガラスです」と言いました。Bが言ったのは「私はミヤマガラスです」「私はワタリガラスです」のどちらでしょう？

という問題です。

カラスの定義

まず、カラス（鳥としますが）がいて、それは何らかの種類に結びついていることを示します。

abstract sig Bird {
  kind : Kind
}

カラスは、AとBを１羽ずつ、計２羽だけを考えます。

one sig A, B extends Bird {}

カラスの種類はミヤマ、ワタリのどちらかです。

enum Kind {ミヤマ, ワタリ}

そのうちどちらか一方はうそつきです。

one sig うそつき in Kind {}

ここで、黒猫白猫で出てきた、「両含意」が登場します。

1. もしAがうそつきでないならAはミヤマガラスです
2. AがミヤマガラスならばAはうそつきでない

の両方を一度に表現できるのが両含意（<=>）です。

fact {
  not A.kind in うそつき <=> A.kind = ミヤマ
}

最後に、今のところのお約束をつけます。

pred show {}
run show

実行結果

これを実行すると、Alloyは四つの解を提示してくれます。
まずは一つ目。

Aはワタリガラスで、Bがミヤマガラス。うそつきはワタリガラスの方で、Bは正直ですから「私はミヤマガラスです」と言うことでしょう。

ウィンドウの上の「Next」をクリックすると、別の解がある場合にそれを表示してくれます。

AもBもワタリガラスで、うそつきはワタリガラスです。BはAと同じうそつきですから「私はミヤマガラスです」と言うでしょう。

AもBもミヤマガラスで、両方とも正直者です。やはりBは「私はミヤマガラスです」と言うでしょう。

Aがミヤマガラスで、Bがワタリガラス。うそつきはワタリガラスの方で、BはうそつきですからBは「私はミヤマガラスです」と言うはずです。

もう一度ウィンドウの上の「Next」をクリックすると、次のようなダイアログが表示されます。。

「もう他に解は見つからなかった」ということを言っています。

結論

というわけで、見つかった四つの解全てで、Bは「ミヤマガラスです」と答えることになっていました。これが解ということです。
「なんかすっきりしない。」もっとこう、一発で「Bはミヤマガラス！」という解が一つだけ表示されるような方法はないものなのか、と思われるかもしれません。僕も思っています。
僕もまだ勉強中なので、もっといい方法があるかもしれません。思いついたり見つかったりしたら、またここで公開します。

ただ、一番大切なのは、このように

1. 論理的に解を示すこと
2. その解に至った方法をきっちり提示できること

なのです。Alloyはそのソースを提示することで、なぜその解が出てきたことを100％提示できますし、他の人にそれを検証してもらうこともできます。大切なのはそこなのです。

全ソース

abstract sig Bird {
  kind : Kind
}

one sig A, B extends Bird {}

enum Kind {ミヤマ, ワタリ}
one sig うそつき in Kind {}

fact {
  not A.kind in うそつき <=> A.kind = ミヤマ
}

pred show {}
run show

（文責：片山 功士）

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