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