Cвойства композиций подстановок

Для любых подстановок q, l,m справедливы следую-щие свойства:

1. Ассоциативность: q ° l ° m = (q ° l) ° m = q ° (l ° m).

2.Коммутативность c пустой подстановкой: q ° e =e ° q.

Потенциальные возможности подстановок таковы, что с их помощью нельзя добавлять или снимать отрицание с предикатов. Однако, применяя подстановки, можно (не во всех случаях) привести переменные и термы, входящие в предикаты, к единому виду.

Определение. Подстановка q называется унифика-тором множества выражений Е ={E ₁, E ₂,..., E _k } Û когда E₁q=E₂q=...=E_kq. Если унификатор для множества Е суще-ствует, то само множество называется унифицируемым.

Очевидно, унификатор может быть неединственным, поскольку при применении любой композиции подстановок q°l унификатора q с любой подстановкой l будет выпол-няться равенство E₁ql = E₂ql =...= E_k ql.

Определение. Унификатор q называется наиболее об-щим унификатором для множества выражений Е ={E ₁, E ₂,..., E _k } Û когда любой унификатор l множества выра-жений Е можно представить в виде l = q °s, где s - неко-торая подстановка.

Пример 4. Найти унификатор множества E = { P(x,y), P(a,b)}. Унификатором Е является подстановка q ={а/x, b/y}. После её применения Е₁q = Е₂q = Р(a,b).

Рассмотрим более сложные случаи различия выраже-ний. Допустим, имеется множество из k выражений Е ={E₁, E₂,..., E_k }, каждое из которых зависит от s подвыражений:

E₁ = E₁ (e₁₁, e₁₂,...,e_1s);

E₂ = E₂ (e₂₁, e₂₂,...,e_2s);

...

E_k = E_k (e_k1, e_k2,...,e_ks).

Множество подвыражений e_j1, e_j2,...,e_jk, стоящих в каждом из выражений E₁, E₂,..., E_k на j -той позиции, на-зовём подвыражениями с индексом j. Если все такие под-выражения e_j1, e_j2,...,e_jk одинаковы, то назовём их совпа-дающими. Если не все одинаковы (т.е. существуют номера p,q при которых e_jр ¹ e_jq ), то назовём их несовпадающими.

Пример 5. Определить совпадаюшие и несовпадаю-щие подвыражения в множестве выражений Е ={E₁,E₂,E₃ } = {P(x,y,z,u), Р(x,f(a),z,g(z)), Р(x,y,z,g(y))}.

Решение.

j=1: e₁₁ = e₂₁ = e₃₁ =x, Þ подвыражения с индексом j=1 совпадают,

j=2: e₁₂ = e₃₂ =у, e₂₂ =f(a), Þ подвыражения с индексом j=2 не совпадают,

j=3: e₁₃ = e₂₃ = e₃₃ =z, Þ подвыражения с индексом j=3 совпадают,

j=4: e₁₄ = u, e₂₄ =g(z), e₃₄ = g(x), Þ подвыражения с индексом j=4 не совпадают.

Таким образом, подвыражения, стоящие на первых и третьих позициях, совпадают, а на вторых и четвёртых позициях - не совпадают.

Определение. Рассмотрим множество выражений Е={E ₁, E ₂,..., E _k }, вида:

E₁ = E₁ (e₁₁, e₁₂,...,e_1s);

E₂ = E₂ (e₂₁, e₂₂,...,e_2s);

...

E_k = E_k (e_k1, e_k2,...,e_ks).

Множеством рассогласований D _j множества выраже-ний Е называются несовпадающие подвыражения e_j1, e_j2,...,e_jk с минимальной величиной индекса j. Если для всех индексов 1 £ j £ s подвыражения совпадают, то множество рассогласований множества выражений Е принимаем рав-ным нулю: D _j = Æ.

Для множества Е = {P(x,y,z,u), Р(x,f(a),z,g(z)), Р(x,y,z, g(y))} из Примера 5 множеством рассогласований будет D ₂ = {y, f(a)}. Рассмотрим на этом множестве Е, каким образом можно, последовательно устраняя рассогласования, унифи-цировать все множество.

1. Вначале множество рассогласований равно D ₂ = {y, f(a)}. Его можно унифицировать при помощи подстановки q = {f(a)/y} на множестве Е. После применения q получим:

E₁q = P(x, f(a), z, u), E₂q = Р(x, f (a), z, g (z)), E₃q = Р(x, f(a), z, g (f (a)).

2. Для индексов j=1,2,3 подвыражения совпадают. Мно-жество рассогласований равно D₄ = {u, g(z), g(f(a))}. Его можно унифицировать при помощи подстановки q₂ = {f(a)/z, g(f(a))/u} на множестве Е. После применения q₂ получим:

E₁qq₂ = P(x, f(a), f(a), g(f(a))), E₂qq₂ = Р(x, f(a), f(a), g(f(a))), E₃qq₂ = Р(x, f(a), f(a), g(f(a))).

Таким образом, множество Е унифицируемо и найден-

ный унификатор имеет вид: q°q₂ = {f(a)/y, f(a)/z, g(f(a))/u}.

В общем случае для определения унифицируемости множества выражений Е и нахождения наиболее общего унификатора (если он существует) применяется