今回はAlloy本から普通にパズル、とその先に見えたこと。

問題

Alloy本 A.3.4 Halmos の握手問題

あるパーティーで、Alice と Bob は４組のカップルを招いた。
互いに知り合いだった者もいれば、そうでない者もいた。礼儀正しい者もいれば、そうでない者もいた。
そのため何人かは握手をしたが、ゲストのすべての組み合わせで握手が交わされたわけではない（もちろん、自分とも自分のパートナーとも握手した者は１人もいなかった）。
Alice はパーティーの終わりに、興味本位で何人と握手したかを全員に訊いて回った。
彼女は９人から９つの異なる回答を得た。
Bob と握手したのは何人だろうか？

リスト

書くこと自体は特に問題なかった。
ただ１点気になったのが「Alice と Bob がカップルだとは問題文に書かれていない」こと。
文脈からカップルであると仮定して、コメントを残す形とした。

one sig Alice, Bob extends Person {}
sig Guest extends Person {}
abstract sig Person {
    partner : Person-this,
    shake: set Person-this-partner,
    shakes: #shake
}
fact {
    partner = ~partner
    shake = ~shake
    Alice.partner = Bob     // とは明言されてないけど..
}

fact disjShakes {
    #shakes[Person-Alice] = #(Person-Alice)
}
run {} for 5 int, exactly 10 Person

check {Bob.shakes=4} for 5 int, exactly 10 Person

結果

Bobの握手数は４、反例はなかった。

図を見て「全員、握手回数をパートナーと合わせると８になるようだ」と思い、確認してみた。

check { all p:Person | add[p.shakes, p.partner.shakes] = #Guest }
 for 5 int, exactly 10 Person

「全員、握手回数をパートナーと合わせるとゲスト人数になる」に反例はなかった。
人数を増やしていくと反例探しにかかる時間が厳しいので数え方を変えないといけないだろう。

追加調査

Alice と Bob がカップルでなかったら？

さて、気になっていた件を少し確認してみよう。
Alice と Bob がカップルではなく、握手したかもしれないと考えたらどうだろう。
少し修正して試してみると、Bob の握手数は 4,5,6,7,8,9 の６通りになった。

まだ気になることがある。
「握手が交わされたのは Alice,Bob,ゲスト の間だけ」とは問題文に書かれていない。
Alice と Bob それぞれのパートナーが「招かれてはいないがホスト関係者として参加していた」なら？
パーティー参加者以外のケータリング業者と握手した者がいたら...

だんだん叙述トリックを読んでいるような気分になってきた。
「厳密に言葉通り」を追求すると解がなくなるのは確実なのでやめておこう。

原典はどうだった？

探してみると、本家リポジトリにソースがあった。
　handshake.als

冒頭にコメントがあるので読むと最初の行にいきなり "Hilary and Jocelyn are married. They invite four couples who are friends for dinner." とある。
他に握手対象がいなかったかについても "When they arrive, they shake hands with each other." なので they, each other に含まれない文章外の人とは握手していない、と読める。
原文では明記されていたのだ。
（まあ Hilary と Jocelyn は arrive した１つめの they に含まれないので each other にも含まれないという解釈もできるが、冒頭の２文に現れる面々が２つめの they および each other の対象と考えるべきだろう）

かなり注意深く行われたという翻訳作業でも、日本語にした時点であいまいになってしまったようだ。

ところで

• 「全員、握手回数をパートナーと合わせると８になる」証明も handshake.als のコメントに書かれている。
• 直々に書かれた handshake.als だが、Spouses の記述がくどいように思う。
  そこそんなにかみくだいて説明するほど大事ですかね？

参考

• Daniel Jackson：抽象によるソフトウェア設計 ―Alloyではじめる形式手法
• handshake.als