Title
Decidability for Left-Linear Growing Term Rewriting Systems
Abstract
A term rewriting system is called growing if each variable occurring on 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-nonlinear 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 right-ground 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.
Year
DOI
Venue
1999
10.1006/inco.2002.3157
Information and Computation/information and Control
Keywords
DocType
Volume
termination property,left-linear term,depth zero,rightground term,joinability,growing term rewriting system,right-hand side,term rewriting systems,reachability,sequentiality,left-hand side,right-linear term,normalizing strategy
Conference
178
Issue
ISSN
ISBN
2
Information and Computation
3-540-66201-4
Citations 
PageRank 
References 
37
1.45
17
Authors
2
Name
Order
Citations
PageRank
Takashi Nagaya1371.45
Yoshihito Toyama253349.60