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

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

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ż

• unifikacja w znaczeniu technicznym.
• rezolucja