Стили и методы программирования




Управление исполнением программы


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

Пример 6.3.1. Две последовательности выражений


где a, b — константы, а латинские буквы из конца алфавита — переменные, унифицируются в


подстановкой


А в двух последовательностях


никакие два соответственных выражения унифицированы быть не могут.

Уже в приведенном примере видно, что унификация — глобальная операция.

Заметим, что логический алгоритм унификации обладает свойством частичного исполнения: если унифицировать две подструктуры, то после исполнения унифицирующей подстановки можно продолжить унификацию остальных подструктур, и результат унификации не изменится. Так что выражения могут унифицироваться одно за другим5).

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

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

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


Содержание  Назад  Вперед