弱単項TRSのE重なり性について
スポンサーリンク
概要
- 論文の詳細を見る
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のクラスにおいてもこの証明手法が適用可能であることを示す.
- 2012-10-15
著者
関連論文
- ツーバイフォーパネル部材の最適木取ソフトウェアの開発
- 非線形TRSのE重なり性について
- A-011 An Extension of E-overlapping Notion in Term Rewriting Systems and its Applications
- 非線形TRSのE重なり性判定問題について(計算量理論)
- A-017 厳密解法と発見的手法の組合せによるサイズ可変ビンパッキング問題の解法(モデル・アルゴリズム・プログラミング,一般論文)
- The Joinability and Related Decision Problems for Semi-constructor TRSs(計算理論)
- The Confluence Problem for Flat TRSs(New Trends in Theory of Computation and Algorithm)
- The Reachability and Related Decision Problems for Semi-Constructor TRSs (Theoretical Computer Science and its Applications)
- The Joinability and Unification Problems for Confluent Semi-Constructor TRSs (Evolutionary Advancement in Fundamental Theories of Computer Science)
- 単項的TRSにおける単ー化問題について
- 弱単項TRSのE重なり性について
- Shibboleth・CAS連携による東海アカデミッククラウド認証基盤の構築(学生セッション,一般)
- Shibboleth・CAS連携による東海アカデミッククラウド認証基盤の構築