| 研究概要 |
書き換え理論において近年注目されている自動証明向き停止性判定法として,依存対法という手法が知られている。この停止性証明法は,十分広いクラスの書き換え系に対して,効率的で強力な自動判定のできる手法であるが,高階関数のあるプログラムには使えない,という問題点があった。
高階関数とは,データとして関数を受け渡しできる関数であり,プログラムの汎用性を高めるための,関数型言語の本質的な機能の1つである。そこで、より広範囲のプログラムに対して,書き換えによる停止性自動証明法が使えるよう,高階性を考慮して依存対法の理論を拡張し,その成果を,書き換えに関する国際会議であるRTA2005で発表した。具体的には,まず,高階関数が許される場合の極小な無限書き換え系列の基本性質を詳細に解析し,依存対の定義を高階性を考慮したものに拡張した。これにより,関数型の項が許される場合に,プログラムの停止性判定問題が関数定義間の依存関係を考慮した順序制約の解消問題に変換できるようになった。
停止性に関連する項書き換えの基礎理論についても考察を深めた。まず,木準同型写像による書き換え系の変換によって,停止性を保証する手法を新たに提示した。また,自動証明向きの停止性証明法の基礎付けを与える木の埋め込み定理を,型付き項へ適用できるように拡張した。
さらに,書き換えによる到達可能性の決定可能性と決定不能性の問題についても,従来研究が十分でなかった準構成子項書き換え系のクラスに対する新たな結果を得た。この研究結果は,停止性だけでなく,単一化問題などへの適用が期待できる。到達可能性に関する研究成果は,学術誌Information Processing Lettersに公表予定である。
|
