Decidability of Termination of Grid String Rewriting Rules
Alfons Geser · SIAM Journal on Computing · 2002
Termination of string rewriting is known undecidable. Termination of string rewriting with only one rule is neither known decidable nor known undecidable. This paper presents a decision procedure for rules $u\rightarrow v$ such that some letter b from u occurs as often or less often in v. We call such rules "grid" rules. By far most rules are grid rules. Grid rules cover all rules which terminate by a total division order. Thus total division orders are shown to be irrelevant for the termination problem of one-rule string rewriting.