2008 Fiscal Year Annual Research Report
関数型言語の解析・検証・効率的実行のための書換え系理論の研究
| Project/Area Number |
18500011
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
酒井 正彦 Nagoya University, 大学院・情報科学研究科, 教授 (50215597)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
草刈 圭一朗 名古屋大学, 大学院・情報科学研究科, 准教授 (90323112)
西田 直樹 名古屋大学, 大学院・情報科学研究科, 助教 (00397449)
粕谷 英人 愛知県立大学, 情報科学部, 助教 (10295579)
|
|---|
| Keywords | 項書換え系 / 関数型言語 / 停止性 / 合流性 / 単純型書換え系 / 定理自動証明 |
|---|
| Research Abstract |
本研究の目的は、項書換え系においてこれまでに得られている種々の理論的結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。項書換え系と関数型言語のギャップとしては、高階性、優先順序、エラー処理、モジュール機能などが挙げられる。一方、項書換え系での理論的研究としては、停止性、合流性、計算戦略、定理自動証明、E単一化、プログラム変換等が挙げられる。
今年度は以下の成果が得られた。
1. これまでに提案している高階書換え系に対する依存対法による停止性証明法において、(1)証明可能なクラスを拡張し、「関数安全渡し」と名付けた。(2)1階のシステムにおける「利用可能規則」の手法を高階のシステム用に拡張した。
2. 高階書換え系に対して、書換え可能な項(リデックス)の集合を認識する木オートマトンの構成法を示した。これにより、書換え関係の反射的推移的閉包を含む関係を認識する木オートマトンが構成できるようになり、到達可能性を保証するツールの作成が可能になった。
3. 1階の項書換え系における正規化戦略を高階書換え系に拡張した。実際に、(1)与えられた項の書換えるべき箇所を発見する手続き、(2)この戦略が適用可能な書換え系かを判定する手続きを明らかにした。
4. プレスブルーガ文などの具体的に意味が与えられた条件を付加した項書換え系の停止性を示す簡約化順序を与えた。これにより、C風の手続き型言語のプログラムの正しさの証明ツールを強化できる。
5. 線形な左シャロー項書換え系のクラスでは、最内到達可能性と文脈依存到達可能性がいずれも決定可能であることを示した。
6. 依存対の右辺が線形かつシャローである項書換え系に対して、停止性、最内停止性、文脈依存停止性がいずれも決定可能な性質であることを示した。これは、昨年度得られた結果の拡張になっている。
|
