Логическое программирование
Если в предыдущих разделах было описание только задач и вычислительных структур, но не алгоритмов, то теперь будет рассмотрен вопрос о том, насколько подходящими являются формализмы логики непосредственно для алгоритмических вычислений. Это будет обсуждено на направлении, которому в предыдущие годы было уделено большое внимание, так называемого логического программирования.
В логическом программировании предикаты над заданной вычислительной структурой (как истинностные значения, числа и последовательности) описываются логическими формулами очень простого вида. Тогда запросы к логической программе можно сформулировать, основываясь на специфицированных предикатах, путем задания формул со свободны ми идентификаторами. Тогда система выполнения логической программы систематически ищет решение для запроса. Решение состоит в отыскании подстановок для свободных идентификаторов в запросе таким образом, что так модифицированные запросы логически следуют из спецификаций для предикатов. Этот способ действий используется в языке программирования Пролог, который нашел широкое практическое применение.
Решение задач в логическом программировании
Логическая программа состоит из формул вида (пусть С и В, - логические выражения, в простейшем случае 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), однако обратное, вообще говоря, неверно.
Унификация
При выполнении логических программ путем применения правил преобразования типичными являются операции над термами. Примером этому служит вопрос о применимости некоторого правила. На этот вопрос можно ответить с помощью методики унификации.
Унификация является операцией на множестве термов. Результатом унификации является подстановка, которая для каждого терма заданного множества в качестве результата выдает один и тот же терм. Такая подстановка называется унификатором. Но, не для каждого множества существует такого рода унификатор - в этом случае множество называется не унифицируемым.
