TY - GEN
T1 - Decidability for left-linear growing term rewriting systems
AU - Nagaya, Takashi
AU - Toyama, Yoshihito
N1 - Funding Information:
1A preliminary version of this paper was presented at the 10th International Conference on Rewriting Techniques and Applications, Trento, July 1999. This work was partially supported by Grants 10139214 and 10680346 from Ministry of Education, Science and Culture of Japan.
Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1999.
PY - 1999
Y1 - 1999
N2 - A term rewriting system is called growing if each variable occurring both the left-hand side and the right-hand side of a rewrite rule occurs at depth zero or one in the left-hand side. Jacquemard showed that the reachability and the sequentiality of linear (i.e., left-right-linear) growing term rewriting systems are decidable. In this paper we show that Jacquemard's result can be extended to left-linear growing rewriting systems that may have right-non-linear rewrite rules. This implies that the reachability and the joinability of some class of right-linear term rewriting systems are decidable, which improves the results for rightground term rewriting systems by Oyamaguchi. Our result extends the class of left-linear term rewriting systems having a decidable call-by-need normalizing strategy. Moreover, we prove that the termination property is decidable for almost orthogonal growing term rewriting systems.
AB - A term rewriting system is called growing if each variable occurring both the left-hand side and the right-hand side of a rewrite rule occurs at depth zero or one in the left-hand side. Jacquemard showed that the reachability and the sequentiality of linear (i.e., left-right-linear) growing term rewriting systems are decidable. In this paper we show that Jacquemard's result can be extended to left-linear growing rewriting systems that may have right-non-linear rewrite rules. This implies that the reachability and the joinability of some class of right-linear term rewriting systems are decidable, which improves the results for rightground term rewriting systems by Oyamaguchi. Our result extends the class of left-linear term rewriting systems having a decidable call-by-need normalizing strategy. Moreover, we prove that the termination property is decidable for almost orthogonal growing term rewriting systems.
UR - http://www.scopus.com/inward/record.url?scp=84957661421&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84957661421&partnerID=8YFLogxK
U2 - 10.1007/3-540-48685-2_22
DO - 10.1007/3-540-48685-2_22
M3 - Conference contribution
AN - SCOPUS:84957661421
SN - 3540662014
SN - 9783540662013
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 256
EP - 270
BT - Rewriting Techniques and Applications - 10th International Conference, RTA 1999, Proceedings
A2 - Narendran, Paliath
A2 - Rusinowitch, Michael
PB - Springer Verlag
T2 - 10th International Conference on Rewriting Techniques and Applications, RTA 1999
Y2 - 2 July 1999 through 4 July 1999
ER -