Ербранови алгебрични структури

Ербранови алгебрични структури

Нека  = ((c₁, c₂, …, c_r), (f₁, f₂, …, f_m), (T₁, T₂, …, T_k)) е език от първи ред.

При това, нека r  1, т.е. в езика има константни символи.

Алгебрична система _E = (H, (a₁, a₂, …, a_r), (F₁, F₂, …, F_m), (P₁, P₂, …, P_k)

в  се нарича ербранова, ако тя изпълнява следните условия:

1. 
   H е множеството от всички основни термове в .
   
2. 
   a_i = c_i, i = 1, 2, …, r.
   
3. 
   За всяко i = 1, 2, …, m, ако f_i е n-местен функционален символ, то F_i (₁, ₂, …, _n) = f_i (₁, ₂, …, _n) за произволни основни термове
   

Естествено, всеки език  има повече от една ербранова алгебрична структура, тъй като за интепретацията на предикатните символи няма ограничения от дефиницията.

ербранова _E в . Тогава е в сила равенството

Доказателство: индукция по построението на .

Нека  е константа,  = c_i, i  { 1, 2, …, r }. Тогава v () = a_i = c_i и

 (X₁/v (X₁), X₂/v (X₂), …, X_n/v (X_n)) = c_i.

Нека  е променлива,  = X_i, i  { 1, 2, …, n }. Тогава v () = v (X_i) и

 (X₁/v (X₁), X₂/v (X₂), …, X_n/v (X_n)) = v (X_i).

Нека  = f_i (₁, ₂, …, _l), където f_i е l-местен функционален символ и твърдението е изпълнено за термовете ₁, ₂, …, _l.

Тогава v () = F_i (v (₁), v (₂), …, v (_n)) = F_i (₁ (X₁/v (X₁), …, X_n/v (X_n)), …,

_l (X₁/v (X₁), …, X_n/v (X_n))) = f_i (₁ (X₁/v (X₁), …, X_n/v (X_n)), …,

_l (X₁/v (X₁), …, X_n/v (X_n))) = f_i (₁, ₂, …, _l)(X₁/v (X₁), X₂/v (X₂), …, X_n/v (X_n)) =  (X₁/v (X₁), X₂/v (X₂), …, X_n/v (X_n)). Използвали сме индукционното предположение и дефиницията за ербранова структура.

ербранова _E в , то v () = .

_l (X₁, X₂, …, X_n)), j  { 1, 2, …, k } е атомарна формула в  (T_j е l-местен функционален символ) и v е оценка в ербранова _E в .

Тогава _E, v A  P_j (₁, ₂, …, _l) = true,

където _j = _j (X₁/v (X₁), X₂/v (X₂), …, X_n/v (X_n)), j = 1, 2, …, n.

₁, ₂, …, _l са основни термове. Тогава _E A  P_j (₁, ₂, …, _l) = true.

множеството от всички основни атоми, които са вярни в _E.

Ясно е, че _E еднозначно определя . Ще покажем, че е в сила и обратното. Нека M е произволно множество от основни атоми.

Определяме ербранова алгебрична система _E, като задаваме интерпретация на предикатните символи:

за всяко j  { 1, 2, …, k}, ако T_j е n-местен предикатен символ, то

P_j (₁, ₂, …, _n) = true, ако T_j (₁, ₂, …, _n)  M,

P_j (₁, ₂, …, _n) = false, ако T_j (₁, ₂, …, _n)  M

за прозволни основни термове ₁, ₂, …, _n.

От горното следствие, _E T_j (₁, ₂, …, _n)  P_j (₁, ₂, …, _n) = true 

 T_j (₁, ₂, …, _n)  M  M = . По този начин можем да отъждествяваме всяка ербранова алгебрична система с множеството от вярните основни атоми в нея. Нека M е множество от основни атоми.

Нека F е формула в . Бележим M F, ако F, където е ербрановата алгебрична система съответна на M.

Още казваме, че M е ербранов модел на F.

Естествено, ако A е основен атом, то M A  A  M.

Ако v е произволна оценка бележим M, v F, ако , v F.

С M* ще бележим множеството от всички основни атоми в .
Нека C е хорнова клауза, C = X₁X₂…X_s (A (X₁, X₂, …, X_s) 

 B₁ (X₁, X₂, …, X_s)  B₂ (X₁, X₂, …, X_s)  … B_n (X₁, X₂, …, X_s)).

