Лекция 13. Корректность операционной семантики. Полнота операционной семантики (1161905)
Текст из файла
Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 13.Корректность операционнойсемантики.Полнота операционной семантикилогических программ.КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИУ нас есть два типа ответов на запросы к логическимпрограммам:Iправильные ответы , которые логически следуют изпрограммы;Iвычисленные ответы , которые конструируются по ходуSLD-резолютивных вычислений.Правильные ответы — это то, что мы хотим получить,обращаясь с вопросами к программе.Вычисленные ответы — это то, что нам в действительностивыдает компьютер (интерпретатор программы).Какова связь между правильными ивычисленными ответами?КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИОпределение правильного ответаПусть 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 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИОпределение вычисленного ответаПусть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.КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИТеорема (корректности операционной семантики)ПустьIG0 = ? C1 , C2 , . . . , Cm — целевое утверждение,IP = {D1 , D2 , . . .
, DN } — хорновская логическая программа,Iθ — вычисленный ответ на запрос 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 0 = (Dj2 , θ2 , G2 ), . . . , (Djn , θn , )— это успешное вычисление длины n − 1, порожденноезапросом G1 . Значит, по предположению индукции,θ0 = θ2 . . . θn |VarG1 — правильный ответ на запрос G1 .Значит,P |= ∀Z (C1 &C2 & . .
. &A1 & . . . &Ar & . . . &Cm )θ1 θ0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & . . . &A1 & . . . &Ar & . . . &Cm )θ1 θ0следуетP |= ∀Z (A1 & . . . &Ar )θ1 θ0 .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеТаким образом,P |= ∀Z A0 θ1 θ0 .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & .
. . &A1 & . . . &Ar & . . . &Cm )θ1 θ0следуетP |= ∀Z (A1 & . . . &Ar )θ1 θ0 .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеТаким образом,P |= ∀Z A0 θ1 θ0 .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & . . . &A1 & . .
. &Ar & . . . &Cm )θ1 θ0следуетP |= ∀Z (A1 & . . . &Ar )θ1 θ0 .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеP |= ∀Z (A1 & . . . &Ar )θ1 θ0 → A0 θ1 θ0 .Таким образом,P |= ∀Z A0 θ1 θ0 .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & . . .
&A1 & . . . &Ar & . . . &Cm )θ1 θ0следуетP |= ∀Z (A1 & . . . &Ar )θ1 θ0 .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеP |= ∀Z (A1 & . . . &Ar )θ1 θ0 → A0 θ1 θ0 .Таким образом,P |= ∀Z A0 θ1 θ0 .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Из P |= ∀Z (C1 &C2 & . .
. &A1 & . . . &Ar & . . . &Cm )θ1 θ0следуетP |= ∀Z (A1 & . . . &Ar )θ1 θ0 .Поскольку Dj1 ∈ P, верноP |= ∀X (A1 & . . . &Ar → A0 ).Значит, верно такжеP |= ∀Z (A1 & . . . &Ar )θ1 θ0 → A0 θ1 θ0 .Таким образом,P |= ∀Z A0 θ1 θ0 .И, наконец, вспомнив, что A0 θ1 = Ci θ1 (почему? ), заключаемP |= ∀Z Ci θ1 θ0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Итак, из P |= ∀Z (C1 &C2 & . . . &A1 & . .
. &Ar & . . . &Cm )θ1 θ0следуетP |= ∀Z (C1 & . . . &Ci−1 &Ci+1 & . . . Cm )θ1 θ0 .Мы показали, чтоP |= ∀Z Ci θ1 θ0 .Значит,P |= ∀Z (C1 & . . . &Ci−1 &Ci &Ci+1 & . . . Cm ) θ1 θ0 .{z} |{z}|G0θЗначит, θ1 θ0 |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 } и пустьkSVarti = {Z1 , . . . , Zr }.i=1Выберем некоторое множество новых «свежих» констант{c1 , . . . , ck }, не содержащихся ни в программе P, ни взапросе G , ни в термах подстановки θ, и рассмотримподстановку λ = {Z1 /c1 , Z2 /c2 , . . . , Zr /cr }.Поскольку θ — правильный ответ, верно P |= ∀Z1 . . . ∀Zk G0 θ.Запрос G00 = G0 θλ — основной пример запроса G0 , и поэтомуP |= G0 θλ.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛОГИЧЕСКИХ ПРОГРАММДоказательство.Общий замысел доказательства1. Вначале покажем, что запрос G00 = G0 θλ, обращенный кмножеству [P] основных примеров программных утвержденийпрограммы P, имеет успешное SLD-резолютивное вычисление(лемма об основных вычислениях ).2.
Затем покажем, что исходный запрос G0 , обращенный ксамой программе P, имеет успешное SLD-резолютивноевычисление с таким вычисленным ответом η, для котороговерно равенство θλ = ηρ0 для некоторой подстановки ρ0(лемма о подъеме для хорновских дизъюнктов ).3. Затем покажем, что отсюда следует равенство θ = ηρ длянекоторой подстановки ρ.ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХЛемма об основных вычислениях.ПустьP = {D1 , D2 , . .
. , DN } — хорновская логическая программа,G00 =?C10 , C20 , . . . Cn0 — основной запрос,и при этом верно P |= G00 .Тогда существует успешное SLD-резолютивное вычислениезапроса G00 , обращенного к множеству [P] основных примеровпрограммных утверждений программы P.ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.{D1 , D2 , .
. . , DN } |= C10 &C20 & . . . &Cn0⇐⇒множество дизъюнктов {D1 , D2 , . . . , DN , ¬C10 ∨¬C2 ∨. . .∨¬Cn0 }противоречиво.⇐⇒ (по теореме Эрбрана)существует такое конечное множество основных примеров0 } ⊆ [P], чтопрограммных утверждений {D10 , D20 , . . . , DM000множество дизъюнктов {D1 , D2 , . . . , DM , ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0 }противоречиво.⇐⇒ (по теореме полноты метода резолюций)0 , ¬C 0 ∨¬C 0 ∨. . .∨¬C 0 }из системы дизъюнктов {D10 , D20 , . .
. , DMn12резолютивно выводим пустой дизъюнкт .ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы0 , ¬C 0 ∨ ¬C 0 ∨ · · · ∨ ¬C 0 }.{D10 , D20 , . . . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.негативные дизъюнктысмешанные дизъюнктыD10 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1D20 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2...0 =ADM∨0M ¬A1M ∨ · · · ∨ ¬A`MG00 = ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы0 , ¬C 0 ∨ ¬C 0 ∨ · · · ∨ ¬C 0 }.{D10 , D20 , .
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
