項書き換えシステム(TRS)の重要な性質に合流性があり、これまでの研究により、TRSが有限停止性又は線形性をみたす場合について、多くの成果が得られていた。他方、TRSが非停止かつ非線形の場合についてはほとんど研究されずにきたが、最近、本研究者らによって、書き換えグラフを用いる手法及び条件付TRSを用いる手法が新たに導入され、合流性に関する幾つかの新しい結果が示された。 本研究では、この合流性に関する研究をさらに発展させることを目的として、まず右定項TRSについて考察し、そのクラスでは非E重なり性及び非ω重なり性が共に合流性を保証する。判定可能な十分条件であることを明らかにした。次に、右定項TRSのクラスを真に含む単純右線形TRSのクラスについて考察し、そのクラスにおいても非E重なり性が合流性を保証する十分条件であることを明らかにした。さらに、E重なりのあるTRSの合流性について考察し、E危険対に着目した、合流性を保証する十分条件を幾つか導くことに成功した。 本研究では、また、合流性を保証する条件を導くためにこれまで提案された異なる2つの手法に対して、系列正規化可能性という概念を新たに導入することにより、統合化が可能であることを明らかにすると共に、この統合化された手法を用いて、従来の結果を拡張し、より一般化した条件を明らかにした。さらに、強い深さ保存性をみたすTRSのクラスについても考察し、非E重なり性がその合流性を保証する十分条件であることを明らかにした。 以上の本研究の成果より、合流性に関する研究において、所期の目標を十分に達成することができた。さらにTRSの簡約化戦略及び関数型プログラムの効率の良い実行系を実現する方法についても基礎研究を行い、新しい知見を得た。
|