2011 Fiscal Year Annual Research Report
| Project/Area Number |
22500023
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
大堀 淳 東北大学, 電気通信研究所, 教授 (60252532)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
上野 雄大 東北大学, 電気通信研究所, 助教 (60551554)
森畑 明昌 東北大学, 電気通信研究所, 助教 (10582257)
|
|---|
| Keywords | コンパイラ / 証明論 / 最適化 / プログラミング言語処理系 |
|---|
| Research Abstract |
平成23年度の研究計画の主なものは以下の3点であった.
(A)コンパイルの各中間言語の操作的意味に正確に対応するカット除去システムの定義
具体的には,昨年度までに得られた成果を,A正規形変換に現れる中間言語に適用し,実際にラムダ計算の操作的意味論を導出可能な証明論の確立を計画した.
(B)各証明変換の再定義及びその正しさの証明
具体的には,前年度に得られた証明変換がカット除去が可能であるとの性質を保存するとの性質を,ラムダ計算にも続く関数型言語のコンパイルに応用し,コンパイル変換が操作的意味論を保存するすることを導く枠組みを構築することを計画した.
(C)アプリケーションに特化したコンパイルのための証明論的拡張
昨年度,基礎的な枠組み構築の研究を遂行中に,この証明論的なコンパイルの枠組みは,種々の応用分野に要求される高度なプログラムの記述システムへの拡張の可能性が見いだされた,この知見を基礎に,命題論理を様相論理に拡張することによる,ゲームプログラミング環境のための証明論的基礎の構築の可能性を探求することを計画した.
(A)に関しては,自然演繹およびシーケント計算のそれぞれのカット除去システムから,ラムダ計算およびA正規形の自然意味論が厳密に導けるとの結果を得た.(B)に関しては,コンパイラのA正規形変換の中でcommutative conversionを含まない前半部分に関して,証明変換のカット除去性の保存性から,コンパイル変換が意味を保存することが帰結するとの結果を得た.
(C)に関しては,様相論理の枠組みがゲームアプリケーションの記述に適しており,ある形をした様相論理式の組合せからゲームシーンの進行シーケンスがほぼ系統的に導ける可能性があるとの知見を得た.
|
| 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等の雑誌への掲載には通常通常年以上を要するものであり,研究自体はほぼ計画通りの進展でと考える.
|
| Strategy for Future Research Activity |
過去2年間で,コンパイルの重要なステップであるA正規形変換に関しては,基礎的な性質の証明を完了しているので,それらをすべてまとめた論文の完成をめざす.また,これまでに得られた成果を,ゲームプログラムの基礎づけなどの本研究に続く次の研究へと発展させる土台の構築を目指す.
|
