Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs

Keita UCHIYAMA  Masahiko SAKAI  Toshiki SAKABE 

Publication
IEICE TRANSACTIONS on Information and Systems  Vol.E93-D  No.5  pp.953-962
Publication Date: 2010/05/01
Online ISSN: 1745-1361
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Term Rewriting Systems
Keyword: 
looping sequence,  argument propagation, 

Full Text: PDF

Summary: 
In this paper, we show that the termination and the innermost termination properties are decidable for the class of term rewriting systems (TRSs for short) all of whose dependency pairs are right-linear and right-shallow. We also show that the innermost termination is decidable for the class of TRSs all of whose dependency pairs are shallow. The key observation common to these two classes is as follows: for every TRS in the class, we can construct, by using the dependency-pairs information, a finite set of terms such that if the TRS is non-terminating then there is a looping sequence beginning with a term in the finite set. This fact is obtained by modifying the analysis of argument propagation in shallow dependency pairs proposed by Wang and Sakai in 2006. However we gained a great benefit that the resulted procedures do not require any decision procedure of reachability problem used in Wang's procedure for shallow case, because known decidable classes of reachability problem are not larger than classes discussing in this paper.