2017 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 | プログラム意味論 / ゲーム意味論 / 交差型システム / generalised species |
|---|
| Outline of Annual Research Achievements |
本研究は関数型プログラミング言語もモデルであるλ計算について「ゲーム意味論と交差型システムの対応関係」を確立し、得られた知見を基に並行計算のモデルであるπ計算の交差型システムを設計した上で検証等へ応用するものであった。
（１）λ計算については、前年の実施状況報告書で報告したように、当初の想定を超えた深い対応関係が明らかとなった。今回得られた結果は、当初想定していたものに比べ、次の２つの点で深い: (i) 当初想定していた対応は proof-irrelevant と呼ばれる種類のものであったが、今回得られたものはさらに強い proof-relevant な対応関係である、(2) 組み合わせ論という別の分野との繋がりをも与える。具体的には、組み合わせ論の概念である Joyal's species を拡張した generalised species というものがあり、これが交差型システムの proof-relevant なものであるが、ゲーム意味論によるλ計算の解釈と generalised species による解釈が一致することを示した。この結果はトップ会議である ACM/IEEE Symposium on Logic in Computer Science 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
λ計算については、当初の計画を超えた結果を得ている。一方でπ計算については、当初の計画は素朴すぎたため困難に突き当たっているものの、困難を乗り越えるために実施したπ計算そのものに対する研究が、非常に興味深い重要な結果を与えた。当初の計画通りの進展ではないものの、予定していた程度かそれ以上の重要な結果を得ている。
|
| Strategy for Future Research Activity |
λ計算と交差型システムの対応関係については非常に興味深い結果を得ている。今後は、理論的な研究を進めると同時に、対応関係の応用も目指す。一方でπ計算については、当初と異なる方向で興味深い結果を得ており、こちらの研究を継続して行う。また当初の目的であったπ計算の交差型システムの設計についても、改めて取り組む。
|
| Causes of Carryover |
π計算に関する研究成果の発表が次年度にずれ込んだため。次年度に発表を行う旅費として使用する。
|
