2004 Fiscal Year Annual Research Report
関数型言語の解析・検証・効率的実行のための書換え系理論の研究
| Project/Area Number |
15500007
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
酒井 正彦 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
草刈 圭一朗 名古屋大学, 大学院・情報科学研究科, 講師 (90323112)
西田 直樹 名古屋大学, 大学院・情報科学研究科, 助手
粕谷 英人 愛知県立大学, 情報科学部, 助手 (10295579)
|
|---|
| Keywords | 項書換え系 / 関数型言語 |
|---|
| Research Abstract |
本研究の目的は、項書換え系においてこれまでに得られている種々の理論的結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。項書換え系と関数型言語のギャップとしては、高階性、優先順序、エラー処理、モジュール機能などが挙げられる。一方、項書換え系での理論的研究としては、停止性、合流性、計算戦略、定理自動証明、E単一化、プログラム変換等が挙げられる。
今年度は以下の研究を行った。
1.初年度にほぼ結果を導いていた、依存対法による停止性証明の高階への拡張について論文にまとめた。その結果、書き換え系の右辺に変数の入れ子があり、かつ、データのコピーが起こる場合にはこの方法が適用ができず、さらに研究が必要であることが分かった。
2.初年度に引続き、高階関数が扱える高階書換え系において、頭正規形を得るための必須リデックスを計算する機構について研究した。強逐次近似とNV近似に基づく必須リデックスが、木オートマトン技術とデブロイ記法を用いて決定可能であることが分かった。
3.項書換え系に余剰変数が含まれる場合でも、両辺が線形であれば最内ナローイングによる計算で全ての解が求められることが分かった。これにより、全解探索計算の効率化が可能になる。
4.関数型言語におけるcase文の機能は、条件つき項書換え系のうち決定的なクラスによりモデル化される。このクラスの条件つき項書き換え系を、紐解き変換により項書換え系に変換したときに等価となる二つの条件を明らかにした。(1)生成された書き換え系が右線形かつ変数非消去。(2)生成された書き換え系が左線形
|
