Ещё одни лекции В.А. Захарова, страница 21
Описание файла
PDF-файл из архива "Ещё одни лекции В.А. Захарова", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 21 страницы из PDF
θ1 = {X1 /a, X /Y1 L1 }?.G1 =?elem(a, L1 )elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?.θ2 = {X2 /a, L1 /Y2 L2 }G2 =?elem(a, L2 )SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X ).G0 =?elem(a, X )elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );. θ1 = {X1 /a, X /Y1 L1 }?.G1 =?elem(a, L1 )elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?.θ2 = {X2 /a, L1 /Y2 L2 }.G2 =?elem(a, L2 )elem(X3 ,Y3 L3 ) ← elem(X3 ,L3 );.θ3 = {X3 /a, L2 /Y3 L3 }?G3 =?elem(a, L3 )SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X ).G0 =?elem(a, X )elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.
θ1 = {X1 /a, X /Y1 L1 }?.G1 =?elem(a, L1 )elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?.θ2 = {X2 /a, L1 /Y2 L2 }G2 =?elem(a, L2 ). θ3 = {X3 /a, L2 /Y3 L3 }?G3 =?elem(a, L3 )и. т. д. до ∞Бесконечное вычисление.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯТеперь у нас есть два типа ответов на запросы к логическимпрограммам:правильные ответы, которые логически следуют изпрограммы;вычисленные ответы, которые конструируются по ходуSLD-резолютивных вычислений.Правильные ответы — это то, что мы хотим получить,обращаясь с вопросами к программе.Вычисленные ответы — это то, что нам в действительностивыдает компьютер (интерпретатор программы).Какова связь между правильными ивычисленными ответами?КОНЕЦ ЛЕКЦИИ 12.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.
ЗахаровЛекция 13.Корректность операционнойсемантики.Полнота операционной семантикилогических программ.КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИУ нас есть два типа ответов на запросы к логическимпрограммам:правильные ответы , которые логически следуют изпрограммы;вычисленные ответы , которые конструируются по ходуSLD-резолютивных вычислений.Правильные ответы — это то, что мы хотим получить,обращаясь с вопросами к программе.Вычисленные ответы — это то, что нам в действительностивыдает компьютер (интерпретатор программы).Какова связь между правильными ивычисленными ответами?КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИОпределение правильного ответаПусть P — логическая программа, G — запрос к P смножеством целевых переменных Y1 , . . .
, Yk .Тогда всякая подстановка θ = {Y1 /t1 , . . . , Yk /tk } называетсяответом на запрос G к программе P.Ответ θ = {Y1 /t1 , . . . , Yk /tk } называется правильным ответомна запрос G к программе P, еслиP |= ∀Z1 . . . ∀ZN G θ,где {Z1 , . . . , ZN } =ki=1Varti .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИОпределение вычисленного ответаПустьG0 = ? C1 , C2 , . . .
, Cm — целевое утверждение с целевымипеременными Y1 , Y2 , . . . , Yk ,P = {D1 , D2 , . . . , DN } — хорновская логическая программа,comp = (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.КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИТеорема (корректности операционной семантики)ПустьG0 = ? C1 , C2 , . . . , Cm — целевое утверждение,P = {D1 , D2 , . . . , DN } — хорновская логическая программа,θ — вычисленный ответ на запрос G0 к программе P.Тогда θ — правильный ответ на запрос G0 к программе P.Доказательство.Рассмотрим успешное вычисление, порожденное запросом G0 клогической программе P:comp = (Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . . .
, (Djn , θn , )Покажем индукцией по длине вычисления n, чтоθ = (θ1 θ2 . . . θn )|Y1 ,Y2 ,...,Yk — это правильный ответ.КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Базис индукции (n = 1). ТогдаG0 =? C1Dj1 = A0 ;θ1 ∈ НОУ(C1 , A0 ).Значит, C1 θ1 = A0 θ1 . Поскольку Dj1 ∈ P, мы приходим кследующему выводу:P |= ∀X A0 ,почему?и, следовательно,P |= ∀Z A0 θ1 ,почему?P |= ∀Z C1 θ1 ,почему?и, следовательно,и, следовательно, θ = θ1 |Y1 ,Y2 ,...,Yk — это правильный ответ.КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Индуктивный переход (n − 1 → n). ПустьG0 = ? C1 , C2 , . .
. , Ci , . . . , CmDj1 = A0 ← A1 , . . . , Ar ;θ1 ∈ НОУ(Ci , A0 ),G1 = ? (C1 , C2 , . . . , A1 , . . . , Ar , . . . , Cm )θ1 .Тогдаcomp = (Dj2 , θ2 , G2 ), . . . , (Djn , θn , )— это успешное вычисление длины n − 1, порожденноезапросом G1 . Значит, по предположению индукции,θ = θ2 . . . θn |VarG1 — правильный ответ на запрос G1 .Значит,P |= ∀Z (C1 &C2 & . . . &A1 & . . . &Ar & .
. . &Cm )θ1 θ .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & . . . &A1 & . . . &Ar & . . . &Cm )θ1 θследуетP |= ∀Z (A1 & . . . &Ar )θ1 θ .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеТаким образом,P |= ∀Z A0 θ1 θ .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & . . . &A1 & . . . &Ar & . . . &Cm )θ1 θследуетP |= ∀Z (A1 & . . . &Ar )θ1 θ .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . .
&Ar → A0 ).Значит, верно такжеТаким образом,P |= ∀Z A0 θ1 θ .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & . . . &A1 & . . . &Ar & . . . &Cm )θ1 θследуетP |= ∀Z (A1 & . . . &Ar )θ1 θ .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеP |= ∀Z (A1 & . . . &Ar )θ1 θ → A0 θ1 θ .Таким образом,P |= ∀Z A0 θ1 θ .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & . . . &A1 & .
. . &Ar & . . . &Cm )θ1 θследуетP |= ∀Z (A1 & . . . &Ar )θ1 θ .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеP |= ∀Z (A1 & . . . &Ar )θ1 θ → A0 θ1 θ .Таким образом,P |= ∀Z A0 θ1 θ .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & . . . &A1 & . .
. &Ar & . . . &Cm )θ1 θследуетP |= ∀Z (A1 & . . . &Ar )θ1 θ .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеP |= ∀Z (A1 & . . . &Ar )θ1 θ → A0 θ1 θ .Таким образом,P |= ∀Z A0 θ1 θ .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Итак, из P |= ∀Z (C1 &C2 & . .
. &A1 & . . . &Ar & . . . &Cm )θ1 θследуетP |= ∀Z (C1 & . . . &Ci−1 &Ci+1 & . . . Cm )θ1 θ .Мы показали, чтоP |= ∀Z Ci θ1 θ .Значит,P |= ∀Z (C1 & . . . &Ci−1 &Ci &Ci+1 & . . . Cm ) θ1 θ . G0θЗначит, θ1 θ |VarG0 = (θ1 θ2 . . . θn )|Y1 ,Y2 ,...,Yk = θ — правильныйответ на запрос G0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИИтак, всякий вычисленный ответ — правильный.А можно ли вычислить любой правильный ответ?Полна ли наша операционная семантика?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛОГИЧЕСКИХ ПРОГРАММПроблема полнотыПусть θ — правильный ответ на запрос G0 к хорновскойлогической программе P, т. е. P |= ∀Z G0 θ.Существует ли такое успешное SLD-резолютивное вычисление,порожденное запросом G0 к программе P(Dj1 , η1 , G1 ), (Dj2 , η2 , G2 ), .
. . , (Djn , ηn , ),которое вычисляет ответ θ, т. е. θ = (η1 η2 . . . ηn )|VarG0 ?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛОГИЧЕСКИХ ПРОГРАММТеорема полноты.ПустьP = {D1 , D2 , . . . , DN } — хорновская логическая программа,G0 =?C1 , C2 , . . . Cm — запрос с множеством целевыхпеременных Y1 , Y2 , . . . , Yk ,θ — правильный ответ на запрос G0 к хорновскойлогической программе P.Тогда существует такой вычисленный ответ η на запрос G0 кпрограмме P, чтоθ = ηρдля некоторой подстановки ρ.Теорема полноты гласит, что каждый правильный ответ — этопример (частный случай) некоторого вычисленного ответа .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛОГИЧЕСКИХ ПРОГРАММДоказательство.Пусть θ = {Y1 /t1 , .
. . , Yk /tk } и пустьki=1Varti = {Z1 , . . . , Zr }.Выберем некоторое множество новых «свежих» констант{c1 , . . . , ck }, не содержащихся ни в программе P, ни взапросе G , ни в термах подстановки θ, и рассмотримподстановку λ = {Z1 /c1 , Z2 /c2 , . . . , Zr /cr }.Поскольку θ — правильный ответ, верно P |= ∀Z1 . .
. ∀Zk G0 θ.Запрос G0 = G0 θλ — основной пример запроса G0 , и поэтомуP |= G0 θλ.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛОГИЧЕСКИХ ПРОГРАММДоказательство.Общий замысел доказательства1. Вначале покажем, что запрос G0 = G0 θλ, обращенный кмножеству [P] основных примеров программных утвержденийпрограммы P, имеет успешное SLD-резолютивное вычисление(лемма об основных вычислениях ).2. Затем покажем, что исходный запрос G0 , обращенный ксамой программе P, имеет успешное SLD-резолютивноевычисление с таким вычисленным ответом η, для котороговерно равенство θλ = ηρ для некоторой подстановки ρ(лемма о подъеме для хорновских дизъюнктов ).3.
Затем покажем, что отсюда следует равенство θ = ηρ длянекоторой подстановки ρ.ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХЛемма об основных вычислениях.ПустьP = {D1 , D2 , . . . , DN } — хорновская логическая программа,G0 =?C1 , C2 , . . . Cn — основной запрос,и при этом верно P |= G0 .Тогда существует успешное SLD-резолютивное вычислениезапроса G0 , обращенного к множеству [P] основных примеровпрограммных утверждений программы P.ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.{D1 , D2 , . . . , DN } |= C1 &C2 & .
. . &Cn⇐⇒множество дизъюнктов {D1 , D2 , . . . , DN , ¬C1 ∨¬C2 ∨. . .∨¬Cn }противоречиво.⇐⇒ (по теореме Эрбрана)существует такое конечное множество основных примеров } ⊆ [P], чтопрограммных утверждений {D1 , D2 , . . . , DMмножество дизъюнктов {D1 , D2 , . . . , DM , ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬Cn }противоречиво.⇐⇒ (по теореме полноты метода резолюций) , ¬C ∨¬C ∨. . .∨¬C }из системы дизъюнктов {D1 , D2 , . . .