2021-12-05T14:45:32Zhttps://nagoya.repo.nii.ac.jp/oaioai:nagoya.repo.nii.ac.jp:000190532021-03-01T16:24:06ZDecidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency PairsUCHIYAMA, KeitaSAKAI, MasahikoSAKABE, Toshiki(c)一般社団法人電子情報通信学会。本文データは学協会の許諾に基づきCiNiiから複製したものであるlooping sequenceargument propagationIn 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.一般社団法人電子情報通信学会2010-05engjournal articlehttp://hdl.handle.net/2237/21159https://nagoya.repo.nii.ac.jp/records/190530916-8532IEICE transactions on information and systemsE93D5953962https://nagoya.repo.nii.ac.jp/record/19053/files/e93-d_5_953.pdfapplication/pdf505.8 kB2018-02-21