Означаваме с C формулата A  B₁  B₂  … B_n.

Всяка формула D = C (X₁/₁, X₂/₂, …, X_n/_n), където ₁, ₂, …, _n са основни термове, наричаме частен случай на хорновата клауза C.

Основният атом A (X/) наричаме глава на частния случай D.

Крайното множество от основни атоми { B_i (X/) | i  { 1, 2, …, n } } наричаме опашка на частния случай D. Главата на D бележим с head (D), а опашката бележим с tail (D).

Тогава M C  M D за всеки частен случай D на C.

Доказателство: нека C = X₁X₂…X_s (A (X)  B₁ (X)  B₂ (X)  …

 B_n (X)). Нека M C и D е частен случай на C, D = C (X/).

Нека v е оценка, такава че v (X_i) = _i, i = 1, 2, …, s.

Имаме M, v C  M, v C  M, v A или М, v B₁ или …или

 M A (X/) или М, v B₁ (X/) или …или M, v B_n (X/) 

 M A (X/)  B₁ (X/)  … B_n (X/), т.е. M C (X/)  M D.

Обратно, нека M D за всеки частен случай D на C.

Ще покажем, че M C. Достатъчно е да покажем, че M C.

Нека v е оценка. Нека v (X_i) = _i, i = 1, 2, …, n. Естествено, C (X/) е частен случай на C. Имаме M C (X/)  M A (X/) или

Тогава M P  M е модел на всеки частен случай на

хорнова клауза от P.

Доказателство: M P  М е модел на всяка хорнова клауза от P 

 M е модел на всеки частен случай на хорнова клауза от P.
Твърдение: Нека M  M*. Нека C е хорнова клауза, D е частен

случай на C. Тогава M D  tail (D)  M  head (D)  M.

Доказателство: нека D = A  B₁  B₂  … B_n, където A, B_i,

i = 1, 2, …, n са основни атоми. Тогава M D  M A или М B₁

или …или M B_n  А  М или B₁  M или …или B_n  M 

 head (D)  M или tail (D)  M  tail (D)  M  head (D)  M.

Доказателство: ще покажем, че M* е ербранов модел на P.

Имаме M* P  M* е модел на всеки частен случай на

хорнова клауза от P  tail (D)  M*  head (D)  M* за всеки частен случай D на хорнова клауза от P. Последното е изпълнено, тъй като M* се състои от всички основни атоми.

Доказателство: нека D е частен случай на хорнова клауза от P.

Да предположим, че tail (D)  M_P. Нека M е произволен ербранов

модел на P. Имаме M_P  M  tail (D)  M  head (D)  M, тъй като M е ербранов модел на P. Така head (D) лежи във всеки ербранов модел на P  head (D)  M_P. Така M_P P.

Моделът M_P на P се нарича най-малък ербранов модел на P.
Теорема: М_P = OUTPUT (P) за всяка логическа програма P.

Доказателство: нека A  OUTPUT (P). Тогава P A. Имаме M_P P 

 M_P A  A  M_P. Така OUTPUT (P)  M_P.

За обратното включване ще покажем, че OUTPUT (P) е модел на P.

Нека D е частен случай на хорнова клауза от P.

Нека tail (D)  OUTPUT (P). Тогава P B за всеки основен

атом B  tail (D). Ще покажем, че P head (D).

Нека  е произволен модел на P. Тогава  е модел на всеки частен случай на всяка хорнова клауза от P   D   B за някоя

B  tail (D) или  head (D). Oт друга страна, P B за всяко B  tail (D),  P   B за всеки B  tail (D). Така  head (D).

Получихме, че P head (D), т.е. head (D)  OUTPUT (P) 

 OUTPUT (P) е ербранов модел на P  M_P  OUTPUT (P).

Като комбинираме двете включвания получаваме М_P = OUTPUT (P).

подмножества на M*. Да напомним, че P (M*) = (P (M*), , ) е

област на Скот. Дефинираме изображение T_P : P (M*)  P (M*) по следния начин: T_P (M) = { A | съществува частен случай D на хорнова клауза от P, такъв че A = head (D) и tail (D)  M }.
Твърдение: Дефинираното T_P е непрекъснато изображение на

P (M*) в P (M*).

Доказателство: първо ще покажем, че T_P е монотонно.

Нека M  N. Нека A  T_P (M). Тогава съществува частен случай D на хорнова клауза от P, такъв че A = head (D) и tail (D)  M 

