LbP Unifikation

Begriff

Unifikation bedeutet Vereinheitlichen oder Passendmachen von zwei Termen. Es ist dem Musterabgleich (pattern matching) sehr verwandt, aber nicht identisch.

Die Paarbildung, die zueinander passende Terme eingehen, darf nicht mit einer Wertzuweisung verwechselt werden. Unifikation ist vielmehr eine bilaterale Angelegenheit.

Algorithmus

Input: Zwei Terme T_1 und T_2, die unifiziert werden sollen.
Output: \Theta, der allgemeinste Unifikator von T_1 und T_2, oder Fehler.
Algorithmus:

Initialisiere die Substitution \Theta als leere Menge.

Initialisiere den Stapel mit der Gleichung T_1=T_2, und Fehler mit false.

Solange der Stapel nicht leer ist und nicht Fehler tue:

Pop X=Y vom Stapel

Falls

(1) X eine Variable ist, die nicht in Y vorkommt:

Substituiere X durch Y im Stapel und in \Theta.

Füge X=Y in \Theta an.

(2) Y eine Variable ist, die nicht in X vorkommt:

Substituiere Y durch X im Stapel und in \Theta.

Füge Y=X in \Theta an.

(3) X und Y identische Konstanten oder Variablen sind:

Setzte fort.

(4) X ist f(X_1,\ldots,X_n) und Y ist f(Y_1,\ldots,Y_n), wobei f ein Funktor

und n>0 sind: Push X_i=Y_i, i=1,\ldots,n, auf den Stapel.

(5) Sonst setze Fehler gleich true.

Wenn Fehler, dann gib no aus, sonst \Theta.

Der sog. occur check "sitzt" in der fett hervorgehobenen Formulierung "... die nicht in ... vorkommt." Ein solcher Test kann verhindern, dass der Algorithmus versucht, X durch f(X) zu substituieren.

In praktischen Prolog-Implementationen wird eine solche Überprüfung aus Effizienzgründen weggelassen, was schliesslich zu einem Abbruch der Berechnung oder sogar einem Systemabsturz führt. Wir erhalten einen StackOverflowError.