1996 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の合流性を保証するものであり,また,この深さ保存牲を拡張した重さ保存性の概念を導入することにより,この十分条件を拡張すると共に,強重なり性を満たす場合についても合流性を保証する判定可能な十分条件を明らかにした.本研究では,次に,左線形TRSの合流性問題に対しても見直しを行い,長い間,未解決であった(inverse para11el closed条件)問題に対して,その解決の突破口を開く研究成果を初めて得ることに成功した.さらに,本研究では,これらの研究成果に基づく,停止性を前提としない新しい完備化法について考察し,その基礎となるいくつかの研究成果を得た.
|
-
[Publications] GOMI,H.: "On the Church-Rosser Property of Non-E-overlapping and Strongly Depth-Preserving TRS's" Trans.IPS.Japan. 27・12. 2147-2160 (1996)
-
[Publications] OYAMAGUCHI,M.: "A New Parallel Closed Condition for Church-Rosser of Left-Linear TRS's" Proc.8th Int.Conf.on RTA'97. (1997)
-
[Publications] GOMI,H.: "On the Church-Rosser Property of Depth-Preserving TRS's" 情報基礎理論ワークショップ. 67-72 (1996)
-
[Publications] GOMI,H.: "On the Church-Rosser Property of Root-E-overlapping and Depth-Preserving TRS's" 信学技報. COMP96-72. 9-16 (1997)
-
[Publications] OYAMAGUCHI,M.: "On the Church-Rosser Property of Left-Linear TRS's" 10th Term Rewriting Meeting. (1996)
