Основные понятия и методы теории формальных систем. Волохович А.В. - 26 стр.

очевидно, никакая подстановка неприменима и никакая резольвента
не образуется. Отсюда следует определение того, что является
подстановкой.
      Подстановкой будем называть конечное множество вида {t 1 /x 1 ,
t 2 /x 2 , …, t n /x n }, где любой t i – терм, а любая х i – переменная (1 ≤ i ≤
n), отличная от t i .
      Подстановка называется фундаментальной, если все t i (1 ≤ i ≤ n)
являются фундаментальными термами. Подстановка, не имеющая
элементов, называется пустой подстановкой и обозначается через ε.
Пусть Θ = {t 1 /x 1 , t 2 /x 2 , …, t n /x n } – подстановка и W – выражение.
Тогда WΘ будем называть примером выражения W, полученного
заменой всех вхождений в W переменной х i , (1 ≤ i ≤ n) на вхождение
терма t i . WΘ будет называться фундаментальным примером
выражения W, если Θ – фундаментальная подстановка.
      Например, применив к W ={ Р (х, f( у) ) ∨ ¬ Q (z)}
фундаментальную подстановку Θ = {а/х, g(b)/у, f(а)/z}, получим
фундаментальный пример WΘ ={Р(a, f(g(b))) ∨ ¬ Q (f(a))}. Пусть Θ =
{t 1 /x 1 , t 2 /x 2 , …, t n /x n } и λ = {u 1 /y 1 , u 2 /y 2 , …, u m /y m } – две подстановки.
Тогда композицией Θλ двух подстановок Θ и λ называется
подстановка, состоящая из множества

                   {t 1 λ/x 1 , t 2 λ/x 2 , …, t n λ/x n , u 1 /y 1 , u 2 /y 2 , …, u m /y m },

в котором вычеркиваются t i λ/x i у в случае t i λ=x i и u i /y i если y i
находится среди x 1 , x 2 , …, x n .
    Пример. Θ = {g(x,y)!х, z/у} и λ = {a/x, b/y, c/w, y/z}, Θλ= {g(a,b)!х,
у/у, а/х, b/у, с/w, у/z} {g(a,b)!х, с/w, у/z}. Можно показать, что
композиция подстановок ассоциативна, т. е. (Θλ)μ= Θ(λμ) .
    Подстановку Θ будем называть унификатором для множества
выражений {W 1 , W 2 , …, W k }, если W 1 Θ= W 2 Θ= …= W k Θ . Будем
говорить, что множество выражений {W 1 , W 2 , …, W k } унифицируемо,
если для него имеется унификатор. Унификатор σ для множества
выражений {W 1 , W 2 , …, W k } называется наиболее общим
унификатором (Н0У) тогда и только тогда, когда для каждого
унификатора Θ для этого множества выражений найдется
подстановка λ такая, что Θ = σ λ.
    Опишем теперь алгоритм унификации, который находит НОУ,
если множество выражений W унифицируемо, и сообщает о неудаче,
если это не так.
1. Установить k = 0, W k = W и σ k = ε. Перейти к пункту 2.
2. Если W k не является одноэлементным множеством, то перейти к
   пункту 3. В противном случае положить σ = σ k и окончить работу.



26