| 研究課題/領域番号 |
11680352
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
酒井 正彦 名古屋大学, 大学院・工学系研究科, 助教授 (50215597)
|
|---|
| 研究分担者 |
粕谷 英人 愛知県立大学, 情報科学部, 助手 (10295579)
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
坂部 俊樹 名古屋大学, 大学院・工学系研究科, 教授 (60111829)
|
|---|
| キーワード | 項書換え系 / 正規化戦略 / 関数型言語 |
|---|
| 研究概要 |
本研究の目的は、項書換え系における計算戦略の結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。そのため、規則間に優先順序がついた項書換え系、高階関数、モジュールを持つ項書換え系の上での計算戦略を解析・明らかにすることが必要である。
本年度は、昨年度に引続き以下を行った。
1.高階関数が扱える高階書換え系において、頭正規形を得るための必須リデックスを計算する機構について研究した。このための技術として、強逐次近似とNV近似の概念を高階に拡張した。また、Δ-木オートマトンとそれに基づくGTTにより、デブロイ記法の高階項が正規形であること、ならびに、項の到達可能性が決定可能であることの証明のための大まかな道筋を与えることができた。
2.与えられた高階書換え系が停止性をもつことを示す有効な条件について研究した。停止性を持つことが分かれば、いかなる戦略で計算を行っても解が求められるので、これは重要である。具体的な手法としては、項書換え系の依存対に基づく手法を高階の場合に拡張した。この手法は無限計算列を引き起こす引き起こす可能性のある場所に注目して停止性の証明のしやすいシステムに変換する方法である。しかしながら、高階の場合には、注意すべき場所が規則からは予想が難しいため、これらを行うことが可能な書換え系のクラスを明らかにした。
3.以上の研究の他、逆計算を行うプログラムへの変換を与え、それによる逆計算の戦略の研究にも着手した。
|