съществува частен случай D на хорнова клауза от P, такъв че

A = head (D) и tail (D)  N  A  T_P (N). Така T_P (M)  T_P (N).

Нека M₀  M₁  … M_k  …е монотонна редица от елементи на P (M*).

Достатъчно е да покажем, че T_P ( ) = .

Естествено, от монотонността имаме  T_P ( ).

Нека A  T_P ( ). Тогава съществува частен случай D на хорнова клауза от P, такъв че A = head (D) и tail (D)  . Тъй като tail (D) е крайно множество, то съществува k  N, такова че tail (D)  M_k.

При това положение, A  T_P (M_k). Така T_P ( )  и твърдението е доказано.
От теоремата на Кнастер-Тарски T_P притежава най-малка неподвижна точка. Да я означим с L_P, L_P  M*. Да напомним, че L_P също е най-малка квазинеподвижна точка.
Твърдение: Нека M  M* е ербранов модел на P. Тогава T_P (M)  M.

Доказателство: нека A  T_P (M). Тогава съществува частен случай C на хорнова клауза от P, такъв че A = head (D) и tail (D)  M. Тъй като M е ербранов модел на P, то M е модел на D, tail (D)  M  A  M.

Така T_P (M)  M.
Следствие: L_P  M_P.

Доказателство: тъй като M_P е модел на P, то T_P (M_P)  M_P  M_P е квазинеподвижна точка на T_P  L_P  M_P, тъй като L_P е най-малка квазинеподвижна точка на T_P.

Доказателство: нека D е частен случай на хорнова клауза от P.

Да предположим, че tail (D)  M. Тогава head (D)  T_P (M) 

head (D)  M. Така M е ербранов модел на P.

Доказателство: имаме T_P (L_P)  L_P, тъй като L_P е квазинеподвижна точка на T_P. Тогава L_P е ербранов модел на P  М_P  L_P.

OUTPUT (P)  M наричаме твърдение за частична коректност на програмата P. От горните твърдения е ясно, че такова твърдение следва от всяко едно от следните твърдения: T_P (M)  M, M е модел на P.

Твърдение от вида OUTPUT (P) = M наричаме твърдение за тотална коректност на програмата P. Твърденията за тотална коректност са значително по-силни и се доказват по-трудно.
Ще разгледаме един пример. Нека P е следната логическа програма:

is_int (0) & X (is_int (f (X))  is_int (X)). В PROLOG тази програма се записва по следния начин:

is_int (0).

is_int (f (X)) :- is_int (X).

Нека M = { is_int (fⁿ (0)) | n = 0, 1, …}.

Ще покажем, че OUTPUT (P)  M.

Както отбелязахме, достатъчно е да покажем, че T_P (M)  M.

Нека A  T_P (M). Тогава съществува частен случай D на хорнова клауза от P, такъв че A = head (D) и tail (D)  M. Ако D е частен случай на първата клауза, то D = is_int (0), tail (D) = , A = is_int (0)  A  M.

Нека D е частен случай на втората клауза. Имаме tail (D) = { is_int (X/) }, където  e основен терм, tail (D)  M  is_int (X/)  M   = fⁿ (0) за някое n  N. При това положение, A = head (D) = is_int (f (X))(X/) =

= is_int (f (X))(X/fⁿ (0)) = is_int (fⁿ⁺¹ (0))  M.

Така T_P (M)  M  OUTPUT (P)  M.
Схеми на програми.
Стандартни схеми
Нека  = ((c₁, c₂, …, c_r), (f₁, f₂, …, f_m), (T₁, T₂, …, T_k)) е език от първи ред.

Считаме, че функционалният символ f_i е a_i-местен, i = 1, 2, …, m и предикатният символ T_j е b_j-местен, j = 1, 2, …, k.

Нека разполагаме с изброимо множество от променливи, които ще означаваме с главни латински букви (X, Y, …), евентуално с индекси.
Дефинираме синтактичното понятие оператор в езика :

1. 
   Оператор за присвояване - l. Z_i := Z_j, l  N, Z_i, Z_j са променливи.
   
2. 
   Оператор за присвояване на константа - l. Z_i := c_j, l  N, Z_i е променлива, j  { 1, 2, …, r }.
   
3. 
   Оператор за присвояване на резултат от операция -
   

1. 
   Оператор за условен преход - l. if T_j (Z₁, Z₂, …, ) then l₁ else l₂,
   

