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



              

Развитие языка Prolog


Британско-канадская группа, создававшая Prolog, первоначально ориентировалась на задачи математической лингвистики, где сложные преобразования данных сопряжены с проверкой гипотез.

Это естественно навело их на ортогональный Рефалу подход1), формально мотивированный математической логикой. Наличие именно формальной мотивировки оказало медвежью услугу языку Prolog и всему направлению. Его сущность оказалась замаскирована примитивным методологически-теоретическим анализом и неадекватным названием: логическое программирование.

Prolog вдохновлялся ограничением классического исчисления предикатов, предложенным Хорном. Как известно (см., например, книгу [20]), в классической логике в любой достаточно богатой теории появляются чистые теоремы существования, когда из доказательства невозможно выделить построение требуемого объекта. Если ограничиться конъюнкциями импликаций вида

x1, . . . , xn
y1, . . . , yk . . . (A1&· · ·&An
B),

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

¬A. Такие формулы называются хорновыми.

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

x1, . . . , xn (A1&· · ·&An
B).

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

x1, . . . , xn (¬A1
· · ·
¬An
B).

Именно от последней формы представления хорновых утверждений получила имя основная структура данных языка Prolog. Но тот факт, что импликация преобразована в дизъюнкцию, на самом деле нигде в этом языке не используется, он послужил лишь для установления взаимосвязей с алгоритмом метода резолюций [30], который в тот момент был последним криком моды в автоматическом доказательстве теорем (и действительно громадным концептуальным продвижением).


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