| 研究概要 |
項書き換えシステム(TRS)の最も基本的で重要な性質の1つに合流性(Church-Rosser性)があり,これまで多くの研究者の注目を集め盛んに研究されてきた.しかしながら,まだ幾つかの重要な未解決問題が残されており,さらなる研究の発展が望まれていた.そこで,本研究では,まず非線形かつ非停止であるTRSの合流性について考察し,深さ保存性(及び重さ保存性)の概念の導入と新しい証明手法の考案により,合流性を保証する新しい十分条件を明らかにした.この十分条件はTRSの右線形性を必要としないという点で類例のないものであり,またこの証明手法を発展させることにより,すべての種類の拡張重なり性を持つTRSのクラスに適用可能な,合流性を保証する十分条件を初めて得ることにも成功した.さらに,この十分条件を基礎に,すべてのTRSに適用可能な,拡張危険対の(決して失敗することのない)完備化法を初めて提示することに成功した.これらの研究成果は,従来の方法では対応できなかった,非線形非停止TRSのクラスに対する定理の自動証明システムの実現を可能とするものであり,今後の成果が期待される.
本研究では,また左線形TRSの合流性に関する有名な未解決問題についても考察し,書き換え系列に対して強単調性の概念を新たに導入することにより,その解決の突破口を開く研究成果を初めて得ることに成功した.この研究成果をさらに拡張する研究を現在も継続して行っており,全面的解決までにあと一歩のところにいる.
さらに,本研究では,最も基本的で重要な問題の1つである単一化について考察し,その問題が合流性を満たす右定項TRSのクラスという広いクラスにおいて可解であるという,新しい注目すべき結果を得ることに成功した.また,ここで提示した新しい証明手法は今後のさらなる研究の発展に役立つものと期待される.
|
