Логическое программирование

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

P:-Q,R.

где P, Q и R есть некоторые термы. В декларативной интерпретации это значит "P истинно, если Q и R истинны" или "Из Q и R следует P". А в процедурной интерпретации – "Чтобы решить задачу P, сначала нужно решить подзадачу Q, а затем – подзадачу R".

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

Декларативный смысл программы определяет, является ли данная цель истинной и, если да, при каких значениях переменных она истинна. Для точного определения декларативного смысла определим понятие конкретизации предложения. Конкретизацией предложения `C` называется результат подстановки в него на место каждой переменной некоторого терма. Подстановка, позволяющая сделать равными два терма, называется унификатором.

Пусть дана некоторая программа и цель (запрос) `G`. Цель G истинна (логически следует из программы) тогда и только тогда, когда в программе существует такое предложение `C`, для которого существует такая конкретизация `Z`, что 1) голова `Z` совпадает с `G`, и 2) все цели в теле `Z` истинны. Для определения конкретизации `Z` достаточно выполнить сопоставление головы `C` и цели `G` по ранее рассмотренному алгоритму, который дает наиболее общий унификатор.

Процедурная семантика определяет, как Пролог-система отвечает на запросы. Эту процедуру можно описать следующим образом. Пусть `G_1,G_2,…,G_m` – список текущих целей. Если список целей пуст – работа процедуры завершается успехом, выводятся значения подстановок для переменных, содержавшихся в исходном запросе. Если список не пуст, просматриваются предложения программы от начала к концу до обнаружения предложения `C`, у которого голова сопоставима с целью `G_1`. Если такого предложения нет, то работа процедуры завершается неудачей. Если предложение `C` найдено и имеет вид "`H:–B_1,…,B_n.`", то выполняется переименование переменных в `C` таким образом, чтобы в предложении и в списке целей не было одинаковых переменных. После этого выполняется сопоставление цели `G_1` и головы `H`. Подстановка, унифицирующая эти термы, используется для замены переменных в теле правила `B_1,…,B_n` и в списке целей `G_2,…,G_m`. Новым списком целей становится список `B’_1,…,B’_n,G’_2,…,G’_m`. Для вычисления его истинности вызывается рекурсивно та же самая процедура. Если ее выполнение завершается успехом, то вычисление истинности списка целей `G_1,\ G_2,\ …,\ G_m` также успешно. Если же выполнение завершается неудачей, то происходит возврат к старому списку целей `G_1,G_2,…,G_m`, и продолжается просмотр текста программы, начиная с предложения, непосредственно следующего за предложением `C`, в поисках другого предложения, которое позволит доказать истинность запроса.

Рассмотрим пример программы.

большой(медведь).          % 1
большой(слон).             % 2
маленький(кот).            % 3
коричневый(медведь).       % 4
черный(кот).               % 5
серый(слон).               % 6
темный(Z):-черный(Z).      % 7
темный(Z):-коричневый(Z).  % 8

Пусть запрос (исходный список целей) имеет вид

?-темный(X),большой(X).

Просматриваем программу, чтобы найти предложение, голова которого сопоставима с первой целью темный(X). Предложение 7 будет найдено первым. После замены первой цели конкретизированным телом предложения 7 список целей будет иметь вид

черный(X),большой(X).

Программа просматривается снова в поисках предложения, голова которого сопоставима с целью черный(X). Находим предложение 5. У этого предложения нет тела, поэтому список целей после подстановки X=кот сокращается до

большой(кот).

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

черный(X),большой(X)

и продолжаем просмотр программы после предложения 5 для определения предложения, голова которого сопоставима с целью черный(X). Ни одно предложение не найдено. Возвращаемся к списку целей

темный(X),большой(X).

Такой процесс отмены выполненных конкретизаций переменных и восстановления старого списка целей называется возвратом (backtracking). Продолжаем просмотр программы после предложения 7. Находим предложение 8. Заменив первую цель телом предложения после подстановки Z=X, получим

коричневый(X),большой(X).

Просматриваем программу и находим предложение 4. После использования подстановки X=медведь списком целей станет

большой(медведь).

После просмотра программы обнаруживаем предложение 1, у которого нет тела. Список целей становится пустым. Это указывает на успешное завершение, и решение было получено при X=медведь.