Лекции 12-23. Математическая логика (после колка) (1161871), страница 3
Текст из файла (страница 3)
θ1 = {X1 /c, Y1 /a, L1 /b nil}?.G1 =?elem(c, b nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );.θ2 = {X1 /X2 , Y2 /b, L2 /nil}?G2 =?elem(c, nil)elem(X3 ,X3 L3 );Нет унификатора.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)..G0 =?elem(c, a b nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.. θ1 = {X1 /c, Y1 /a, L1 /b nil}?.G1 =?elem(c, b nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );.θ2 = {X1 /X2 , Y2 /b, L2 /nil}?G2 =?elem(c, nil)elem(X3 ,Y3 L3 ) ← elem(X3 ,L3 );Нет унификатора.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)..G0 =?elem(c, a b nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );..
θ1 = {X1 /c, Y1 /a, L1 /b nil}?.G1 =?elem(c, b nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );.θ2 = {X1 /X2 , Y2 /b, L2 /nil}?G2 =?elem(c, nil)failureНет SLD-резольвентыТУПИК!SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X )SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 6.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :? elem(a, X )G0 =?elem(a, X )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 );.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 )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 & . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
