Лекции по логическо програмиране

Умножение на субституции

нека ₁ и ₂ са субституции; дефинираме функция  (x) от множеството  на променливите в множеството от всички термове по следния начин:  (x) = (x₁)₂ за всяко x  ;

ще покажем, че  (x) е субституция, т.е.  (x)  x най-много за краен брой променливи x; за целта ще покажем, че за всяко x   ако

 (x)  x, то ₁ (x)  x или ₂ (x)  x; да допуснем противното –

 (x)  x и ₁ (x) = x, ₂ (x) = x за някоя променлива x  ; тогава

 (x) = (x₁)₂ = x₂ = x, което е противоречие; ясно е, че

₁ (x)  x или ₂ (x)  x е изпълнено само за краен брой

променливи x, тъй като ₁ и ₂ са субституции; така  (x)  x само за краен брой променливи x, т.е.  (x) е субституция; тази субституция наричаме произведение на субституциите ₁ и ₂, означаваме  = ₁₂; така x(₁₂) = (x₁)₂;

Y([X/Y][Y/a]) = (Y[X/Y])[Y/a] = Y[Y/a] = a;

така [X/Y][Y/a] = [X/a, Y/a];
ще покажем, че  =  =  за всяка субституция ;

действително за всяко x   имаме x() = (x) = x (от съответното твърдение за термове)   = ; също, за всяко x   имаме

действително, x()= x = x за всяка променлива x,

различна от X и Y; също X() = (X) = Y = X,

Y() = (Y) = X = Y; така  = ;

например [X/Y][Y/X] = [Y/X], [Y/X][X/Y] = [X/Y] и така

[X/Y][Y/X]  [Y/X][X/Y];
Твърдение: ако E е терм или безкванторна формула и ₁, ₂ са субституции, то E(₁₂) = (E₁)₂;

Доказателство: първо да разгледаме случая когато E е терм;

провеждаме индукция по постронието на E;

База: ако E е константа, то E(₁₂) = E, (E₁)₂ = E₂ = E 

E(₁₂) = (E₁)₂; ако E  , то E(₁₂) = (E₁)₂ от дефиницията за произведение на субституции;

Предположение: нека E = f (T₁, T₂, …, T_n) и твърдението е изпълнено за термовете T₁, T₂, …, T_n;

Стъпка: имаме E(₁₂) = f (T₁(₁₂), T₂(₁₂), …, T_n(₁₂)); от индукционното предположение T₁(₁₂) = (T₁₁)₂,

T₂(₁₂) = (T₂₁)₂, …, T_n(₁₂) = (T_n₁)₂; тогава

E(₁₂) = f ((T₁₁)₂, (T₂₁)₂, …, (T_n₁)₂) =

= (f (T₁₁, T₂₁, …, T_n₁))₂ = (E₁)₂;

сега да разгледаме случая когато E е безкванторна формула;

провеждаме индукция по построението на E;

База: нека E = p (T₁, T₂, …, T_n);

тогава E(₁₂) = p (T₁(₁₂), T₂(₁₂), …, T_n(₁₂)); тъй като

T₁, T₂, …, T_n са термове от по-горе T₁(₁₂) = (T₁₁)₂,

T₂(₁₂) = (T₂₁)₂, …, T_n(₁₂) = (T_n₁)₂;

така E(₁₂) = p ((T₁₁)₂, (T₂₁)₂, …, (T_n₁)₂) =

= (p (T₁₁, T₂₁, …, T_n₁))₂ = (E₁)₂;

ако E  П₀, E = true или E = fail, то E(₁₂) = E и (E₁)₂ = E₂ = E 

E(₁₂) = (E₁)₂;

Предположение: нека твърдението е изпълнено за безкванторните формули G, F₁, F₂, …, F_n (n > 2);

Стъпка:

ако E = G, то E(₁₂) = (G(₁₂)); от индукционното предположение G(₁₂) = (G₁)₂  E(₁₂) = ((G₁)₂) = ((G₁))₂ =

= ((G)₁)₂ = (E₁)₂;

ако E = F₁ & F₂ & … & F_n, то

E(₁₂) = F₁(₁₂) & F₂(₁₂) & … & F_n(₁₂); от индукционното предположение F₁(₁₂) = (F₁₁)₂, F₂(₁₂) = (F₂₁)₂, …,

F_n(₁₂) = (F_n₁)₂; така E(₁₂) = (F₁₁)₂ & (F₂₁)₂ & … & (F_n₁)₂ =

= (F_n₁ & F_n₁ & … & F_n₁)₂ = ((F₁ & F₂ & … & F_n)₁)₂ = (E₁)₂;

ако E = F₁  F₂  …  F_n, то

E(₁₂) = F₁(₁₂)  F₂(₁₂)  …  F_n(₁₂); от индукционното предположение F₁(₁₂) = (F₁₁)₂, F₂(₁₂) = (F₂₁)₂, …,

F_n(₁₂) = (F_n₁)₂; така E(₁₂) = (F₁₁)₂  (F₂₁)₂  …  (F_n₁)₂ =

= (F_n₁  F_n₁  …  F_n₁)₂ = ((F₁  F₂  …  F_n)₁)₂ = (E₁)₂;

Доказателство: нека x  ;

тогава x ((₁₂)₃) = (x(₁₂))₃ = ((x₁)₂)₃;

също x (₁(₂₃)) = (x₁)(₂₃) = ((x₁)₂)₃ – тук използваме, горното твърдение за терма (x₁);

така x ((₁₂)₃) = x (₁(₂₃)) за всяко x    (₁₂)₃ = ₁(₂₃);

нека ₁, ₂, …, _k (k  0) е редица от субституции; дефинираме произведение ₁₂…_k на ₁, ₂, …, _k с индукция по k;

База: при k = 0 под произведение на празната редица разбираме субституцията ;

Предположение: нека е дефинирано произведението

₁₂…_k-1, k  1;

Стъпка: дефинираме ₁₂…_k-1_k = (₁₂…_k-1)_k;

според тази дефиниция, произведение на една субституция е самата субституция, произведение на две субституции е произведението на субституции от по-горе;
нека k  0, l  0; с индукция по l ще покажем, че

₁₂…_k_k+1_k+2…_k+l = (₁₂…_k)(_k+2…_k+l);

База: при l = 0 ₁₂…_k = (₁₂…_k) и твърдението е изпълнено;

Предположение:

нека ₁₂…_k_k+1_k+2…_k+l-1 = (₁₂…_k)(_k+2…_k+l-1), l  1;

Стъпка: тогава ₁₂…_k_k+1_k+2…_k+l = (₁₂…_k_k+1_k+2…_k+l-1)_k+l;

от индукционното предположение (₁₂…_k_k+1_k+2…_k+l-1)_k+l =

= ((₁₂…_k)(_k+2…_k+l-1))_k+l; от асоциативността на умножението на субституции ((₁₂…_k)(_k+2…_k+l-1))_k+l = (₁₂…_k)((_k+2…_k+l-1)_k+l) =

= (₁₂…_k)(_k+2…_k+l);