Стили и методы программирования
Развитие языка Prolog
Британско-канадская группа, создававшая Prolog, первоначально ориентировалась на задачи математической лингвистики, где сложные преобразования данных сопряжены с проверкой гипотез.
Это естественно навело их на ортогональный Рефалу подход1), формально мотивированный математической логикой. Наличие именно формальной мотивировки оказало медвежью услугу языку Prolog и всему направлению. Его сущность оказалась замаскирована примитивным методологически-теоретическим анализом и неадекватным названием: логическое программирование.
Prolog вдохновлялся ограничением классического исчисления предикатов, предложенным Хорном. Как известно (см., например, книгу [20]), в классической логике в любой достаточно богатой теории появляются чистые теоремы существования, когда из доказательства невозможно выделить построение требуемого объекта. Если ограничиться конъюнкциями импликаций вида
где каждая составляющая является элементарной формулой и само доказанное утверждение имеет такой же вид, то получить построение из доказательства возможно, поскольку у нас не остается даже косвенных способов сформулировать и нетривиально использовать что-либо похожее на A
От лишних кванторов можно избавиться при помощи сколемизации, когда кванторы существования заменяются на функцию, аргументами которой являются все переменные, связанные ранее стоящими кванторами всеобщности2). Таким образом, мы приходим к простейшему виду хорновых формул (хорновы импликации):
Применив к последней формуле преобразование, выполненное лишь в классической логике, мы приходим к хорновым дизъюнктам:
Именно от последней формы представления хорновых утверждений получила имя основная структура данных языка Prolog. Но тот факт, что импликация преобразована в дизъюнкцию, на самом деле нигде в этом языке не используется, он послужил лишь для установления взаимосвязей с алгоритмом метода резолюций [30], который в тот момент был последним криком моды в автоматическом доказательстве теорем (и действительно громадным концептуальным продвижением).
Forekc.ru
Рефераты, дипломы, курсовые, выпускные и квалификационные работы, диссертации, учебники, учебные пособия, лекции, методические пособия и рекомендации, программы и курсы обучения, публикации из профильных изданий