Интеллектуальные информационные системы. Макаренко С.И. - 126 стр.

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


                                     125