Match-bounded string rewriting systems

Abstract

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. © Springer-Verlag Berlin Heidelberg 2003.