| 研究課題/領域番号 |
15500007
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
酒井 正彦 名古屋大学, 大学院・情報科学研究科, 教授 (50215597)
|
|---|
| 研究分担者 |
坂部 俊樹 名古屋大学, 大学院・情報科学研究科, 教授 (60111829)
草刈 圭一朗 名古屋大学, 大学院・情報科学研究科, 講師 (90323112)
西田 直樹 名古屋大学, 大学院・情報科学研究科, 助手 (00397449)
粕谷 英人 愛知県立大学, 情報科学部, 助手 (10295579)
|
|---|
| 研究期間 (年度) |
2003 – 2005
|
| キーワード | 項書換え系 / 関数型言語 / 正規化戦略 / 停止性証明 / 潜在帰納法 / 最外戦略 |
|---|
| 研究概要 |
本研究の目的は、項書換え系における理論的結果を関数型言語に適用する上で妨げとなっているギャップを取り除くことにある。本研究では、以下の事柄について検討し、成果を得ることができた。
1.依存対法による高階書換え系の停止性証明法では、書き換え系の右辺に変数の入れ子があり、かつ、データのコピーが起こる場合にはこの方法が適用ができない。そこで、対象を若干制限のあるシステムである単純型項書換え系に変更して研究した結果、これまでの強い制限を取り除くことに成功した。
2.高階書換え系において、強逐次近似とNV近似に基づく必須リデックスが決定可能であることを、木オートマトン技術とデブロイ記法を利用して示した。
3.項書換え系の帰納的定理を証明するための潜在帰納法は、高階性を持つ場合に拡張した場合には、その部分クラスに対応することが分かった。このため、帰納的定理であっても潜在帰納法により帰納的定理ではないと答えがでる可能性が生ずる。この問題が起きないための条件を与えた。
4.非直交な重なりを持つ書換え系において最外戦略が完全であるための条件とそれを満たすような書換え系を生成するための等価変換法を示した。
5.構成子項書換え系の逆関数を定義する書換え系の生成法を与えた。また、項書換え系に余剰変数が含まれる場合でも、両辺が線形であれば最内ナローイングによる計算で全ての解が求められることが分かった。
|
