Термове
дадена е сигнатура , ;
за краткост 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;
Сподели с приятели: |