| 研究課題/領域番号 |
18500011
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
酒井 正彦 名古屋大学, 大学院情報科学研究科, 教授 (50215597)
|
|---|
| 研究分担者 |
坂部 俊樹 名古屋大学, 大学院情報科学研究科, 教授 (60111829)
草刈 圭一朗 名古屋大学, 大学院情報科学研究科, 助教授 (90323112)
西田 直樹 名古屋大学, 大学院情報科学研究科, 助手 (00397449)
粕谷 英人 愛知県立大学, 情報科学部, 助手 (10295579)
|
|---|
| キーワード | 項書換え系 / 関数型言語 / 停止性証明 / 単純型書換え系 / 滞在帰納法 |
|---|
| 研究概要 |
本研究の目的は、項書換え系においてこれまでに得られている種々の理論的結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。項書換え系と関数型言語のギャップとしては、高階性、優先順序、エラー処理、モジュール機能などが挙げられる。一方、項書換え系での理論的研究としては、停止性、合流性、計算戦略、定理自動証明、E単一化、プログラム変換等が挙げられる。
今年度は以下の成果が得られた。
1.依存対法による停止性証明において、実行規則の概念を高階に拡張した。また、直積型は高階関数と共に用いられると停止性証明が難しくなるため、直積項へのラベル付け方を提案した。
2.潜在帰納法により高階性を持つ単純型項書換え系の定理自動証明系を試作した。帰納的定理の自動証明を実用に近づけるためのリップリングと呼ばれる補題探索手法が高階の場合にでも利用できることを示し、それを実装・実験した。
3.等式集合Eを法とする書換えにおいて、解を求めるE単一化を実現するため、E中の扱いづらい等式を書換え規則に置き換えるためには、危険対の概念に基づいて新たに得られる規則も同時に追加すれば良いことが分かった。
4.停止性が決定可能となる、項書換え系の部分クラスを示した。また、繰り返し構造を持たない無限書換え系列のある部分クラスを定義し、そのいくつかの例を示した。
|
