unifikacja

Unifikacja (ang. unification) – operacja na dwóch lub więcej drzewach, która znajduje takie przyporządkowanie zmiennych, że drzewa te są równe. Np. (w notacji lispowej): (+ x 2) i (+ (+ z 7) y) są unifikowalne dla y=2 i x=(+ z 7). (+ x 2) i (+ y 3) nie są unifikowalne. Podobnie unifikowalne nie są (* x 2) i (+ x x) ani (+ 2 3) i (+ 3 2) – unifikacja dotyczy tylko symboli, a nie ich znaczenia. Unifikator to wygenerowany w ten sposób zbiór przyporządkowań. Algorytm wygląda tak: * jeśli po jednej stronie jest zmienna, dorzucamy ją do unifikatora i zamieniamy wszystkie jej wystąpienia na to co występuje po drugiej stronie. Należy zająć się też przypadkiem szczególnym, kiedy druga strona zawiera wystąpienie tej zmiennej – zależnie od implementacji x i (+ x 1) mogą się unifikować, nie unifikować, bądź też powodować niezamierzone zapętlenie. * jeśli po obu stronach są te same stałe, unifikacja się powiodła * jeśli po obu stronach są te same relacje n-arne, unifikacja się powiodła o ile powiodła się unifikacja wszystkich n-poddrzew, przy czym unifikator dotyczy wszystkich poddrzew. * jeśli po obu stronach są różne stałe bądź relacje, unifikacja się nie powiodła.