| 研究概要 |
項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,関数型プログラムの効率の良い実行,プログラムの仕様と実現の正当性検証など非常に重要な問題を包含していることから,これまで多くの研究者の注目を集め,盛んに研究されてきた.しかしながら,まだ多くの重要な未解決問題が残されており,さらなる研究の発展が望まれている.そこで本研究では,TRSの最も基本的で重要な性質の1つである合流性(Church-Rosser性)について研究を行い,合流性に関する未解決問題に対して,新しい概念とアイデアを導入することによって,解決の突破口を開き,その本質に迫る研究成果を得ることに成功した.
すなわち,まず非線形TRSの合流性に関する研究を行い,TRSの右線形牲を必要としない,合流性を保証する判定可能な十分条件を初めて明らかにした.この条件は非強重なり性と強い深さ保存性の条件を満たすTRSの合流性を保証するものであり,また,この深さ保存牲を拡張した重さ保存性の概念を導入することにより,この十分条件を拡張すると共に,強重なり性を満たす場合についても合流性を保証する判定可能な十分条件を明らかにした.本研究では,次に,左線形TRSの合流性問題に対しても見直しを行い,長い間,未解決であった(inverse para11el closed条件)問題に対して,その解決の突破口を開く研究成果を初めて得ることに成功した.さらに,本研究では,これらの研究成果に基づく,停止性を前提としない新しい完備化法について考察し,その基礎となるいくつかの研究成果を得た.
|
