НОУ ІНТУІТ, Лекція, Мова програмування Пролог
Уніфікація
Однією з найважливіших аспектів програмування на Пролозі є поняття уніфікації ( ототожнення ) і конкретизації змінних.
Пролог намагається ототожнити терми за підтвердження, чи узгодження, цільового затвердження. Наприклад, у програмі з "Базові поняття" для узгодження запиту - собака (Х) цільове твердження собака (X) було ототожнено з фактом собака (Рекс), в результаті чого змінна Х стала конкретизованою: Х = рекc.
Змінні, що входять до тверджень, ототожнюються особливим чином — зіставляються. Факт доводиться всім значень змінної (змінних). Правило доводиться всім значень змінних у головному цільовому твердженні за умови, що хвостові цільові твердження доведені. Передбачається, що змінні у фактах та головних цільових твердженнях пов'язані квантором загальності. Змінні набувають конкретних значень на час доказу цільового затвердження.
У тому випадку, коли змінні містяться тільки в хвостових цільових твердженнях, правило вважається доведеним, якщо цільове хвостове твердження істинно для одного або більше значень змінних. Змінні, що містяться лише у хвостових цільових твердженнях, пов'язані квантором існування. Таким чином, вони набувають конкретних значень на той час, коли цільове твердження, в якому змінні були узгоджені, залишається доведеним.
Терм Х зіставляється з термом Y за такими правилами. Якщо Х і Y — константи, то вони можна порівняти, тільки якщо вони однакові. Якщо Х є константою чи структурою, а Y — неконкретизованою змінною, то Х і Y можна порівняти і Y набуває значення Х (і навпаки). Якщо Х і Y - структури, то вони порівняні тоді і тількитоді, коли вони одні й самі головний функтор і арность і з їх відповідних компонент сопоставима. Якщо Х і Y - неконкретизовані (вільні) змінні, то вони можна порівняти, в цьому випадку кажуть, що вони зчеплені. (Таблиця 7.1) наведено приклади ототожнюваних та неототожних термів.
| джек(Х) | джек (людина) | так: Х = людина |
| джек (особистість) | джек (людина) | ні |
| джек(Х,Х) | джек(23,23) | так: Х = 23 |
| джек(Х.Х) | джек (12,23) | ні |
| джек( . ) | джек(12,23) | так |
| f(Y,Z) | Х | так: X = f (Y, Z) |
| Х | Z | так: X = Z |
Зауважимо, що Пролог знаходить найбільш загальний уніфікатор термів. В останньому прикладі (табл.7.1) існує нескінченна кількість уніфікаторів:
Проте Пролог знаходить найбільш загальний: Х = Z.
Слід сказати, що у більшості реалізацій Прологу підвищення ефективності його роботи допускається існування циклічних уніфікаторів . Наприклад, спроба ототожнити терми f(X) і Х призведе до циклічного уніфікатора X=f(X) , який визначає нескінченний терм (f(f(f(f(. ))))))) . У програмі це іноді викликає нескінченний цикл.
Можливість ототожнення двох термів перевіряється за допомогою оператора = .