Ещё одни лекции В.А. Захарова, страница 18

. . , Cm называются подцелями запроса G ,mпеременные множестваVarCi называются целевымипеременными ,i=1запрос называется пустым запросом ,запросы будем также называть целевыми утверждениями .Для удобства обозначения условимся в дальнейшем факты A;рассматривать как правила A ←; с заголовком A и пустымтелом.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПримеры.Пусть D = elem(X , Y Z ) ← elem(X , Z ); — программноеутверждение. Тогда.D = D{X /Y , Z /nil} = elem(Y , Y nil) ← elem(Y , nil);пример программного утверждения D,.D = elem(X , Y Z ) ← elem(X , Z );вариант программного утверждения D,.D = D{X /1, Y /2, Z /nil} = elem(1, 2 nil) ← elem(1, nil);основной пример программного утверждения D,ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПример логической программыsi_ro(Xs , Xs , V , A, nil) ← in(Xs , V , V1 );si_ro(Xs , Xd , V , A, Z ) ← in(Xs , V , V1 ), in(Xd , V1 , V2 ),R(Xs , Xd , V2 , A, Z );.

. ... .. ...R(Xs , Xd , V , A, (Xs Xd nil) nil) ← in(Xs Xd nil, A, A1 );R(Xs , Xd , V , A, (Xs Y nil) Z )← in(Y , V , V1 ),in(Xs Y nil, A, A1 ),R(Y , Xd , V1 , A1 , Z );.. .in(X , X Y , Y );in(X , Z Y , Z V ) ← in(X , Y , V );и запроса к ней.... .. . ..

. .. . .. .? si_ro(4, 2, 1 2 3 4 nil, (1 2 nil) (2 3 nil) (2 4 nil) (3 1 nil) nil, Z )Что же вычислит программа в ответ на этот запрос?ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫКак нужно понимать логические программы?Главная особенность логического программирования —полисемантичность : одна и та же логическая программа имеетдве равноправные семантики, и поэтому человек–программисти компьютер–вычислитель имеют две разные точки зрения напрограмму.Программисту важно понимать, ЧТО вычисляет программа.Такое понимание программы называется декларативнойсемантикой программы.Компьютеру важно «знать», КАК проводить вычислениепрограммы. Такое понимание программы называетсяоперационной семантикой программы.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫКак нужно понимать логические программы?Декларативная семантикаОперационная семантикаПравило A0 ← A1 , A2 , .

. . , An ;Если выполнены условия Чтобы решить задачу A0 ,A1 , A2 , . . . , An , то справедли- достаточно решить задачиA1 , A2 , . . . , An .во и утверждение A0 .Факт A0 ;Утверждение A0 считается Задача A0 объявляется реверным.шенной.Запрос ?C1 , C2 , . . . , CmПри каких значениях целевых Решитьсписокзадачпеременных будут верны все C1 , C2 , . . . , Cm .отношения C1 , C2 , . . . , Cm ?ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПример истолкования логической программы..P : elem(X , X L);elem(X , Y L) ← elem(X , L);Декларативная семантика1. Всякий предмет X входитв состав того списка, заголовком которого он является2.

Если предмет X содержится в хвосте списка, то X содержится и в самом списке.Операционная семантика1. Считается решенной задача поиска предмета X в любом списке, содержащем X вкачестве заголовка.2. Чтобы обнаружить предметX в списке, достаточно найтиего в хвосте этого списка.ДЕКЛАРАТИВНАЯ СЕМАНТИКАБолее строгое описание семантик требует привлеченияаппарата математической логики.Логические программы и логические формулыКаждому утверждению логической программы сопоставимлогическую формулу:Правило: D = A0 ← A1 , A2 , . . . , An ;D = ∀x1 .

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

