Основы современных компьютерных технологий
Пролог и логическое программирование
Логическое программирование (ЛП) - это направление в программировании, основанное на идеях и методах математической логики. Термин "логическое программирование" в литературе по информатике трактуется в широком и узком смысле.
В широком толковании в ЛП включают круг понятий, методов, языков и систем, в основе которого лежит идея описания задачи совокупностью утверждений на некотором логическом языке и получение решения задачи путем построения логического вывода в некоторой формальной дедуктивной системе. Классы формул, используемые для описания задач, методы вывода и модели вычислений, используемые в таких системах, очень разнообразны. Поэтому различные их комбинации образуют специфические стили программирования: концептуальное, функциональное (аппликативное) и другие.
Наибольшие практические результаты достигнуты в системах программирования, где в качестве логических программ используются специальные классы логических формул - хорновские дизъюнкты, а в качестве способа их использования применяются специальные методы логического вывода - варианты метода резолюций. Программирование с использованием таких систем называют хорновским и резолюционным, но чаще всего - логическим программированием, перенося узкую трактовку термина на более широкое понятие. Самыми известными системами такого рода являются реализации языка Пролог (Программирование в терминах логики - Programming in logic). Рассмотрим основные идей и понятия ЛП в узком смысле.
Неформально логическая программа описывает множество объектов, множество функций и отношений на этих объектах. Строится логическая программа как набор утверждений об объектах, функциях и отношениях. Такое описание является статическим и никакого вычислительного процесса не задаст, т.е. можно считать, что это описание определяет базу данных, в которой хранятся объекты и заданные на них функции и отношения, например, в виде графиков.
Конкретному применению логической программы соответствует понятие запроса (цели) - например, каково значение функции, заданной логической программой, при данном значении аргумента.
Вычисление ответа на запрос соответствует доказательству существования такого объекта. Правила, по которым проводятся вычисления, образуют процедурную - операционную - семантику логической программы. Успехи языка Пролог обусловлены тем, что, с одной стороны, с помощью используемых в нем логических формул - хорновских дизъюнктов - можно описать многие практические задачи, а с другой - найдена простая интерпретация этих формул и построена достаточно эффективная реализация системы логического программирования.
Правило в Прологе имеет вид:
A0
где А0,А1,.. .Аm - атомы. Атом А0 называется заголовком, а А1... -Аm- телом правила. Тело
304
может быть пустым (при m=0) - такие правила называют фактами. Атом имеет вид
?(t1,t2,...tn)
где ? - n-арный предикатный символ или имя отношения; t1, t2,...tn- термы.
Терм - это либо имя переменной, либо константа, либо составной терм вида f (t1 ,t2. . .tn), f - n-арный функциональный символ. Функции, задаваемые логической программой, представляются в виде отношений - n-местная функция y=f(x1,x2...xn) представляется в виде (n+1)-местного отношения вида F(x1,x2...xn,y).
Запрос (цель) имеет вид:
< С1С2...Сr-
где r ?0 и С1С2...Сr- атомы.
Каждое правило допускает логическую и процедурную интерпретации (семантики). Логическая интерпретация правила A0 < Ar...Am - "истинность А0 следует из истинности А1 и истинности А2, и... и истинности Аm" или "А0 истинно, если истинны А1 и А2, и... и Аm". Таким образом, правила рассматриваются как формулы языка логики предикатов вида:
? x1, ? x2... ? xn(A1? A2?... ? Am> A0).
Здесь ? - квантор общности, ? - логическая связка И, > - логическая связка ЕСЛИ - ТО.
В Прологе, в силу традиции, данные формулы записываются в обратную сторону и используются другие обозначения для логических связок: ? обозначается "," (запятой) или словом and; ? обозначается ";" (точкой с запятой) или словом or ; > обозначается в теории |, а в языке программирования используется конструкция ":-" (двоеточие и минус) или слово if.
Все переменные в предложениях связаны квантором общности, поэтому обычно знак квантора ? опускается.
Формула с использованием связок > и ? может быть преобразована в эквивалентную, но имеющую связки ¬ (HE) и ? (ИЛИ), формулу вида:
A0? ¬A1? ¬A2?... ? ¬Am(m ? 0).
Такие формулы и называются хорновскими дизъюнктами, а стиль программирования - хорновским.
Процедурная интерпретация правил Пролога вида:
А0:-А1, А2... Аm или А0 if А1 and A2 and ... and Am
следующая: "для достижения цели А0 необходимо последовательно достичь целей А1 , А2 . . . Am"
Соответственно, для фактов (когда m = 0) имеет место логическое прочтение: "А0 истинно", процедурная интерпретация факта: "цель А достигнута".
Логическая семантика запроса G: С1,С2...Сr(с переменными x1,х2...хi) к логической программе понимается как требование вычислить все значения переменных x1,х2...хi, при которых утверждение С1 ? С2 ?... ? Сr логически следует из утверждений программы или, записывая это, как принято в логике, необходимо показать, что
? G
305
т.е. запрос G логически следует (выводим) из логической программы . При этом оказывается, что доказательство выводимости G из аналогично тому, чтобы показать
, ¬ G ?
т.е. присоединение отрицания запроса G к программе приводит к противоречию. Однако последнее выполнить в классе формул, с помощью которых записывается Пролог-программа, существенно проще, и имеется эффективный метод доказательства - метод резолюций, одна из версий которого и применяется в Прологе.
Метод резолюций, получив на вход логическую программу с присоединенным к ней запросом в виде множества хорновских дизъюнктов, пытается построить вывод пустого дизъюнкта, обозначаемого символом D. Если это ему удается, тогда цель допускается, в противном случае отвергается. Реализуется метод резолюций с помощью двух правил: правила резолюции и правила склейки, которые во время работы вызывают процедуру унификации - сопоставления.
Унификация - процесс, на вход которого поступает два терма и для них находится унификатор. Унификатором двух термов называется подстановка, которая делает термы одинаковыми.
Если унификатор существует, то термы называются унифицируемыми и для них отыскивается наиболее общий унификатор, если нет - процедура унификации сообщает об отказе.
Пусть имеются два терма t1=ОТЕЦ(Х,У) и t2=ОТЕЦ("ПЕТР", "ПАВЕЛ"). Унификатором этих двух термов будет подстановка ?=(Х="ПЕТР", Y="ПАВЕЛ"), т.е. если в терм t1 вместо переменных X и Y подставить значения из соответствующих мест терма t2, термы станут одинаковыми, а значением их будет пример ОТЕЦ("ПЕТР", "ПАВЕЛ").
Пусть теперь t1=ОТЕЦ(Х,"ИВАН") и t2=ОТЕЦ("ПЕТР", "ПАВЕЛ"). В этом случае унификация невозможна, так как с помощью подстановки термы нельзя сделать одинаковыми - на втором месте в обоих термах стоят разные константные выражения. Если бы термы были, например, вида t1=ОТЕЦ(Х,"ИВАН") и t2=ОТЕЦ("ПЕТР",Z), тогда ?=(Х="ПЕТР", Z="ИBAH"), и пример для этих термов ОТЕЦ("ПЕТР", "ИВАН").
Правило резолюции позволяет из дизъюнктов
D1 = ¬ A1(t) ? A2 ? ... ?An
D2 = ¬ A1(s) ? B1 ? ... ? Bm
получить новый дизъюнкт D = Q(A2 ?... ? An ? B1 ?... ? Bm).
Здесь ? - наиболее общий унификатор термов t и s, обеспечивает их равенство и означает, что все подстановки унификатора выполнены для всех атомов, входящих в дизъюнкты D1 D2. Дизъюнкты D1 D2 называют родителями дизъюнкта D. В дизъюнкте D отсутствует пара: A (? t)? A1 (?s), при этом (?t) = (?s) и пара является тавтологией (тождественно-истинной) и может быть удалена из дальнейших вычислений, что и выполняет правило резолюции.
Правило склейки позволяет из дизъюнкта A(t) ?A(s) ? B1 ?...? Bn получить дизъюнкт ?(A(t) ? B1.? ... ? Bn), т.е. осуществляется "склеивание" одинаковых атомов, полученных после унифицирующей подстановки ?t = ?s.
306
Работу метода резолюции опишем на примере, приведенном ранее. Запишем множество утверждений и фактов в виде логической программы, используя прологообразный синтаксис:
Предложения 1- 4 являются утверждениями Пролога, предложения 5-10 - факты. Переменные в каждом утверждении являются локальными - их область действия одно утверждение.
Запрос: ? ¬ ВЫП_РЕЙС(Z). Доказательство запроса приведено ниже.
307
Запрос
Правило
Подстановка
?¬ВЫП_РЕЙС(Z)
4
Z=X4
?¬ВЗЛЕТЕЛ(Х4)
2
Х4=Х2
?¬ ГОТОВ(Х2) ? ¬ ДАНО РАЗР(Х2) ? ¬ НЕ_НАХ_ВЗП(Х2)
1
Х2=Х1
? ¬ ПРОВЕРЕН(Х1) ? ¬ ЗАПРАВЛЕН(Х1) ? ¬ ДАНО_РАЗР(Х1) ? ¬ НЕ_НАХ_ВЗП(Х1)
5
Х1=ЯК-42
? ¬ЗАПРАВЛЕН(ЯК-42) ? ¬ ДАНО РАЗР(ЯК-42) ? ¬ НЕ_НАХ_ВЗП(ЯК-42)
6
7 ¬ДАНО РАЗР(ЯК-42) ? ¬ НЕ_НАХ_ВЗП(ЯК-42)
9
? ¬ НЕ_НАХ_ВЗП(ЯК-42)
10
?
В результате доказательства мы вывели логически пустой дизъюнкт D, следовательно, цель допускается. Композиция подстановок Z=X4=X2=X1 =ЯК-42 на наш запрос дает ответ 7=ЯК-42. Любая другая подстановка, например, Х1 =ТУ-134, приводит в тупик.
308
304 :: 305 :: 306 :: 307 :: 308 :: Содержание
