Es ist offensichtlich, daß kontextfreie Systeme (d. h. linke Regelseiten haben Länge 1) die Klasse CF (kontextfreie Sprachen) erhalten, und es ist ein klassisches Resultat (Book 198?) daß invers kontextfreie Systeme (d. h. rechte Regelseiten haben Länge 1) die Klasse REG (reguläre Sprachen) erhalten.
Hibbard (1974) definiert context-limited Systeme und zeigt, daß sie CF erhalten. Wir geben dafür einen neuen Beweis, aus dem auch sofort folgt, daß inverse context-limited Systeme, die wir deleting nennen, REG erhalten. Wir stellen weiter fest, daß deleting systeme terminierend sind (folgt direkt aus der Definition), und für inverse deleting systeme Termination entscheidbar ist.
Um diese Resultate für weitere Klassen von Systemen zu benutzen, definieren wir die folgende Transformation: Wir annotieren jede Buchstabenposition mit einer natürlichen Zahl, und schreiben nach jedem Ersetzungsschritt auf jede Stelle des Redukts den Nachfolger des Minimums der Annotationen des Redexes.
Wenn diese match height für ein System R (oder sein Inverses) global beschränkt ist, dann ist das annotierte System endlich und (invers) deleting, und wir können Termination entscheiden. Dieses Verfahren läßt sich automatisieren, da match-boundedness (für fixierte Schranke) entscheidbar ist.
Eine Verschärfung des Verfahrens erhalten wir schließlich dadurch, daß wir match-boundedness nicht für beliebige Startwörter, sondern nur für rechte Seiten von Forward-Closures untersuchen.
Mit diesen Methoden können wir beispielsweise für viele Einregel-Wort-Ersetzungs-Systeme automatische Terminationsbeweise führen - darunter in vielen Fällen, die selbst für geübte Menschen schwer sind.
{ baab -> aababa } und { aabb -> bbbaaa }von Hand nachzuweisen -- oder probieren Sie es doch lieber mit der Implementierung der o. g. Algorithmen: http://theo1.informatik.uni-leipzig.de/~joe/bounded/