Abstract of Paper

Match-Bounded String Rewriting Systems
by Alfons Geser, Dieter Hofbauer and Johannes Waldmann

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.