[logic-ml] Talk by Takeshi Tsukada (Tohoku U.), Monday Next Week

[Ichiro Hasuo]

みなさま，

東京大学の蓮尾です．来週の月曜日，東北大の塚田武志さんをお迎えして
ご講演いただきます．ハードコアなゲーム意味論のお話のようです :-)

事前の登録等不要です．ぜひお越しください！

蓮尾 一郎
東京大学 コンピュータ科学専攻
http://www-mmm.is.s.u-tokyo.ac.jp/

========================================================
Mon 11 June 2012, 16:40-18:10
Takeshi Tsukada (Tohoku U, http://www.kb.ecei.tohoku.ac.jp/~tsukada/)
２レベルゲーム意味論による共通型の解釈
場所： 東京大学 本郷キャンパス 理学部7号館1階 102教室
（アクセス： http://www-mmm.is.s.u-tokyo.ac.jp/ の一番下を見てください）

本発表では２レベルゲーム意味論という新しいゲーム意味論を導入し、
これを用いることで共通型システムのゲーム的解釈が与えられることを示
す。ゲーム意味論と共通型理論は近年の高階モデル検査（＝高階再帰スキー
ムという文法が生成する木のモデル検査）の理論において重要な役割を果
たしており、これらの間の関係を明らかにすることは高階モデル検査の理
論の進展のための重要な課題であると認識されてきた。これまでも直感的
な対応関係は知られていたが、形式的な対応関係は本発表で導入する２レ
ベルゲーム意味論によるものがはじめてである。

 ２レベルゲームは、その名が示す通り、上層のゲームと下層のゲームの
２つ（とそれらの間の関係）から成る。下層のゲームは項の計算を表し、
上層のゲームは項の性質の証明を表す。このふたつのゲームは密接に関係
しており、その関係は上層のゲームから下層のゲームへの写像として表現
される。

本発表では、２レベルゲームに関する次の結果について述べる。
 (A) （単純型システムの詳細化であるような）共通型システムにおける
   型導出は２レベルゲームの勝利戦略として解釈することができる。
   さらに、２レベルゲーム意味論は共通型システムに対して fully
   complete である。つまり、すべての（２レベルゲームにおける）
   勝利戦略はある（共通型システムの）型導出の解釈となっている。
 (B) 共通型システムの重要な性質に主拡張補題というものがある。これ
   に対応する性質を、２レベルゲームも満たすことを示す。この証明
   は純粋にゲーム意味論的手法で行うことができる。

 また最後に、２レベルゲーム意味論の高階モデル検査への応用と今後の
展開についてに述べる。

参考文献：
[1] C.-H. Luke Ong and Tsukada Takeshi.  Two-Level Game
Semantics, Intersection Types, and Recursion Schemes.  ICALP
2012 (to appear).