. , Yk .Тогда всякая подстановка θ = {Y1 /t1 , . . . , Yk /tk } называетсяответом на запрос G к программе P.Ответ θ = {Y1 /t1 , . . . , Yk /tk } называется правильным ответомна запрос G к программе P, еслиkгде {Z1 , . . . , ZN } =Varti .P |= ∀Z1 . . . ∀ZN G θ,i=1Теперь вопрос: как искать правильные ответы?ДЕКЛАРАТИВНАЯ СЕМАНТИКАПусть σ = Const, Func, Pred — некоторая сигнатура.РассмотримHσ — эрбрановский универсум сигнатуры σ (множествоосновных термов);Bσ — эрбрановский базис сигнатуры σ (множествоосновных атомов);эрбрановские интерпретации сигнатуры σ:I ⊆ Bσ ,I = {A : A ∈ Bσ , I |= A}Определение (модели для логической программы)Пусть P — логическая программа, I — H-интерпретация.Тогда I называется эрбрановской моделью для программы P,если для любого программного утверждения D, D ∈ P, верноI |= D(сокращенная запись I |= P).ДЕКЛАРАТИВНАЯ СЕМАНТИКАЛемма (о модели для логической программы)Эрбрановская интерпретация I является моделью длялогической программы P тогда и только тогда, когда длялюбого основного примера программного утвержденияD = A0 ← A1 , .

. . , An , D ∈ [P] верно{A1 , . . . , An } ⊆ I ⇒ A0 ∈ IДоказательство.(Необходимость) Пусть D ∈ P и D = Dθ — основнойпример. Тогда I — модель для P ⇒ I |= D ⇒ I |= D ⇒I |= A1 & . . . &An → A0 ⇒ если I |= A1 & . . . &An , то I |= A0 ⇒если I |= A1 , . .

. I |= An , то I |= A0 ⇒если {A1 , . . . , An } ⊆ I , то A0 ∈ I .(Достаточность) Сами.ДЕКЛАРАТИВНАЯ СЕМАНТИКАСледствиеКаждая хорновская логическая программа P имеет хотя быодну эрбрановскую модель.Доказательство.Самостоятельно. (Покажите, что в качестве одной из моделейвсегда можно взять максимальную интерпретацию I = BP ).Пример.ПрограммаP(X , f (X )) ← R(X );R(f (Y )) ← P(Y );имеет H-модель I = ∅.ДЕКЛАРАТИВНАЯ СЕМАНТИКАЛемма (о пересечении моделей)Если H-интерпретации I1 и I2 являются моделями длялогической программы P, то H-интерпретация I0 = I1 ∩ I2также является моделью для P.Доказательство.Воспользуемся леммой о модели для логической программы.Пусть D = A0 ← A1 , . .

. , An , D ∈ [P]. Тогда{A1 , . . . , An } ⊆ I0⇒{A1 , . . . , An } ⊆ I1⇒{A1 , . . . , An } ⊆ I2A0 ∈ I1⇒ A0 ∈ I0A0 ∈ I2ДЕКЛАРАТИВНАЯ СЕМАНТИКАТеорема (о наименьшей модели)Всякая хорновская логическая программа P имеетнаименьшую эрбрановскую модель.Доказательство.1. Каждая хорновская логическая программа P имеет хотябы одну эрбрановскую модель.2. Рассмотрим множество IP всех H-моделей логическойпрограммы P. Как было показано, I = ∅. Поэтому,согласнолемме о пересечении H-моделей, интерпретацияMP =I также является H-моделью программы P.I ∈IPПри этом для любой H-модели I верно MP ⊆ I .

Такимобразом, MP — это наименьшая эрбрановская модель дляпрограммы P.ДЕКЛАРАТИВНАЯ СЕМАНТИКАТеорема (характеристическое свойствонаименьшей модели)Пусть G =?A — запрос к хорновской логической программе P.Пусть A0 = Aθ — основной пример атома A. ТогдаP |= A0 ⇐⇒ A0 ∈ MP .Доказательство.Допустим P = {D1 , . .

. , DN }. ТогдаP |= A0 ⇐⇒ |= (D1 & . . . &DN ) → A0 ⇐⇒S = {D1 , . . . , DN , ¬A0 } — противоречивая система ⇐⇒S не имеет H-моделей (теорема о H-интерпретациях ) ⇐⇒для любой H-интерпретации I : I |= P влечет A0 ∈ I ⇐⇒I = MP (теорема о наименьшей модели )A0 ∈I ∈IPДЕКЛАРАТИВНАЯ СЕМАНТИКАТеорема (об основном правильном ответе)Пусть G =?C1 , C2 , . . .

