1997 Fiscal Year Annual Research Report
書き換えシステムの基本的性質の解明と完備化手続きに関する研究
| Project/Area Number |
08680362
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Mie University |
|---|
Principal Investigator |
大山口 通夫 三重大学, 工学部, 教授 (50111828)
|
|---|
| Keywords | 項書き換えシステム / 左線形TRS / 合流性 / Church-Rosser / 完備化手続き / 非線形TRS / 強重なり性 / 重さ保存性 |
|---|
| Research Abstract |
項書き換えシステム(TRS)は等式の集合上で推論や簡約(計算)を行うための計算モデルであり,その応用例として,定理の自動証明,関数型プログラムの効率良い実行,プログラムの仕様と実現の正当性検証など非常に重要な問題を包含していることから,これまで多くの研究者の注目を集め,盛んに研究されてきた.しかしながら,まだ多くの重要な未解決問題が残されており,さらなる研究の発展が望まれている.そこで本研究では,前年度よりTRSの最も基本的で重要な性質の1つである合流性(Church-Rosser性)について研究を行い,合流性に関する未解決問題に対して,新しい概念とアイデアを導入することによって,その本質に迫る研究成果を得ることに成功すると共に,定理の自動証明などに必要不可欠な危険対の完備化法について研究を行い,従来提案されていた方法よりも広範囲の問題解決に利用可能な(TRSの停止性を前提としない)新しい完備化法を明らかにすることに成功した.
特に,本年度の研究成果としては新しい完備化法を提示したことであり,この方法は(前年度に研究を行った)強い深さ保存性を満たすTRSのクラスが十分広いクラスを包含していることに着目して,その合流性を保証する(前年度に導いた)条件が一般の等式論理の完備化手続きに十分利用できることを明らかにすることにより,得られたものである.また,前年度に引き続き,左線形TRSに対する長い間未解決であった(inverse parallel closed 条件)問題についても研究を行い,前年度に得られた,その解決の突破口を開く研究成果をさらに拡張することに成功した.以上のことより,本年度の研究計画の所期の目的を達成することができた.
なお,完備化法についてのさらなる研究及び未解決問題の全面的な解決をめざす研究は次年度も引き続き行う予定である.
|
-
[Publications] OYAMAGUCHI,M.: "A New Parallel Closed Condition for Church-Rosser of Left-Linear TRS's" Proc.8th Int.Conf.on RTA'97 LNCS. 1232. 187-201 (1997)
-
[Publications] 松浦 邦博: "非線形TRSのE重なり性について" 電子情報通信学会論文誌. J80-D-I. 847-855 (1997)
-
[Publications] GOMI,H.: "On the Church-Rosser Property of Root-E-overlapping and strongly Depth-Preserving TRS's" Trans.IPS.Japan. (掲載決定). (1998)
-
[Publications] OYAMAGUDHI,M.: "On the upside-parallel-closed condition of loft-linear TRS's" 12th Term Rewriting Meeting. (1997)
