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 -