Выполнение и трассировка программы

Алгоритм выполнения Пролог-программы основан на механизме прямого перебора с возвратом и операции сопоставления (унификации).

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

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

Если при поиске решения обнаружено несколько вариантов доказательства истинности цели, то Пролог-система запоминает альтернативные варианты решения - точки возврата.

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

РАССМОТРИМ ПРИМЕР ВЫПОЛНЕНИЯ ПРОЛОГ-ПРОГРАММЫ

База знаний:

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

a(1).

a(Y):- c(Y),d(Y).

b(2).

c(1).

c(2).

d(2).

e.

Запрос

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

ДЕРЕВО ВЫВОДА

На рисунках представлено дерево вывода. Жирными линиями в дереве обозначены И-деревья– для доказательства такого дерева необходимо, чтобы каждая его ветка «опиралась» на истинное утверждение. ИЛИ-деревья исходят из вершин с точками возврата, такое дерево истинно, если хотя бы одна ветка опирается на истинное утверждение. Пунктирные линии – альтернативные ветки, не рассматриваемые на данном этапе (либо ложные, либо еще не рассмотренные).

В данном примере получение решения складывается из трех этапов. Вначале рассматривается первая подцель – она имеет два предложения в базе, заголовки которых сопоставимы с ней, поэтому она является точкой возврата. Выбирается первое сверху предложение – это факт a(1), при этом свободная переменная X получает значение 1. Первая цель запроса доказана. Вторая цель - b(1) (X уже связана со значением 1) не сопоставляется ни с одним правилом базы, следовательно, является ложной.

Бэктрекинг – возврат к ближайшей точке возврата, т.е. a(X). На втором дереве отображен вывод по второй альтернативе. Связываются две переменные X из запроса и Y из правила для предиката a. Фактически запрос ?-a(X),b(X),e подменяется на новый набор целей ?‑c(Y),d(Y),b(Y),e. Первая подцель – это c(Y) – она является новой точкой ветвления, так как унифицируется с двумя предложениями в базе. Первое предложение – факт приводит к унификации Y с 1, но следующая в наборе подцель d(1) – ложна.

Третье дерево отражает альтернативу для c(Y) с унификацией Y=2. Для этой альтернативы истинны все последующие цели из набора (они унифицируются с соответствующими фактами).