Prolog #8.1: Семантика – Вычислительная модель

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

1. Выберем атом из запроса и определим, есть ли факт, или голова правила с которой можно унифицировать этот атом. Если нет, тогда запрос ошибочен.
2. Разрешить запрос фактом или правилом заменяя атом телом правила (в случае факта это означает просто удаление атома)

Этот цикл повторяется до тех пор, пока запрос не зафейлится, или атом не будет удален. В под главах мы посмотрим на этот процесс более детально.

8.1. Унификация

Унификация – это процесс нахождения унификатора для двух атомов. Для того, чтобы унифицироваться два атома должны обладать одинаковой структурой, если мы игнорируем константы и переменные. Так как атомы могут содержать вложенные применения функций в их аргументах, нам потребуется рекурсивный алгоритм.

Давайте начнем с некоторых определений, которые сделают определение алгоритма более понятным.

Definition 1

Терм определяется индуктивно так:

1. Переменная или константа – это терм.
2. Если f – это н-арная имя функции и t1…tn – это термы, тогда f(t1,…,tn) – тоже терм.
3. Любое выражение терм только тогда, когда оно получено используя 1 и 2.

Definition 2

Пусть p – это н-арный предикат и t1,…,tn – термы. Тогда p(t1, …, tn) – это атом.

Интуитивно, алгоритм унификации сначала проверят чтобы два атома начинались с одного и того же предикатного символа – если нет, значит не унифицируется. Если совпадают, тогда алгоритм проверяет что термы обладают той же структурой. Создается стэк, состоящий из пар соответствующих термов (из двух атомов). На данный момент алгоритм последовательно удаляет пары термов сверху стека и сравнивает их структуры. До тех пор, пока они совпадают, алгоритм продолжает работу; если встречено критическое различие, тогда атомы не могут быть унифицированы и алгоритм завершается. Алгоритм будет продолжать обрабатывать пары из стэка пока стэк не пуст, а к тому  моменту унификатор (наиболее общий) должен быть найден.

Перед тем как продолжать, пересмотрим определения главы 8.3 для подстановки, примера, унификатора и наиболее общего унификатора.

Definition 3

Алгоритм унификации
Предположим, что A_1(t_1, …, t_n) и A_2(s_1, …, s_m) – атомы.
Алгоритм: 
   Если A_1 и A_2 разные предикаты или n <= m
     Тогда вывод зафейлен
   Иначе
     Инициализировать подстановку пустой подстановкой
     стэк - парами (t_i, s_i)
     Failure - false
   Пока стэк не пуст и !Failure делать:
     pop (X, Y) из стэка
     case 
       X - это переменная которой нет в Y
         заменить Y на X в стэке
         и в подстановке 
         добавить X = Y в подстановку

       Y - это переменная, которой нет в X:
         заменить X на Y в стэке
         и подстановке
         добавить Y = X в подстановку

       X и Y - одинаковые константы или переменные
         continue

       X - это f(x_1, ..., x_n) и Y - это (y_1, ..., y_n)
         для некоторой функции f и n > 0:
         push (x_i, y_i), i = 1, ..., n, на стэке
      
       иначе: Failure = true

Если Failure - вывести Failed
Иначе - вывести подстановку

Есть несколько вещей, которые вы должны знать об этом алгоритме:

1. Наиболее важной вещью являются то, что если два атома унифицируются, тогда алгоритм всегда возвращает наиболее общий унификатор для двух атомов.
   
2. В первых двух компонентах выражения case “нет в” называется проверкой вхождения. Это условие ограждает от подстановки такой как X = f(X), которая не может быть унифицирована в конечное время. Интересная штука, это то, что проверка вхождения очень требовательна к вычислительным ресурсам, так что большинство реализаций Пролога не используют её. Это делает реализацию быстрой, но не безопасной.

Пример 8 – Пример унификации I

Рассмотрим два атома p(a, f(Y)) и p(X, f(g(X))) – унифицируются ли они? Запустив алгоритм на этих атомах получим следующую трассировку:

1. Изначально: Та как предикаты те же (имя совпадает), то стэк будет [(a,X), (f(Y ), f(g(X)))], и Om = fi.
   
2. Pop(a, X) из стэка, оставляя [(f(Y ), f(g(X)))]. По второму случаю мы устанавливаем Om = {X = a} и применяем Om к стэку, что дает [(f(Y ), f(g(a)))].
   
3. Pop(f(Y), f(g(a))) из стэка, оставляя []. По четвертому случаю, стэк – [(Y, g(a)], Om ничего не присваивается.
   
4. Pop(Y, g(a)) из стэка, оставляя []. По первому случаю, Om = {X = a, Y = g(a)} – т.к стэк пустой можно не применять подстановку
   
5. 
   

   Стэк пустой, Om = {X = a, Y = g(a)} – это наиболее общий унификатор для двух атомов.

Пример 9 – Пример унификации II

Рассмотрим два атома p(a, f(X)) и p(X, f(b)) – унифицируются? Быстрая проверка заставляет нас подумать, что ответ – нет, ибо Х должен иметь а и b в качестве подставляемых значений. Как это получить из алгоритма? Следующий список отражает то, что происходит в течении каждого прохода через алгоритм.

1. Изначально: Так как имена предикатов совпадают, мы устанавливаем стэк [(a,X), (f(X), f(b))] и Om = fi.


2. Pop(a, X) из стэка, оставляя [(f(X), f(b))]. По второму случаю получаем Om = {X = a} и применяем подстановку к стеку, получая [(f(a), f(b))].


3. Pop(f(a), f(b)) из стэка, оставляя []. По четвертому случаю, мы присваиваем стэку [(a, b)], ничего не присваивая Om.


4. Pop(a, b) из стэка, оставляя []. По третьему случаю, так как а и b разные константы, алгоритм возвращает false.