2004 Fiscal Year Annual Research Report
| Project/Area Number |
16500004
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, 大学院・システム情報工学研究科, 助教授 (10195000)
|
|---|
| Keywords | メタ・プログラム / オブジェクト・プログラム / 高階抽象構文 / 定理証明 |
|---|
| Research Abstract |
本年度は、まず、メタ・プログラムの実例を調査した。部分計算、コンパイラで用いられるCPS変換等のプログラム変換などを対象として、メタ・プログラムとオブジェクト・プログラムがどのような言語で記述され、その信頼性の保証には、どのような仕組みが必要であるか、また、実際に定理証明システムを用いて、これらのメタ・プログラムの検証を行うにはどうしたらよいか、等を実例に基づいて検討した。その結果、変数の表現をどうするかの選択が定理証明のしやすさに大きな影響を及ぼすことが判明した。特に、高階抽象構文に基づく表現では、定理証明の段階で困難が生じることが判明した。この困難の解消のため、通常は、高階抽象構文の採用をあきらめることが多いが、数学的にエレガントで人間にもわかりやすい高階抽象構文を基礎と置いたメタ・プログラムの定式化を行うことができれば、非常に有益な成果であるという観測のもと、本研究では、これを採用することとした。定理証明における問題点を克服するため、次年度は、実際にtwelfやCoqなどの定理証明システムを用いた検証例を作成することとした。
次に、効率的なプログラム変換などで使われる技法を表現するため、コントロールオペレータを導入したメタ・プログラミングについて考察した。従来から、shift/resetを用いた言語に対する検証規則の研究を行ってきたが、本年度は、その結果を拡張し、任意の個数のshift/resetを混在したプログラムに対しても、完全な推論ができる等式系を特定し、そのことに対する型理論的証明を与えることに成功した。
|
