| 研究概要 |
高階書き換えシステムの基礎技術であるユニフィケーション,パターンマッチング,停止性,合流性の理論的な解析と実験を行った。具体的には,等号論理のもとでのユニフィケーション・アルゴリズムの効率的な実現法の検討,停止性を保証するための新しい経路順序の提案と解析,複雑なシステムを単純なシステムに分解して解析するためのモジュラ条件の検討,効率的な計算メカニズムを実現するための計算戦略の実験を行った。この結果,合流条件と停止条件に関しては、従来知られていた結集よりも一般的な条件を明らかにすることができた。新たに得られた知見は以下のとおりである。
1.計算結果の一意性を保証するために合流条件を検証する場合,非線形な書き換え規則の取り扱いが困難であった。しかし、非線形オペレータの入れ子の数で式のランクを定めることにより,従来よりも拡張された合流条件を求めることができた。
2.高階書き換えシステムの計算結果の存在保証を行うために,従来知られていた再帰経路順序よりも強力な再帰分解順序による停止条件を明らかにできた。
|
