Prolog

Синтаксис Пролога - это синтаксис предложений логики предикатов первого порядка, записанных в так называемой форме предложений (форме, при которой кванторы не выписываются

явно), а точнее, в виде частного случая таких предложений - в виде

формул Хорна

(предложений, имеющих самое большее один положительный литерал). Клоксин и Меллиш (1981 г.) приводят пролог-программу, которая преобразует предложения исчисления предикатов

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

принципе резолюций

, применяющемся для автоматического доказательства теорем, который был предложен Робинсоном в его классической статье (1965 г.). В Прологе используется особая стратегия доказательства теоремы методом резолюций, носящая название SLD. Введение в исчисление предикатов первого порядка и доказательство теорем, основанное на методе резолюций, можно найти у Нильсона (1981 г.). Математические вопросы, касающиеся свойств процедурной семантики Пролога в их связи с логикой, проанализированы Ллойдом (1984 г.)

.

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

Упражнение

2. 10.    Что будет, если пролог-системе задать такой вопрос:

        ?-   Х  =  f( X).

Успешным или неуспешным будет здесь сопоставление? По определению унификации в логике, сопоставление должно быть неуспешным, а что будет в соответствии с нашим определением сопоставления из раздела 2.2? Попробуйте объяснить, почему многие реализации Пролога отвечают на вышеприведенный вопрос так:

        X  =   f(f(f(f(f(f(f(f(f(f(f(f(f(f(f( ...

Посмотреть ответ

Резюме

К настоящему моменту мы изучили нечто вроде базового Пролога, который называют еще "чистый Пролог". Он "чист", потому что довольно точно соответствует формальной логике. Расширения, преследующие цель приспособить язык к некоторым практическим нуждам, будут изучены дальше (гл. 3, 5, 6. 7). Важными моментами данной главы являются следующие:

Простые объекты в Прологе - это атомы, переменные и числа. Структурные объекты, или структуры, используются для представления объектов, которые состоят из нескольких компонент.

Структуры строятся посредством функторов. Каждый функтор определяется своими именем и арностью.

Тип объекта распознается исключительно по его синтаксической форме.

Область известности (лексический диапазон) переменных - одно предложение. Поэтому одно и то же имя в двух предложениях обозначает две разные переменные.

Структуры могут быть естественным образом изображены в виде деревьев. Пролог можно рассматривать как язык обработки деревьев.

Операция сопоставление берет два терма и пытается сделать их идентичными, подбирая соответствующую конкретизацию переменных в обоих термах.

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

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

Запятая между целями означает их конъюнкцию. Точка с запятой между целями означает их дизъюнкцию.

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

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

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

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

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

В данной главе обсуждались следующие понятия:

объекты данных:

        атом, число, переменная, структура

терм

функтор, арность функтора

главный функтор терма

сопоставление термов

наиболее общая конкретизация

декларативная семантика