Конспект установочных лекций по комплексному курсу Информатика, Теория информации

       

Логическое программирование


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

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

Решение задач в логическом программировании

Логическая программа состоит из формул вида (пусть С и В, - логические выражения, в простейшем случае true и false, а также предикаты на константах), называемых "условиями Хорна" (англ. "Нот - Klausein"):

BÜB1ÙB2Ù….ÙBn.

Выражения Вi называются предпосылками или подцелями (англ. subgools), а С называется заключением. Множество подцелей может также быть пустым или состоять только из

true; тогда формулу мы называем фактом,

а другие условия - правилами.

При формулировании Hom-Klauseln-программ будут использовать следующие соглашения. Идентификаторы будут записывать большими буквами, а обозначения функций (включая нуль-местные функции для представления констант) - малыми.

Выполнение логических программ

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

С <= B1 Ù ... Ù Bk,                              (R)

являющееся частью логической программы. Пусть надо доказать (или опровергнуть) условие

fake <= S1Ù ... Ù



Sn.                         (G)

Правило (R) применимо к условию (G), если существует подстановка с

C[t1/X1, ..., tm/Хm] = Sj[t1/X1, ..., tm/Хm].

Другими словами, общая справедливость (G) опровержима (ведет к противоречию), если условие

                       ~             ~      ~           ~     ~               ~  

false <= S1Ù ... Ù Sj-1ÙB1Ù…ÙBkÙSj+1Ù… ÙSn           (G )

 опровержимо с

~

Si = Si[t1/X1, ..., tm/Хm],

~

Bi=Bi[t1/X1, ...tm/Xm].

Эту редукцию подцели к модифицированной редукции с помощью применения правила назовем резолюцией.

           ~

Если (G ) опровержимо, то опровержимо также и (G), однако обратное, вообще говоря, неверно.

Унификация

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

Унификация является операцией на множестве термов. Результатом унификации является подстановка, которая для каждого терма заданного множества в качестве результата выдает один и тот же терм. Такая подстановка называется унификатором. Но, не для каждого множества существует такого рода унификатор - в этом случае множество называется не унифицируемым.


Содержание раздела