Termersetzungsregel

Die Termersetzungssysteme (TES) sind ein formales Berechnungsmodell in der Theoretischen Informatik. Sie bilden insbesondere die Grundlage der Logik- und funktionalen Programmierung. Ferner spielen sie eine wichtige Rolle beim Wortproblem und bei der Terminierungsanalyse.

Termersetzungssysteme sind Mengen von so genannten Termersetzungsregeln. Diese Mengen kann man sich wie Gleichungssysteme zwischen Termen vorstellen, bei dem die Gleichungen nur von links nach rechts angewendet werden dürfen.

Beispiel

plus(0      , y) $\rightarrow$ y   
plus(succ(x), y) $\rightarrow$ succ(plus(x, y))

Die oben stehenden Regeln bilden einen Termersetzungssystem, welches die Addition zweier natürlicher Zahlen berechnet. Die Regeln besagen, dass beispielsweise jedes Vorkommen von plus(0,y) in einem Term durch y ersetzt werden darf. Dabei kann y selbst ein beliebiger Term sein.

Termersetzungssysteme sind turing-vollständig, stehen also was die Berechnungsstärke angeht anderen Formalismen wie den Turingmaschinen, dem Lambda-Kalkül oder Registermaschinen in nichts nach. Da sie vergleichsweise einfach strukturiert sind und von Computern gut gehandhabt werden können, stellen die Termersetzungssysteme ein wichtiges Hilfsmittel in der computergestützten Analyse von Algorithmen dar.

Definitionen

Um ein Termersetzungssystem aufzubauen, benötigt man zunächst eine klare Vorstellung von den zu Grunde liegenden Begriffen.

Terme

Für eine Menge Σ von Funktionssymbolen und eine (unendliche) Menge $\mathcal{V}$ von Variablen definiert man die Menge ${\mathcal{T}}(\Sigma, {\mathcal{V}})$ der Terme induktiv wie folgt:

• Jede Variable und jedes nullstellige Funktionssymbol ist ein Term.
• Sind $t_1, \dots, t_n$ Terme und ist f ein n-stelliges Funktionssymbol, so ist $f(t_1,\dots, t_n)$ ebenfalls ein Term.

Ohne formale Definition seien noch folgende Begriffe erwähnt:

• Eine Substitution ordnet einigen Variablen neue Terme zu. Eine Substitution wirkt auf einen Term, indem jedes Vorkommen einer Variable durch den von der Substitution vorgegebenen Term ersetzt wird. Lautet die Substitution beispielsweise σ = {x / f(x,y)} und ist t = g(x) ein Term, so ist tσ = g(f(x,y)) der Term, der durch Anwenden von σ auf t entsteht.
• Ein Term t matcht einen Term s, wenn es eine Substitution σ gibt, so dass tσ = s gilt. Beispielsweise matcht g(x) den Term g(s(y)).

Termersetzungsregeln

Eine Termersetzungsregel ist ein Paar $l \rightarrow r$ zweier Terme l,r, wobei l keine Variable sein darf und ferner in r keine Variable vorkommen darf, die nicht auch in l vorkommt. Der Grund dieser Einschränkung hängt mit der Terminierung eines Termersetzungssystems zusammen und wird im entsprechenden Abschnitt näher erläutert.

Die Termersetzungsrelation

Die "Funktionsweise" eines Termersetzungssystems wird über die so genannte Termersetzungsrelation $\rightarrow_{\mathcal{R}}$ definiert.

Anschauliche Beschreibung

Passt auf einen Term s oder einen Teilterm von s die linke Seite einer Regel, so kann man diese linke Seite in s durch die rechte Seite der entsprechenden Regel ersetzen und so einen neuen Term t erhalten. Dies soll an einigen Beispielen gezeigt werden. Dazu betrachten wir das einfache Termersetzungssystem

f(x,y) -> x

• Den Term f(s(y),g(x)) kann man mit dieser Regel zu s(y) auswerten.
• g(f(a,b)) kann man zu g(a) auswerten.
• f(f(a,b),c) kann man in einem Schritt sowohl zu f(a,c) als auch zu f(a,b) auswerten.

Formale Definition

Ein Term s wertet zu t aus, geschrieben $s \rightarrow_{\mathcal{R}} t$, falls folgendes gilt:

• Es gibt eine Substitution σ und
• eine Regel $l \rightarrow_{\mathcal{R}} r$ in $\mathcal{R}$, so dass
• s den Term lσ enthält und
• t an derselben Stelle den Term rσ enthält, ansonsten aber mit s übereinstimmt.

Fragestellungen

Je nach Anwendungsbereich eines Termersetzungssystems gibt es mehrere Fragestellungen, welche von Interesse sind. Dies sind unter anderem:

Terminierung

Hierbei stellt man sich die Frage, ob es zu einem Termersetzungssystem $\mathcal{R}$ Terme gibt, die eine unendliche Kette von Auswertungen $s \rightarrow_{\mathcal{R}} s_1 \rightarrow_{\mathcal{R}} s_2 \rightarrow_{\mathcal{R}} \dots$ erlauben, oder ob alle Ableitungen aller Terme stets endlich sind. Ist letzteres der Fall, nennt man $\mathcal{R}$ auch terminierend oder fundiert.

