Document

値渡しのゲームの圏における
深さ優先戦略について
産業技術総合研究所
システム検証研究ラボ
松岡聡
ゲーム意味論とは(歴史）
• もともとは線型論理の意味論
(Blass, Abramsky & Jagadeesan)
• 高階のプログラミング言語についての意味論
(Abramsky一派、Hyland & Ong)
値渡しゲームの圏CBV
• 本田と吉田による
• Hyland & Ong のポインター・名前渡しゲーム
の圏の変種
値渡しゲームの圏の重要性
• C言語は値渡しである
• ソフトウェア検証に応用を持つ
１階のプログラムならばプログラムを正確に
意味を保存しつつオートマトンに変換できる
• 合成で閉じている(プログラムモジュールごと
に検証可能）
例
int succ(int x) {
return x+1;
}
値渡しゲームの圏における意味
私
私は
succに
いる
敵
int nを
渡す
私
nをもらって
n+1を返す
例２
int foo (int bar(int)) {
return succ(bar(5));
}
値渡しゲームの圏における意味
私
敵
foo
にい
る
bar
に
いる
私
敵
5を bar(5)
敵に
渡すを返す
私
succ(bar(5))
を返す
アリーナ（ゲーム盤）
例
nat= ω
nat
nat->nat =
nat
nat=>nat
ここでnat=>natはsingleton {*}
アリーナ(ゲーム盤）
nat
nat
nat
nat
nat
nat
nat=>nat
nat
nat
nat
nat
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat=>nat
nat=>nat
(nat=>nat)=>nat
nat=>nat
(nat=>nat)=>nat=>nat
nat
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat
nat
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat
(((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat)=>nat
ポラリティ
nat
nat
nat
nat
nat
nat
nat=>nat
nat
nat
nat
nat
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat=>nat
nat=>nat
(nat=>nat)=>nat
nat=>nat
(nat=>nat)=>nat=>nat
nat
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat
nat
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat
(((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat)=>nat
例
プルーフネット
nat
nat
nat
nat
nat
nat
nat=>nat
nat
nat
nat
nat
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat=>nat
nat=>nat
(nat=>nat)=>nat
nat=>nat
(nat=>nat)=>nat=>nat
nat
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat
nat
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat
(((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat)=>nat
戦略τ（その１）
nat 12
nat 10nat 11
nat 9
nat
nat 13
nat 8
nat
nat
nat=>nat 7 nat
nat=>nat 6
nat
nat=>nat
(nat=>nat)=>nat
nat=>nat
(nat=>nat)=>nat=>nat 5
nat=>nat 4
(nat=>nat)=>(nat=>nat)=>nat
nat
(nat=>nat)=>(nat=>nat)=>nat=>nat 3
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat 2
(((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat)=>nat 1
戦略τ（その２）
nat
nat
nat
nat
nat
nat=>nat
nat
nat=>nat
(nat=>nat)=>nat=>nat
nat
nat
nat
nat 17
nat=>nat
nat 16
(nat=>nat)=>nat
nat=>nat 15
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat 14
nat
(nat=>nat)=>(nat=>nat)=>nat=>nat 3
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat 2
(((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat)=>nat 1
戦略τ（その３）
nat
nat
nat
nat
nat
nat=>nat
nat
nat 21
nat 20
nat
nat
nat
nat=>nat 19
(nat=>nat)=>nat 18
nat=>nat
(nat=>nat)=>nat=>nat
nat=>nat 15
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat 14
nat
(nat=>nat)=>(nat=>nat)=>nat=>nat 3
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat 2
(((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat)=>nat 1
戦略τ（その４）
nat
nat
nat
nat
nat
nat
nat=>nat
nat
nat
nat
nat
nat 22
nat=>nat 19
(nat=>nat)=>nat 18
nat=>nat
(nat=>nat)=>nat=>nat
nat=>nat 15
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat 14
nat 23
(nat=>nat)=>(nat=>nat)=>nat=>nat 3
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat 2
(((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat)=>nat 1
別のアリーナ（ゲーム盤）
例
nat
nat nat
nat
nat
nat=>nat
nat
nat
nat
nat=>nat
nat
nat
(nat=>nat)=>nat=>nat
nat=>nat
nat
(nat=>nat)=>nat
nat=>nat
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat
(nat=>nat)=>(nat=>nat)=>nat=>nat
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat
ポラリティ
例
nat
nat nat
nat
nat
nat=>nat
nat
nat
nat
nat=>nat
nat
nat
(nat=>nat)=>nat=>nat
nat=>nat
nat
(nat=>nat)=>nat
nat=>nat
nat=>nat
(nat=>nat)=>(nat=>nat)=>nat
(nat=>nat)=>(nat=>nat)=>nat=>nat
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat
プルーフ・ネット
例
nat
nat
3
nat
nat
nat
nat->nat
nat
nat
nat
nat->nat
nat
nat
(nat->nat)->nat->nat
nat=>nat
nat
(nat=>nat)=>nat
nat=>nat
nat->nat
(nat->nat)->(nat->nat)->nat
(nat->nat)->(nat->nat)->nat->nat
((nat->nat)->(nat->nat)->nat->nat)->(nat->nat)->(nat->nat)->nat
戦略σ1（ｐλ(-)を使った）（その１）
nat
nat 10
nat 9
nat nat
nat
nat
nat=>nat
nat=>nat
(nat=>nat)=>nat=>nat
nat
nat
nat=>nat 19
nat 17
nat 16
(nat=>nat)=>nat 18
nat=>nat 15
nat=>nat 4
(nat=>nat)=>(nat=>nat)=>nat 14
(nat=>nat)=>(nat=>nat)=>nat=>nat 3
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat 2
戦略σ1（ｐλ(-)を使った）（その２）
nat
nat
nat 12 nat
nat 11
nat=>nat
nat
nat=>nat 6
nat 20
nat
nat 21
nat=>nat 19
nat
nat
(nat=>nat)=>nat 18
(nat=>nat)=>nat=>nat 5
nat=>nat 15
nat=>nat 4
(nat=>nat)=>(nat=>nat)=>nat 14
(nat=>nat)=>(nat=>nat)=>nat=>nat 3
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat 2
戦略σ1（ｐλ(-)を使った）（その３）
nat
nat
nat
nat
nat 8
nat 13
nat=>nat 7
nat=>nat 6
nat
nat
nat
nat 22
nat=>nat 19
nat
(nat=>nat)=>nat 18
(nat=>nat)=>nat=>nat 5
nat=>nat 15
nat=>nat 4
(nat=>nat)=>(nat=>nat)=>nat 14
(nat=>nat)=>(nat=>nat)=>nat=>nat 3
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat 2
戦略σ2（ｐλ’(-)を使った）（その１）
nat
nat 10
nat 9
nat nat
nat
nat
nat=>nat
nat=>nat
(nat=>nat)=>nat=>nat
nat
nat
nat=>nat
nat 17
nat 16
(nat=>nat)=>nat
nat=>nat 15
nat=>nat 4
(nat=>nat)=>(nat=>nat)=>nat 14
(nat=>nat)=>(nat=>nat)=>nat=>nat 3
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat 2
戦略σ2（ｐλ’(-)を使った）（その２）
nat
nat
nat 12 nat
ｎat 11
nat=>nat
nat
nat=>nat 6
nat 20
nat
nat
(nat=>nat)=>nat=>nat 5
nat 21
nat=>nat 19
nat
(nat=>nat)=>nat 18
nat=>nat 15
nat=>nat 4
(nat=>nat)=>(nat=>nat)=>nat 14
(nat=>nat)=>(nat=>nat)=>nat=>nat 3
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat 2
戦略σ2（ｐλ’(-)を使った）（その３）
nat
ｎat
nat
nat
nat 8
nat 13
nat
nat=>nat 7
nat=>nat 6
nat
nat
(nat=>nat)=>nat=>nat 5
nat
nat 22
nat=>nat 19
(nat=>nat)=>nat 18
nat=>nat 15
nat=>nat 4
(nat=>nat)=>(nat=>nat)=>nat 14
(nat=>nat)=>(nat=>nat)=>nat=>nat 3
((nat=>nat)=>(nat=>nat)=>nat=>nat)=>(nat=>nat)=>(nat=>nat)=>nat 2
ゲームのプレー
σ1とτによるプレー
1 2 3 1 1 1 1 4 5 6 7 8 9 1 1 1 1 2 2 1 1 2 2
4 5 8 9
6 7 0 1 0 1 2 3 2 3
σ2とτによるプレー
1 2 3 1 1 4 5 1 1 6 7 8 9 1 1 1 1 2 2 1 1 2 2
4 5
8 9
6 7 0 1 0 1 2 3 2 3
いままでわかったこと
• pλ(-)を使った戦略は通常の値渡しの戦略で
あるが、pλ’(-) を使った戦略も、ある種の値渡
しの戦略に対応している

Download Report