Основы современных компьютерных технологий

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


Логическое программирование (ЛП) - это направление в программировании, основанное на идеях и методах математической логики. Термин "логическое программирование" в литературе по информатике трактуется в широком и узком смысле.

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

Наибольшие практические результаты достигнуты в системах программирования, где в качестве логических программ используются специальные классы логических формул - хорновские дизъюнкты, а в качестве способа их использования применяются специальные методы логического вывода - варианты метода резолюций. Программирование с использованием таких систем называют хорновским и резолюционным, но чаще всего - логическим программированием, перенося узкую трактовку термина на более широкое понятие. Самыми известными системами такого рода являются реализации языка Пролог (Программирование в терминах логики - 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) if ПРОВЕРЕН(Х1) and ЗАПРАВЛЕН(Х1).


  • ВЗЛЕТЕЛ(Х2) if ГОТОВ(Х2) and ДАНО_РАЗР(Х2) and (НЕ_НАХ_ВЗП(Х2).


  • НАХ_ВЗП(Х3) if ГОТОВ(ХЗ) and ДAHO_PA3P(X3) and not (ВЗЛЕТЕЛ(ХЗ).


  • ВЫП_РЕЙС(Х4) if (ВЗЛЕТЕЛ(Х4).


  • ПРОВЕРЕН(ЯК-42)


  • ЗАПРАВЛЕН(ЯК-42)


  • ПРОВЕРЕН(ТУ-134)


  • ЗАПРАВЛЕН(ИЛ-62)


  • ДАНО_РАЗР(ЯК-42)


  • НЕ_НАХ_ВЗП(ЯК-42).


  • Предложения 1- 4 являются утверждениями Пролога, предложения 5-10 - факты. Переменные в каждом утверждении являются локальными - их область действия одно утверждение.

  • Представим утверждения в форме дизъюнктов:


  • ГОТОВ(Х1) ¬ ? ПРОВЕРЕН(Х1) ¬? ЗАПРАВЛЕН (X1).


  • ВЗЛЕТЕЛ(Х2) ¬ ? ГОТОВ(Х2) ¬ ? ДАНО_РАЗР(Х2) ¬ ? НЕ_НАХ_ВЗП(Х2).


  • НАХ_ВЗП(ХЗ) ¬ ? ГОТОВ(ХЗ) ¬ ? ДАНО_РАЗР(ХЗ) ¬ ? ВЗЛЕТЕЛ(ХЗ)


  • ВЫП_РЕЙС(Х4) ¬ ? ВЗЛЕТЕЛ(Х4)


  • ПРОВЕРЕН(ЯК-42)


  • ЗАПРАВЛЕН(ЯК-42)


  • ПРОВЕРЕН(ТУ-134)


  • ЗАПРАВЛЕН(ИЛ-62)


  • ДАНО_РАЗР(ЯК-42)


  • НЕ_НАХ_ВЗП(ЯК-42)


  • Запрос: ? ¬ ВЫП_РЕЙС(Z). Доказательство запроса приведено ниже.

    Запрос Правило Подстановка
    ?¬ВЫП_РЕЙС(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  
    ?    
    307

    В результате доказательства мы вывели логически пустой дизъюнкт D, следовательно, цель допускается. Композиция подстановок Z=X4=X2=X1 =ЯК-42 на наш запрос дает ответ 7=ЯК-42. Любая другая подстановка, например, Х1 =ТУ-134, приводит в тупик.

    308

    304 :: 305 :: 306 :: 307 :: 308 :: Содержание


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