Unifikacja (informatyka) - Google

Unifikacja (informatyka)

Z Wikipedii

Skocz do: nawigacji, szukaj

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 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.

[edytuj] Kod

 Ta sekcja wymaga dopracowania zgodnie z zaleceniami edycyjnymi.
Należy w niej poprawić: {{{2}}}.
Po naprawieniu wszystkich błędów można usunąć tę wiadomość.

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"))]
;;

[edytuj] 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.

[edytuj] Zobacz też:


4000 GB w zsypie
Serwer, z którego nielegalnie można było pobrać 4000 gigabajtów nielegalnych gier, filmów, muzyki i programów zabezpieczyli policjanci z KWP. Administratorowi i właścicielowi serwera grozi do pięciu lat więzienia.
Społecznościowy antywirus?
Czy możliwe jest wykorzystanie potencjału społeczności internetowych, lub użytkowników sieci do ochrony komputera przed zagrożeniami płynącymi z sieci? Producent oprogramowania antywirusowego, Panda Security, właśnie takie rozwiązania planuje wprowadzić w swoich najnowszych produktach.
Mozilla aktualizuje Thunderbird'a
W ostatnią środę Mozilla udostępniła na swoich serwerach najnowszą wersję programu pocztowego Thunderbird 2.0.0.16, wzbogaconą o dziewięć zasadniczych poprawek.
Internetowy tablet z Firefoksem
Michael Arrington planuje stworzyć stylowy tablet, który służyć ma wyłącznie do surfowania w internecie.
Wielofunkcyjna stacja dokująca
Stacje dokujące i huby USB to urządzenia przygotowane z myślą o osobach, którym ciągle brakuje gniazd przyłączeniowych.
Linki: Strona gwna