書き換えシステムの基本的性質の解明と関数型プログラムの評価戦略に関する研究

1993 Fiscal Year Annual Research Report

• Project/Area Number: 05680272
• Research Institution: Mie University
• Principal Investigator: 大山口 通夫 三重大学, 工学部, 教授 (50111828)
• Keywords: 項書き換えシステム / 合流性 / 非E重なり / 非ω重なり / 右定項TRS / 単純右線形TRS

Research Abstract

項書き換えシステム(TRS)の重要な性質に合流があり、これまでの研究により、TRSが有限停止性又は線形性をみたす場合について、多くの成果が得られていた。他方、TRSが非停止かつ非線形の場合にはほとんど研究されずにきたが、最近、書き換えグラフの概念を導入することにより、右定項かつ非E重なりなTRSは合流性をみたすことが本研究代表者らによって示された。しかしながら、右定項TRSの非E重なり性を判定する問題は未解決のまま残されていた。そこで本研究では、この問題に対して考察し、判定可能であることを示した。次に、本研究では、非ω重なり性が右定項TRSの非E重なり性を保証し、かつ効率良く調べられる十分条件であることを示した。これらの結果より、非E重なり性及び非ω重なり性が共に右定項TRSの合流性を保証する、判定可能な十分条件であることを明らかにした。
さらに、本研究では従来の結果を拡張して、右定項TRSのクラスを真に含む単純右線形TRSのクラスにおいても、非E重なり性が合流性を保証する十分条件であることを明らかにした。単純右線形TRSの非E重なり性を判定する問題は一般に非可解であるが、非強重なり性が非E重なり性を保証する、判定可能な十分条件であることが知られており、また、本研究では、深さ保存的な単純右線形TRSにおいては、非強重なり性よりも弱い条件である非ω重なり性が非E重なり性を保証する十分条件であることを示した。本研究では、また、TRSがE重なりする場合の合流性についても考察し、そのE危険対に着目した、合流性を保証する十分条件を幾つか導くことに成功した。
以上の本研究の成果により、当初の計画通り、所期の目標を十分に達成したと考えられる。なお、合流性についての研究は、さらなる成果が期待されるため、次年度においても引き続き行う予定である。

Research Products

• [Publications] 松浦 邦博: "非線形TRSの合流性を保証する判定可能な十分条件について" 電気関係学会東海支部連合大会講演論文集. 306-306 (1993)
• [Publications] 松浦 邦博: "非線形TRSのE重なり性判定問題について" 冬のLAシンポジウム. (in press). (1994)
• [Publications] OYAMAGUCHI,M.: "Some Decidable Conditions for Confluence of Right-Grownd TRS's" 5th Term Rewriting Meeting. (in press). (1994)