Лекции В.А. Захарова (1157993), страница 27
Текст из файла (страница 27)
?R(b) t6?t?t?Q(V ), R(b)@I@@@@@@R t?R(b)@6?tДерево SLD-резолютивных вычисленийПрограмма P:P(X , Y ) ← R(X ), !, Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;Q(b) ←; ?P(U, V ), R(U)t@ ?Q(U), R(U)Rt@∗(1)(2)(3)(4)(5)!?t?R(U), , Q(V ), R(U)t?!, Q(V ), R(b)∗?6Сработал оператор отсечения.Построение деревавычислений завершено. ?R(b) tПри этом часть ветвейбыла отсечена.6?t?t?Q(V ), R(b)@I@@@@@@R t?R(b)@6?tОПЕРАТОР ОТСЕЧЕНИЯПрограммное утверждениеA0 ← A1 , . . .
, Ak , !, Ak+1 , . . . , An ;содержащее оператор отсечения можно прочитывать двояко:IЧтобы решить задачу A0 нужно найти только первоерешение задач A1 , . . . , Ak и далее решать задачиAk+1 , . . . , An . Если решение задач A1 , . . . , Ak найти неудается, то воспользоваться альтернативнымипроцедурами решения задачи A0 .IЧтобы решить задачу A0 нужно проверить условияA1 , .
. . , Ak . Если эти условия выполнены, то приступить крешению задач Ak+1 , . . . , An и не обращаться к другимвариантам решения задачи A0 . Если же эти условия невыполнены, то обратиться к альтернативным способамрешения задачи A0 .ОПЕРАТОР ОТСЕЧЕНИЯТаким образом, оператор отсечения позволяет удобноиспользовать в логическом программировании стандартныеконструкции императивного программирования.IВетвление. S0 : if P then S1 else S2 fiPif −then−else : S0 ← P, !, S1 ;S0 ← S2 ;IИтерация. S0 : while P do S1 odPwhile−do : S0 ← P, !, S1 , S0 ;S0 ←;ОПЕРАТОР ОТСЕЧЕНИЯС введением в логические программы оператора отсечениятеорема полноты операцинной семантики относительнодекларативной семантики перестают быть справедливыми.ОПЕРАТОР ОТСЕЧЕНИЯПрограммы P1 и P2 вычисления гласных буквP1Elem_Vow (X , XElem_Vow (X , ZVowel(a) ←;Vowel(e) ←;Vowel(i) ←;Vowel(o) ←;Vowel(u) ←;Vowel(y ) ←;..P2Y ) ← Vowel(X );Y ) ← Elem_Vow (X , Y );..!Elem_Vow (X , X Y ) ← Vowel(X ), ;ElemV ow (X , Z Y ) ← Elem_Vow (X , Y );Vowel(a) ←;Vowel(e) ←;Vowel(i) ←;Vowel(o) ←;Vowel(u) ←;Vowel(y ) ←;равносильны в декларативной семантике , и запрос...G :?Elem_Vow (X , o n e nil)для обеих программ имеет два правильных ответа θ1 = {X /o}и θ2 = {X /e}.ОПЕРАТОР ОТСЕЧЕНИЯПрограммы P1 и P2 вычисления гласных буквP1Elem_Vow (X , XElem_Vow (X , ZVowel(a) ←;Vowel(e) ←;Vowel(i) ←;Vowel(o) ←;Vowel(u) ←;Vowel(y ) ←;..P2Y ) ← Vowel(X );Y ) ← Elem_Vow (X , Y );..!Elem_Vow (X , X Y ) ← Vowel(X ), ;ElemV ow (X , Z Y ) ← Elem_Vow (X , Y );Vowel(a) ←;Vowel(e) ←;Vowel(i) ←;Vowel(o) ←;Vowel(u) ←;Vowel(y ) ←;но неравносильны в операционной семантике : запрос...G :?Elem_Vow (X , o n e nil)к P1 вычисляет θ1 = {X /o} и θ2 = {X /e},а тот же запрос к P2 вычисляет только θ1 = {X /o}.ОПЕРАТОР ОТСЕЧЕНИЯС введением в логические программы оператора отсечениятеорема полноты операцинной семантики относительнодекларативной семантики перестает быть справедливыми.Поэтому оператором отсеченияосторожно.! нужно пользоваться оченьА что еще полезного и удобногоможно встроить в логические программы?КОНЕЦ ЛЕКЦИИ 16.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.
ЗахаровЛекция 17.Отрицание в логическомпрограммировании.Оператор not.Встроенные предикаты ифункции.Оператор вычисления значений.Модификация баз данных.ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИОтрицание ¬ — это очень полезная логическая связка. Частомы обращаемся с вопросами, используя отрицание.ПримерP : птица(орел) ←;птица(воробей) ←;птица(пингвин) ←;летает(орел) ←;летает(воробей) ←;летает(самолет) ←;Сформулируем вопрос: какая птица не летает?G : ? птица(X ), ¬летает(X )Какой ответ мы ожидаем получить на этот запрос?ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИПримерС точки зрения декларативной семантики, для полученияответа на этот запрос нужно выяснить, выполняется лилогическое следованиеP |= ∃X (птица(X )&¬летает(X )),где P = {птица(орел), птица(воробей), птица(пингвин),летает(орел), летает(воробей), летает(самолет)}Оно не выполняется, т.
к.BP |= P, BP 6|= ∃X (птица(X )&¬летает(X )).Значит, ответ на этот запрос должен быть отрицательным:такой птицы нет .ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИПримерОднако в обыденной жизни мы в таких случаях даем совсемдругой ответ.Обнаружив, что в нашей базе знаний Pесть сведение птица(пингвин) инет никаких сведений о том, что летает(пингвин),мы отвечаем:«Насколько позволяет судить наша база знаний, нелетающаяптица — это пингвин».В юрипруденции такой подход к решению вопроса о виновностичеловек называется презумпцией невиновности :в случае отсутствия свидетельств виновностичеловек считается невиновным.ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИМы можем распространить принцип презумпции невиновностии на логические программы.Допущение Замкнутости МираПусть имеется некоторое непротиворечивое множествозамкнутых формул Γ (например, хорновская логическаяпрограмма) и замкнутая формула ϕ (например, запрос илиотдельная подцель).Тогда формула ¬ϕ является логическим следствием множестваΓ в допущении замкнутости мираΓ |=CWA ¬ϕ,если неверно, что ϕ логически следует из Γ, т.
е. Γ 6|= ϕ.Здесь CWA — аббревиатура C losed W orld A ssumption.ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИСуть Допущения Замкнутости Мира (CWA) состоит в том, чтопри извлечении CWA-логических следствий из базы знаний Γ(|=CWA ) нужно рассматривать не все модели для Γ, а толькотакую минимальную модель, в которой истинными являютсяодни лишь классические следствия (|=) из Γ.Такая минимальная модель существует, вообще говоря, невсегда (например, если Γ = {A ∨ B}).Но в случае хорновских логических программ, минимальноймоделью для программы P является наименьшая эрбрановскаямодель MP .ОТРИЦАНИЕ В ЛОГИЧЕСКОМПРОГРАММИРОВАНИИОбратимся к орнитологическому примеру.ПримерP = {птица(орел), птица(воробей), птица(пингвин),летает(орел), летает(воробей), летает(самолет)}ϕ= птица(пингвин) & ¬летает(пингвин)ТогдаP |=CWA птица(пингвин), поскольку MP |= птица(пингвин),P |=CWA ¬летает(пингвин), поскольку MP 6|= летает(пингвин).Значит, P |=CWA птица(пингвин) & ¬летает(пингвин).ОПЕРАТОР notИтак, теперь к логическим программам можно обращаться сзапросами, содержащими отрицания подцелей, идекларативная семантика умеет разумно обращаться с такимотрицательными подцелями.Нам остается научить этому обращению компьютер, т.
е.ввести в операционную семантику правила для обработкиотрицательных подцелей.Однако здесь нас ожидает неприятный сюрприз.ОПЕРАТОР notПредположим, что имеется запрос G : ?¬C0 к программе P.Чтобы получить утвердительный ответ на запрос G (т. е.доказать, что P |=CWA ¬C0 ), интерпретатор должен проверить,что MP 6|= C0 .Для этого интерпретатор должен убедиться, что запросG 0 : ?C0 к программе P не имеет ни одного успешноговычисления.Но эта задача является алгоритмически неразрешимой(почему? ).Да потому, что к ней сводится проблема останова машинТьюринга.Следовательно, никакой интерпретатор логических программне может гарантировать получение утвердительного ответа назапрос G : ?¬C0 даже в том случае, если этот ответ существует.ОПЕРАТОР notАлгоритмическая неразрешимость проблемы существования(отсутствия) успешного вычисления логических программ —это непреодолимое препятствие на пути создания такойоперационной семантики, которая была бы адекватнадекларативной семантике в рамках Допущения ЗамкнутостиМира.Можно лишь построить такой интерпретатор (операционнойсемантики), который как можно лучше соответствует CWA приобращении с отрицательными подцелями ¬C0 .Для этого в язык логического программирования был введенспециальный (встроенный) оператор not.ОПЕРАТОР notАргументами оператора not являются атомы.Для вычисления ответов на запрос ? not(C0 ) вводится правилоSLDNF-резолюции (N ot as F ailure), которое определяетсяследующим образом.Правило SLDNF-резолюцииПусть имеется запрос G0 : ? not(C0 ), C1 , .
. . , Cn к программе P.Для вычисления SLDNF-резольвенты G11. формируется запрос G 0 : ? C0 к программе P;2. проводится построение (обход) дерева вычислений Tзапроса G 0 : ? C0 ;3. в зависимости от устройства дерева T возможен один изтрех исходов.ОПЕРАТОР notПравило SLDNF-резолюцииВариант 1: Успех.Дерево T конечно, и все его ветви (SLD-резолютивныевычисления) являются тупиковыми.Тогда запрос G0 : ? not(C0 ), C1 , .
. . , Cn имеетSLDNF-резольвенту G1 = ? C1 , . . . , Cn , которая получается сиспользованием пустой подстановки ε.G 0 : ? C0t@T @t⇒@failureG0 : ? not(C0 ), C1 , . . . , Cn@ε?tG1 : ? C1 , . . . , CnОПЕРАТОР notОперационная семантика оператор notВариант 2: Неудача.При построении (обходе) дерева T было обнаруженоуспешное вычисление.Тогда запрос G0 : ? not(C0 ), C1 , . . . , Cn не имеетSLDNF-резольвент, и вычисление этого запроса являетсятупиковым .G 0 : ? C0G0 : ? not(C0 ), C1 , . . . , Cnt@T @t⇒@@failureR@failureОПЕРАТОР notОперационная семантика оператор notВариант 3: Бесконечное вычисление.Дерево T бесконечно и при его построении (обходе) небыло обнаружено успешных вычислений.Тогда запрос G0 : ? not(C0 ), C1 , .
. . , Cn не имеетSLDNF-резольвент, и вычисление этого запроса являетсябесконечным («сингулярная бесконечность»).G 0 : ? C0t@T @t⇒@failureG0 : ? not(C0 ), C1 , . . . , Cn@R∞@∞ОПЕРАТОР notОперационная семантика оператор notВариант 3: Бесконечное вычисление.Дерево T бесконечно и при его построении (обходе) небыло обнаружено успешных вычислений.Тогда запрос G0 : ? not(C0 ), C1 , .
. . , Cn не имеетSLDNF-резольвент, и вычисление этого запроса являетсябесконечным («сингулярная бесконечность»).Условие существования бесконечного вычисления запросаnot(C0 ) описано не вполне строго, поскольку обнаружениеуспешного вычисления существенно зависит от стратегииобхода дерева SLD-резолютивных вычислений. Так, например,стандартная стратегия обхода в глубину может не обнаружитьсуществующего успешного вычисления (почему? ).ОПЕРАТОР notТеорема (корректности SLDNF-резолюции)Если запрос G : ? not(C0 ) к хорновской логической программеP имеет успешное SLDNF-резолютивное вычисление, тоP |=CWA ¬∃y C0 .ДоказательствоСамостоятельно .А вот обратное утверждение (теорема полноты) дляSLDNF-резолютивного вычисления будет уже неверно.ОПЕРАТОР notПример.Рассмотрим программу поиска всех тех букв X слова L0 ,которые не содержатся в слове L00 .P : S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ← ;E (X , Y L) ← E (X , L);..и обратимся к ней с запросом..
..G0 : ? S(X , a b nil, b c nil)...S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);.. ..?S(X , a b t nil, b c nil)(1)(2)(3)..S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil)(1).. ..?t?E (X , a.b .nil),not(E (X , b .c .nil))θ1 = {X1 /X , L0 /aL00 /bbcnil,nil}..S(X , L0 , L00 ) ← E (X , L0 ), not(E (X , L00 ));E (X , X L) ←;E (X , Y L) ← E (X , L);(1)(2)(3).. ..?S(X , a b t nil, b c nil)..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
