Unifikacja (informatyka)

Z Wikipedii, wolnej encyklopedii
Przejdź do nawigacji Przejdź do wyszukiwania

Unifikacja (ang. unification) to 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]