LbP Unifikation

Aus ProgrammingWiki

Wechseln zu: Navigation, Suche

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 und , die unifiziert werden sollen.
Output: , der allgemeinste Unifikator von und , oder Fehler.
Algorithmus:

Initialisiere die Substitution als leere Menge.
Initialisiere den Stapel mit der Gleichung , und Fehler mit false.
Solange der Stapel nicht leer ist und nicht Fehler tue:
Pop vom Stapel
Falls
(1) eine Variable ist, die nicht in vorkommt:
Substituiere durch im Stapel und in .
Füge in an.
(2) eine Variable ist, die nicht in vorkommt:
Substituiere Y durch X im Stapel und in .
Füge in an.
(3) und identische Konstanten oder Variablen sind:
Setzte fort.
(4) ist und ist , wobei f ein Funktor
und sind: Push auf den Stapel.
(5) Sonst setze Fehler gleich true.
Wenn Fehler, dann gib no aus, sonst .

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.

Persönliche Werkzeuge