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

8.2 Резолюция

После того, как интерпретатор Пролог принял запрос от пользователя, интепретатор проходит через цикл в котором есть две активности: унификация и резолюция. С унификацией мы только что разобрались. Перед тем как смотреть резолюцию мы посмотрим на действия интепретатора более глубоко. Когда интерпретатор вводит запрос у него есть программа, состоящая из фактов и правил, и запроса которые есть конъюнкция атомов. Интерпретатор запускает следующий алгоритм

Пока запрос не пуст:
  выбрать атом из запроса
  выбрать факт или правило с которым атом унифицирется

  Если их нет вернуть failed
  Иначе
    если выбран факт
    Тогда
      убрать атом из запроса
    Иначе, если выбрано правило
      заменить атом в запросе
      на тело выбранного правила

вернуть succeeded

Этот алгоритм игнорирует много деталей, но несет в себе сущность (главное) действий интерпретатора. Подстройка к запросу, которая появляется если унификация успешна – это и есть процесс резолюции. Теперь мы детализируем что происходит во время резолюции.

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

На самом деле, есть два вопроса. Для начала, как мы используем наибольший общий унификатор возвращаемый алгоритмом чтобы определить значения подстановок? Далее, как мы можем убедиться что вернули все возможные значения подстановок? Этот вопрос привносит процесс называемый бэктрекингом и это то, что происходит, когда пользователь печатает точку с запятой.

8.3 Запросы

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

Запросы позволяют вопросам обрабатываться в зависимости от информации заложенной в программе. В случае, если запрос содержит 0 переменных, на вопрос будет дан ответ “да” или “нет”. Этот тип запроса называется основным вопросом. Например, запрос

?- edge(a, b).

вопрошает есть ли грань от а к b. Если запрос выводим из программы, Пролог возвратит “да”. Иначе будет возвращено “нет”. Заметьте, что точка тоже обязательная часть запроса.

Более сложный запрос – запрос в котором более одного атома. Например, запрос

?- edge(a, b),edge(e, b).

означает вопрос: “Есть ли грань от узла а к узлу b И от узла e к узлу b"?”. Отсюда похоже на запятые встречающихся в телах правил, запятая которая находится внутри запроса обрабатывается как конъюнкция. Оглядываясь на программу, показанную в Примере 2.1 – легко увидеть, что Пролог ответит “да” на оба запроса

?- edge(a, b). %% и
?- edge(a, b),edge(e, b).’

С другой стороны, Пролог отвечат “нет” на запрос

?- edge(b, a).

так как нет ребра из узла b в узел a.

Атомы в запросе могут содержать переменные. Они называются не основными запросами. Запрос

?- edge(a, X).

является примером не основного запроса. Переменные которые есть в запросе обрабатываются как экзистенциальные. Это означает, что их значения схожи с переменными, которые находятся в теле правила, но не в голове того же правила. Запрос

?- edge(a, X).

отсюда, обозначает вопрос “Существует ли узел Х такой, что существует грань из узла а к Х?”. Обращаясь снова к Примеру 2.1 мы ожидаем что Пролог возвратит “да”, так как узел а соединен с узлами а и е. И в самом деле, это и есть ответ Пролога. Однако, в дополнении к этому, Пролог предоставит объяснение (в данном случае узел) для переменной Х в запросе, который объясняет почему запрос истинен. Отсюда, объяснение для Х в данном запросе должно быть или b или е. Чтобы разъяснить это, если мы запустим запрос

?- edge(a, X).

Пролог ответит: X = b, что обозначает “Есть такой Х, что edge(a, X) истинен, и b это один такой Х.

Механизм пролога для нахождения обоснований для переменных называется унификаций. Можно думать об этом как об обобщенном сопоставлении по образцу. Следующие определения формализуют это.

Definition 4

Подстановка – это конечное множество равенств

{X1 = t1,X2 = t2, . . . , Xn = tn}, где каждый Хi – это переменная, и ti – это терм, X1, …, Xn – различные переменные, и Xi отлична от ti. Каждое Xi = ti называется привязкой для Xi.

Обычно, мы обозначаем подстановки греческой буквой Om, …, возможно с индексом.

Пример 10 – Подстановка

Множество Om = {X = a, Y = b} – это подстановка, но y = {X = a, X = b} и бl = {X = a, Y = Y} нет, потому что в y одна и таже переменная появляется дважды на левой стороне привязки. В бl привязка Y = Y нарушает ограничение, что каждый Xi должен отличаться от ti в определении подстановки.

Definition 5

Предположим Om – это подстановка {X = b, Y = a}, y – это подстановка {X = Y, Y = a} и бl – подстановка {X = Y, Y = a, W = b}. предположим Е – это атом p(X, Y, Z). Тогда

1. ЕOm = p(b, a, Z).


2. Ey = p(Y, a, Z).


3. Eбl = p(Y, a, Z). – да уж название получилось)

В первом случае переменные X и Y в Е заменены на b и а. Заметьте, что переменная Z не затронута подстановкой Om, потому что нет привязки вида Z = t.

Во втором случае, важно обнаружить, что замена переменных термами происходит одновременно. Так, переменные X в Е заменены на Y в то же время как Y заменен на a. Мы не меняем Y на а в результирующем выражении – не p(a, a, Z) получается.

Последний случай демонстрирует что могут существовать привязки в подстановке, которые не влияют на выражение. Так, тут т.к. в Е нет W, привязка W = b излишня.

Предположим, что А и B два выражения. Подстановка Om называется унификатором А и B если AOm синтаксически идентично BOm. Мы говорим, что А и B унифицируются если существует унификатор.

Если, вдобавок, Om – это наименьшая возможная подстановка, унифицирующая два атома, мы говорим, что Om – это наиболее общий унификатор, НОУ.