LOGIKA ALGORYTMICZNA 4. Unifikacja. Podstawieniem nazywamy zbi´or sko´nczony postaci {t

LOGIKA ALGORYTMICZNA 4. Unifikacja.

Podstawieniem nazywamy zbi´or sko´nczony postaci {t₁/v₁, ..., t_n/v_n}, gdzie v_i s¸a parami r´o˙znymi zmiennymi, a t_i s¸a termami z t_i 6= v_i, 1 ≤ i ≤ n. Je´sli wszystkie t_i s¸a termami podstawowymi, to podstawienie nazywa si¸e podstawowym. Przez ε oznaczamy puste podstawienie.

Je´sli E jest pewnym wyra˙zeniem (np. termem lub formu l¸a), a θ = {t1/v1, ..., tn/vn} jest podstawieniem, to przez Eθ oznaczamy wyra˙zenie otrzymane z E przez zamian¸e ka˙zdego wyst¸epowania v_i na t_i. Wtedy Eθ nazywa si¸e przyk ladem wyra˙zenia E.

Z lo˙zeniem podstawie´n θ = {t1/x1, ..., tn/xn} i λ = {u1/y1, ..., um/ym} nazywa si¸e

podstawienie (oznaczane przez θ◦λ) otrzymane ze zbioru {t₁λ/x₁, ..., t_nλ/x_n, u₁/y₁, ..., u_m/y_m} przez wykre´slanie wszystkich sk ladnik´ow t_iλ/x_i, gdzie t_iλ = x_i, i wszystkich sk ladnik´ow

ui/yi, gdzie yi ∈ {x1, ..., xn}.

4.1. Uwagi. (a) θ ◦ ε = ε ◦ θ = θ;

(b) (θ ◦ λ) ◦ µ = θ ◦ (λ ◦ µ);

(c) Dla ka˙zdego wyra˙zenia E zachodzi E(θ ◦ λ) = (Eθ)λ.

4.2. Zadania. Znale´z´c θ ◦ λ dla

(a) θ = {f (y)/x, z/y} i λ = {a/x, b/y, y/z};

(b) θ = {g(z)/x, f (x)/y} i λ = {g(y)/x, r(a, z)/y, b/z}.

Podstawienie θ nazywa si¸e unifikatorem zbioru wyra˙ze´n {E₁, ..., E_k} je´sli E₁θ = E₂θ = ... = E_kθ. Unifikator θ nazywa si¸e najog´olniejszym, je´sli dla ka˙zdego unifikatora λ zbioru {E1, ..., Ek} istnieje podstawienie µ takie, ˙ze λ = θ ◦ µ.

Rozpatrzmy zbi´or litera l´ow {L₁, L₂, ..., L_n} taki, ˙ze dla pewnego symbolu rela- cyjnego P wszystkie L_imaj¸a posta´c P (t₁, ..., t_l) lub wszystkie L_imaj¸a posta´c ¬P (t₁, ..., t_l).

Znajd´zmy pierwsz¸a z lewej pozycj¸e, na kt´orej pewne Li i Lj maj¸a r´o˙zne symbole. W ka˙zdym L_i pozycja ta okre´sla pocz¸atek pewnego termu t⁰_i (wyst¸epuj¸acego w L_i jako podterm). Zbi´or {t⁰₁, ..., t⁰_n} nazywa si¸e zbiorem niezgodno´sci wyra˙ze´n L₁, L₂, ..., L_n.

4.3. Zadania. Znale´z´c zbi´or niezgodno´sci w W :

(a) W = {¬R(f (x), a), ¬R(f (x), f (x)), ¬R(f (x), g(b))}, (b) W = {Q(x, r(a, f (x, y))), Q(x, r(a, g(x))), Q(x, r(a, a))}.

(c) W = {P (x, f (z)), P (x, a), P (x, g(h(x)))},

Algorytm unifikacji. Niech W b¸edzie pewnym zbiorem litera l´ow.

Krok 0. Niech W₀ := W , ε₀ := ε.

Krok k + 1. Niech σk b¸edzie podstawieniem zbudowanym na kroku k i niech W_k := W σ_k.

Ruch 1. Je´sli wszystkie litera ly zbioru W_k s¸a r´owne, to nast¸epuje zako´nczenie (STOP); σk jest najog´olniejszym unifikatorem zbioru W . Je´sli zbi´or Wk zawiera r´o˙zne litera ly, to niech D_k b¸edzie zbiorem niezgodno´sci w W_k.

Ruch 2. Je´sli D_k zawiera zmienn¸a v_k i term t_k, nie zawieraj¸acy v_k, to wykonujemy Ruch 3. W przypadku, gdy takiej pary nie ma, nast¸epuje zatrzymanie algorytmu:

zbi´or W_k nie jest unifikowalny.

Ruch 3. Niech σ_k+1 := σ_k◦ {t_k/v_k} i W_k+1 := W_k{t_k/v_k}. Przej´scie do Kroku

1

k + 2.

4.4. Twierdzenie unifikacji. Je´sli zbi´or litera l´ow W jest unifikowalny, to algo- rytm unifikacji ko´nczy prac¸e w trakcie wykonywania Ruchu 1 pewnego kroku k + 1.

Wtedy σ_k jest najog´olniejszym unifikatorem. Je´sli W_k nie jest unifikowalny, to algo- rytm unifikacji ko´nczy prac¸e w trakcie wykonywania Ruchu 2 pewnego kroku k + 1.

4.5. Zadanie. Znale´z´c najog´olniejszy unifikator zbioru W (w przypadku, gdy zbi´or jest unifikowalny):

(a) W = {P (a, x, f (g(y))), P (z, f (z), f (u))}, (b) W = {P (f (a), x, z), P (y, y, g(x))}, (c) W = {P (f (a), g(x)), P (y, y)}.

2