はじめに
情報工学の有名な思考実験とかをまとめました
二人の将軍問題
概要
敵城の近くに谷を挟んで二つの軍隊がいる
同時に攻撃しないと敵城を陥落させられないので谷を経由してメッセンジャーを送り攻撃時間を決める
ただし谷には敵兵に捕まるかもしれないので必ずしも手紙が送られるとは限らない(何回か送れば届く可能性はある)
メッセンジャーを無制限に送られるとすると,お互いに攻撃時間を合意することができるか
結論
合意することができない
理由
AからBに攻撃時間の書かれた手紙を送ったとする
Aはたくさんのメッセンジャーを送る
BはAから送った手紙を受け取って合意したことをAからBに手紙を送る
AはBからその手紙を受け取り,その手紙に対する確認の手紙を送る
BはAからその手紙を受け取り,その手紙に対する確認の手紙を送る
・・・以上の無限ループ
確認の手紙が届かなかった場合は送った手紙が届いたのかわからないので
その前の手紙に対する確認をしたことにはならない
その前の手紙に対しても同じことがいえるので帰納法的に考えると不可能
情報工学上の応用
ネットワーク上での通信で双方が合意することが不可能であることを示している
一般にはTCPの3-way-handshakeのように数回で打ち切る
ビザンチン将軍問題
概要
いくつかの軍隊が城を包囲している,攻撃するか撤退するかを合意したい
ただし,軍隊には反逆者がいて不適切な戦略を伝える
この状況で反逆者以外の軍隊全隊が一致して攻撃あるいは撤退にできるか
結論
反逆者が全体の三分の位置にみたなければ可能
理由
4人で反逆者1人の場合不可能であることを証明する
そこから全体の三分の一以上の反逆者がいる場合不可能であるという結論に一般化できる
ここに書くには余白が狭すぎるので細かい証明はこのpdfにお任せします
情報工学上の応用
分散ネットワーク上に故障したプロセスや悪意のあるプロセス(ビザンチン故障と呼ばれる)から
条件付きで合意することができる
食事する哲学者の問題
概要
円卓を哲学者5人で囲み,円卓の上には5つの皿が哲学者の前にありその間に1つずつフォークが置いてある
哲学者は左右2つのフォークを使って食事をして食事が終わるとフォークを置く
この時各哲学者が左のフォークをとって右のフォークを取るといった方法を取ると
右のフォークが置かれるのを待ち続けて飢え死んでしまう
このような哲学者が飢え死にを回避する方法はあるか
結論
ウェイターを配する解法やChandy / Misra の解法などがある
理由
これも全て説明すると長いのでChandy / Misra の解法だけ記述する
フォークには dirty と clean の2つの状態があり,初期状態は dirty
食事したい場合は必要なフォークを要求する
要求されたフォークを持つ哲学者は、持っているフォークが clean なら持ち続け,dirty ならそれを手放す.フォークを要求した側に送る際,それを clean 状態にする。
食事が終わると,フォークは dirty 状態になる.他の哲学者がそのフォークを要求したことがあったら、そのフォークを clean 状態にする
その他の証明などは例のごとくWikipediaにお任せします
ちなみにモニタを使った解法などではフォークを両隣に占有されると飢え死んでしまう
情報工学上の応用
並列処理時にリソース共有がデッドロックに入らないようにする(排他処理)ことができる
停止性問題
概要
プログラムが停止するかがわかるプログラムは存在するか
結論
存在しない
理由
「あるプログラムが停止する時は停止せず,停止しないと停止するプログラム」自身が停止するかを判定する
停止しないなら,停止しないという結論で停止しているので矛盾
停止したら,停止していないことになるので矛盾
情報工学上の応用
コンピュータ(チューリングマシン)では解けない問題がある
プログラムでは無限ループになるかを完全には判定できない