| 研究概要 |
高階書き換えシステムの基礎技術である停止性,合流性,計算戦略についての理論的解析を進めるとともに,プログラムの等価変換法と書き換えシステムによる自動証明法の実験を行い,以下の成果を得た。
1.高階書き換えシステムの停止性を保証する条件として,改良再帰分解順序を解析し,適用可能な条件を明らかにした。
2.型情報を利用した停止性,合流性の判定手法として,永続性にもとづく解析手法を開発した。
3.書き換え規則に重なりがある場合の計算戦略について解析し,効率的な書き換え方法について提案した。
4.複雑なシステムを単純なシステムに分解して解析する新しいモジュラ条件を明らかにした。
5.書き換え規則の適用順序が定められているシステムの操作的意味論を与え,効率的な計算メカニズムの理論的な基礎付けを行なった。
|
