Decidability of Termination Properties for Term Rewriting Systems Consisting of Shallow Dependency Pairs

摘要

In this paper, we show some decidable properties: termination, innermost termination and context-sen­sitive termination for the class of term rewriting systems (TRSs for short) whose dependency pairs are right-ground or right-linear shallow. Here, the right-linearity is not required for innermost termination. By analyzing argument propagation in the dependency pairs proposed by Wang and Sakai [11], we show that there exists a looping sequence if a TRS in the class is not terminating. One of benefit of our approach is that decision of reachability and joinability is not necessary in the decision procedure.%本稿では，右定項または右線形シヤローな依存対のみを持つ項書換え系に対して，停止性，最内停止性，文脈依存停止性がそれぞれ決定可能であることを示す．ここで最内停止性については右線形性を必要としない．Wang，Sakai［11］が右線形シヤロー項書換え系の停止性の決定可能性を示すために用いた依存グラフに串ける引数の伝播の解析の手法を応用して，該当するクラスの項書換え系では，停止性を持たないならばループする書換え系列が存在することを示す．これにより停止性が決定可能なクラスを広げ，さらに最内停止性，文脈依存停止性に応用する．本手法による決定手続きは，Wang，Sakai［11］らの手法とは異なり，到達可能性と合流可能性の判定を必要としないという特長を持つ．