Отождествимы ?
джек (личность)
джек(Х,Х)
джек(Х.Х)
джек( . )
f(Y,Z)
Х
джек (человек)
джек(23,23)
джек (12,23)
джек(12,23)
Х
Z
нет
да: Х=23
нет
да
да: X=f(Y,Z)
да: X=Z
Заметим, что Пролог находит наиболее общий унификатор термов. В последнем примере (рис.2.1) существует бесконечное число унификаторов:
X-1, Z-2; X-2, Z-2; ....
но Пролог находит наиболее общий: Х=Z.
Следует сказать, что в большинстве реализации Пролога для повышения эффективности его работы допускается существование циклических унификаторов. Например, попытка отождествить термы f(X) и Х приведет к циклическому унификатору X=f(X), который определяет бесконечный терм f(f(f(f(f(...))))). В программе это иногда вызывает бесконечный цикл.
Возможность отождествления двух термов проверяется с помощью оператора =.
Ответом на запрос
?- 3+2=5.
будет
нет
так как термы не отождествимы (оператор не вычисляет значения своих аргументов), но попытка доказать
?-строка(поз(Х)) -строка(поз(23)).
закончится успехом при
Х=23.
Унификация часто используется для доступа к подкомпонентам термов. Так, в вышеприведенном примере Х конкретизируется первой компонентой терма поз(23), который в свою очередь является компонентой терма строка.
Бывают случаи, когда надо проверить, идентичны ли два терма. Выполнение оператора = = заканчивается успехом, если его аргументы - идентичные термы. Следовательно, запрос
?-строка(поз(Х)) --строка (поз (23)).
дает ответ
нет
поскольку подтерм Х в левой части (X - свободная переменная) не идентичен подтерму 23 в правой части, Однако запрос
?- строка (поз (23)) --строка (поз (23)).
дает ответ
да
Отрицания операторов = и - = записываются как \= и \= = соответственно.
