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

Рассмотрим особенности алгоритма унификации в MLL:

1. Термы в MLL унифицируются при выполнении условий унификации, которые являются одинаковыми для   предков и доменов: XY и XY  0.

2. Пусть х является термом уровня i, и в тоже время, он является   предком терма следующего нижележащего уровня. Терм х унифицируется и автоматически унифицируются- предок терма следующего нижележащего уровня.

Приведем разработанный алгоритм унификации для модифицированного синтаксиса MLL.

Шаг 1. Установить k=0, W_k =W, S_k =, где W – унифицируемые выражения, S_k – наиболее общий унификатор и  – пустая подстановка.

Шаг 2. Если W_k является одноэлементным множеством, то W унифицируемо, S=S_k и стоп. В противном случае переход к шагу З.

Шаг 3. Каждая из литер в W_k рассматривается, как цепочка символов и выделяются первые подвыражения литер, не являющихся одинаковыми у всех элементов W_k, т.е. образуется так называемое множество рассогласований типа { (v_k/V_k)//V, (t_k/T_k)//T }.

Если v_k – переменная, а t_k – терм, или v_k­ – функция, а t_k  переменная или функция, то перейти к шагу 4.

В противном случае стоп: W не унифицируемо.

Шаг 4. Проверка условий унификации предков.

Если V  T или V  T = Z () (условия унификации выполняются), то перейти к шагу 5.

В противном случае стоп: W не унифицируемо.

Если предками являются термы и они совпадают, то перейти к шагу 5.

В противном случае стоп: W не унифицируемо.

Шаг 5. Проверка условий унификации доменов:

а) если v_k – переменная, определенная на домене V_k, а t_k константа, определенная на домене T, и T  V, то перейти к шагу 6. В противном случае стоп: W не унифицируемо.

б) если v_k – переменная, определенная на домене V_k, а t_k переменная, определенная на домене T_k, и T_kV_k=Z_k (), то перейти к шагу 6. В противном случае стоп: W не унифицируемо.

в) если v_k - переменная, определенная на домене V_k, а t_k – функция, определенная на домене T_k, и T_k  V_k=Z_k () , то перейти к шагу 6. В противном случае стоп: W не унифицируемо.

г) если v_k - функция, определенная на домене V_k, а t_k функция, определенная на домене T_k, и T_k  V_k или V_k  T_k ,то перейти к шагу 6. В противном случае стоп: W не унифицируемо.

Шаг 6. Если v_k - переменная, а t_k - константа или функция, то S_k+1 = S_k  {t_k / v_k } и W_k+1 = W_k{ t_k / v_k }, где  - композиция подстановок, а запись W_k{ t_k / v_k } обозначает замену v_k на t_k в W_k (см. замечание).

Если v_k - переменная, а t_k - переменная, то S_k+1 = S_k  {z_k/t_k, z_k/v_k } и W_k+1 = W_k{z_k / t_k, z_k / v_k }, где z_k -переменная, отличная от v_k и t_k .

Если v_k и t_k - функции, то в унифицируемое выражение подставляется функция, область значений которой является подмножеством области значений другой функции.

Замечание. Запись {t_k /v_k } означает замену (v_k/V_k)//V на (t_k/T_k)//T во всех вхождениях v_k как терм и замену v_k на t_k во всех вхождениях v_k как-предка. Аналогично, когда v_k и t_k определены на термах.

Шаг 7. k=k+1, перейти к шагу 2.

В случае, когда объекты состоят из одной компоненты, сортность термов не указывается в префиксе и шаг проверки унификации доменов термов в формулах пропускается, поскольку области определения термов однозначно задаются их -предками.

Рассмотрим пример использования разработанного алгоритма унификации. Пример приведен для случая, когда объекты в качестве компонент имеют несколько объектов. Иерархические структуры приведены на рис. 22, 23.

Пример 3. W={ P( (a₁/A₁)//X, (x₀/X₀)//a₁, (y₁/Y₁)//Y, (f((x₀/X₀)//a₁)/W₀)//y₁),

P((v₁/V₁)//V,(g((w₁/W₁)//W)/X₀)//v₁,(w₁/W₁)//W, (w₀/W₀)//w₁) }

1. W₀=W; S₀=

2. { (a₁/A₁)//X, (v₁/V₁)//V} – множество рассогласований

3. Полагаем, что X  V и A₁  V₁,

4. S₁=S₀  {a₁/v₁}

W1= { P( (a₁/A₁)//X, (x₀/X₀)//a₁, (y₁/Y₁)//Y, (f((x₀/X₀)//a₁)/W₀)//y₁),

P( (a₁/A₁)//X, (g((w₁/W₁)//W)/X₀)//a₁, (w₁/W₁)//W, (w₀/W₀)//w₁) }

5. {(x₀/X₀)//a₁, (g((w₁/W₁)//W)/X₀)//a₁} – множество рассогласований.

S₂=S₁ { g((w₁/W₁)//W)/x₀ }

W₂= { P( (a₁/A₁)//X, (g((w₁/W₁)//W)/X₀)//a₁, (y₁/Y₁)//Y,(f((g((w₁/W₁)//W)/X₀)//a₁)/W₀)//y₁ ),

P( (a₁/A₁)//X, (g((w₁/W₁)//W)/X₀)//a₁, (w₁/W₁)//W, (w₀/W₀)//w₁) }

7. { (y1/Y1)//Y, (w1/W1)//W} – множество рассогласований

8. Полагаем, что WY=Z () и W₁Y₁=Z₁ ().

9. S₃=S₂{z/y₁, z/w₁}

W₃= { P( (a₁/A₁)//X, (g((z/Z₁)//Z)/X₀)//a₁, (z/Z₁)//Z,

(f((g((z/Z₁)//Z)/X₀)//a₁)/W₀)//z ),

P( (a₁/A₁)//X, (g((z/Z₁)//Z)/X₀)//a₁, (z/Z₁)//Z,

(w₀/W₀)//z) }

10. { (f((g((z/Z₁)//Z)/X₀)//a₁)/W₀)//z, (w₀/W₀)//z } – множество рассогласований

11. S₄=S₃  { f((g((z/Z₁)//Z)/X₀)//a₁)/w₀}

W₄= { P( (a₁/A₁)//X, (g((z/Z₁)//Z)/X₀)//a₁, (z/Z₁)//Z,

(f((g((z/Z₁)//Z)/X₀)//a₁)/W₀)//z ),

P( (a₁/A₁)//X, (g((z/Z₁)//Z)/X₀)//a₁, (z/Z₁)//Z,

(f((g((z/Z₁)//Z)/X₀)//a₁)/W₀)//z ) } =

{ P( (a₁/A₁)//X, (g((z/Z₁)//Z)/X₀)//a₁, (z/Z₁)//Z, (f((g((z/Z₁)//Z)/X₀)//a1)/W₀)//z ) }

12. W₄ - одноэлементное множество; S=S_k

Стоп.

В качестве процедуры вывода используется линейная входная резолюция, которая является полной для хорновских дизъюнктов и обладает большей эффективностью по сравнению с разработанными модификациями принципа резолюции.

Рис. 22. Иерархические структуры для примера 3

Рис. 23. Иерархические структуры для примера 3