Termersetzungssystem

Grundidee und Bedeutung

Ein Termersetzungssystem (TES) ist ein formales Berechnungsmodell der Theoretischen Informatik. Es besteht aus einer Menge gerichteter Termersetzungsregeln. Diese ähneln Gleichungen zwischen Termen, dürfen aber nur von links nach rechts angewendet werden. TES bilden insbesondere eine Grundlage der Logikprogrammierung und der funktionalen Programmierung. Außerdem sind sie für das Wortproblem, die Terminierungsanalyse und die computergestützte Untersuchung von Algorithmen wichtig.

Termersetzungssysteme sind turingvollständig: Ihre Berechnungsstärke entspricht der von Turingmaschinen, dem Lambda-Kalkül und Registermaschinen. Zugleich sind sie vergleichsweise einfach aufgebaut und können von Computern gut verarbeitet werden.

Ein einfaches TES für die Addition natürlicher Zahlen lautet:

• plus(0, y) → y • plus(succ(x), y) → succ(plus(x, y))

Dabei wird 0 durch den Term 0, die Zahl 1 durch succ(0), die Zahl 2 durch succ(succ(0)) und so weiter dargestellt. Die erste Regel erlaubt es, jedes Vorkommen von plus(0, y) durch y zu ersetzen. Die Variable y darf hierbei für einen beliebigen Term stehen und muss nicht selbst eine natürliche Zahl darstellen.

Terme, Substitutionen und Regeln

Aus einer Menge Σ von Funktionssymbolen und einer unendlichen Variablenmenge 𝒱 wird die Termmenge 𝒯(Σ, 𝒱) induktiv definiert:

• Jede Variable und jedes nullstellige Funktionssymbol, also jede Konstante, ist ein Term. • Sind t₁, …, tₙ Terme und ist f ein n-stelliges Funktionssymbol, dann ist auch f(t₁, …, tₙ) ein Term.

Eine Substitution ordnet bestimmten Variablen neue Terme zu. Sie wirkt auf einen Term, indem jedes Vorkommen einer betroffenen Variable ersetzt wird. Für σ = {x/f(x,y)} und t = g(x) entsteht beispielsweise tσ = g(f(x,y)).

Ein Term t matcht einen Term s, wenn eine Substitution σ existiert, für die tσ = s gilt. So matcht g(x) den Term g(f(x,y)).

Eine Termersetzungsregel ist ein Paar l → r aus zwei Termen l und r. Dabei darf die linke Seite l keine Variable sein. Außerdem darf auf der rechten Seite r keine Variable vorkommen, die nicht bereits in l enthalten ist.

Ablauf einer Termersetzung

Die Funktionsweise eines TES wird durch die Termersetzungsrelation →ᴿ beschrieben. Passt die linke Seite einer Regel auf einen vollständigen Term s oder auf einen Teilterm von s, darf dieser passende Teil durch die rechte Seite ersetzt werden. Daraus entsteht ein neuer Term t.

Für die Regel f(x,y) → x gelten beispielsweise folgende Ersetzungen:

• f(s(y),g(x)) → s(y) • g(f(a,b)) → g(a) • f(f(a,b),c) kann in einem Schritt entweder zu f(a,c) oder zu f(a,b) ausgewertet werden.

Formal gilt s →ᴿ t, wenn es eine Substitution σ und eine Regel l →ᴿ r aus 𝓡 gibt, sodass s den Term lσ enthält. Der Term t enthält an derselben Stelle rσ und stimmt an allen übrigen Stellen mit s überein. Weil in einem Term mehrere passende Stellen oder Regeln vorhanden sein können, ist der nächste Auswertungsschritt nicht immer eindeutig.

Terminierung und Konfluenz

Bei der Terminierung fragt man, ob ein TES 𝓡 einen Term besitzt, der eine unendliche Auswertungskette s →ᴿ s₁ →ᴿ s₂ →ᴿ … erlaubt. Sind sämtliche Ableitungen aller Terme endlich, heißt 𝓡 terminierend oder fundiert. Da Termersetzungssysteme turingvollständig sind, ist die Terminierungsfrage im Allgemeinen unentscheidbar. Für viele konkrete Systeme kann die Terminierung dennoch automatisch nachgewiesen werden.

