2.7. Замечания о взаимосвязи между Прологом и логикой

2.7. Замечания о взаимосвязи между Прологом и логикой

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

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

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

Упражнение

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

?- X = f( X).

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

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