Unifikacja (informatyka)
Z Wikipedii, wolnej encyclopedia
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.
Ten artykuł od 2021-04 wymaga zweryfikowania podanych informacji. |
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.