| 研究課題/領域番号 |
18500011
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
酒井 正彦 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
|
|---|
| 研究分担者 |
坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
草刈 圭一朗 名古屋大学, 大学院・情報科学研究科, 准教授 (90323112)
西田 直樹 名古屋大学, 大学院・情報科学研究科, 助教 (00397449)
粕谷 英人 愛知県立大学, 情報科学部, 講師 (10295579)
|
|---|
| キーワード | 項書換え系 / 関数型言語 / 停止性 / 合流性 / 単純型書換え系 / 定理自動証明 |
|---|
| 研究概要 |
本研究の目的は、項書換え系においてこれまでに得られている種々の理論的結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。項書換え系と関数型言語のギャップとしては、高階性、優先順序、エラー処理、モジュール機能などが挙げられる。一方、項書換え系での理論的研究としては、停止性、合流性、計算戦略、定理自動証明、E単一化、プログラム変換等が挙げられる。
今年度は以下の成果が得られた。
1.SMLに代表される関数型言語における例外処理を持つプログラムの停止性を示すための、文脈依存項書換え系への一変換法を示し、いくつかの例題プログラムに対して停止性証明の実験を行った。
2.前年度から研究を続けていた高階項書換え系の静的依存対法の基本理論を論文にまとめ、また、1階の系で有効な引数切り落とし法と実行規則の手法を高階に拡張を試みある程度の結果が得られた。
3.項書換え系の枠組における逆プログラムの利用により、与えられた単射関数を計算するプログラムからその逆関数を計算するプログラムの合成を行う際に、完備化技術が有効であることを示した。
4.線形な右シャロー項書換え系のクラスでは、文脈依存かつ最内な書換えによる到達可能性が決定可能な性質であることを示した。
5.前年度に得られた結果である、文脈依存停止性が決定可能なクラス「依存対の右辺が線形かつシャローでな項書換え系」のクラスの拡張を行った。
|
