ВВОД программ
Введение списка утверждений в Пролог-систему осуществляется с помощью встроенного предиката consult. Аргументом предиката consult является атом, который обычно интерпретируется системой как имя файла, содержащего текст программы на Прологе. Файл открывается, и его содержимое записывается в базу данных. Если в файле встречаются управляющие команды, они сразу же выполняются. Возможен случай, когда файл не содержит ничего, кроме управляющих команд для загрузки других файлов. Для ввода утверждений с терминала в большинстве реализации Пролога имеется специальный атом, обычно user. С его помощью утверждения записываются в базу данных, а управляющие команды выполняются немедленно.
Помимо предиката consult, в Прологе существует предикат reconsult. Он работает аналогичным образом. Но перед добавлением утверждений к базе данных из нее автоматически удаляются те утверждения, головные цели которых сопоставимы с целями, содержащимися в файле перезагрузки. Такой механизм позволяет вводить изменения в базу данных. В Прологе имеются и другие методы добавления и удаления утверждений из базы данных. Некоторые реализации языка поддерживают модульную структуру, позволяющую разрабатывать модульные программы.
|
|
В заключение раздела дадим формальное определение синтаксиса Пролога, используя форму записи Бэкуса-Наура, иногда называемую бэкусовской нормальной формой (БНФ).
запрос::- голова утверждения
правило::– голова утверждения:- хвост утверждения
факт::- голова утверждения
голова утверждения::-атом | структура
хвост утверждения::- атом структура,
термы::-терм [,термы]
терм::- число | переменная | атом | структура
структура::-атом (термы)
Данное определение синтаксиса не включает операторную, списковую и строковую формы записи. Полное определение дано в приложении А. Однако, любая программа на Прологе может быть написана с использованием вышеприведенного синтаксиса. Специальные формы только упрощают понимание программы. Как мы видим, синтаксис Пролога не требует пространного объяснения. Но для написания хороших программ необходимо глубокое понимание языка.
Одним из наиболее важных аспектов программирования на Прологе являются понятия унификации (отождествления) и конкретизации переменных.
Пролог пытается отождествить термы при доказательстве, или согласовании, целевого утверждения. Например, в программе из гл. 1 для согласования запроса?- собака(Х) целевое утверждение собака (X) было отождествлено с фактом собака (реке), в результате чего переменная Х стала конкретизированной: Х= рекc.
Переменные, входящие в утверждения, отождествляются особым образом - сопоставляются. Факт доказывается для всех значений переменной (переменных). Правило доказывается для всех значений переменных в головном целевом утверждении при условии, что хвостовые целевые утверждения доказаны. Предполагается, что переменные в фактах и головных целевых утверждениях связаны квантором всеобщности. Переменные принимают конкретные значения на время доказательства целевого утверждения.
|
|
В том случае, когда переменные содержатся только в хвостовых целевых утверждениях, правило считается доказанным, если хвостовое целевое утверждение истинно для одного или более значений переменных. Переменные, содержащиеся только в хвостовых целевых утверждениях, связаны квантором существования. Таким образом, они принимают конкретные значения на то время, когда целевое утверждение, в котором переменные были согласованы, остается доказанным.
Терм Х сопоставляется с термом Y по следующим правилам. Если Х и Y - константы, то они сопоставимы, только если они одинаковы. Если Х является константой или структурой, а Y - неконкретизированной переменной, то Х и Y сопоставимы и Y принимает значение Х (и наоборот). Если Х и Y - структуры, то они сопоставимы тогда и только тогда, когда у них одни и те же главный функтор и арность и каждая из их соответствующих компонент сопоставима. Если Х и Y - неконкретизированные (свободные) переменные, то они сопоставимы, в этом случае говорят, что они сцеплены. В (Таблица 2) приведены примеры отождествимых и неотождествимых термов.
Таблица 2. Иллюстрация унификации.
Терм1 | Терм2 | Отождествимы? |
джек(Х) джек (личность) джек(Х,Х) джек(Х.Х) джек(.) f(Y,Z) Х | джек (человек) джек (человек) джек(23,23) джек (12,23) джек(12,23) Х Z | да: Х=человек нет да: Х=23 нет да да: X=f(Y,Z) да: X=Z |
Заметим, что Пролог находит наиболее общий унификатор термов. В последнем примере (рис.2.1) существует бесконечное число унификаторов:
X-1, Z-2; X-2, Z-2;....
но Пролог находит наиболее общий: Х=Z.
Следует сказать, что в большинстве реализации Пролога для повышения эффективности его работы допускается существование циклических унификаторов. Например, попытка отождествить термы f(X) и Х приведет к циклическому унификатору X=f(X), который определяет бесконечный терм f(f(f(f(f(...))))). В программе это иногда вызывает бесконечный цикл.
Возможность отождествления двух термов проверяется с помощью оператора =.
Ответом на запрос
?- 3+2=5.
будет
нет
так как термы не отождествимы (оператор не вычисляет значения своих аргументов), но попытка доказать
?-строка(поз(Х)) -строка(поз(23)).
закончится успехом при
Х=23.
Унификация часто используется для доступа к подкомпонентам термов. Так, в вышеприведенном примере Х конкретизируется первой компонентой терма поз(23), который в свою очередь является компонентой терма строка.
Бывают случаи, когда надо проверить, идентичны ли два терма. Выполнение оператора = = заканчивается успехом, если его аргументы - идентичные термы. Следовательно, запрос
?-строка(поз(Х)) --строка (поз (23)).
дает ответ
нет
поскольку подтерм Х в левой части (X - свободная переменная) не идентичен подтерму 23 в правой части, Однако запрос
?- строка (поз (23)) --строка (поз (23)).
дает ответ
да
Отрицания операторов = и - = записываются как \= и \= = соответственно.