Съкращение:
FOL означава First-Order Predicate Language.
Терм
Дефиниция (терм)
Индуктивна дефиниция (спомнете си дефиницията на кореново дърво от ДМ):
- Всяка индивидна променлива е терм;
- Всяка индивидна константа е терм;
- Ако $\tau_1, \tau_2, \cdots, \tau_n$ са термове, а $s_f \in \mathrm{S}_{f}$ и $\sharp[sf] = n$, то $s_f(\tau_1, \tau_2, \cdots, \tau_n)$ също е терм.
Ще бележим термовете над езика $\mathcal{L}$ с $\mathcal{T}_\mathcal{L}$.
Забележка: Терм е чисто синтактично понятие(за това имаме $\mathrm{S}_{f}$ - символи на функции(само имената на фукциите), не истински фунции). Тук просто си построяваме всички възможно композиции от функции.
Забележка: Термовете са building blocks на функционално програмиране.
Примери
Следните думи са термове в езика на Пеановата аритметика: $x$, $e$, $\cdot(x, x)$, $\cdot(x, \cdot(x, x))$, $S(0)$, $+(S(x), S(S(0)))$.
Забележка: Под $\cdot(x, x)$ всъщност 'разбираме' $x \cdot x$ (кога е правилно операцията да стои отпред и кога - между аргументите си, ще спорим друг път).
Дефиниция (стойност на терм)
Нека $\mathcal{L}$ е FOL, $\mathcal{C}$ е структура за $\mathcal{L}$ и $v$ е оценка. За всеки терм $\tau$ от $\mathcal{T}_\mathcal{L}$ дефинираме стойност на $\tau$ в $\mathcal{C}$ при оценка $v$. Ако $\tau$ е терм, стойноста му в структура $\mathcal{C}$ и оценка $v$ ще отбелязваме с $\|\tau\|^\mathcal{C}[v]$. Дефиницията ще извършим по индукция:
- Ако $\tau \in \mathrm{S}_{v}$ , $\tau = s_v$, тогава стойността е просто оценката на $s_v$ : $\|s_v\|^\mathcal{C}[v] \leftrightharpoons v(s_v) \in C$;
- Ако $\tau \in \mathrm{S}_{const}$, $\tau = s_{const}$, стойността не зависи от оценката, а само от интерпретацията (т.е. от $\mathcal{C}$): $\|s_{const}||^\mathcal{C}[v] \leftrightharpoons s_{const}^\mathcal{C} \in C$;
- И в общия случай, когато $\tau$ е функция приложена към няколко терма $\tau = s_f(\tau_1, \cdots, \tau_n)$, където ${s_f} \in \mathrm{S}_{f}$ , $\sharp[{s_f}] = n$ и $\tau_i$ са термове, за които $\|\tau_i\|^\mathcal{C}[v]$ е дефинирано, тогава просто заместваме $s_f$ с неговата интерпретация и термовете с техните оценки:
Забележка: вижте как стойността на терма винаги е елемент от $C$
Забележка: $\leftrightharpoons$ означава "равно по дефиниция". Ще го използваме консистентно оттук нататък.
Дефиниция (Var[t])
Нека $\tau$ е терм. С $\mathrm{Var}[\tau]$ ще отбелязваме множеството на всички променливи, срещащи се в $\tau$. Строгата дефиниция е по индукция:
- $\mathrm{Var}[s_v] \leftrightharpoons \{ s_v \} \quad s_v \in \mathrm{S}_v$
- $\mathrm{Var}[s_c] \leftrightharpoons \varnothing \quad s_c \in \mathrm{S}_{const}$
- $\mathrm{Var}[s_f(\tau_1, \cdots, \tau_n)] \leftrightharpoons \mathrm{Var}[\tau_1] \cup \cdots \cup \mathrm{Var}[\tau_n] , s_f \in \mathrm{S}_f, \sharp[{s_f}] = n$
Дефиниция (рестрикция)
Нека $f : A \to B$ е функция и $R \subseteq A$ е подмножество на дефиниционното множество на $f$.
$f \upharpoonright R$ или рестрикция на $f$ до $R$ наричаме функцията $f' : R \to B$, за която $f'(x) = f(x)\ \forall x \in R$.
С други думи рестрикцията на функция до множество е нова функция която има по-ограничено дефиниционно множество (не е дефинирана навсякъде, където е дефинирана оригиналната функция), но стойностите които заема са същите като оригиналната функция.
Твърдение (равенство на стойностите на термовете)
Нека $v_1$ и $v_2$ са оценки в $\mathcal{C}$ и $\tau$ е терм.
Ако $v_1 \upharpoonright \mathrm{Var}[\tau] = v_2 \upharpoonright \mathrm{Var}[\tau]$, то $\|\tau\|^\mathcal{C}[v_1] = \|\tau\|^\mathcal{C}[v_2]$.
Ако променливите на терма имат един и същи стойности при различни оценки - стойностите на целите термове също ще са еднакви при различните оценки.
Важно - оценките са различни, но структурата е една - $\mathcal{C}$
Доказателство: Ще извършим доказателство по индуктивното построение на $\tau$.
- Нека $\tau = x$. Да видим какво означава $v_1 \upharpoonright \mathrm{Var}[\tau] = v_2 \upharpoonright \mathrm{Var}[\tau]$:
$\star$ - рестрикцията на функция до $\{ x \}$ - интересуваме се от функционалната стойност на $x$. Затова и $v_1(x) = v_2(x)$.
- Нека $\tau = c$. Оценката на индивидните константи не зависи от оценката $v_i$:
- Нека $\tau = f(\tau_1, \cdots, \tau_n)$ и твърдението е вярно за $\tau_i$.
Първо ще докажем, че стойностите на $\tau_i$ при двете оценки се запазват - за целта трябва да покажем, че $v_1 \upharpoonright \mathrm{Var}[\tau_i] = v_2 \upharpoonright \mathrm{Var}[\tau_i]$ за всяко $\tau_i$ и да използваме индуктивното предположение. От дефиницията на $\mathrm{Var}[\tau]$ имаме:
(4)Комбинираме с даденото:
(5)Оттук веднага получаваме, че $\|\tau_i\|^\mathcal{C}[v_1] = \|\tau_i\|^\mathcal{C}[v_2]$. Сега остава да разпишем стойността на $\tau$ при двете оценки:
(6)Дефиниция (затворен терм)
Нека $\tau$ е терм. Казваме, че той е затворен ако $\mathrm{Var}[\tau] = \varnothing$.
Следствие (от горното твърдение за затворен терм)
Ако $\tau$ е затворен терм и $v_1, v_2$ са две оценки в структура $\mathcal{C}$, то $\|\tau\|^\mathcal{C}[v_1] = \|\tau\|^\mathcal{C}[v_2] = \tau^\mathcal{C}$.
Т.е. ако термът няма никакви индивидни променливи, неговата стойност зависи единствено от структурата, затова може да записваме $\tau^\mathcal{C}$.
Дефиниция
Ще дефинираме $\tau^\mathcal{C}[[a_1, \cdots, a_k]]$.1
Нека $x_1, \cdots, x_k$ са индивидни променливи и $\{ x_1, \cdots, x_k \} \supseteq \mathrm{Var}[\tau]$.
Нека $a_1, \cdots, a_k$ са произволни обекти от универсума $A$.
Нека $v_1, v_2$ са две произволни оценки, за които $v_1(x_i) = a_i = v_2(x_i)$ (това е по-силно от $v_1 \upharpoonright \{ x_1, \cdots, x_k \} = v_2 \upharpoonright \{ x_1, \cdots, x_k \}$, защото искаме функциите да съвпадат върху ограниченото множество и специфично задаваме функционалните им стойности).
Сега използваме предното твърдение: $\| \tau \|^\mathcal{C}[v_1] = \|\tau\|^\mathcal{C}[v_2]$. Следователно за произволна оценка, изпълняваща горните условия имаме, че стойността на терма $\tau$ е една и съща. Тя зависи единствено от избора на обекти от универсума $a_1, \cdots, a_k$. Следователно на всеки един такъв избор на обекти може да съпоставим стойност на терма $\tau$ при оценка изпълняваща горепосочените условия. Ще записваме тази съпоставена стойност като $\tau^\mathcal{C}[[ a_1, \cdots, a_k ]]$.
Дефиниция (термална функция):
Нека $\mathcal{C} = \langle A, \mathbb{I} \rangle$ е структура за $\mathcal{L}$.
Нека $F : A^k \to A$ е функция. Ще казваме, че $F$ е термална, ако съществува терм $\tau$ с $k$ индивидни променливи ($\sharp[\tau] = k$) $x_1, \cdots, x_k$ и
$F(a_1, \cdots, a_k) = \tau^\mathcal{C}[[a_1, \cdots, a_k]]$
Пример
Нека $\mathcal{N} = \langle \{ 0, 1, \cdots \}, 0, S, +, \cdot, < \rangle$ е структура на Пеановата аритметика.
- полиномите с $\mathbb{N}$ коефициенти са термални функции в $\mathcal{N}$;
- функцията $f(x) = 2^x$ не е термална в $\mathcal{N}$;
- функцията $f(x) = x$ е термална;
- функцията $f(x) = c$ е термална, само ако $c \in \mathbb{C}\mathrm{onst}$;