リニアな状態遷移を持つパズル１ - 教えて！アロイ人！

宣教師と土人の問題

昔から非常によく知られているパズルですが、意外に日本語のWeb上に回答例が見当たらないので取り上げてみます。

川のこちら側に３人の宣教師と３人の土人がいます。こちらの川岸に２人乗りのボートが１艘あり、これを使って６人全員を対岸に移したいのですが、一時的にも宣教師の数が土人の数より少なくなると土人は宣教師を食べてしまいます。何とか無事に全員を対岸まで渡らせる手順を考えて下さい。

僕がこの問題にはじめて触れたのは小学校の時で、父に教えてもらって一生懸命考えた記憶があります。今考えても、この問題を考えた人はすごいなぁ、とつくづく思うのですが、ちょっと考えて無理そうなことを、「いいやできるはず」という意思をもって解を探索する直感と意思を持つ人間になりたいものです。

ただ、この「宣教師と土人」というモデルは、そろそろ変えていかないとまずいような気がしなくもありません。人権団体とか、あまり論理パズルの本とか読まないんでしょうか。

状態遷移

これまで手がけてきた「うそつき」の論理パズルは、全て「ある特定の時点」のことのみに言及していて、時間的な前後関係や、操作することで状態が変化していくようなものはありませんでした。
しかし、このパズルには時間軸があり、川をボートで渡ることで状態が変化し、変化した状態からまた先の状態を考えてゴールを目指す必要があります。考えればパズルとして、こういうものは珍しくないというかむしろ普通なのですが、Alloyでこういうものを扱う時は、これまでになかった道具を使っていく必要があります。それが「状態」と「遷移」です。これについては、Alloyのチュートリアルに、よく似た「農夫の川渡り」の問題の解が取り上げられているので、それを参考に考えていくことにします。

さて、我々はいつも「特定の状態にあって、何かをきっかけに次の状態に移る」ということを繰り返しており、それを「時の流れ」と捉えることができますが、このパズルでは時間の流れを、

1. 最初の状態（全員こっちがわにいて、ボートもこちらにある）
2. 次の状態（前の状態から、1人もしくは2人の人間があっちがわにうつっていて、ボートはあっち側にある）
3. 次の次の状態（前の状態から、1人もしくは2人の人間がこっちに戻っていて、ボートはこっち側にある）
4. 次の次の次の状態（前の状態から、1人もしくは2人の人間があっちがわにうつっていて、ボートはあっち側にある）
5. （以下略）

を繰り返していく操作とと考えることができます。
つまり、「ある状態と、その次の状態の間に成り立たなければならない条件」を定義することで、時間の流れを定義することができるということです。

ただし、これに加えて、

• どの時点でも、どちらの岸でも宣教師の数が土人の数より少なくならないように（ただし宣教師がいない場合は可）
• 最終的に全員があっちがわにいる

という条件を加えて、パズルの定義が完成することになります。

登場人物と場、状態の定義

それでは、まず最初に登場人物の定義を行いますが、その前に、今回使用するAlloyのライブラリを読み込んでおく必要があります。今は特に細かいことを考えなくてもかまいません。

open util/ordering[状態] as ord

util/orderingというライブラリを、「状態」というシグネチャの管理のために開き、それをordという名前で管理する、という宣言になります。

次は、人の定義に入ります。今回のパズルでは、パズルの状態を管理するために「状態」というシグネチャを導入しますので、人間をあらわすPersonオブジェクトは特に何もフィールド（ステータス）を持つ必要はありません。

abstract sig Person {}

続いて、宣教師と土人の定義です。

sig 宣教師 extends Person {}
sig 土人 extends Person {}

そして、状態の定義に入ります。このシグネチャを使い、ある時点で宣教師と土人、それにボートがどうなっているかを管理します。

sig 状態 {
  こっち: set Person,
  あっち: set Person,
  ボート : one Place  
}

enum Place {こっちにある, あっちにある}

