// この投稿は 数学 Advent Calendar 2016 の 23 日目の記事です。
前回の命題論理を実装する (C#) では命題論理を扱うためのライブラリを作成しました。
今回は、このライブラリを利用して複雑な問題をいくつか解いてみます。
騎士と悪漢
まず、前回でも紹介した書籍 Raymond Smullyan「記号論理学: 一般化と記号化」から、問題を 2 つ引用します。
すべての住民は騎士または悪漢のいずれかであり、騎士はつねに本当のことを言い、悪漢はつねに噓をつく。
問題 1.3
住民 A, B がおり、A は「私たちは二人とも悪漢だ」と言った。
A, B はそれぞれ騎士か悪漢か？問題 1.5
住民 A, B がおり、A は「私たちは同種 (二人とも騎士または二人とも悪漢のいずれか) だ」と言った。
A, B はそれぞれ騎士か悪漢か？
普通に考えて解くこともできますが、この状況を記号で表すことを考えます。
住民 X が騎士であるという命題を 
したがって、問題 1.3 では 
前回作成したライブラリ Blaze を使って、次のように解くことができます。
実行すると、問題 1.3 では A が悪漢、B が騎士と確定します。
問題 1.5 では B が騎士と確定しますが、A は確定できません。
数当てゲーム
さて次に、David Gale「Tracking the Automatic ANT: And Other Mathematical Explorations」という書籍から、
数当てゲームを紹介します。
- プレイヤーは 2 人
- それぞれのプレイヤーに数が割り当てられており、自身の数を知っているが、相手の数は知らない
- 2 人の持つ数は、連続する 2 つの自然数 (つまり、差は 1)
- ターン制で、相手の数を当てれば終了 (わかったら宣言し、わからなければ発声しない)
- 先攻・後攻の区別はなく、いずれが宣言してもよい
どちらのプレイヤーが何ターン目に相手の数を当てることができるか？
自分の数が 9 だとすると、与えられた条件から相手の数は 8 または 10 の 2 通りに絞られます。
ここまではすぐにわかるのですが、いずれかを確定させるには相手の将来の行動あるいは実際の行動の原因を推測する必要があります。
相手がどう考えているかを考える、という日常生活においても重要な能力を問われているようでもあります。
小さい数値でいくつか試してみましょう。
2 人のプレイヤーには対称性がありますが、ここでは大小関係を固定して、プレイヤー A が n、プレイヤー B が n+1 を持つとします。
以下では、各プレイヤーの心理状況を書くことにします。
n=1 の場合、
- A「B=2 しかありえない。」
- B「A=1 または A=3。A=1 ならば、A は 1 ターン目に当てるはず。A=3 ならば、A は 1 ターン目に静観するはず。」
したがって、A が 1 ターン目で当てて終了します。
n=2 の場合、
- A「B=1 または B=3。B=1 ならば、B は 1 ターン目に当てるはず。B=3 ならば、B は 1 ターン目に静観するはず。」
- B「A=2 または A=4。A=2 ならば、A は 2 ターン目に当てるはず (B が 1 ターン目に静観するため)。
A=4 ならば、A は 2 ターン目まで静観するはず。」
したがって、1 ターン目は両方静観し、A が 2 ターン目で当てて終了します。
このように、相手がどのように行動してくるかをあらかじめシミュレートしておけば、実際の行動に応じて相手の数を確定できることになります。
この方針でプログラミングしたものが NumberGuessConsole (GitHub) です (コードが長いため、ここには記載しません)。
このプログラムを A=8, B=9 で実行した結果です。A が 8 ターン目に当てました。
(「X @ n」は X が n ターン目に当てることを表します。)
各プレイヤーの脳内であらかじめシミュレーターを実行することで、値を確定させるための条件を得ます。
A の Knowledge には ((B = 7)≢(B = 9))∧((B = 7)⇒(B @ 7))∧((B = 9)⇒～(B @ 7)) と入っています。
B が 7 ターン目に静観したため、A は B=9 だとわかりました。
結果として、小さいほうの数 n を持つプレイヤーが n ターン目に相手の数 n+1 を当てることになります。
(プログラミングをしなくても、同様の方針により少し複雑な数学的帰納法で証明できます。)
前回: 命題論理を実装する (C#)
作成したライブラリ
Blaze (GitHub)
Blaze (NuGet Gallery)
作成したサンプル
PropositionsConsole (GitHub)
NumberGuessConsole (GitHub)
バージョン情報
.NET Framework 4.5
参照
Raymond Smullyan「記号論理学: 一般化と記号化」
David Gale「Tracking the Automatic ANT: And Other Mathematical Explorations」
