| 研究課題/領域番号 |
11680352
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
酒井 正彦 名古屋大学, 工学研究科, 教授 (50215597)
|
|---|
| 研究分担者 |
粕谷 英人 愛知県立大学, 情報科学部, 助手 (10295579)
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
坂部 俊樹 名古屋大学, 工学研究科, 教授 (60111829)
|
|---|
| 研究期間 (年度) |
1999 – 2002
|
| キーワード | 項書換え系 / 正規化戦略 / 関数型言語 |
|---|
| 研究概要 |
本研究の目的は、項書換え系における計算戦略の結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。そこで、平成11年度から平成14年度の4年間にわたって、以下の事柄について検討し、いくつかの成果を得ることができた。
1.これまでにNV書き換え系のクラスは決定可能であることが知られているが、計算量が大きいため実現されていなかった。実験の結果、現在の技術では数行の書き換え系についてのみNVクラスに属しているかの判定が可能であることが判明した。また、次に計算すべき場所を示すインデックスを求める問題についても、クラス判定とほぼ同レベルの実行時間、記憶領域が必要であることが分かった。
2.強逐次的な優先順序付き書換え系について、頭正規形を得るためのインデックスを効率良く求めるシステムを試作・評価した。解が無限の大きさになるために正規形が存在しないが解の内で確定した部分を表す頭正規形が存在する場合にこれを求めるために、項書換え系の根インデックスの概念を優先順序つき書換え系へ拡張した。
3.高階関数が扱える高階書換え系において、必須リデックスの計算により、頭正規形を(存在すれば)求められることを示した。これにより、必須リデックスを計算する戦略が正規化戦略であることが判明した。
4.依存対に基づく手法に用いて、与えられた高階書換え系が停止性をもつことを示す条件について研究した。高階の場合には、注意すべき場所が規則からは予想が難しいため、これらを行うことが可能な書換え系のクラスを明らかにした。
5.複数存在する解を全て求めるためには一般には全解探索が必要であり、たとえ停止性をもつ計算システムでも、求解のコストは大きい。停止性を持つ項書換え系が、右線形かつ根重なりの性質を満たす場合に、全ての求解の効率化できることを示した。これは、探索空間の枝刈りが可能であることを意味する
|
