Ein formales System, das aus einer Menge gerichteter Umformungsregeln besteht, mit denen Terme durch musterbasierte Ersetzungen und Substitutionen in andere Terme transformiert werden.

Prinzip

Regeln der Form l -> r werden auf Vorkommen von Instanzen von l in einem größeren Term angewandt mittels Matching und Substitution; wiederholte Anwendung ergibt Reduktionsfolgen, deren Eigenschaften (Terminierung, Konfluenz) Existenz und Eindeutigkeit normaler Formen bestimmen.

Demonstration

Mit den Regeln { f(a) -> b, f(x) -> g(x) } und dem Term f(f(a)) wendet man innerlich f(a) -> b an und erhält f(b), dann ggf. f(x) -> g(x) zu g(b); unterschiedliche Anwendungsreihenfolgen können zu unterschiedlichen Ergebnissen führen, wenn das System nicht konfluente ist.

Fehlanwendung

Zu erwarten, dass ein TRS eindeutige Normalformen oder Terminierung liefert, ohne Konfluenz oder Terminierung nachzuweisen; Regeln anzuwenden ohne auf Variable-Capture oder notwendige Nebenbedingungen zu achten.

Konsequenz

Bei geeigneter Ausgestaltung liefert ein TRS algorithmische Normalisierung, Entscheidungsverfahren für äquationale Theorien und eine operationelle Semantik für Programmiersprachen und Theorembeweiser.

Umkehrung

Die gerichtete Natur umkehren, indem man Regeln als bidirektionale Gleichungen (l ↔ r) betrachtet, um eine äquationale Theorie zu bilden; dies hebt die Reduktionsrichtung auf und verschiebt den Fokus von Berechnung zu Gleichheitsbegründung.

Abgrenzung

Gilt für Terme ersten Grades unter einer gegebenen Signatur und Regelmenge; Standard-TRSs schließen höherordentliche Bindungskonstrukte, nebenwirkungsbehaftete Operationen oder kontextuelle Beschränkungen aus, sofern nicht ausdrücklich erweitert.

Semantische Spannung

Spannung zwischen der Auffassung von Regeln als deterministische Rechenschritte (Rewriting) und als logische Gleichungen (Equations), wobei Richtung und Strategie in der einen Sicht kritisch, in der anderen nachgeordnet sind; beide Perspektiven beeinflussen Korrektheitskriterien.

Synthese

Ein Term Rewriting System ist eine syntaktische Maschine aus gerichteten Ersetzungsregeln, die durch Matching und Substitution Termtransformationen ausführt; seine Wirksamkeit hängt von Metaeigenschaften wie Terminierung und Konfluenz ab, die Determiniertheit und Entscheidbarkeit steuern.