依存対を利用したAC停止性の証明法
スポンサーリンク
概要
- 論文の詳細を見る
項書換え系において, ArtsとGieslは依存対と依存対グラフの概念を導入することにより無限列の詳細な解析を行ない, 停止性を証明するための効果的な手法を開発した.本研究ではこの概念をAC項書換え系に拡張し, AC項書換え系のACを法とした停止性を効果的に証明するための新しい手法を提案する.残念ながら依存対グラフの作成は計算不能である.それゆえに, 我々は近似依存対グラフを効果的に作成するためのアルゴリズムをΩ-書き換えやΩ_v-書き換えの手法を用いることにより設計する.
- 社団法人電子情報通信学会の論文
- 1998-03-24
著者
関連論文
- 高階項書換え系における改良再帰分解順序について
- 高階項書換え系の停止性について
- 依存対を用いた文脈依存書換え系の停止性判定について
- 消去法による項書換え系の停止性判定について
- 消去法による項書換え系の停止性判定について
- 項書換え系の合流性を保存する合併条件について
- 依存対を利用したAC停止性の証明法
- 条件付き項書換え系の合流性について
- 重なりのある強逐次系のインデックス簡約について
- 項書き換え系のパーシステント性の順序付きソートによる拡張
- Extending persistency of confluence with ordered sorts
- Top-down labelling and modularity of term rewriting systems
- Persistency of confluence
- Persistency of confluence
- 単純右線形項書換えシステムの合流性について
- 条件付き項書換え系の合流性について
- NVNF-逐次系におけるインデックスの決定可能性
- E重なりのある単純右線形項書き換えシステムの合流性について