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-sensitive 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.