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



страница3/22
Дата01.06.2017
Размер2.18 Mb.
#22581
ТипЛекции
1   2   3   4   5   6   7   8   9   ...   22

Термове

дадена е сигнатура , ;

за краткост 0-местните функционални символи ще наричаме константи, въпреки че константите са 0-местните функции;

провеждаме индуктивна дефиниция за понятието терм:

База: всяка константа е терм; всяка променлива е терм;

Предположение: нека f  Фn, n > 0 и T1, T2, …, Tn са термове;

Стъпка: тогава думата f (T1, T2, …, Tn) е терм;

Заключение: няма други термове;

термовете от базата наричаме прости термове, термовете от стъпката наричаме съставни термове;
примери за термове със сигнатурата на семейство Вазови:

next (ivan)

next (next (ivan))

prev (ivan)

prev (next (ivan))

prev (next (X))


ясно е, че всеки терм е префиксен израз над , което допълнително с достатъчното условие осигурява еднозначен синтактичен анализ на термовете;
за всеки терм T определяме VAR (T) – множеството на променливите на T с индукция по построението на T:

База: ако T е константа, определяме VAR (T) = ; ако T е променлива, определяме VAR (T) = { T};

Предположение: нека T = f (T1, T2, …, Tn), където T1, T2, …, Tn са термове и VAR (T1), VAR (T2), …, VAR (Tn) са дефинирани;

Стъпка: тогава дефинираме

VAR (T) = VAR (T1)  VAR (T2)  …  VAR (Tn);

Заключение: за всеки терм T, VAR (T) е дефинирано;


като следствие от еднозначния синтактичен анализ на термовете, множеството VAR (T) е еднозначно определено;
Твърдение: за всеки терм T, VAR (T) е крайно множество;

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

База: ако Т е константа, то VAR (T) =  и VAR (T) е крайно множество; ако T е променлива, то VAR (T) = { T} и VAR (T) отново е крайно множество;

Предположение: нека T = f (T1, T2, …, Tn), където T1, …, Tn са термове и VAR (T1), …, VAR (Tn) са крайни множества;

Стъпка: тогава VAR (T) = VAR (T1)  …  VAR (Tn) е крайно множество, тъй като е крайно обединение на крайни множества;

Заключение: за всеки терм T, VAR (T) е крайно множество;


за примера със семейство Вазови с индукция по построението може да се покаже, че всеки съставен терм съдържа не повече от една променлива;
казваме, че термът T е затворен терм, ако VAR (T) = ;
ще дадем още една индуктивна дефиниция за затворен терм;

База: всички константи са затворени термове;

Предположение: нека f  Фn, n > 0 и T1, …, Tn са затворени термове;

Стъпка: тогава f (T1, …, Tn) е затворен терм;

Заключение: няма други затворени термове;
Твърдение: Двете дефиниции за затворен терм са еквивалентни;

ще покажем, че за всеки затворен терм T (от индукцията) имаме VAR (T) = , т.е. T е затворен в смисъла на първата дефиниция;

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

База: ако T е константа, то VAR (T) =  и твърдението е изпълнено;

Предположение: нека T = f (T1, T2, …, Tn), където T1, …, Tn са затворени термове и VAR (T1) = VAR (T2) = … = VAR (Tn) = ;

Стъпка: тогава VAR (T) = VAR (T1)  VAR (T2)  …  VAR (Tn) =

=     …   = ;

ще покажем, че за всеки терм T или VAR (T)   или T е затворен в смисъла на индуктивната дефиниция;

така, ако VAR (T) = , то T е затворен терм в смисъла на индуктивната дефиниция;

доказателството извършваме с индукция по построението на T;

База: ако T е константа, то T е затворен терм в смисъла на индуктивната дефиниция; ако T е променлива,

то VAR (T) = { T}  ;

Предположение: нека T = f (T1, T2, …, Tn) и за T1, T2, …, Tn твърдението е изпълнено;

Стъпка: ако съществува индекс i  { 1, 2, …, n},

такъв че VAR (Ti)  , то VAR (T) = VAR (T1)  …  VAR (Tn)   и твърдението е изпълнено; ако VAR (T1) = VAR (T2) = …= VAR (Tn) = , то по индукционното предположение T1, T2, …, Tn са затворени термове в смисъла на индуктивната дефиниция и тогава T също е затворен терм в смисъла на индуктивната дефиниция;

Семантика на термовете

фиксираме структура S с носител D и интерпретации 0, 1, …;

0, 1, …; съответно на функционалните и на предикатните символи;
на всеки затворен терм T съпоставяме елемент от D, който наричаме стойност на затворения терм T в S;

означаваме стойността на T в S с T S;

дефиницията е с индукция по построението на T;

База: ако T е константа, то T S = 0 (T);

Предположение: нека T = f (T1, T2, …, Tn), където T1, …, Tn са затворени термове и T1S, …, TnS са дефинирани;

Стъпка: тогава T S = f S (T1S, …, TnS) (или T S = n (f) (T1S, …, TnS));


под оценка на променливите в S разбираме тотално изображение на множеството на променливите в D;

нека v е оценка на променливите в S; на всеки терм T

съпоставяме елемент от D, който наричаме стойност на терма T в S при оценка v;

означаваме стойността на T в S при оценка v с T S, v;

дефиницията е с индукция по построението на T;

База: ако T е константа, T S, v = 0 (T) = T S; ако T е променлива,

T S, v = v (T);

Предположение: нека T = f (T1, T2, …, Tn) и T1S, v, T2S, v, …, TnS, v са дефинирани;

Стъпка: тогава T S, v = f S (T1S, v, T2S, v, …, TnS, v);
Твърдение: ако T е затворен терм, то T S, v = T S за всяка оценка v;

Доказателство: нека v е произволна оценка; провеждаме

индукция по построението на T;

База: ако T е константа, то от дефиницията на T S, v имаме

T S, v = 0 (T) = T S;

Предположение: нека T = f (T1, T2, …, Tn), където T1, …, Tn са затворени термове и T1S, v = T1S, T2S, v = T2S, …, TnS, v = TnS;

Стъпка: тогава T S, v = f S (T1S, v, T2S, v, …, TnS, v) =

= f S (T1S, …, TnS) = T S; индукционното предположение използваме при второто равенство;


Твърдение: ако T е терм, v и u са оценки, които съвпадат върху VAR (T), то T S, v = T S, u;

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

База: ако T е константа, то T S, v = T S = T S, u; ако T е променлива,

то T S, v = v (T), T S, u = u (T); но T  VAR (T)  v (T) = u (T) 

T S, v = T S, u;

Предположение: нека T = f (T1, T2, …, Tn) и твърдението е изпълнено за T1, …, Tn;

Стъпка: тъй като v и u съвпадат върху VAR (T) и

VAR (T) = VAR (T1)  VAR (T2)  …  VAR (Tn), то v и u съвпадат върху VAR (Ti), i = 1, 2, …, n; от индукционното предположение

T1S, v = T1S, u, T2S, v = T2S, u, …, TnS, v = TnS, u

T S, v = f S (T1S, v, T2S, v, …, TnS, v) = f S (T1S, u, T2S, u, …, TnS, u) = T S, u;






Сподели с приятели:
1   2   3   4   5   6   7   8   9   ...   22




©obuch.info 2024
отнасят до администрацията

    Начална страница