, Cm — запрос к хорновской логическойпрограмме P. Пусть Y1 , . . . , Yk — целевые переменные,t1 , . . . , tk — основные термы.Тогда подстановка θ = {Y1 /t1 , . . . , Yk /tk } являетсяправильным ответом на запрос G к программе P тогда итолько тогда, когда {C1 θ, . . . , Cm θ} ⊆ MP .Доказательство.Самостоятельно. (На основании характеристического свойстванаименьшей модели).ДЕКЛАРАТИВНАЯ СЕМАНТИКАИТОГИЛогическая программа P — это база знаний, состоящая иззаконов (фактов и правил), описывающих устройствонекоторого математического мира (задачи).В этом математическом мире истинным считается то итолько то, что удовлетворяет законам базы знаний —ничего лишнего.Этот математический мир — наименьшая эрбрановскаямодель MP .Правильным ответом на запрос к базе знаний считаетсятакой ответ, который логически следует из базы знаний(программы).Все правильные ответы на любые запросы к логическойпрограмме P нужно искать в наименьшей модели MP .ДЕКЛАРАТИВНАЯ СЕМАНТИКАТеперь ясно, каков смысл логических программ, какие ответына запросы к программ считаются правильными, и гденаходятся правильный ответы.

Математику этого достаточно,для того чтобы создавать программы.Но этого совершенно недостаточно вычислительномуустройству, для того чтобы вычислять ответы на запросы кпрограммам.Теперь нам нужно выяснить,КАК ВЫЧИСЛЯТЬ ОТВЕТЫ НА ЗАПРОСЫ?КОНЕЦ ЛЕКЦИИ 12.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 12.Хорновские логическиепрограммы: синтаксис.Декларативная семантикалогических программ.Операционная семантикалогических программ:SLD–резолютивные вычисления.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПАРАДИГМЫ ПРОГРАММИРОВАНИЯИмперативное программирование : программа — это автомат,описывающий последовательности операторов (команд).Математическая модель: машины Тьюринга–Поста.Языки: Assembler, Pascal, C, Java.Функциональное программирование : программа — это системауравнений, описывающая вычисляемую функцию.Математическая модель: λ-исчисление Черча–Клини,уравнения Эрбрана–Геделя.Языки: Lisp, ML, Haskell.Логическое программирование : программа — это множествоформул, описывающих условия решаемой задачи.Математическая модель: логические исчисления.Языки: Prolog, Godel.ПАРАДИГМА ЛОГИЧЕСКОГОПРОГРАММИРОВАНИЯ$''ОПИСАНИЕ ЗАДАЧИПРОГРАММАДекларативная семантика&'$Операционная семантика%&$ОПИСАНИЕ ЗАДАЧИ = ПРОГРАММАДекларативнаясемантика&⇐⇒Операционнаясемантика%%ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫСинтаксис логических программПусть σ = Const, Func, Pred — некоторая сигнатура, вкоторой определяются термы и атомы.«заголовок» ::= «атом»«тело» ::= «атом» | «тело», «атом»«правило» ::= «заголовок» ← «тело»;«факт» ::= «заголовок»;«утверждение» ::= «правило» | «факт»«программа» ::= «пусто» | «утверждение» «программа»«запрос» ::= | ? «тело»ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПримерыПравило: L(паша, Y ) ← L(Y , X ), L(паша, X );заголовоктелоФакт: L(даша, саша);Запрос (целевое утверждение ):? Умный(X ), Добрый(X ), Красивый(X ), Любит(X , меня) подцельподцельЗдесь X — целевая переменная .подцельподцельХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫПример логической программы...P : elem(X , X L);elem(X , Y L) ← elem(X , L);concat(nil, Y , Y );concat(U X , Y , U Z ) ← concat(X , Y , Z );common(X , Y ) ← elem(U, X ), elem(U, Y );и запроса к ней..