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.

Authors

• Alfons Geser
• Dieter Hofbauer
• Johannes Waldmann

Keywords

No keywords are indexed for this paper.