「こっち」と「あっち」には、0人以上の(set）人（Person）がいることを示しえいます。ボートの状態「Place」は「あっちにある」か「こっちにある」かのどちらかです。

基本的な（静止的な）事実の定義

続いて、ひとつの状態の中で定められる制約を記述します。

• ゲームの最初の時点で、人はすべてこっち側にいる。あっち側には誰もいない。

first.こっち = Person && no first.あっち

「first」というのは、util/orderingの中で定義されている言葉で、遷移するステータスの最初の状態を表します。
また、= Personという表現は初めて出てきましたが、これは、「first.こっち」という集合、つまり最初の状態でこっちにいる人、というのが、Person全体の集合と同じであることを示しています。

• ゲームの最初の時点で、ボートはこちらがわにある

first.ボート = こっちにある

• 宣教師は三人、土人も三人

  #宣教師 = 3
  #土人 = 3

＃というのは、それに続くシグネチャの実際の数を示します。

• 土人の数が宣教師より多くなってはならない

all s : 状態 | 安全[s.こっち] && 安全[s.あっち]

述語（pred）を使って、すべての「状態」において、「こっち」と「あっち」の両方で成り立たなければならない条件を記述しています。

pred 安全 [group : set Person] {
  #(group & 宣教師) >= #(group & 土人) || #(group & 宣教師) = 0
}

「安全」とは、指定されたグループの中の宣教師の数が、同じグループの土人の数より同じか大きい、もしくは宣教師がいないかのどちらかである。
ということを示しています。
「#(group & 宣教師)」というのがちょっとわかりにくいかも知れません。groupは、上の「安全[s.こっち]」で与えられた「s.こっち」に相当します。こっちは「set Person」つまり人のこっち側にいる人の集合です。一方「宣教師」というのは、このゲームで登場する全ての宣教師の集合を意味します。この二つの「&」をとるというのは、両者の共通する要素だけを抜き出すということです。つまり、#(group & 宣教師)は、「特定の人の集まりのうち、宣教師の数を数える」という意味で使うことができるのです。

川を渡るとはどういうことか

それでは、いよいよ人が川を渡ります。

pred 川を渡る [移動元, 移動先, 移動元', 移動先' : set Person] {
  (one a : Person |
    a in 移動元 &&
    移動元' = 移動元 - a &&
    移動先' = 移動先 + a) ||
  (some disj a, b : Person |
    (a + b) in 移動元 &&
    移動元' = 移動元 - (a + b) &&
    移動先' = 移動先 + (a + b))
}

上で定義した「川を渡る」という述語（pred）の前半は「一人で川を渡るということ」、後半は「二人で川を渡ること」を意味しています。その間にある「||」という縦棒二つは「or」で、「川を渡ると言うのは一人で渡るか二人で渡るかのどちらかが起こることである」ことを表しています。
注目すべきは述語の引数で、移動元、移動先、移動元'、移動先'の四つが渡ってきています。前半の二つは、渡る前の、川のあちらとこちら（どっちがどっちかはわかりません）を、後半の二つは渡った後の川のあちらとこちら（やはりどっちがどっちかわはまだわかりません）を表しています。

というわけで定義の中身を見ていきます。前半の「一人で川を渡る」を抜き出してみると、

one a : Person |
    a in 移動元 &&
    移動元' = 移動元 - a &&
    移動先' = 移動先 + a

これは、誰か一人について、

1. その人は移動元にいて
2. 移動した後の移動元（移動元'）は、移動する前の移動元（移動元）からaを抜いた（取り去った）もので、
3. 移動した後の移動先（移動先'）は、移動する前の移動先（移動先）にaを追加したものである。

ということを言っているわけです。
aが移動するためにはaが移動元にいなければなりませんし、aが移動したら、移動元からはaがいなくなり、移動先にaが増える。そういうことを述べているのです。それを踏まえて上の定義を納得できるまでじっと眺めてください。
ちなみに、上でなにげなくやっている加算（＋）と減算（－）ですが、これは整数の加減算ではなく、「集合の加減算」です。「集合」を感じるということはAlloyを理解するためには必須といってもいいほど重要なことなのですが、ここでは軽く触れるだけにして、イメージだけつかんでください。
それでは後半です。

some disj a, b : Person |
    (a + b) in 移動元 &&
    移動元' = 移動元 - (a + b) &&
    移動先' = 移動先 + (a + b)

さきほどと似たようなものですが、二人いるぶんちょっと記述が長いです。
あるaさんとbさんについて、

1. aさんとbさんの両方が移動元にいて、
2. 移動した後の移動元（移動元'）は、移動する前の移動元（移動元）からaさんとbさんの両方を抜いた（取り去った）もので、
3. 移動した後の移動先（移動先'）は、移動する前の移動先（移動先）にaさんとbさんの両方を追加したものである。

（先頭がoneではなくsomeになっている理由は、ちょっと自分でも納得できる説明が出来ないので割愛させてください。僕の勉強不足ですすみません。）
これで、「川を渡ること」が定義できました。次に実際に川を渡る状態遷移を定義します。

状態の遷移（うつりかわり）

最初のところで「util/ordering[状態]」という定義をしましたが、実はこの行によって「状態」というものが

• 「first」から始まり
• ある状態sのの次の状態はs.nextとなっていて
• 「last」で終わる直線的な状態の移り変わりをするものである

ということが定義されていました。
これを使って、「今」と「次」の状態について、どのようなことが成り立つかを「川を渡る」を使って示します。

fact 状態遷移 {
  all 今 : 状態, 次 : 今.next {
    今.ボート = こっちにある =>
        川を渡る [今.こっち, 今.あっち, 次.こっち, 次.あっち]
    else
        川を渡る [今.あっち, 今.こっち, 次.あっち, 次.こっち]
    今.ボート != 次.ボート
  }
}

このfactには「状態遷移」という名前をつけていますが、これはなくてもかまいません。
中を見てみると、全ての「今」と「次」について、つまり、全ての状態と状態のつながりの間には次の条件が成り立つと言っています。
その中身は、

1. 今、ボートがこっちにあるなら、次の状態は人が一人か二人こっちからあっちに渡った状態
2. そうでないなら、次の状態は人が一人か二人あっちからこっちに渡った状態
3. 次の状態では、今の状態と必ずボートの場所が違っている

という三つの条件です。「川を渡る」の引数の前半後半が入れ替わっていることに注目してください。

最後に、ゴールの状態をrunコマンドに与え、6人の人間で、最大12の状態でゴールを目指します。

run { last.あっち = Person } for 6 but 12 状態

なんで12かと言いますと、20ぐらいから初めて、少しずつ減らしていっただけです。

実行結果

横に長くなってしまったので、分割して画面を貼ります。

全部で11手、最初の状態を入れて12個の状態が並びました。これらの状態と状態の間で、指定した状態遷移の条件や、宣教師が土人より多いといった条件が全て守られていて、ボートがこっちからあっちへと渡っている状態遷移となっていることを確認してください。

おわりに

今回は少しトピックが多くなりました。状態の遷移を扱うことは非常に重要なことで、パズルに限らずこの世で普通に起こっている出来事を普通にモデリングする際に極めて重要な考え方になりますので頭がちゃんと納得できるまで考えてみてください。ちなみに、こういう「状態と状態との間で成り立つ命題」を扱う論理学を「様相論理」と言います。きちんと勉強しようとするとかなり面倒ですが、こういう形で慣れておくと難しいことを知らなくても使いこなすことができるようになると思います。

全ソース

open util/ordering[状態] as ord

abstract sig Person {}

sig 宣教師 extends Person {}
sig 土人 extends Person {}

sig 状態 {
  こっち: set Person,
  あっち: set Person,
  ボート : one Place  
}

enum Place {こっちにある, あっちにある}

fact {
  first.こっち = Person && no first.あっち
  first.ボート = こっちにある
  #宣教師 = 3
  #土人 = 3
  all s : 状態 | 安全[s.こっち] && 安全[s.あっち]
}

pred 安全 [group : set Person] {
  #(group & 宣教師) >= #(group & 土人) || #(group & 宣教師) = 0
}

pred 川を渡る [移動元, 移動先, 移動元', 移動先' : set Person] {
  (one a : Person |
    a in 移動元 &&
    移動元' = 移動元 - a &&
    移動先' = 移動先 + a) ||
  (some disj a, b : Person |
    (a + b) in 移動元 &&
    移動元' = 移動元 - (a + b) &&
    移動先' = 移動先 + (a + b))
}

fact 状態遷移 {
  all 今 : 状態, 次 : 今.next {
    今.ボート = こっちにある =>
        川を渡る [今.こっち, 今.あっち, 次.こっち, 次.あっち]
    else
        川を渡る [今.あっち, 今.こっち, 次.あっち, 次.こっち]
    今.ボート != 次.ボート
  }
}

run { last.あっち = Person } for 6 but 12 状態

（文責：片山 功士）

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