Zwar ist die Frage nach der Terminierung in jedem turingvollständigen Berechnungssystemen unentscheidbar. Es existieren jedoch eine Menge fortgeschrittener Techniken, um die Terminierung vieler Termersetzungssysteme automatisch nachzuweisen. Ein allgemeiner Ansatz ist, eine fundierte Ordnung $\succ$ mit $\rightarrow_{\mathcal{R}}\subseteq\succ$ zu finden, so dass $l \succ r$ für alle Regeln $l \rightarrow_{\mathcal{R}} r$ des TES gilt. Außerdem muss diese Ordnung erhalten bleiben, wenn man Substitutionen auf l und r anwendet (die Ordnung muss stabil sein) oder wenn l und r als Teilterme eines anderen Terms auftreten (die Ordnung muss monoton sein). Es existieren noch zahlreiche andere Methoden. Man kann die Terme beispielsweise als Polynome oder Matrizen interpretieren sowie eine genauere Analyse der Abhängigkeiten der Funktionssymbole untereinander durchführen. Hierfür sei auf die weiterführende Literatur verwiesen.

Konfluenz

Ausgehend von einem Term kann es mehrere mögliche Ableitungen geben. Mit Konfluenz meint man die Eigenschaft eines Termersetzungssystems, dass zwei Terme, die in mehreren Schritten auf unterschiedliche Art aus einem Ausgangsterm hervorgehen, stets wieder zu einem Term zusammengeführt werden können. Eine damit zusammenhängende Frage ist, ob die durch ein Termersetzungssystem beschriebene Berechnung für dieselbe Eingabe stets zu demselben Ergebnis (eindeutige Normalform) kommt. Konfluenz ist im Allgemeinen ebenso unentscheidbar wie die Terminierung.

Ein Termersetzungssystem, das terminiert und konfluent ist, bezeichnet man auch als konvergent. Für solche Systeme existiert zu jedem Term eine eindeutige Normalform.

Anwendungen

Als mathematisch relativ leicht handhabbares Konstrukt eignen sich Termersetzungssysteme für die computergestützte Behandlung von Problemen aus der theoretischen Informatik. Einige Anwendungen sind:

Entscheidungsverfahren für das Wortproblem

Ein Termgleichungssystem $\mathcal{E}$ ist eine Menge von Gleichungen zwischen Termen. Unter dem Wortproblem für $\mathcal{E}$ versteht man die Frage, ob eine Gleichung s = t gilt unter der Voraussetzung, dass die Gleichungen in $\mathcal{E}$ wahr sind. Als Beispiel könnte man in $\mathcal{E}$ die Gruppenaxiome kodieren:

f(x,f(y,z)) = f(f(x,y),z)
f(x,e) = x
f(x,i(x)) = e

Hierbei ist f die Gruppenverknüpfung, das neutrale bzw. inverse Element ist e bzw. i(x). Man sucht nun nach einem Verfahren, automatisch Gleichungen wie i(e) = e oder i(i(x)) = x auf ihren Wahrheitsgehalt hin zu überprüfen.

Zu diesem Zweck konstruiert man zum Gleichungssystem $\mathcal{E}$ ein äquivalentes und konvergentes Termersetzungssystem $\mathcal{R}$. Äquivalent bedeutet hier, dass s = t gilt genau dann wenn $s \leftrightarrow_{\mathcal{R}}^* t$. Die Schreibweise $\leftrightarrow_{\mathcal{R}}^*$ bedeutet, dass die Termersetzungsrelation hier beliebig oft und in beiden Richtungen angewendet werden kann.

Hat man nun ein solches konvergentes TES gegeben, lässt sich das Wortproblem s = t lösen, indem man einfach s und t mittels $\rightarrow_{\mathcal{R}}$ solange auf beliebige Weise auswertet, bis keine weitere Auswertung mehr möglich ist. Da das TES nach Voraussetzung konvergent ist, gibt es keine unendliche Auswertung. Das Verfahren selbst terminiert also. Da das TES außerdem konfluent ist, spielt es keine Rolle, welche der möglichen Auswertungen man wählt. Führt nun die Auswertung der beiden Terme zu ein und demselben Term, so gilt s = t für die Gleichungen von $\mathcal{E}$.

Da das Wortproblem unentscheidbar ist, lässt sich nicht immer ein konvergentes Termersetzungssystem finden, das das Wortproblem für das entsprechende Gleichungssystem entscheidbar macht.

Terminierungsanalyse

Da für Termersetzungssysteme so viele mächtige Techniken existieren, welche die Terminierung nachweisen können, transformiert man Programme höherer Programmiersprachen in Termersetzungssysteme und wendet diese Techniken darauf an. Das Tool AProvE, welches an der RWTH Aachen entwickelt wird, hat dies bisher für die Programmiersprachen Prolog und Haskell implementiert.

Die Behandlung imperativer und objektorientierter Sprachen, wie z.B. Java, ist Gegenstand aktueller Forschung.

Literatur

• F. Baader, T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1999.
• J. Avenhaus. Reduktionssysteme. Springer-Verlag, 1995. ISBN 3-540-58559-1

Weblinks

• http://aprove.informatik.rwth-aachen.de/ Ein Tool, welches unter anderem die Terminierung von Termersetzungssystemen sowie Prolog- und Haskell-Programmen automatisch beweisen kann.