|Abstract of Paper|
Match-Bounded String Rewriting Systems
by Alfons Geser, Dieter Hofbauer and Johannes Waldmann
We investigate rewriting systems on strings by annotating letters with natural numbers, so called match heights. A position in a reduct will get height h+1 if the minimal height of all positions in the redex is h. In a match-bounded system, match heights are globally bounded. Exploiting recent results on deleting systems, we prove that it is decidable whether a given rewriting system has a given match bound. Further, we show that match-bounded systems preserve regularity of languages. Our main focus, however, is on termination of rewriting. Match-bounded systems are shown to be linearly terminating, and--more interestingly--for inverses of match-bounded systems, termination is decidable. These results provide new techniques for automated proofs of termination.