氏名: 大野 健治 (289634130)
論文題目: 項書換え系における停止性のモジュラー性に関する研究
論文概要
項書換え系において、停止性・合流性等の性質がモジュラーであるとは、
性質Pを持つ二つの項書換え系から、書換え規則の和をとることにより構成
される項書換え系においても性質Pが成り立つことを意味する。
一般に、項書換え系においては、多くの重要な性質はモジュラー性を持た
ない。しかし、二つの項書換え系の関数記号間に条件を与えることにより、
モジュラー性をもつような項書換え系の組であるクラスを定義でき、
disjointやconstructor-sharing等のクラスが提案されている。このような
クラスの中で、階層的結合は、下位階層にあたる項書換え系の被定義関数
記号と、上位階層にあたる項書換え系の構成子記号に重なりを許すもので
あり、disjoint,constructor-sharingを含んだ、より大きなクラスである。
この階層的結合では、proper-extensionというサブクラスにおいて停止性
がモジュラー性を持つことが示されている。
本論文では、被定義関数記号の共有を許すように拡張した、新しい階層的
結合を与え、その上で停止性がモジュラー性を持つようなサブクラスを、
Artsらにより提案された依存対を用いて定義した。さらに、このサブクラ
スがproper-extensionを含むことを示した。また、階層的結合において、
停止性のモジュラー性が証明されているサブクラスは、書換え規則の左辺
に重なりのない項書換え系を対象としているが、条件を加えることにより、
変数のコピーを許さない項書換え系においても停止性がモジュラーとなる
ことを示した。
目次に戻る