2007 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)
|
|---|
| Keywords | 項書換え系 / 関数型言語 / 停止性 / 合流性 / 単純型書換え系 / 定理自動証明 |
|---|
| Research Abstract |
本研究の目的は、項書換え系においてこれまでに得られている種々の理論的結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。項書換え系と関数型言語のギャップとしては、高階性、優先順序、エラー処理、モジュール機能などが挙げられる。一方、項書換え系での理論的研究としては、停止性、合流性、計算戦略、定理自動証明、E単一化、プログラム変換等が挙げられる。
今年度は以下の成果が得られた。
1.高階の機能を持つ型なし言語へのソフトタイプと呼ばれる軟らかい型システムを導入した。プログラムが型づけ可能であれば、「必ずエラーが起こる」、[エラーが起こる場合がある」、[エラーを起こさない」のいずれかが分かる。プログラムへの型付けアルゴリズムの開発は今後の課題である。
2.依存対法による停止性証明法における引数フィルタによる改良手法は、型つき高階書換え系に適用しようとすると型を破壊してしまうという欠点を改良した。
3.定理自動証明法の完備化手続きに対して、等式に付加された条件がプレスブルーガ文の場合の処理を加え能力の増強を行うと共に、これを利用したC風の手続き型言語のプログラムの正しさの証明実験を行うことにより有効性を確かめた。
4.準構成子項書換え系のクラスでは、最内停止性と文脈依存停止性がいずれも決定可能であることを示した。
5.長さ2の文字列書換え系のクラスでは、停止性と合流性がいずれも決定不能な性質であることを示した。
|
