Termersetzungssystem

formales Berechnungsmodell in der Theoretischen Informatik

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 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)  →  y
   plus(succ(x), y)  →   succ(plus(x, y))

Die oben stehenden Regeln bilden ein Termersetzungssystem, welches als die Addition zweier natürlicher Zahlen verstanden werden kann. Dies erfordert, dass man die Zahl 0 mit dem Term 0, die Zahl 1 mit dem Term succ(0), die Zahl 2 mit dem Term succ(succ(0)) usw. repräsentiert. Die Regeln besagen, dass beispielsweise jedes Vorkommen von in einem Term durch ersetzt werden darf. Dabei kann selbst ein beliebiger Term sein, muss also insbesondere auch keine natürliche Zahl darstellen.

Termersetzungssysteme sind turingvollstä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

Bearbeiten

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

Für eine Menge   von Funktionssymbolen und eine (unendliche) Menge   von Variablen definiert man die Menge   der Terme induktiv wie folgt:

  • Jede Variable und jedes nullstellige Funktionssymbol (d. h. jede Konstante) ist ein Term.
  • Sind   Terme und ist   ein n-stelliges Funktionssymbol, so ist   ebenfalls ein Term.

Man bemerke, dass diese Definition genau der Definition eines mathematischen Termes entspricht.

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   und ist   ein Term, so ist   der Term, der durch Anwenden von   auf   entsteht.
  • Ein Term   matcht einen Term  , wenn es eine Substitution   gibt, so dass   gilt. Beispielsweise matcht   den Term  .

Termersetzungsregeln

Bearbeiten

Eine Termersetzungsregel ist ein Paar   zweier Terme  , wobei   keine Variable sein darf und ferner in   keine Variable vorkommen darf, die nicht auch in   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

Bearbeiten

Die „Funktionsweise“ eines Termersetzungssystems wird über die Termersetzungsrelation   definiert.

Anschauliche Beschreibung

Bearbeiten

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

   f(x,y) → x
  • Den Term   kann man mit dieser Regel zu   auswerten.
  •   kann man zu   auswerten.
  •   kann man in einem Schritt sowohl zu   als auch zu   auswerten.

Formale Definition

Bearbeiten

Ein Term   wertet zu   aus, geschrieben  , falls folgendes gilt:

  • Es gibt eine Substitution   und
  • eine Regel   in  , so dass
  •   den Term   enthält und
  •   an derselben Stelle den Term   enthält, ansonsten aber mit   übereinstimmt.

Fragestellungen

Bearbeiten

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

Terminierung

Bearbeiten

Hierbei stellt man sich die Frage, ob es zu einem Termersetzungssystem   Terme gibt, die eine unendliche Kette von Auswertungen   erlauben, oder ob alle Ableitungen aller Terme stets endlich sind. Ist letzteres der Fall, nennt man   auch terminierend oder fundiert.

Zwar ist die Frage nach der Terminierung in jedem turingvollständigen Berechnungssystem unentscheidbar. Jedoch existiert eine Menge fortgeschrittener Techniken, um die Terminierung vieler Termersetzungssysteme automatisch nachzuweisen. Ein allgemeiner Ansatz ist, eine fundierte Ordnung   mit   zu finden, so dass   für alle Regeln   des TES gilt. Außerdem muss diese Ordnung erhalten bleiben, wenn man Substitutionen auf   und   anwendet (die Ordnung muss stabil sein) oder wenn   und   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

Bearbeiten

Ausgehend von einem Term kann es mehrere mögliche Ableitungen geben. Mit Konfluenz bezeichnet 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. Es ist entscheidbar, ob ein terminierendes Termersetzungssystem konfluent ist.[1]

Anwendungen

Bearbeiten

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

Bearbeiten

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

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

Hierbei steht das zweistellige Funktionssymbol   für die Gruppenverknüpfung, die einstellige Funktion   liefert die inversen Elemente, und die Konstante   bezeichnet das neutrale Element;  ,   und   sind Variablen. Man sucht nun nach einem Verfahren, automatisch Gleichungen wie   oder   auf ihren Wahrheitsgehalt hin zu überprüfen.

Zu diesem Zweck konstruiert man zum Gleichungssystem   ein äquivalentes und konvergentes Termersetzungssystem  . Äquivalent bedeutet hier, dass   gilt genau dann wenn  . Die Schreibweise   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   lösen, indem man einfach   und   mittels   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   für die Gleichungen von  .

Da das Wortproblem unentscheidbar ist, lässt sich nicht immer ein konvergentes Termersetzungssystem finden, das das Wortproblem für das entsprechende Gleichungssystem entscheidbar macht. Ein Verfahren zu Konstruktion von konvergenten Termersetzungssystemen ist das Knuth-Bendix Vervollständigungsverfahren.[1] Es berechnet im Erfolgsfall zu einer gegebenen Gleichungsmenge und einer fundierten Termordnung ein äquivalentes und konvergentes Termersetzungssystem. Allerdings ist weder die Termination noch der Erfolg des Knuth-Bendix Vervollständigungsverfahrens garantiert. Für den Fall der Gruppenaxiome oben berechnet das Knuth-Bendix Vervollständigungsverfahren z. B. das folgende konvergente Termersetzungssystem:

   f(x, e)          ->  x
   f(e, x)          ->  x
   f(x, i(x))       ->  e
   f(i(x), x)       ->  e
   f(f(x,y), z)     ->  f(x, f(y,z))
   f(x, f(i(x),y))  ->  y
   f(i(x), f(x,y))  ->  y
   i(e)             ->  e
   i(i(x))          ->  x
   i(f(x, y))       ->  f(i(y), i(x))

Terminierungsanalyse

Bearbeiten

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 beispielsweise Java, ist Gegenstand aktueller Forschung.

Literatur

Bearbeiten
Bearbeiten

Einzelnachweise

Bearbeiten
  1. a b D. E. Knuth, P. B. Bendix: Simple word problems in universal algebra. In: Computational Problems in Abstract Algebra. Pergamon Press, 1970.