Decidability for left-linear growing term rewriting systems

Takashi Nagaya, Yoshihito Toyama

研究成果: Article査読

28 被引用数 (Scopus)


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.

ジャーナルInformation and Computation
出版ステータスPublished - 2002 11 1

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • 情報システム
  • コンピュータ サイエンスの応用
  • 計算理論と計算数学


「Decidability for left-linear growing term rewriting systems」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。