Unifikation: Terme durch Variablenbelegung angleichen

Unifikation ist ein Verfahren aus der Informatik, das zwei Terme durch eine Substitution (Variablenbelegung) gleich macht: Man sucht eine Ersetzung, nach der beide Ausdrücke identisch werden. Entwickelt wurde der Algorithmus 1965 von John Alan Robinson als Kern der Resolution – der Beweistechnik, auf der die logische Programmierung aufbaut.

Wie Unifikation arbeitet

Gegeben sind zwei Terme, zum Beispiel f(X, a) und f(b, Y). Der Unifikator ersetzt Variablen durch Terme, sodass beide Ausdrücke übereinstimmen: X = b, Y = a liefert in beiden Fällen f(b, a). Regeln dabei:

Eine Variable kann mit einem beliebigen Term unifiziert werden – auch mit einer Funktion wie g(c).
Zwei verschiedene Konstanten oder Funktionssymbole passen nie zusammen (a und b unifizieren nicht).
Die Substitution muss konsistent sein: Ist X schon an a gebunden, darf eine zweite Bindung X = b nicht mehr entstehen.
Der Occurs-Check verhindert zyklische Bindungen wie X = f(X) (kein endlicher Term).

Der Algorithmus findet immer den allgemeinsten Unifikator (Most General Unifier, MGU) – die Substitution mit den wenigsten Annahmen. Alle anderen Lösungen entstehen daraus durch weitere Ersetzungen.

Einsatz in Prolog und darüber hinaus

In Prolog geschieht Unifikation bei jedem Aufruf: Ein Anfrageziel wie grosseltern(anna, Z) wird mit dem Kopf einer Regel unifiziert, Variablen werden dabei gebunden. Derselbe Mechanismus steckt in:

der Typinferenz funktionaler Sprachen (Hindley-Milner, etwa bei Haskell und OCaml),
Musterabgleich in Logik- und Constraintsystemen,
deduktiven Datenbanken und automatischen Beweisern.

Als mathematische Grundlage dient die Termersetzung (Rewriting); verwandt, aber ein anderes Ziel hat die Anti-Unifikation (größte gemeinsame Verallgemeinerung zweier Terme).