Механизм возврата

Механизм возврата и процедурная семантика

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

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

В качестве примера рассмотрим утверждения:

меньше(X.Y) :-

XY, write(X),

write ('меньше, чем'),write(Y).

меньше(Х.У) :-

XY, write(Y),

write ('меньше, 4CM'),write(X).

Целевое утверждение

?- меньше (5, 2).

сопоставляется с головой первого утверждения при Х=5 и У=2. Одна­ко не удается согласовать первый член конъюнкции в теле утвержде­нияX<Y. Значит, Пролог нс может использовать первое утвержде­ние для согласования целевого утверждения меньше(5, 2). Тогда Пролог переходит к следующему утверждению, голова которого со­поставима с целевым утверждением. В нашем случае это второе утверждение. При значениях переменных Х=5 и Y=2 тело утверждения согласуется. Целевое утверждениеменьше(5,2) доказано, и Пролог выдает сообщение «2 меньше, чем 5». Запрос

?-меньше (2, 2).

сопоставляется с головой первого утверждения, но тело утверждения согласовать не удается. Затем происходит сопоставление с головой второго утверждения, но согласовать тело опять-таки оказывается невозможно. Поэтому попытка доказательства целевого утвержде­ния меньше(2, 2) заканчивается неудачей.

Такой процесс согласования целевого утверждения путем прямого продвижения по программе мы называем прямой трассировкой (forward tracking). Даже если целевое утверждение согласовано, с помощью прямой трассировки мы можем попытаться получить другие варианты его доказательства, т.е. вновь согласовать целевое утверждение.

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