| 研究概要 |
項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,関数型プログラムの効率良い実行,プログラムの仕様と実現の正当性検証など非常に重要な問題を包含していることから,これまで多くの研究者の注目を集め,盛んに研究されてきた.しかしながら,まだ多くの重要な未解決問題が残されており,さらなる研究の発展が望まれている.そこで本研究では,前年度よりTRSの最も基本的で重要な性質の1つである合流性(Church-Rosser性)について研究を行い,合流性に関する未解決問題に対して,新しい概念とアイデアを導入することによって,その本質に迫る研究成果を得ることに成功すると共に,定理の自動証明などに必要不可欠な危険対の完備化法について研究を行い,従来提案されていた方法よりも広範囲の問題解決に利用可能な(TRSの停止性を前提としない)新しい完備化法を明らかにすることに成功した.
特に,本年度の研究成果としては新しい完備化法を提示したことであり,この方法は(前年度に研究を行った)強い深さ保存性を満たすTRSのクラスが十分広いクラスを包含していることに着目して,その合流性を保証する(前年度に導いた)条件が一般の等式論理の完備化手続きに十分利用できることを明らかにすることにより,得られたものである.また,前年度に引き続き,左線形TRSに対する長い間未解決であった(inverse parallel closed 条件)問題についても研究を行い,前年度に得られた,その解決の突破口を開く研究成果をさらに拡張することに成功した.以上のことより,本年度の研究計画の所期の目的を達成することができた.
なお,完備化法についてのさらなる研究及び未解決問題の全面的な解決をめざす研究は次年度も引き続き行う予定である.
|