1. 
   Оператор за безусловен преход - l. goto l₁, l, l₁  N. Тук числото l₁ се нарича адрес на прехода.
   
2. 
   Оператор за край - l. stop, l  N.
   

Числото l  N във всичките случаи се нарича етикет на оператора.

(итеративна схема) в езика :

Input (X₁, X₂, …, X_n)

Output Y

O₀; O₁; …; O_q;

end
Тук n  1 и X₁, X₂, …, X_n са различни помежду си входни променливи,

Y е променлива, O_i е оператор в  за всяко i  { 0, 1, …, q }. При това за тези оператори са в сила следните ограничения:

1. 
   Етикетът на операторът O_l е l, l = 0, 1, …, q.
   
2. 
   Адресите на преходите във всички оператори са в интервала [0, q].
   
3. 
   O_q е оператор за край, оператор за условен преход или оператор за безусловен преход.
   

Ще дадем пример за стандартна схема.

Нека  = (c; f, g; T), където f е едноместен, g е двуместен, T е едноместен.

Тогава следният синтактичен обект е коректна стандартна схема:

Input (X)

Output Y

0. 
   Y := c;
   
1. 
   if T (x) then 5 else 2;
   
2. 
   Y := g (X, Y);
   
3. 
   X := f (X);
   
4. 
   goto 1;
   
5. 
   stop;
   

Естествено, има смисъл да говорим за семантиката на схема едва когато са интерпретирани константите, функционалните символи и предикатните символи на езика .

Нека  = (H, (p₁, p₂, …, p_r), (F₁, F₂, …, F_m), (P₁, P₂, …, P_k)) е алгебрична система в . В контекста на схемите на програми, алгебричните системи се наричат тип данни. Нека S е стандартна схема от горния общ вид.

Нека Z₁, Z₂, …, Z_p са всички променливи, които участват в S.

Ще дефинираме две изображения val : N x Hⁿ x { Z₁, Z₂, …, Z_p }  H и

count : N x Hⁿ  [0, q] с едновременна индукция по първия аргумент.

Неформално val ще определя съдържанието на променливите на всяка стъпка от изпълнението на схемата, а count ще определя етикетът на следващия оператор за изпълнение отново на всяка стъпка от изпълнението.

Нека s = (s₁, s₂, …, s_n)  Hⁿ, Z  { Z₁, Z₂, …, Z_p }.

1. 
   val (0, s, Z) = s_i, ако Z е входната променлива X_i, i  { 1, 2, …, n } и
   

1. 
   Нека step  N, val (step, s, Z_i) = t_i  H, i = 1, 2, …, p,
   

1. 
   Ако O_l = l. Z_i := Z_j, i, j  { 1, 2, …, p }, то
   

val (step+1, s, Z) = val (step, s, Z), ако Z  Z_i;

count (step+1, s) = l+1. Да отбележим, че O_l е оператор за

присвояване, така че l < q и l+1  [0, q].

1. 
   Ако O_l = l. Z_i := c_j, i  { 1, 2, …, p}, j  { 1, 2, …, r }, то
   

val (step+1, s, Z) = val (step, s, Z), ако Z  Z_i;

count (step+1, s) = l+1. Отново l < q и l+1  [0, q].

1. 
   Ако O_l = l. Z_i := f_j ( , , …, ), i, i_s  { 1, 2, …, p},
   

val (step+1, s, Z) = F_j ( , , …, ), ако Z = Z_i,

val (step+1, s, Z) = val (step, s, Z), ако Z  Z_i;

count (step+1, s) = l+1. Отново l < q и l+1  [0, q].

1. 
   Ако O_l = if T_j ( , , …, ) then l₁ else l₂, l₁, l₂  N,
   

val (step+1, s, Z) = val (step, s, Z);

count (step+1, s, Z) = l₁, ако P_j ( , , …, ) = true,

count (step+1, s, Z) = l₂, ако P_j ( , , …, ) = false.

Да отбележим, че по дефиниция l₁, l₂  [0, q].

1. 
   Ако O_l = l. goto l₁, l₁  N, то
   

count (step+1, s) = l₁. Да отбележим, че по дефиниция

l₁  [0, q].

1. 
   Ако O_l = l. stop, то
   

count (step+1, s) = count (step, s).

данни  по следния начин: < S,  > (s)  t  съществува k  N и съществува l  N, такива че count (k, s) = l, O_l = l. stop и val (k, s, Y) = t.

