| 研究概要 |
高階書き換えシステムの基礎技術である停止性,合流性,計算戦略についての理論的解析を進めるとともに,プログラムの等価変換法と書き換えシステムによる自動証明法の実験を行ない,以下の成果を得た。
1。高階書き換えシステムの停止性を保証する条件として,改良再帰分解順序を解析し,適用可能な条件を明らかにした。これは従来の停止条件の拡張となっている。
2。型情報を利用した停止性,合流性の判定手法として永続性にもとづく解析手法を開発した。この手法はモジュラ解析が困難なシステムにも適用可能である。
3。書き換え規則に重なりがある場合の計算機戦略について解析し,効率的な書き換え方法について提案した。また,この方法が決定可能であることを明らかにした。
4。プログラムの新しい等価変換手法を提案し,計算機上で変換システムの実験を行い,その有効性を確認した。
5。書き換え手法にもとづく帰納的定理証明法として,書き換え帰納法の解析を行うとともに,潜在帰納法との比較評価を行った。
6。依存対を利用した停止性の証明手法の実装を行い,実験を通して有効性を確認した。また、結合律・可換律を含むシステムの停止性の証明も可能となるように拡張を行った。
|
