2016 Fiscal Year Research-status Report
| Project/Area Number |
16K16004
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
塚田 武志 東京大学, 大学院情報理工学系研究科, 助教 (50758951)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | プログラム意味論 / ゲーム意味論 / 交差型システム / 微分λ計算 / π計算 |
|---|
| Outline of Annual Research Achievements |
本研究の目的である「交差型システムとゲーム意味論の関わり」について，以下の成果をあげた．
（１）λ計算における交差型とゲーム意味論の対応関係について，型システムの概念である「型」とゲーム意味論の概念である「プレイ」の間に多対一の対応が存在することを示した．加えて微分λ計算という別の分野との関わりも明らかとなった．この結果は，大雑把に言えば，交差型システム、微分λ計算、そしてゲーム意味論の３つが本質的に同じ対象を記述していることを示しており，例えば微分λ計算の問題を解くのにゲーム意味論の伝統的なアイデアが使えることを示した．この結果はプログラム意味論分野の主要国際会議である ACM/IEEE Symposium on Logic in Computer Science 2016 に採録された．さらに，この結果を発展させ，微分λ計算やゲーム意味論が組み合わせ論的なアイデアと繋がっていることを示した．
（２）並行計算における交差型とゲーム意味論の対応関係について，並行計算のモデルである非同期π計算にゲーム意味論を与え，そこから交差型システムを抽出した．得られた交差型システムは完全であったが，健全性は持たないことを示した．健全性を持たないのは，並行計算に特有うの現象であるデッドロックが原因であることを突き止め，（強い意味で）デッドロックの起きないプログラムについては，型システムが完全かつ健全であることを示した．以上の結果は論文にまとめられ，International Conference on Foundations of Software Science and Computation Structures 2017 に採録が決定している．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
申請書の実施計画の平成２８年度分を課題は，大きく二つに分けられた．
（１）関数型プログラミング言語（またはλ計算）に関する部分については，当初の計画以上に進展していると言える．当初の計画であった「関数型プログラミング言語における交差型とゲーム意味論の対応」については、想定通りの結果を得ることができ、プログラミング言語意味論分野の主要国際会議である国際会議 ACM/IEEE Symposium on Logic in Computer Science 2016 に採録された．さらに当初の想定よりも深い結果が明らかとなり，組み合わせ論との繋がりまで明らかとなった．
（２）並行計算に関する部分については，当初の計画以上に進展した面もあったが、一方で当初の予定よりも困難であると判明した部分もある．当初の計画では，初年度にCCSという比較的簡単な並行計算のモデルについて研究を行い，翌年度以降に難しいが応用的な意義の大きいπ計算の研究に移る予定であった．扱うモデルの複雑さの意味では，現在の進捗は当初の計画を超え，π計算についてゲーム意味論と交差型システムを与えることに成功している（International Conference on Foundations of Software Science and Computation Structures 2017 に採録が決定）．一方で，得られた交差型の性質については，当初の目論見とは異なり，完全性を持つが健全性を持たないことが分かった．ここには本質的な困難があり，どうやって乗り越えるかは翌年度以降の新しい課題として残った．
|
| Strategy for Future Research Activity |
本年度の研究で明らかとなった交差型システムとゲーム意味論の関係については，組み合わせ論や層などの数学的概念との関係が明らかとなってきており，この方向の研究については翌年度意向も精力的に取り組んでいく．並行計算については，当初の予定とは異なり健全性を得ることに本質的な困難があることが明らかとなったため，この困難を乗り越える方策を模索していく．線形論理のアイデアが適用できる可能性があり，まずはその検討を行う．
|
| Causes of Carryover |
当初の予定では簡単な並行計算のモデルから始めて難しいモデル（π計算）の分析に移行する計画だったが，直接π計算のゲーム意味論の構成に成功したため，予定していた書籍が今年度には必要なくなったため．
|
| Expenditure Plan for Carryover Budget |
予定していた書籍の購入を次年度に行う．
|
