Unifikacja (informatyka)
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.
Kod
[edytuj | edytuj kod]Kod dla prostoty prezentacji nie zajmuje się w sposób szczególny przypadkiem, kiedy po jednej stronie występuje ta sama zmienna co po drugiej.
type utree = Var of string | Const of string | Unary of string * utree | Binary of string * utree * utree ;; let rec find_var sv = function Var v -> if v = sv then true else false | Const c -> false | Unary (op,a) -> find_var sv a | Binary (op,a,b) -> (find_var sv a) or (find_var sv b) ;; exception NotUnificable ;; let ureplace sv rt t = let rec ureplace_aux = function Var v -> if sv = v then rt else Var v | Const c -> Const c | Unary (op,a) -> Unary (op,ureplace_aux a) | Binary (op,a,b) -> Binary (op,ureplace_aux a,ureplace_aux b) in List.map (function (a,b) -> ureplace_aux a, ureplace_aux b) t ;; let rec unify = function [] -> [] | (Var v, rt)::t -> (v,rt)::unify (ureplace v rt t) | (rt, Var v)::t -> (v,rt)::unify (ureplace v rt t) | (Unary (op1,a1),Unary (op2,a2))::t -> if op1 = op2 then unify ((a1,a2)::t) else raise NotUnificable | (Binary (op1,a1,b1), Binary (op2,a2,b2))::t -> if op1 = op2 then unify ((a1,a2)::(b1,b2)::t) else raise NotUnificable | _ -> raise NotUnificable ;; unify [Binary ("+", Var "x", Const "2"), Var "y"] ;; unify [(Binary ("+", Var "x", Const "2"), Binary ("+", Binary ("+", Var "z", Const "7"), Var "y"))] ;;
AC-unifikacja
[edytuj | edytuj kod]Unifikację można zmodyfikować włączając do niej reguły łączności (Associativity) i przemienności (Commutativity) niektórych symboli. Jeśli uznamy łączność i przemienność plusa (+ 2 3) i (+ 3 2) się unifikują, podobnie (+ 2 (+ 3 4)) i (+ (+ 4 2) 3). W takim wypadku zamiast drzew używa się w praktyce multizbiorów: (+ {2, 3, 4}) i (+ {4, 2, 3}) są oczywiście unifikowalne.
AC-unifikacja nie jest jednak jednoznaczna, np. (+ x (+ 2 y)) i (+ 2 (+ 3 4)) można unifikować równie dobrze przez x=3 y=4 jak przez x=4 y=3.
Zobacz też
[edytuj | edytuj kod]- unifikacja w znaczeniu technicznym.
- rezolucja