Унификация. Одним из наиболее важных аспектов программирования на Про­логе являются понятия

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

Пролог пытается отождествить термы при доказательстве, или согласовании, целевого утверждения. Например, в программе из гл. 1 для согласования запроса?- собака(Х) целевое утверждение соба­ка (X) было отождествлено с фактом собака (реке), в результате чего переменная Х стала конкретизированной: Х= рекc.

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

В том случае, когда переменные содержатся только в хвостовых целевых утверждениях, правило считается доказанным, если хвосто­вое целевое утверждение истинно для одного или более значений пе­ременных. Переменные, содержащиеся только в хвостовых целевых утверждениях, связаны квантором существования. Таким образом, они принимают конкретные значения на то время, когда целевое ут­верждение, в котором переменные были согласованы, остается дока­занным.

Терм Х сопоставляется с термом Y по следующим правилам. Ес­ли Х и Y - константы, то они сопоставимы, только если они одинако­вы. Если Х является константой или структурой, а Y - неконкретизи­рованной переменной, то Х и Y сопоставимы и Y принимает значе­ние Х (и наоборот). Если Х и Y - структуры, то они сопоставимы тог­да и только тогда, когда у них одни и те же главный функтор и ар­ность и каждая из их соответствующих компонент сопоставима. Если Х и Y - неконкретизированные (свободные) переменные, то они со­поставимы, в этом случае говорят, что они сцеплены. В (Таблица 2) при­ведены примеры отождествимых и неотождествимых термов.

Таблица 2. Иллюстрация унификации.

Терм1	Терм2	Отождествимы?
джек(Х) джек (личность) джек(Х,Х) джек(Х.Х) джек(.) 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)).

дает ответ

да

Отрицания операторов = и - = записываются как \= и \= = соот­ветственно.

Дата добавления: 2015-07-14