Пролог-автомат (pa) в поисковом движке FAIND: унификация термов

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

Пролог-машина пытается отождествить термы при доказательстве, или согласовании, целевого утверждения.

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

смертен(Некто) :- человек(Некто).

переменная Некто неявно квантифицируется как "любой".

Переменные принимают конкретные значения на время доказательства целевого утверждения.

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

Терм Х сопоставляется с термом 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