2014 Fiscal Year Annual Research Report
| Project/Area Number |
25540023
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| Project Period (FY) |
2013-04-01 – 2015-03-31
|
| Keywords | コントロール抽象 / 関数型プログラム言語 / 計算モデル / 型システム / プログラム変換 |
|---|
| Outline of Annual Research Achievements |
本研究は、コントロール抽象を提供する「コントロールオペレータ」を用いた計算体系において、必要呼び、値呼び、名前呼びなど様々な計算戦略に関する未解明の課題について、特に論理学および型理論の観点から探究を行うことを目的とした研究である。より具体的には、「限定継続」をプログラム中から直接操作する機能を提供する「限定継続コントロールオペレータ」に関して、その論理的解釈を与える型システムに基づき、体系の定式化、意味論との関係、システムの作成などを行った。
本年度の研究では、限定継続コントロールオペレータ shift/resetの「返り値型の変化」機能について研究を行った。前年度の研究により、この機能をもつshift/resetを、この機能を持たないshift/resetに帰着する変換を与えていたが、この変換が多くの例で適用可能なことまでしか示せていなかった。本年度の研究では、本研究の変換が適用可能か範囲を定式化し、その範囲のすべてのプログラムが正しく変換できることを厳密に証明した。この目的のため、shift/resetに対する基本的な型システムであるDanvy-Filinskiの型システム、および、その拡張であるAsai-Kameyamaの型システムを取り上げ、拡張された体系で型付け可能であれば、本研究の変換で、型付けを保存して変換されることを厳密に証明した。この成果は、限定継続コントロールオペレータをもつ体系に関する理論的成果を、ＭＬなどの標準的関数型プログラム言語において、そのまま活用することが可能となる、という意義を持つものである。上記の研究成果を査読付き国際会議に投稿して採録され、発表を行った。
本研究は今年度が最終年度であるため、まとめとなる活動を行い、研究成果と、本研究の過程で新たに見つかった研究課題について整理した。
|
