値渡しのゲームの圏における 深さ優先戦略について 産業技術総合研究所 システム検証研究ラボ 松岡聡 ゲーム意味論とは(歴史) • もともとは線型論理の意味論 (Blass, Abramsky & Jagadeesan) • 高階のプログラミング言語についての意味論 (Abramsky一派、Hyland & Ong) 値渡しゲームの圏CBV • 本田と吉田による • Hyland & Ong のポインター・名前渡しゲーム の圏の変種 値渡しゲームの圏の重要性 • C言語は値渡しである • ソフトウェア検証に応用を持つ 1階のプログラムならばプログラムを正確に 意味を保存しつつオートマトンに変換できる • 合成で閉じている(プログラムモジュールごと に検証可能) 例 int succ(int x) { return x+1; } 値渡しゲームの圏における意味 私 私は succに いる 敵 int nを 渡す 私 nをもらって n+1を返す 例2 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 戦略τ(その1) 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 戦略τ(その2) 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 戦略τ(その3) 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 戦略τ(その4) 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(pλ(-)を使った)(その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(pλ(-)を使った)(その2) 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(pλ(-)を使った)(その3) 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(pλ’(-)を使った)(その1) 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(pλ’(-)を使った)(その2) nat nat nat 12 nat nat 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(pλ’(-)を使った)(その3) nat nat 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λ’(-) を使った戦略も、ある種の値渡 しの戦略に対応している
© Copyright 2024 ExpyDoc