PPLサマースクール2015
プログラミング言語のゲーム意味論
― 線形近似の視点から ―
日本ソフトウェア科学会 (JSSST) プログラミング論研究会 (PPL) 主催
日本ソフトウェア科学会第32回大会 併設企画
2015年 9月 8日 (日) 10:00 - 13:00
早稲田大学 西早稲田キャンパス
Webページ: http://ppl.jssst.or.jp/?ss2015
講師：塚田武志（東京大学大学院情報理工学系研究科)
 

概要 †

ゲーム意味論とはプログラムや証明の意味論であって、プログラムや証明の振る舞いを分析・理解するための道具としてゲームとその上の戦略を用いるものです。このアプローチは1990年代に始まったもので、現在も精力的に研究されています。

本講演では、最も基本的な結果である、関数型プログラミング言語PCFのゲーム意味論を理解することを目指します。そのための足がかりとして、ゲーム意味論のインタラクティブな側面と線形近似の理論としての側面を紹介します。

ゲーム意味論はインタラクティブな意味論だと言われます。基本的なアイデアは、「プログラム（Proponent）」とそれを呼び出す「環境（Opponent）」の間でどのようなメッセージが交換されるかに注目するというものです。メッセージとしては、例えば、「O→P：返値はなんですか？」「P→O：第一引数の値は何ですか？」「O→P：第一引数の値は true です」などといったものが考えられます。このメッセージのやり取りをゲームに見立てて、そのルールはどうなっているかだとか、プログラムに対応する戦略はどのようなものかを考察するのが、ゲーム意味論です。

他方で、ゲーム意味論は線形近似の理論だと見ることもできます。ここでいう線形とは、線形論理における線形性であって、すなわち各引数をちょうど一度ずつ使うプログラムのことです。一般のプログラムは必ずしも線形ではありませんが、線形プログラムで近似できることが知られています。実は「プログラムの線形近似」と「プログラムと環境とで交換されたメッセージの列」は同じものです。線形近似というアイデアは、ゲーム意味論に新しい表現と視点を与えてくれます。

なお、受講にあたっては、λ計算や型システムについての学部程度の知識を有していることが推奨されます。

↑

講師紹介 †

塚田武志（東京大学）

東京大学大学院情報理工学系研究科 助教。ゲーム意味論や交差型システムと、これらの関数型プログラミング言語の分析・検証への応用に関する研究を行っている。

↑

チュートリアルとの連携について †

PPLサマースクール2015後に， 企画委員会による チュートリアル(計算機科学者のためのゲーム理論入門)) が同会場で予定されております． 今回，両方，申し込めるように時間調整を行っておりますので， PPLサマースクール2015とチュートリアル(定理証明支援系Coq入門)は 合わせて参加をご検討ください．

↑

参加費・参加申し込み †

PPLサマースクールの参加費は以下の通りです．

学生会員1000円, 学生非会員2000円, 一般会員2000円, 一般非会員3000円

参加ご希望の方は， 日本ソフトウェア科学会第32回大会共通の 参加登録ページ(準備中)からお申し込みください． 人数把握のため， また，当日の現金の扱い避けるため， 事前登録をお願いしております．

PPLサマースクールとチュートリアルの 両方への参加を希望される場合はそれぞれについて参加登録をお願いいたします．

↑

問い合わせ先 †

PPLサマースクール2015 幹事
前田 敦司 (つくば大学)
E-mail: maeda [at] cs [dot] tsukuba.ac.jp

↑

過去のサマースクール †