Термове в език на предикатното смятане от 1ви ред

Съкращение:
FOL означава First-Order Predicate Language.

Терм

Дефиниция (терм)

Индуктивна дефиниция (спомнете си дефиницията на кореново дърво от ДМ):

1. Всяка индивидна променлива е терм;
2. Всяка индивидна константа е терм;
3. Ако $\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$ с неговата интерпретация и термовете с техните оценки:

(1)

\begin{align} \|s_f(\tau_1, \cdots, \tau_n) \|^\mathcal{C}[v] \leftrightharpoons {s_f}^\mathcal{C}(\|\tau_1\|^\mathcal{C}[v], \cdots, \|\tau_n\|^\mathcal{C}[v]) \in C \end{align}

Забележка: вижте как стойността на терма винаги е елемент от $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]$:

(2)

\begin{eqnarray} v_1 \upharpoonright \mathrm{Var}[\tau] &=& v_2 \upharpoonright \mathrm{Var}[\tau] \iff \\ v_1 \upharpoonright \{ x \} &=& v_2 \upharpoonright \{ x \} \overset{\star}\iff \\ v_1(x) &=& v_2(x) \iff \\ \|x\|^\mathcal{C}[v_1] &=& \|x\|^\mathcal{C}[v_2] \end{eqnarray}

$\star$ - рестрикцията на функция до $\{ x \}$ - интересуваме се от функционалната стойност на $x$. Затова и $v_1(x) = v_2(x)$.

• Нека $\tau = c$. Оценката на индивидните константи не зависи от оценката $v_i$:

(3)

\begin{align} \|c\|^\mathcal{C}[v_1] = c^\mathcal{C} = \|c\|^\mathcal{C}[v_2] \end{align}

• Нека $\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)

\begin{align} \mathrm{Var}[\tau] = \mathrm{Var}[\tau_1] \cup \cdots \cup \mathrm{Var}[\tau_n] \supseteq \mathrm{Var}[\tau_i] \quad \forall i \end{align}

Комбинираме с даденото:

(5)

\begin{align} \left\{\begin{array}{rcl} v_1 \upharpoonright \mathrm{Var}[\tau] &=& v_2 \upharpoonright \mathrm{Var}[\tau] \\ \mathrm{Var}[\tau_i] &\subseteq& \mathrm{Var}[\tau] \\ \end{array}\right\} \Rightarrow v_1 \upharpoonright \mathrm{Var}[\tau_i] &=& v_2 \upharpoonright \mathrm{Var}[\tau_i] \end{align}

Оттук веднага получаваме, че $\|\tau_i\|^\mathcal{C}[v_1] = \|\tau_i\|^\mathcal{C}[v_2]$. Сега остава да разпишем стойността на $\tau$ при двете оценки:

(6)

\begin{align} \left\{\begin{array}{rcccl} \|\tau\|^\mathcal{C}[v_1] &=& \|f(\tau_1, \cdots, \tau_n)\|^\mathcal{C}[v_1] &=& f^\mathcal{C}(\|\tau_1\|^\mathcal{C}[v_1], \cdots, \|\tau_n\|^\mathcal{C}[v_1]) \\ \|\tau\|^\mathcal{C}[v_2] &=& \|f(\tau_1, \cdots, \tau_n)\|^\mathcal{C}[v_2] &=& f^\mathcal{C}(\|\tau_1\|^\mathcal{C}[v_2], \cdots, \|\tau_n\|^\mathcal{C}[v_2]) \\ \end{array}\right\} \Rightarrow \|\tau\|^\mathcal{C}[v_1] = \|\tau\|^\mathcal{C}[v_2] \end{align}

Дефиниция (затворен терм)

Нека $\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]]$.¹
Нека $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}$;

Footnotes

1. За сега си няма име! Ако някой измисли да го допише. Иначе ще го използваме само в следващата дефиниция, така че не е фатално да си остане без име :-)