システムの構成

本システムはhaskellを中心に構成し，画像の出力のみGraphvizを用いている．モデル ケースとして第三章に挙げた誕生日のパズルを実装したプログラムを用いて解きながら，

そのシステムについて説明していく．まずはクリプキモデルの設定をプログラム内部で 行う．

• エージェントの集合 A={a, b}

• 可能世界の集合 W ={3/4,3/5,3/8,6/4,6/7,9/1,9/5,12/1,12/2,12/8}

• Aの到達可能性関係 R_a={((x, y),(x^′, y^′))∈W ×W |x=x^′}

• Bの到達可能性関係 R_b ={((x, y),(x^′, y^′))∈W ×W |y=y^′}

• 付値 V(x/y is the C’s birthday) ={(x, y)} このモデルを計算機上で実装すると，図5.1になる．

エージェント，可能世界，到達可能性関係のそれぞれの情報を birthAgent , birthWorld

, birthRelation が持っている．可能世界は対で表現していて，3月4日という可能

世界は(3,4)として表し，到達可能性関係は(エージェント，可能世界，可能世界)の形を

持っていて，2項目の可能世界から3項目の可能世界に対し繋がっている．また一つ一つ の命題に対しての付値が valueP (p) として与えられ，可能世界を要素に持つ集合とし て定義され，そのvalueP (p)を集めた集合を birthValues として与える．このモデル の可変な情報は Frame に格納されており，Frameには可能世界と，到達可能性関係に ついての情報を保持している．いま設定したモデルの情報を取り出すと，実行画面上で図 5.2のように出力される．

この情報を視覚的に捉えるために，graphvizによって画像を出力する．Frameの情報を 用いて表示したい可能世界の情報と到達可能性関係の情報を使って，内部でプログラミン グしたパーサーによりgraphvizで読み込めるtxtファイルを作り，そのtxtファイルを実 行し画像を出力する．設定したFrameの情報を用いてできた画像が図5.4である．

出来上がったモデルの付値，可能世界に対し告知を与えると真かどうかを評価する．例 えば，いま可能世界(12,2)にいるとする．このとき日にちを知っているBは到達可能性 関係により他の可能世界と繋がっていないので，瞬時に日付が分かる．告知を「Cの誕生 日が12月2日だと分かる」とすると，プログラムにより，論理演算を行い真か偽である かを返してくれる．図5.4はその実行画面である．

このようにして valueF 関数を用いて真偽値を評価する．

公開告知による動的変化

動的な変化を実装するにあたり必要なのはその告知の真理集合である．Frameの中にあ るすべての可能世界に対し告知による真偽値を計算し，真になる可能世界だけを集めたも のが真理集合となり，その集合を更新されたモデルの可能世界とする．さらにFrameの 到達可能性関係でいま偽になる可能世界が入っているものを取り除いてできる集合が更新

図 5.1 モデルの設定

図 5.2 Frame

図 5.3 初期状態

図 5.4 告知の真偽値

図 5.5 モデルの更新

されたモデルでの到達可能性関係となる．告知により変化したモデルのFrameには更新 された可能世界の集合と到達可能性関係を持つ．

図5.5は告知の真理集合と真な到達可能性関係，それによって更新されたモデルを作る

関数 modifyFrame について記述したものである．この関数にFrameと告知を入れるこ

とで，新しいモデルのFrameが生成される．

5.1.2 誕生日の謎をシステムを用いての検証

初期状態は図5.4であり，この図から告知によりどのように変化するか検証していく．

まず告知をプログラム上で表現できる形に変換していく．第三章において形式化された告 知を告知演算子[ ]を省いて表記すると，

• 「エージェントz ∈ AはCの誕生日を知っている」

∨

(x,y)∈[cob]K_z(x/y is the C’s birthday)

1. A「BはCの誕生日がわからないはずです」

ann1 =K_a(∧

(x,y)∈[cob]¬K_b(x/y is the C’s birthday)) 2. B「今のAくんの言葉Cの誕生日がわかりました」

ann2 =∨

(x,y)∈[cob]K_b(x/y is the C’s birthday) 3. A「私もCの誕生日がわかりました」

ann3 =∨

(x,y)∈[cob]Ka(x/y is the C’s birthday) になる．

これをプログラム上で表現したものが図5.6になる．

「エージェントz ∈ AはCの誕生日を知っている」は，命題の集合を meidai として 表し，その命題に対して認識演算子を用い，さらに出来上がった論理式の論理和をとるこ とで表現され， kmm1 ， kdd1 のように記述できる．またann1，ann2，ann3はそれ ぞれ announce1 ， announce2 ， announce3 として記述している．

初期状態のモデルに対しann1を与え更新されたモデルが modifyFrame1 になる．さ らに modifyFrame1 に対しann2を行ったものが modifyFrame2 ，そのモデルに対し ann3を行ったのが modifyFrame3 になる．

これらの更新されたモデルを図で表現する．

この出来上がった図5.7，5.8，5.9は第三章において解いていく過程で用いた図と同じ ものとなっており，このシステムは正しく実装できている．このようにして，意味論を実 装し，可能世界や到達可能性関係や付値を持ったクリプキモデルを与え，告知を形式化し その真偽値を計算することにより，動的に計算機によりシミュレートすることができたと いえる．

図 5.6 告知と変化したFrame

図 5.7 modifyFrame1

図 5.8 modifyFrame2

図 5.9 modifyFrame3