Ein allgemeiner Nachweis sucht eine fundierte Ordnung ≻, für die →ᴿ ⊆ ≻ gilt und bei jeder Regel l →ᴿ r die Beziehung l ≻ r erfüllt ist. Die Ordnung muss stabil sein, also bei Substitutionen erhalten bleiben, und monoton sein, also auch dann erhalten bleiben, wenn l und r als Teilterme eines größeren Terms auftreten. Weitere Verfahren interpretieren Terme beispielsweise als Polynome oder Matrizen oder untersuchen die Abhängigkeiten zwischen Funktionssymbolen.

Konfluenz bedeutet, dass zwei Terme, die auf unterschiedlichen Wegen in mehreren Schritten aus demselben Ausgangsterm entstehen, später stets wieder zu einem gemeinsamen Term weitergeführt werden können. Damit hängt die Frage zusammen, ob dieselbe Eingabe immer dasselbe Ergebnis beziehungsweise eine eindeutige Normalform liefert. Auch Konfluenz ist im Allgemeinen unentscheidbar.

Ein terminierendes und zugleich konfluentens TES heißt konvergent. In einem solchen System besitzt jeder Term eine eindeutige Normalform, also ein Ergebnis, auf das keine Regel mehr angewendet werden kann. Für ein bereits als terminierend bekanntes TES ist entscheidbar, ob es konfluent ist.

Wortproblem und weitere Anwendungen

Ein Termgleichungssystem 𝓔 ist eine Menge von Gleichungen zwischen Termen. Das Wortproblem für 𝓔 fragt, ob eine Gleichung s = t unter der Voraussetzung gilt, dass alle Gleichungen aus 𝓔 wahr sind. Die Gruppenaxiome lassen sich zum Beispiel so kodieren:

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

Dabei bezeichnet das zweistellige Funktionssymbol f die Gruppenverknüpfung, i liefert inverse Elemente und die Konstante e steht für das neutrale Element. Gefragt werden kann dann etwa, ob i(e) = e oder i(i(x)) = x gilt.

Zur Lösung konstruiert man möglichst ein äquivalentes und konvergentes TES 𝓡. Äquivalent bedeutet hier: s = t gilt genau dann, wenn s ↔*ᴿ t gilt. Das Zeichen ↔*ᴿ besagt, dass die Regeln beliebig oft und in beiden Richtungen angewendet werden dürfen. Anschließend wertet man s und t mit →ᴿ aus, bis keine weitere Ersetzung möglich ist. Wegen der Terminierung endet dieser Vorgang; wegen der Konfluenz ist der gewählte Auswertungsweg unerheblich. Entstehen für s und t dieselben Normalformen, gilt s = t bezüglich 𝓔.

Das Wortproblem ist im Allgemeinen unentscheidbar. Daher kann nicht für jedes Gleichungssystem ein entsprechendes konvergentes TES gefunden werden. Das Knuth-Bendix-Vervollständigungsverfahren versucht, aus einer Gleichungsmenge und einer fundierten Termordnung ein äquivalentes, konvergentes TES zu erzeugen. Weder seine Terminierung noch sein Erfolg sind garantiert. Für die genannten Gruppenaxiome liefert es im Erfolgsfall unter anderem die Regeln i(e) → e, i(i(x)) → x und i(f(x,y)) → f(i(y),i(x)) sowie Regeln für das neutrale Element, inverse Elemente und die Assoziativität.

TES werden außerdem zur Terminierungsanalyse von Programmen eingesetzt: Programme höherer Programmiersprachen werden in Termersetzungssysteme umgewandelt, auf die bewährte Terminierungsverfahren angewendet werden können. Das an der RWTH Aachen entwickelte Werkzeug AProvE hat dies für Prolog und Haskell umgesetzt. Die Behandlung imperativer und objektorientierter Sprachen wie Java wird als Gegenstand aktueller Forschung beschrieben.