LbP Unifikation

Wiki-Quelltext dieser Seite.

<language>Prolog</language>
===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 <math>T_1</math> und <math>T_2</math>, die unifiziert werden sollen.<br />
''Output'':	<math>\Theta</math>, der allgemeinste Unifikator von <math>T_1</math> und <math>T_2</math>, oder Fehler.<br />
''Algorithmus'':	
:Initialisiere die Substitution <math>\Theta</math> als leere Menge.
:Initialisiere den Stapel mit der Gleichung <math>T_1=T_2</math>, und Fehler mit <tt>false</tt>.
:Solange der Stapel nicht leer ist und nicht Fehler tue:
::Pop <math>X=Y</math> vom Stapel
::Falls	
:::(1) <math>X</math> eine Variable ist, '''die nicht in <math>Y</math> vorkommt''': <br />
::::Substituiere <math>X</math> durch <math>Y</math> im Stapel und in <math>\Theta</math>.
::::Füge <math>X=Y</math> in <math>\Theta</math> an.
:::(2) <math>Y</math> eine Variable ist, '''die nicht in <math>X</math> vorkommt''': 
::::Substituiere Y durch X im Stapel und in <math>\Theta</math>.
::::Füge <math>Y=X</math> in <math>\Theta</math> an.
:::(3) <math>X</math> und <math>Y</math> identische Konstanten oder Variablen sind:
::::Setzte fort.
:::(4) <math>X</math> ist <math>f(X_1,\ldots,X_n)</math> und <math>Y</math> ist <math>f(Y_1,\ldots,Y_n)</math>, wobei f ein Funktor 
::::und <math>n>0</math> sind: Push <math>X_i=Y_i, i=1,\ldots,n,</math> auf den Stapel.
:::(5) Sonst setze Fehler gleich <tt>true</tt>.
:Wenn Fehler, dann gib <tt>no</tt> aus, sonst <math>\Theta</math>.

Der sog. occur check "sitzt" in der fett hervorgehobenen Formulierung "'''... die nicht in ... vorkommt.'''" Ein solcher Test kann verhindern, dass der Algorithmus versucht, <tt>X</tt> durch <tt>f(X)</tt> 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 <tt>StackOverflowError</tt>.

<code id="4b8bd373aea6d">p(X,f(X)).</code>
<eval id="4b8bd373af23f">p(Z,Z).</run>