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

天使、悪魔、人間

前回のに続き、再び「論理パズル「出しっこ問題」傑作選」からの問題です。

天使、悪魔、人間の３人がいます。
天使は常に真実を語り、悪魔は常にウソをつきますが、人間は真実を語ったりウソをついたりします。
黒いドレスの乙女「私は天使ではありません」
青いドレスの乙女「私は人間ではありません」
白いドレスの乙女「私は悪魔ではありません」
いったい誰が何？

という問題です。

今回は、今まで使っていなかった「述語」というものに触れてみます。

とりあえず場と人の定義。

もうだいぶ目が慣れてきたでしょうか？

abstract sig Person {
  kind : one Kind
}

one sig A_黒ドレス, B_青ドレス, C_白ドレス extends Person {}
enum Kind {天使, 悪魔, 人間}

以上で、3人の乙女とその種類について定義をしました。
さらに前回でも使った制約をいれ、悪魔が二人になったり、人間がいなくなったりしないようにします。

制限の定義

fact {
  all k : Kind | k in Person.kind
  no disj a, b : Person | a.kind = b.kind
}

１行目は、全ての種類は誰かを指していること、２行目は、違う人が同じ種類にならないことを意味しています。

パズルの問題文の定義

問題文を見ると、三つともほとんど同じ形をしていることに気がつきます。
「どれも私は＊＊＊ではありません」という形ですね。こういう場合、引数付きの「述語」を定義して、関数のように使うことができます。

pred 発言 (p : Person, k : Kind) {
  p.kind = 天使 => p.kind != k else p.kind = 悪魔 => p.kind = k
}

「pred」で定義しているのが述語（Predicate）です。predで定義された条件（命題）は、引数を持つことができますが、それとは別に、これまで使ってきた「fact」と決定的な違いがあります。
factは、書いてあるだけで常にどこでも成り立たなければならない条件となりますが、predで定義された条件は、runから直接的に、あるいは間接的に呼び出されない限り有効になりません。
ということを踏まえて、上の定義をもう一度見てみましょう。引数はpとkで、それぞれPersonとKindです。このpとkを使って条件を記述します。
「もしpが（pのkindが）天使ならば、pはkではない。そうでない場合で、pが悪魔ならば、pはkである。」という記述です。
ここで「そうではない場合」というのを示すために「else」という単語が出てきています。普通のプログラミング言語をやったことのある人なら分かると思いますが、「ならば」が「if」だと考えるとこう書くのがしっくりくると思います。
pが人間の場合に触れていませんが、人間は本当かウソかわからないので、何を言っていても何もあてになりません。書く必要がないのです。
これで述語の定義ができました。

述語の呼び出し

先ほど書いたように、述語は呼び出さなければなりません。runの中から、必要な引数を渡して呼び出しましょう。
述語を呼び出すには、述語の名前に続けて、大括弧（［］）ではさんで、カンマ区切りで引数を並べてやります。もちろん引数に渡すものは、述語の定義で指定されたものでなければなりません。

run {
  発言[A_黒ドレス, 天使]
  発言[B_青ドレス, 人間]
  発言[C_白ドレス, 悪魔]
}

述語「発言」を３回分呼び出しました。これを「発言」の定義と照らし合わせれば、問題文に書いてある条件と同じになることがわかると思います。

実行結果

まとめ

今回は述語の使い方を見てきました。実は述語の使い方は非常に幅広く、今回のサンプルではそのほんの一部にしか触れることができていません。述語を使いこなすことで、時間や操作のような概念を取り込むことができるようになり、Alloyはさらに強力なツールとなります。それについてはまたの機会に。

全ソース

abstract sig Person {
  kind : one Kind
}

one sig A_黒ドレス, B_青ドレス, C_白ドレス extends Person {}
enum Kind {天使, 悪魔, 人間}

fact {
  all k : Kind | k in Person.kind
  no disj a, b : Person | a.kind = b.kind
}

pred 発言 (p : Person, k : Kind) {
  p.kind = 天使 => p.kind != k else p.kind = 悪魔 => p.kind = k
}

run {
  発言[A_黒ドレス, 天使]
  発言[B_青ドレス, 人間]
  発言[C_白ドレス, 悪魔]
}

（文責：片山 功士）

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