We introduce a new class of automated proof methods for the termination of rewriting systems on strings. The basis of all these methods is to show that rewriting preserves regular languages. To this end, letters are annotated with natural numbers, called
match heights. If the minimal height of all positions in a redex is
h then every position in the reduct will get height
h+1. In a
match-bounded system, match heights are globally bounded. Using recent results on
deleting systems, we prove that rewriting by a match-bounded system preserves regular languages. Hence it is decidable whether a given rewriting system has a given match bound. We also provide a criterion for the absence of a match-bound. It is still open whether match-boundedness is decidable. Match-boundedness for all strings can be used as an automated criterion for termination, for match-bounded systems are terminating. This criterion can be strengthened by requiring match-boundedness only for a restricted set of strings, namely the set of right hand sides of forward closures.
Key words String Rewriting System - Semi-Thue System - Termination - Match-bounded
Partly supported by the National Aeronautics and Space Administration under NASA Contract No. NAS1-97046 while this author was in residence at the NIA.Acknowledgement This research was supported in part by the National Aeronautics and Space Administration (NASA) while the last two authors were visiting scientists at the Institute for Computer Applications in Science and Engineering (ICASE), NASA Langley Research Center (LaRC), Hampton, VA, in September 2002. The helpful comments of three anonymous referees are gratefully acknowledged, and we thank Hans Zantema for valuable hints and discussions