| 研究課題/領域番号 |
16K16004
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
塚田 武志 東京大学, 大学院情報理工学系研究科, 助教 (50758951)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| キーワード | プログラム意味論 / ゲーム意味論 / 交差型システム / generalised species |
|---|
| 研究実績の概要 |
本研究は関数型プログラミング言語もモデルであるλ計算について「ゲーム意味論と交差型システムの対応関係」を確立し、得られた知見を基に並行計算のモデルであるπ計算の交差型システムを設計した上で検証等へ応用するものであった。
（１）λ計算については、前年の実施状況報告書で報告したように、当初の想定を超えた深い対応関係が明らかとなった。今回得られた結果は、当初想定していたものに比べ、次の２つの点で深い: (i) 当初想定していた対応は proof-irrelevant と呼ばれる種類のものであったが、今回得られたものはさらに強い proof-relevant な対応関係である、(2) 組み合わせ論という別の分野との繋がりをも与える。具体的には、組み合わせ論の概念である Joyal's species を拡張した generalised species というものがあり、これが交差型システムの proof-relevant なものであるが、ゲーム意味論によるλ計算の解釈と generalised species による解釈が一致することを示した。この結果はトップ会議である ACM/IEEE Symposium on Logic in Computer Science 2017 に採録された。
（２）π計算については、前年の実施状況報告書で報告したように、交差型システムの設計には技術的な困難があることが明らかとなっていた。本年度は、この技術的困難を調査するためにπ計算そのものに関する研究を行った。具体的には、π計算の論理的な側面（＝カリー・ハワード・ランベック対応）を明らかにし、"論理的に素直な" π計算の断片を得た。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
λ計算については、当初の計画を超えた結果を得ている。一方でπ計算については、当初の計画は素朴すぎたため困難に突き当たっているものの、困難を乗り越えるために実施したπ計算そのものに対する研究が、非常に興味深い重要な結果を与えた。当初の計画通りの進展ではないものの、予定していた程度かそれ以上の重要な結果を得ている。
|
| 今後の研究の推進方策 |
λ計算と交差型システムの対応関係については非常に興味深い結果を得ている。今後は、理論的な研究を進めると同時に、対応関係の応用も目指す。一方でπ計算については、当初と異なる方向で興味深い結果を得ており、こちらの研究を継続して行う。また当初の目的であったπ計算の交差型システムの設計についても、改めて取り組む。
|
| 次年度使用額が生じた理由 |
π計算に関する研究成果の発表が次年度にずれ込んだため。次年度に発表を行う旅費として使用する。
|
