Bilet_2 (Основы математической логики и логического программирования (разобранные билеты))

Основыматематическойлогики и логическогопрограммированияВ.А. ЗахаровБилет 2.Хорновские логическиепрограммы: синтаксис.Декларативная семантикалогических программ.Операционная семантикалогических программ.Стратегии вычисления логическихпрограмм.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫСинтаксис логических программПусть σ = hConst, Func, Predi — некоторая сигнатура, вкоторой определяются термы и атомы.«заголовок» ::= «атом»«тело» ::= «атом» | «тело», «атом»«правило» ::= «заголовок» ← «тело»;«факт» ::= «заголовок»;«утверждение» ::= «правило» | «факт»«программа» ::= «пусто» | «утверждение» «программа»«запрос» ::= | ? «тело»ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫТерминологияПусть G =?C1 , C2 , .

. . , Cm — запрос. ТогдаIIатомы C1 , C2 , . . . , Cm называются подцелями запроса G ,mSVarCi называются целевымипеременные множествапеременными ,i=1Iзапрос называется пустым запросом ,Iзапросы будем также называть целевыми утверждениями .Для удобства обозначения условимся в дальнейшем факты A;рассматривать как правила A ←; с заголовком A и пустымтелом.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫКак нужно понимать логические программы?Главная особенность логического программирования —полисемантичность : одна и та же логическая программа имеетдве равноправные семантики, два смысла.Человек–программист и компьютер–вычислитель имеют дверазные точки зрения на программу.Программисту важно понимать, ЧТО вычисляет программа.Такое понимание программы называется декларативнойсемантикой программы.Компьютеру важно «знать», КАК проводить вычислениепрограммы. Такое понимание программы называетсяоперационной семантикой программы.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫКак нужно понимать логические программы?Декларативная семантикаОперационная семантикаПравило A0 ← A1 , A2 , .

. . , An ;Если выполнены условия Чтобы решить задачу A0 ,A1 , A2 , . . . , An , то справедли- достаточно решить задачиво и утверждение A0 .A1 , A2 , . . . , An .Факт A0 ;Утверждение A0 считается Задача A0 объявляется реверным.шенной.Запрос ?C1 , C2 , . . . , CmПри каких значениях целевых Решитьсписокзадачпеременных будут верны все C1 , C2 , . . .

, Cm .отношения C1 , C2 , . . . , Cm ?ДЕКЛАРАТИВНАЯ СЕМАНТИКАБолее строгое описание семантик требует привлеченияаппарата математической логики.Логические программы и логические формулыКаждому утверждению логической программы сопоставимлогическую формулу:Правило: D 0 = A0 ← A1 , A2 , . . . , AnD 0 = ∀X1 .

. . ∀Xk (A1 &A2 & . . . &An → A0 ), где {X1 , . . . , Xk } =n[i=0Факт: D 00 = AD 00 = ∀X1 . . . ∀Xk A, где {X1 , . . . , Xk } = VarAЗапрос: G = ? C1 , C2 , . . . , CmG = C1 &C2 & . . . &CmVarAiДЕКЛАРАТИВНАЯ СЕМАНТИКАС точки зрения декларативной семантики,Iпрограммные утверждения D и запросы G — этологические формулы,Iпрограмма P — это множество формул (база знаний),Iа правильный ответ на запрос — это такие значенияпеременных (подстановка), при которой запросоказывается логическим следствием базы знаний.ДЕКЛАРАТИВНАЯ СЕМАНТИКАОпределение (правильного ответа)Пусть P — логическая программа, G — запрос к P смножеством целевых переменных Y1 , .

. . , Yk .Тогда всякая подстановка θ = {Y1 /t1 , . . . , Yk /tk } называетсяответом на запрос G к программе P.Ответ θ = {Y1 /t1 , . . . , Yk /tk } называется правильным ответомна запрос G к программе P, еслиP |= ∀Z1 . . . ∀ZN G θ,где {Z1 , . . . , ZN } =k[i=1Varti .ДЕКЛАРАТИВНАЯ СЕМАНТИКАТеорема (об основном правильном ответе)Пусть G =?C1 , C2 , .

. . , Cm — запрос к хорновской логическойпрограмме P. Пусть Y1 , . . . , Yk — целевые переменные,t1 , . . . , tk — основные термы.Тогда подстановка θ = {Y1 /t1 , . . . , Yk /tk } являетсяправильным ответом на запрос G к программе P тогда итолько тогда, когда P |= (C1 & . . . &Cm )θ.ОПЕРАЦИОННАЯ СЕМАНТИКАЛОГИЧЕСКИХ ПРОГРАММКонцепция операционной семантикиПод операционной семантикой понимают правила построениявычислений программы. Операционная семантикаописывает, КАК достигается результат работы программы.Результат работы логической программы — это правильныйответ на запрос к программе. Значит, операционная семантикадолжна описывать метод вычисления правильных ответов.Запрос к логической программе порождает задачу ологическом следствии. Значит, вычисление ответа на запросдолжно приводить к решению этой задачи.Таким методом вычисления может быть разновидностьметода резолюций, учитывающая особенности устройствапрограммных утвержденийSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)ПустьIG = ? C1 , .

. . , Ci , . . . , Cm — целевое утверждение, вкотором выделена подцель Ci ,ID 0 = A00 ← A01 , A02 , . . . , A0n — вариант некоторогопрограммного утверждения, в котором VarG ∩ VarD 0 = ∅,Iθ ∈ НОУ(Ci , A00 ) — наиб. общ. унификатор подцели Ci изаголовка программного утверждения A0 .Тогда запросG 0 = ?(C1 , . . . , Ci−1 , A01 , A02 , . . . , A0n , Ci+1 , . . . , Cm )θназывается SLD-резольвентой программного утверждения D 0 изапроса G с выделенной подцелью Ci и унификатором θ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)ПустьIG0 = ? C1 , C2 , . . .

