| Research Abstract |
項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,関数型プログラムの効率の良い実行,プログラムの仕様と実現の正当性検証など非常に重要な問題を包含していることから,これまで多くの研究者の注目を集め,盛んに研究されてきた.しかしながら,まだ多くの重要な未解決問題が残されており,さらなる研究の発展が望まれている.そこで本研究では,平成8年度よりTRSの最も基本的で重要な性質の1つである合流性(Church-Rosser性)について研究を行い,合流性に関する未解決問題に対して,新しい概念とアイデアを導入することによって,その本質に迫る研究成果を得ることに成功すると共に,定理の自動証明などに必要不可欠な危険対(及び拡張危険対)の完備化法について研究を行い,従来提案されていた方法よりも広範囲の問題解決に利用可能な新しい完備化法を明らかにすることに成功した.
特に,本年度の研究成果としては,非線形非停止TRSの合流性を保証する十分条件として,すべての種類の拡張重なり性に対応可能な十分条件を初めて見つけることに成功すると共に,この十分条件を用いてすべてのTRSに適用可能な,拡張危険対の(決して失敗することのない)完備化法を初めて提示するのに成功したことである.これらの研究成果は,従来の方法では対応できなかった,非線形非停止TRSのクラスに対する定理の自動証明システムの実現を可能とするものであり,今後の成果が期待される.
さらに,本年度の研究では,合流性と並んで最も基本的で重要なTRSの性質である単一化(unification)について考察し,その問題が合流性をみたす右定項TRSのクラスにおいて可解であるという,新しい注目すべき結果を得ることに成功した.この研究成果は停止性をみたさないTRSの広いクラスに対して,単一化問題の可解性を初めて明らかにした点に特色があり,今後さらなる研究の発展が期待される.
以上のことより,本年度の研究計画の所期の目的を達成することができた.なお,本年度は本研究課題の最終年度に当り,これらの研究成果をまとめ,報告書を作成した.
|
