弱単項TRSのE重なり性について

情報処理学会 Web Site

書誌事項

タイトル別名
  • ジャクタンコウ TRS ノ E カサナリ セイ ニ ツイテ
  • On the E-overlapping Property of Weak Monadic TRSs

この論文をさがす

抄録

Unique Normal Form（UN）性およびChurch-Rosser（CR）性は，項書き換えシステム（TRS）における重要な性質である．非E重なり性はUN性を保証する十分条件であり，TRSのいくつかの部分クラスにおいてはCR性を保証する十分条件であることも知られている．しかしながら，非E重なり性は一般に決定不能である．非ω重なり性は決定可能であり，一般のTRSにおいて非E重なり性を保証する十分条件であるか否かは未解決問題として残されているが，深さ保存的TRSや重み保存的TRSといったいくつかの部分クラスにおいて非E重なり性を保証する十分条件であることが知られている．本論文ではこれらのクラスとは比較不能な弱単項TRSのクラスを導入し，このクラスにおいて非ω重なり性が非E重なり性を保証する十分条件であることを示す．ここで，弱単項TRSとはすべての書き換え規則の右辺において，定義記号が出現するならば，根，または定項である部分項にのみ出現するTRSをいう．この結果は，定項TRSの合同閉包（congruence closure）アルゴリズムを利用した新しい証明手法によって得られたものである．本論文ではさらにこの結果を拡張して，弱単項TRSのクラスを拡張した多層TRSのクラスにおいてもこの証明手法が適用可能であることを示す．

Unique normalization (UN) and Church-Rosser (CR) properties are important properties of term rewriting systems (TRSs). Non-E-overlapping property is a sufficient condition to ensure UN of TRSs, and also a sufficient condition to ensure CR for some subclasses of TRSs. However, the non-E-overlapping property is undecidable in general. It is known that non-ω-overlapping property is decidable. It remains open whether the non-ω-overlapping property is a sufficient condition to ensure the non-E-overlapping property for general TRSs, but for some subclasses of TRSs such as depth preserving TRSs and weight preserving TRSs, the non-ω-overlapping property ensures the non-E-overlapping one. In this paper, we introduce the subclass of TRSs named weak monadic TRSs which is incomparable with these subclasses of TRSs, and show that the non-ω-overlapping property is a sufficient condition to ensure the non-E-overlapping property for this class. Here, a weak monadic TRS is such a TRS that for each rewrite rule α→β, every defined symbol occuring in β occurs only either at the root position or in a ground subterm of β. This result is obtained by a new proof technique using a congruence closure algorithm for ground TRSs. Moreover, we extend this result by showing that this technique is applicable to multi-layered TRSs which properly include the class of weak monadic TRSs.

収録刊行物

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