Лекции В.А. Захарова (1157993), страница 20
Текст из файла (страница 20)
θ1 = {X1 /a, X /Y1 L1 }?G1 =?elem(a, L1 )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 );.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 )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 )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-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯТеперь у нас есть два типа ответов на запросы к логическимпрограммам:Iправильные ответы, которые логически следуют изпрограммы;Iвычисленные ответы, которые конструируются по ходуSLD-резолютивных вычислений.Правильные ответы — это то, что мы хотим получить,обращаясь с вопросами к программе.Вычисленные ответы — это то, что нам в действительностивыдает компьютер (интерпретатор программы).Какова связь между правильными ивычисленными ответами?КОНЕЦ ЛЕКЦИИ 12.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 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 & .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
