Декларативное программирование

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

Логическая дедукция

Предположим, нам известно, что Кермит либо на сцене, либо болен, и нам сообщают, что Кермит не на сцене. Можно сделать вывод, что Кермит болен. Это пример дедуктивного метода, который называется резолюцией (resolution).

Для того чтобы лучше понять этот метод, прежде всего условимся обозначать простые высказывания заглавными буквами, а отрицание высказывания — символом «^». Например, обозначим высказывание «Кермит — принц» буквой А, высказывание «Госпожа Пигги — актриса» буквой В. Тогда выражение

A OR В

будет означать: «Кермит — принц, или Госпожа Пигги — актриса». А выражение

В AND -A

будет означать: «Госпожа Пигги — актриса и Кермит не принц». Для обозначения импликации (из А следует В) мы будем использовать стрелку. Например, выражение

А -» В

означает: «Если Кермит — принц, то госпожа Пигги — актриса».

Согласно логической операции резолюции, если у нас есть два высказывания

Р OR Q И

R OR -Q.

то из них следует высказывание

Р OR R.

В таком случае из двух исходных высказываний выводится третье, которое называется резольвентой (resolvent). Обратите внимание на то, что резольвента является логическим следствием исходных высказываний. То есть если исходные высказывания истинны, то и резольвента должна быть истинной. (Если Q истинно, тогда R тоже должно быть истинно; а если Q ложно, тогда Р должно быть истинно. Следовательно, независимо от истинности Q либо Р, либо R должно быть истинным).

Исходные высказывания операции резолюции и их резольвента соединяются линиями (рис. 5.25). Обратите внимание на то, что операцию резолюции можно применить только к высказываниям, имеющим форму логического выражения, то есть высказываниям, компоненты (предикаты) которых соединены логическим оператором, например OR1. Так высказывание Р OR Q является дизъюнкцией, а высказывание Р —> Q нет. Однако этот факт не создает никаких трудностей, поскольку существует теорема математической логики, согласно которой любое высказывание, состоящее из предикатов первого порядка, можно записать в виде дизъюнкции. Мы не будем рассматривать эту теорему, а только отметим, что высказывание Р -> Q эквивалентно высказыванию Q OR -"P.

Набор высказываний называется несовместным, если все высказывания не могут быть истинны одновременно. Другими словами, несовместный набор высказываний является внутренне противоречивым. Самый простой пример — это комбинация высказывания Р и его отрицания -°Р. Специалисты по логике показали, что доказать несовместность высказываний можно с помощью многократного выполнения операции резолюции. Согласно правилу, если в результате многократного выполнения операции резолюции получается пустое высказывание (результат операции резолюции над высказываниями Р и ->Р), то исходный набор высказываний является несовместным. Можно доказать (рис. 5.26) несовместность высказываний

Р OR Q R OR -Q -R -P

Предположим, нам нужно доказать, что из некоторого набора высказываний следует Р. Доказать истинность Р — то же самое, что доказать ложность высказывания "'Р. Поэтому, чтобы показать, что из исходного набора высказываний следует Р, нам просто нужно выполнять операцию резолюции над исходными высказы-

ваниями и высказыванием ->Р, пока мы не получим пустое высказывание. Получив такой результат, можно сделать вывод, что высказывание ~>Р несовместно с исходными высказываниями и, следовательно, из них следует Р.

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

(Маша находится в X) -» (Машина овечка находится в X). где X обозначает любое место, и (Маша находится дома)

В дизъюнктивной форме эти высказывания имеют вид (Машина овечка находится в X) OR -ЧМаша находится в X) и (Маша находится дома)

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

(Машина овечка находится дома) ИЛИ -■(Маша находится дома)

и высказыванием

(Маша находится дома)

можно выполнить операцию резолюции. В результате мы получим

(Машина овечка находится дома)

Процесс присвоения значений переменным (например, присвоение значения «дом» переменной X) для выполнения операции резолюции называется унификацией (unification). Именно эта операция позволяет применять общие высказывания в отдельных прикладных задачах.