Term Rewriting

Was ist Rechnen? Turing sagt: "Zustände auf einem Band ändern." Church (Lambda Kalkül) sagt: "Funktionen anwenden." Term Rewriting sagt: "Suchen und Ersetzen." Du hast Regeln: add(zero, x) -> x add(succ(x), y) -> succ(add(x, y)) Du hast einen Term: add(succ(zero), succ(zero)). Du wendest Regeln an, bis es nicht mehr geht. Ergebnis: succ(succ(zero)) (Das ist 2). Fast jede funktionale Sprache (Haskell) ist im Kern ein Term Rewriting System.

Merksatz: Ein Berechnungsmodell, das auf der wiederholten Anwendung von Ersetzungsregeln auf symbolische Ausdrücke (Terme) basiert, bis eine Normalform erreicht ist.

In Refactoring-Tools (IntelliJ). "Structural Search and Replace". Suche if ($A) { return true; } else { return false; }. Ersetze durch return $A;. Das ist eine Rewrite-Regel auf dem AST. Oder in Optimierern (LLVM): x * 0 -> 0. x + 0 -> x.

1. Strategien

Innermost (Call-by-Value): Ersetze erst die tiefsten Terme. (f(2+2) -> f(4)).
Outermost (Call-by-Name): Ersetze erst den äußersten Term. Für Term Rewriting ist das wichtig, weil manche Strategien endlos laufen, andere nicht.

2. Pattern Matching

Die Basis. Regel f(h(x), y) -> .... Der Term f(h(a), b) passt ($x=a, y=b$). Der Term f(a, b) passt nicht. Effizientes Pattern Matching ist eine Wissenschaft für sich.

1. Knuth-Bendix Completion

Was tun, wenn ein System nicht konfluent ist? (Also verschiedene Wege zu verschiedenen Ergebnissen führen). Man nutzt den Knuth-Bendix-Algorithmus. Der Algorithmus findet "Critical Pairs" (Zustände, die sich spalten) und fügt automatisch neue Regeln hinzu, um die Zweige wieder zusammenzuführen. In der automatischen Theorem-Beweisung (z.B. mit Waldmeister) ist das der Standard, um mathematische Gleichungen in ein effizientes Rechensystem zu verwandeln. Es verwandelt "Suche" in "Rechnen".

2. Termination & Path Orderings

Woher weiß man, dass ein Rewriter jemals anhält? (Termination Problem). In der Forschung nutzt man Recursive Path Orderings (RPO) oder Lexicographic Path Orderings (LPO). Man definiert eine Ordnung auf den Funktionssymbolen. Ein Experte beweist: "Jede Regelanwendung macht den Term in Bezug auf diese Ordnung kleiner." Da Terme nicht unendlich klein werden können, muss der Prozess terminieren. Das ist essentiell für Compiler-Optimierer, damit der Compiler nicht in einer Endlos-Optimierung hängen bleibt.

3. Higher-Order Rewriting (HRS)

In Sprachen wie Haskell oder beim Beweisen von Logik-Formeln gibt es Variablen-Bindungen ($\lambda x. \dots$). Einfaches Pattern Matching (Level 2) reicht hier nicht, da man aufpassen muss, dass man keine Variablen "einfängt" (Variable Capture). HRS nutzt komplexere Unifikations-Algorithmen (Higher-Order Unification), um Regeln auf Funktionen anzuwenden. Das ist die mathematische Basis für Tools wie Isabelle/HOL, mit denen man beweist, dass ein Mikrochip oder ein Betriebssystem-Kernel mathematisch korrekt ist.