みなさま，
東京大学の蓮尾です．来週の月曜日，東北大の塚田武志さんをお迎えして ご講演いただきます．ハードコアなゲーム意味論のお話のようです :-)
事前の登録等不要です．ぜひお越しください！
蓮尾 一郎 東京大学 コンピュータ科学専攻 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).