Информатика. Курс лекций. Громов Ю.Ю - 135 стр.

UptoLike

ВУЗ: 

ТГТУ | Тамбов

Составители: 

Рубрика: 

5.7. ДЕКЛАРАТИВНОЕ ПРОГРАММИРОВАНИЕ*
Выше мы утверждали, что формальная логика позволяет создать общий алгоритм решения задач, на основе которого
можно построить систему декларативного программирования. В данном разделе мы исследуем это утверждение, создав сна-
чала некоторый упрощенный алгоритм, а затем кратко обсудив возможности основанного на нем языка декларативного про-
граммирования.
Логический вывод. Предположим, мы знаем, что лягушонок Кермит либо играет в спектакле, либо болен, и нам сказа-
ли, что сейчас лягушонок Кермит не играет в спектакле. Тогда мы можем сделать вывод, что лягушонок Кермит, должно
быть, болен. Это – пример дедуктивного рассуждения, которое называется резолюцией.
Чтобы лучше понять этот принцип, примем сначала соглашение представлять простые высказывания отдельными бук-
вами, а отрицание высказывания – символом ¬. Например, мы можем представить высказывание "Кермит – принц" буквой
А, а высказывание "Мисс Пигги – актриса" – буквой В. Тогда выражение
A OR В
означает "Кермит – принц или мисс Пигги – актриса", а выражение
B AND ¬A
Означает: "Мисс Пигги – актриса, а Кермит – не принц". Для обозначения отношения "следует" мы будем использовать
стрелку. Например, выражение
A → B
означает: "Если Кермит – принц, то мисс Пигги – актриса".
В общем виде принцип резолюции утверждает, что из двух высказываний
Р OR Q и R OR ¬Q
мы можем вывести высказывание
R OR Q.
В этом случае мы говорим, что два исходных высказывания сводятся к третьему, которое называется резольвентой.
Важно подчеркнуть, что резольвента – это логическое следствие исходных высказываний. Если исходные высказывания ис-
тинны, то резольвента также должна быть истинной. (Если Q – истинно, то R должно быть истинно, но если Q – ложно, то Р
должно быть истинным. Следовательно, независимо от того, является Q истинным или ложным, либо Р, либо R должно быть
истинным.)
Графически мы будем представлять резолюцию двух высказываний так, как показано на рис. 5.19, где мы написали ис-
ходные высказывания и изобразили линии, соединяющие их со своей резольвентой. Заметим, что резолюцию можно приме-
нять только к парам высказываний, которые выражаются в форме предложения, т.е. к высказываниям, элементарные компо-
ненты которых можно соединять булевой операцией OR (ИЛИ). Таким образом, высказывание
P OR Q
выражено в форме предложения, в то время как для высказывания
P → Q
это не так. Эта потенциальная проблема не очень серьезна. В математической логике существует теорема, утверждающая,
что любое высказывание, записанное средствами логики предикатов первого порядка (системы для представления высказы-
ваний, имеющей очень большие выразительные возможности), можно сформулировать в форме предложения. Мы не будем
обсуждать здесь эту важную теорему, но для дальнейших ссылок заметим, что высказывание
P→ Q
эквивалентно высказыванию в форме предложения
Q OR ¬P.
Совокупность высказываний является противоречивой, если все они не могут быть
истинными одновременно. Другими словами, такая совокупность высказываний состоит из
противоречащих друг другу высказываний. Простой пример такой совокупности – объеди-
нение высказывания Р и его отрицания ¬P. Специалисты-логики доказали, что повторное
применение резолюции – это систематический метод проверки непротиворечивости мно-
жества предложений. Если повторный метод резолюции приводит к пустому предложению
(результату резолюции предложения Р с предложением ¬P), то исходная совокупность
высказываний является противоречивой. Например, на рис. 5.20 показано, что совокуп-
ность высказываний
P OR Q R OR ¬Q ¬R ¬Q
является противоречивой.
Предположим, нам необходимо проверить, что из некоторой совокупности высказываний действительно следует выска-
зывание Р. Высказывание Р эквивалентно отрицанию высказывания -P. Следовательно, чтобы показать, что из исходной со-
вокупности высказываний следует высказывание Р, нам нужно лишь применять процедуру резолюции к исходным высказы-
ваниям и высказыванию ¬Р до тех пор, пока мы не получим пустое предложение. Получив пустое предложение, мы можем
прийти к выводу, что высказывание ¬Р противоречит исходным высказываниям, а значит, из исходных высказываний сле-
дует высказывание Р.
Остается решить всего одну проблему, и мы будем готовы к применению процедуры резолюции в реальной программ-
ной среде. Предположим, что имеются два высказывания:
Рис. 5.19. Резолюция
высказываний (P OR Q) и
(R OR ¬Q) с получением
высказывания (Р OR R)

Страницы