2005 Fiscal Year Annual Research Report
関数型言語の解析・検証・効率的実行のための書換え系理論の研究
| Project/Area Number |
15500007
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
酒井 正彦 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
草刈 圭一朗 名古屋大学, 大学院情報科学研究科, 講師 (90323112)
西田 直樹 名古屋大学, 大学院・情報科学研究科, 助手 (00397449)
粕谷 英人 愛知県立大学, 情報科学部, 助手 (10295579)
|
|---|
| Keywords | 項書換え系 / 関数型言語 / 停止性証明 |
|---|
| Research Abstract |
本研究の目的は、項書換え系においてこれまでに得られている種々の理論的結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。項書換え系と関数型言語のギャップとしては、高階性、優先順序、エラー処理、モジュール機能などが挙げられる。一方、項書換え系での理論的研究としては、停止性、合流性、計算戦略、定理自動証明、E単一化、プログラム変換等が挙げられる。
今年度は以下の研究を行った。
1.依存対法による停止性証明の高階への拡張について、初年度の結果では右辺に変数の入れ子がないか、データが複製されないという強い制限を取り除くことに成功した。現在結果を国際論文誌に投稿中である。
2.項書換え系の帰納的定理を証明するための潜在帰納法は、高階性を持つ場合に拡張した場合には、その部分クラスに対応することが分かった。このため、帰納的定理であっても潜在帰納法により帰納的定理ではないと答えがでる可能性が生ずる。この問題が起きないための条件を与えた。
3.依存対法による停止性証明と潜在帰納法の優先順序付き書換え系への拡張は、いずれも、ほぼ自明と思われる条件しか明らかにならず、さらに研究を進める必要がある。
4.非直交な重なりを持つ書換え系において最外戦略が完全であるための条件とそれを満たすような書換え系を生成するための等価変換法を示した。これは、正規化戦略はこれまで最外戦略の特殊な戦略であることから、この研究をさらに進める必要がある。
|
