Алгоритм унификации

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

ШАГ 1. Введём индекс j ₀ = 1. Присвоим Е¢ =E, q =e.

ШАГ 2. Определяем множество рассогласований D_j1 (j₁ – наи-меньший из индексов несовпадающих подвыражений, j₁ ³ j₀). Возможны две ситуации:

а) D_j1 = Æ (для всех индексов унификация подвыражений завершена). Следовательно, исходное множество Е - уни-фицируемо, а q - его наиболее общий унификатор. Выход из алгоритма.

б) D_j1 ¹ Æ (для индекса j₁ подвыражения не совпадают (j₁ – минимальный из всех таких индексов). Переходим на следующий ШАГ 3.

ШАГ 3. В случае наличия ненулевого множества рассо-гласований D_j1 возможны также две ситуации:

а) существует подстановка l, унифицирующая D_j1. Тогда присваиваем q:= q ° l, Е¢:= Е¢ l,

j ₀ := j₁. Переход на ШАГ 2 (Продолжение выполнения алго-ритма).

б) не существует подстановки l, унифицирующей D_j1. В этом случае исходное множество Е - не унифицируемо. Вы-полнение алгоритма прекращается.

Пример 6. Определить унифицируемость множества выражений Е ={E ₁, E ₂, E ₃ , E₄} = {P(x, y, z, u), Р(f(u, z), g(a), z), Р(y, y, z), Р(f(a,z), y, z) }.

Решение.

1. Индекс j ₀ = 1. Присвоим Е¢ =E, q =e.

2. Поскольку подвыражения на первых местах не совпада-

ют, то j₁ =1 и множество рассогласований D₁ = { x, f (u, z), y, f (a, z)}. Подстановка l, унифицирующая D₁, может быть

построена. Она имеет вид: l = {f(a,z)/x, f(a,z)/y, a/u}. При-сваиваем q: = q ° l = l, Е¢:= Е¢ l = { P(f(a, z), f(a, z), z), Р(f(a, z), g(a), z), Р(f(a, z), f(a, z), z), Р(f(a, z), f(a, z), z)}.

3. Подвыражения на вторых позициях не совпадают, следо-вательно, j₁ =2 и множество рассогласований D₂ = {f(a, z)}, g(a)}. Подстановка, унифицирующая D₂, не существует, по-скольку путем замены переменных невозможно унифици-ровать подвыражения f(a,z) и g(a). Таким образом, рассмот-ренное множество выражений не унифицируемо.

За счет применения унификации можно также доби-ваться идентичности литер внутри дизъюнктов. Дублиру-ющие литеры при этом можно устранять. Соответствующая операция называется склейкой. Рассмотрим её строгое определение.

Определение. Пусть некоторый дизъюнкт D_i, содер-жащий множество литер {L}, имеет одинаковые литеры L(E₁), L(E₂),..., L(E_k), обладающие одинаковой положитель-ностью (все одновременно без отрицания либо - с отрица-нием). Если для множества выражений Е={E₁,E₂,...,E_k} cу-ществует наибольший общий унификатор s, то множество литер {L s } называется склейкой для D_i.

Пример 7. Построить склейку для дизъюнкта D_i = Р(х) Ú Р(f(y)) Ú Р(f(a)) Ú Q(y).

Решение. Одинаковыми являются первая, вторая и третья литеры. Е= {х, f(y), f(a)}. Наиболее общий унификатор s = {a/y, f(a)/x}. D_i s = Р(f(a)) Ú Р(f(a)) Ú Р(f(a)) Ú Q(a) = Р(f(a)) Ú Q(a).

Если в результате склейки в D_i s осталась одна литера, то она называется единичной.