Не е трудно да се съобрази, че дефиницията е коректна - попадайки веднъж в оператор stop след това не променяме стойностите на променливите.
Нека S е примерната схема от по-горе.

Нека са дадени двата типа данни

₁ = (N; 1; x.x81, x, y.x*y; x = 0?), ₂ = ({ A, B, …, Z }^*; ; , ; x = ?),

където функциите ,  се дефинират по следния начин:

 (x) = думата x, без първата си буква, ако x  ,

 () = ;

 (x, y) = първата буква на x, долепена до y, ако x  ,

 (, y) = y.

Лесно се проверява, че < S, ₁ > (x)  x! за всяко x  N,

< S, ₂ > (x)  обърнатата дума x за всяко x  { A, B, …, Z}^*.
Рекурсивни схеми
Нека  = ((c₁, c₂, …, c_r), (f₁, f₂, …, f_m), (T₁, T₂, …, T_g)) е език от първи ред.

Считаме, че функционалният символ f_i е a_i-местен, i = 1, 2, …, m и предикатният символ T_j е b_j-местен, j = 1, 2, …, g.

Както в дефиницията на рекурсивните програми считаме, че разполагаме с обектови и функционални променливи.

Всъщност, рекурсивните схеми са обобщение на рекурсивните програми в произволен тип данни (а не в типа на естествените числа).

Означенията за константите от тип Bool и за основните операции от тип Boolⁿ  Bool ще съвпадат с тези при рекурсивните програми.

Абсолютно аналогично се дефинират понятията терм от основен тип, терм от тип Bool и условен терм. Разликите са, че символите за основните операции f : Natⁿ  Nat се заменят с функционалните символи на , символите за основните операции f : Natⁿ  Bool се заменят с предикатните символи на  и символите за Nat-константите се заменят с константните символи на .

₀ (X₁, …, X_n, , , …, ), where

…

(X₁, …, ) = _k (X₁, …, , , , …, )

Тук ₀ е терм от основен тип, който наричаме глава на програмата,

₁, …, _k са термове от основен тип или условни термове.

Нека  = (H, (p₁, p₂, …, p_r), (F₁, F₂, …, F_m), (P₁, P₂, …, P_k)) е тип данни в .

Да напомним, че с F_n^H означаваме множеството на

n-местните частични функции на H.

Навсякъде по-долу означаваме F^H = .
Нека  е (X₁, …, X_n, , , …, ), s  Hⁿ,   F^H.

Дефинираме понятието стойност на терм с индукция по построението:

1. 
   Ако  = c_j, то  (s, )  p_j.
   
2. 
   Ако  = b, където b е булова константа, то  (s, )  b.
   
3. 
   Ако  е променлива,  = X_i, то  (s, )  s_i.
   
4. 
   Ако  = f_j (₁, ₂, …, ), то  (s, )  F_j (₁ (s, ), ₂ (s, ), …, _l (s, )).
   
5. 
   Ако  = T_j (₁, ₂, …, ), то  (s, )  P_j (₁ (s, ), ₂ (s, ), …, _l (s, )).
   
6. 
   Ако  =  (₁, ₂, …, ), където  е l-местна булова операция, то
   

1. 
   Нека  e условен терм,  = if  then ₁ else ₂. Тогава
   

 (s, )  ₂ (s, ), ако  (s, )  ff,

!  (s, ), ако !  (s, ).

1. 
   Нека  e обръщение към функция,  = (₁, ₂, …, ).
   

С всеки терм  (X₁, …, X_n, , , …, ) свързваме оператор

Г_ : F^H  F_n^H, дефиниран по следния начин:

Г_ (₁, ₂, …, _k)(s₁, s₂, …, s_n)   (s₁, s₂, …, s_n, ₁, ₂, …, _k)

за всяко   F^H, s  Hⁿ. Както при рекурсивните програми с предаване по стойност се проверяват последователно монотонността и компактността на Г_. Така за всеки терм , Г_ е непрекъснато изображение на области на Скот.
Нека R е рекурсивна схема от горния общ вид.

За всяко i  { 1, 2, …, k} означаваме, Г_i = .

Разглеждаме системата за изображенията Г₁, Г₂, …, Г_k:

Г₁ (₁, ₂, …, _k) = ₁

Г₂ (₁, ₂, …, _k) = ₂

…

Г_k (₁, ₂, …, _k) = _k

При това  е и най-малко квазирешение.