2011 Fiscal Year Research-status Report
| Project/Area Number |
23650003
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| Project Period (FY) |
2011-04-28 – 2013-03-31
|
| Keywords | プログラム抽出 / コントロールオペレータ / 限定継続 / 型システム / Curry-Howardの対応 / ラムダ計算 / CPS変換 |
|---|
| Research Abstract |
本研究の目的は、階層的な限定継続コントロールオペレータに対応する論理体系を構築し、それに基づいたプログラム抽出法を確立することである。 この目的のため、本年度の研究では、まず、限定継続コントロールオペレータに対応する型システムとそれに対するプログラム変換（CPS変換）について、文献調査および研究を行った。その結果、限定継続コントロールオペレータに対するCPS変換は、二階の存在型を持つ型システムの体系に対するCPS変換と同じ形をしていることがわかり、後者についてさらに研究を深めた結果、二階存在型を持つ型システムにおける型検査問題は決定不能であること等をしめすことができた。これは従来の研究では解かれていなかった未解決問題であり、有意義な成果である。二階存在型はモジュールなどのデータ抽象に利用されるものである。このほか、階層的な限定継続コントロールオペレータに対するCPS変換について考察し、その型の構造についての知見を得た。 これと並行して、プログラム抽出システムについて、現在利用可能なシステムについての文献調査を行うとともに、本研究代表者らによる証明システムの設計の見直しを行った。その結果、本研究で採用するシステムは、本研究代表者らによる既存システムの再設計版とすることになった。関連して、SMTソルバを用いたソフトウェア検証における検証エラーの効率的発見アルゴリズムの設計・実装を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本年度の目的は、現在の技術水準・研究水準を調査し、階層的限定継続コントロールオペレータの論理体系を構築することであり、そのための本質的道具となるCPS変換についての検討を深めた結果、CPS変換を型付けすることができたため、目的はおおむね達成できたと考える。また、本研究の副産物として、未解決問題を１つ解決することができた。
|
| Strategy for Future Research Activity |
来年度は２年計画の２年目であるため、本研究の目的をすべて達成することを目標とする。すなわち、論理体系を構築し、階層的コントロールオペレータを持つプログラムを抽出できるプログラム抽出システムを設計・実装する。このための障害となる課題は現在は見つかっていないが、本手法の有効性を示すための、具体的なプログラム抽出例題を考案する必要があるので、この点に注力していきたい。
|
| Expenditure Plans for the Next FY Research Funding |
本研究では、プログラム抽出システムの作成等のため、プログラミング言語分野における研究実績のある外国人研究員を、平成24年2月から雇用している。平成23年度はその雇用日数が予定より少なくなった関係で若干の繰越額が出たが、平成24年度は、この繰越額を平成24年度予算と合わせて使用することにより、この研究員をさらに２か月程度雇用し、本研究の進展を加速する。また、国内外の他のプログラム抽出システムの実装方式との比較調査、また、本研究の成果発表のため、旅費を使用する。
|
