Унификация. Най-общ унификатор

До сега говорихме за замени в термове, сега ще говорим за тях по друг начин.

Дефиниция (Субституция)

Субституция е крайно множество от вида $\{ x_1/\tau_1,... x_n/\tau_n \}$, където $x_1,... x_n$ са индивидни променливи, а $\tau_1,...\tau_n$ са термове, при това за всяко $i=1..n, \ x_i \neq \tau_i$

Една важна субституция

$\iota$ - йот, това е $\iota \rightleftharpoons \varnothing$ празната субституция

Дефиниция (сигма ‘шапка’)

Нека $\sigma$ е субституция, $\sigma = \{ x_1/\tau_1,...,x_n/\tau_n\}$. Дефинираме изображението $\hat{ \sigma} : \mathcal{T}\cup \{$ безкванторни формули $\} \rightarrow \mathcal{T} \cup \{$ безкванторни формули $\}$.

$\hat\sigma = \begin{cases} \tau_i : x = x_i, i=1..n \\ x : x \notin \{x_1,..,x_n\} \end{cases}$

$\hat\sigma(x) \leftrightharpoons x [x_1/\tau_1,...,x_n/\tau_n]$, $x$ - индивидна променлива
$\hat\sigma(c) \leftrightharpoons c$, $c$ - индивидна константа
$\hat\sigma(f(\tau_1,...,\tau_n)) \leftrightharpoons f(\hat\sigma(\tau_1),...,\hat\sigma(\tau_n))$ , $f(\tau_1,...,\tau_n)$ - терм
$\hat\sigma(p(\tau_1,...,\tau_n)) \leftrightharpoons p(\hat\sigma(\tau_1),...,\hat\sigma(\tau_n))$ , $p(\tau_1,...,\tau_n)$ - атомарна предикатна формула
$\hat\sigma(\neg \varphi ) \leftrightharpoons \neg \hat\sigma(\varphi)$ , $\varphi$ - безкванторна предикатна формула
$\hat\sigma( \varphi_1 \vartheta \varphi_2 ) \leftrightharpoons \hat\sigma( \varphi_1) \vartheta \hat\sigma( \varphi_1), \vartheta \in \{ \And,\lor,\Rightarrow, \Leftrightarrow\}$
Тоест $\hat{\sigma}$ е изображението което прилага субституцията1

Дефиниция

$F: \mathcal{T} \rightarrow \mathcal{T}$. Съществува субституция $\sigma : F = \hat\sigma$ тогава и само тогава когато:
i $F$ е хомоморфизъм в алгебрата на термовете и
ii само за краен брои индивидни променливи $F(x) \neq x$.

Дефиниция (Еквивалентност на субституции)

Две субституции са равни т.с.т.к. съответните им изображения са еднакви.
$\sigma_1 = \sigma_2 \leftrightarrow \hat\sigma_1 = \hat\sigma_2$

Означение

Вместо $\hat\sigma(\tau)$ ще пишем $\tau \sigma$.

Композиция на субституции

Нека $\sigma, \xi$ са субституции. $\sigma = \{ x_1/\tau_1,..,x_n/\tau_n \},\xi = \{ y_1/\varkappa_1,..,y_n/\varkappa_m \}$
Сега имаме $\hat\sigma$ и $\hat\xi$
$F(\tau)=\hat\sigma(\hat\xi(\tau))$ наричаме композиция на изображения.
$F$ е породено от субституции и има субституця $\eta$, която го дефинира:
$\eta = \{y_1/\varkappa_1\sigma,...,y_2/\varkappa_2\sigma , x_{i1}/\tau_{i1},...,x_{il}/\tau_{il}\}\setminus \{ y_i/\varkappa_i\sigma | y_i = \varkappa_i\sigma, i=1..n \}$, където:
$x_{i1},...,x_{il}$ са всички променливи измежду $x_1,..,x_n$, които са различни от $y_1,..y_m$ и $\varkappa_i\sigma$ са съответната $\varkappa$ подложена на субституцията $\sigma$.

Композицията бележим по следния начин $\eta = \sigma \circ \xi$.
И, разбира се, $\hat\eta (\tau) = \hat\sigma(\hat\xi(\tau))$

Свойства на композициите

$\iota \sigma = \sigma = \sigma \iota$
$\xi \circ (\sigma \circ \eta) = (\xi \circ \sigma) \circ \eta$
$\delta(\tau)$ - броят на символите в думата $\tau$
$\delta(\tau) \le \delta(\tau\sigma)$

Дефиниция Преименуваща субституция

Нека $E$ е множество от термове, а $\sigma$ е субституция. Казваме, че $\sigma$ е преименуваща за $E$, ако за всяка променлива $x$ , която се среща в терм от $E$ имаме:
i $x \in \displaystyle \cup_{\tau \in E} Var[\tau] \ \Longrightarrow \ \hat\sigma(x)$ е променлива и
ii $x, y \in \displaystyle \cup_{\tau \in E} Var[\tau] \ \Longrightarrow \ \hat\sigma(x) \neq \hat\sigma(y)$

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License