LectLog13 (1158006), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

θ1 = {X /X1 , Y1 /a, L1 /b c nil}?...G1 =?elem(X1 , b c nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?.θ2 = {X1 /X2 , Y2 /b, L2 /c nil}.G2 =?elem(X2 , c nil)elem(X3 ,X3 nil);.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.. θ1 = {X /X1 , Y1 /a, L1 /b c nil}?...G1 =?elem(X1 , b c nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?.G2 =?elem(X2 , c nil)elem(X3 ,X3 nil);. θ3 = {X2 /c, X3 /c}?G3 = УСПЕХ!.θ2 = {X1 /X2 , Y2 /b, L2 /c nil}SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );..

θ1 = {X /X1 , Y1 /a, L1 /b c nil}?...G1 =?elem(X1 , b c nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?.θ2 = {X1 /X2 , Y2 /b, L2 /c nil}.G2 =?elem(X2 , c nil)elem(X3 ,X3 nil);. θ3 = {X2 /c, X3 /c}?G3 = УСПЕХ!Вычисленный ответ: θ = (θ1 θ2 θ3 )|X = {X /c}SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 5.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :..? elem(c, a b nil)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)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 );.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)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 );.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 /c nil}?G2 =?elem(c, nil)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 /c nil}?G2 =?elem(c, nil)elem(X3 ,X3 nil);Нет унификатора.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 /c 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 /c 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 )elem(X3 ,Y3 L3 ) ← elem(X3 ,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 )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 )elem(X3 ,Y3 L3 ) ← elem(X3 ,L3 );.. θ3 = {X3 /a, L2 /Y3 L3 }?G3 =?elem(a, L3 )и. т. д. до ∞Бесконечное вычисление.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯТеперь у нас есть два типа ответов на запросы к логическимпрограммам:Iправильные ответы, которые логически следуют изпрограммы;Iвычисленные ответы, которые конструируются по ходуSLD-резолютивных вычислений.Правильные ответы — это то, что мы хотим получить,обращаясь с вопросами к программе.Вычисленные ответы — это то, что нам в действительностивыдает компьютер (интерпретатор программы).Какова связь между правильными ивычисленными ответами?КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИТеорема (корректности операционной семантикиотносительно декларативной семантики)Пусть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 ,почему?P |= ∀Z C1 θ,почему?и, следовательно,и, следовательно,и, следовательно, θ — это правильный ответ.КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИДоказательство.Индуктивный переход (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 (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 = θ — правильный ответ на запрос G0 .КОРРЕКТНОСТЬ ОПЕРАЦИОННОЙСЕМАНТИКИИтак, всякий вычисленный ответ — правильный.А можно ли вычислить любой правильный ответ?Полна ли наша операционная семантика?КОНЕЦ ЛЕКЦИИ 13..

Характеристики

Список файлов лекций