, Cm — целевое утверждение,IP = {D1 , D2 , . . . , DN } — хорновская логическая программа.Тогда (частичным) SLD-резолютивным вычислением ,порожденным запросом G0 к логической программе Pназывается последовательность троек (конечная илибесконечная)(Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . . . , (Djn , θn , Gn ), .

. . ,в которой для любого i, i ≥ 1,IDji ∈ P, θi ∈ Subst, Gi — целевое утверждение (запрос);Iзапрос Gi является SLD-резольвентой программногоутверждения Dji и запроса Gi−1 с унификатором θi .SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)Частичное SLD-резолютивное вычислениеcomp = (Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . . . , (Djk , θn , Gn )называетсяIуспешным вычислением (SLD-резолютивнымопровержением), если Gn = ;Iбесконечным вычислением , если comp — это бесконечнаяпоследовательность;Iтупиковым вычислением , если comp — это конечнаяпоследовательность, и при этом для запроса Gnневозможно построить ни одной SLD-резольвенты.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)ПустьIG0 = ? C1 , C2 , . .

. , Cm — целевое утверждение с целевымипеременными Y1 , Y2 , . . . , Yk ,IP = {D1 , D2 , . . . , DN } — хорновская логическая программа,Icomp = (Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . . . , (Djn , θn , ) —успешное SLD-резолютивное вычисление, порожденноезапросом G к программе P.Тогда подстановкаθ = (θ1 θ2 . . . θn )|Y1 ,Y2 ,...,Yk ,представляющая собой композицию всех вычисленныхунификаторов θ1 , θ2 , .

. . , θn , ограниченную целевымипеременными Y1 , Y2 , . . . , Yk ,называется вычисленным ответом на запрос G0 к программе P.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯТеперь у нас есть два типа ответов на запросы к логическимпрограммам:Iправильные ответы, которые логически следуют изпрограммы;Iвычисленные ответы, которые конструируются по ходуSLD-резолютивных вычислений.Правильные ответы — это то, что мы хотим получить,обращаясь с вопросами к программе.Вычисленные ответы — это то, что нам в действительностивыдает компьютер (интерпретатор программы).Какова связь между правильными ивычисленными ответами?КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИТеорема (корректности операционной семантикиотносительно декларативной семантики)ПустьIG0 = ? C1 , C2 , .

. . , Cm — целевое утверждение,IP = {D1 , D2 , . . . , DN } — хорновская логическая программа,Iθ — вычисленный ответ на запрос G0 к программе P.Тогда θ — правильный ответ на запрос G0 к программе P.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИТеорема полноты (главная).Пусть θ — правильный ответ на запрос ?G к хорновскойлогической программе P.Тогда существует такой вычисленный ответ η на запрос ?G кпрограмме P, что θ = ηρ для некоторой подстановки ρ.ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙОпределение.Отображение R, которое сопоставляет каждому непустомузапросу G : ?C1 , C2 , . . . , Cm одну из подцелей Ci = R(G ) в этомзапросе, называется правилом выбора подцелей .Для заданного правила выбора подцелей R вычислениезапроса G к логической программе P называетсяR-вычислением , если на каждом шаге вычисления очереднаяподцель в запросе выбирается по правилу R.Ответ, полученный в результате успешного R-вычисления,называется R-вычисленным .Теорема сильной полнотыКаково бы ни было правило выбора подцелей R, если θ —правильный ответ на запрос G0 к хорновской логическойпрограмме P, то существует такой R-вычисленный ответ η,что равенствоθ = ηρДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММОпределениеДеревом SLD-резолютивных вычислений запроса G0 клогической программе P называется помеченное корневоедерево TG0 ,P , удовлетворяющее следующим требованиям:1.

Корнем дерева является исходный запрос G0 ;2. Потомками каждой вершины G являются всевозможныеSLD-резольвенты запроса G (при фиксированномстандартном правиле выбора подцелей);3. Листовыми вершинами являются пустые запросы(завершающие успешные вычисления) и запросы, неимеющие SLD-резольвент (завершающие тупиковыевычисления).ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММИллюстрация?Gt 0Pq @PP)R@?'TG0 ,P?GitPq t ?Gi0vt) @PPqqq@R t?G 000@?G 00 t?Gi0ii$?Gt j?t?&%СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММОпределениеСтратегией вычисления запросов к логическим программамназывается алгоритм построения (обхода) дереваSLD-резолютивных вычислений TG0 ,P всякого запроса G0 кпроизвольной логической программе PСтратегия вычислений называется вычислительно полной ,если для любого запроса G0 и любой логической программы Pэта стратегия строит (обнаруживает) все успешныевычисления запроса G0 к программы PСТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММФактически, стратегия вычисления — это одна стратегийобхода корневого дерева.