Decidability for Left-Linear Growing Term Rewriting Systems |
| |
Authors: | Takashi Nagaya Yoshihito Toyama |
| |
Affiliation: | a Kanrikogaku Kenkyusho, Ltd. Nishiazabu Minato-ku 3-3-1, Tokyo, 106-0031, Japanf1;b Research Institute of Electrical Communication, Tohoku University, Katahira 2-1-1, Aoba-ku, Sendai, 980-8577, Japanf2 |
| |
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. |
| |
Keywords: | Abbreviations: growing term rewriting systemAbbreviations: reachabilityAbbreviations: sequentialityAbbreviations: joinability |
本文献已被 ScienceDirect 等数据库收录! |
|