LbP Unifikation

Aus ProgrammingWiki

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.

p(X,f(X)).

p(Z,Z).

LbP Unifikation

Aus ProgrammingWiki

Begriff

Algorithmus

Ansichten

Persönliche Werkzeuge

Navigation

Suche

Werkzeuge