13. Корректность операционной семантики. Полнота операционной семантики (В.А. Захаров - Лекции), страница 2

. .∨¬Ak1∨¬C20∨. . .∨¬Cn0ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы0 , ¬C 0 ∨ ¬C 0 ∨ · · · ∨ ¬C 0 }.{D10 , D20 , . . . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.негативные дизъюнктысмешанные дизъюнктыD10 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak10G00 = ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0D2 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2?u... 0 =ADM0M ∨ ¬A1M ∨ · · · ∨ ¬A`Mвозможны резольвенты двух типов@@А это не SLD-резольвента@R@¬A11∨. . .∨¬Ak1∨¬C20∨.

. .∨¬Cn0A02∨¬A22∨. . .∨¬Ar 2∨¬A11∨. . .∨¬Ak1ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Да, пустой дизъюнкт можно резолютивно вывести изсистемы0 , ¬C 0 ∨ ¬C 0 ∨ · · · ∨ ¬C 0 }.{D10 , D20 , . . . , DMn12Но это не обязательно SLD-резолютивный вывод. Рассмотримего более подробно.негативные дизъюнктысмешанные дизъюнктыD10 = A01 ∨ ¬A11 ∨ · · · ∨ ¬Ak1G00 = ¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cn0D20 = A02 ∨ ¬A12 ∨ · · · ∨ ¬Ar 2...0 =ADM∨0M ¬A1M ∨ · · · ∨ ¬A`Mвозможны резольвенты двух типов¬A11∨.

. .∨¬Ak1∨¬C20∨. . .∨¬Cn0A02∨¬A22∨. . .∨¬Ar 2∨¬A11∨. . .∨¬Ak1ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты. В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ),ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты. В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты.

В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cm0A00 ∨ ¬A01 ∨ · · · ∨ ¬A0kHHHHjA000 ∨ ¬A001 ∨ · · · ∨ ¬A00rA00 ∨ ¬A02 ∨ · · · ∨ ¬A0k ∨ ¬A001 ∨ · · · ∨ ¬A00rЕсли правило резолюции вначале применяетсяк двум программным утверждениям,ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты. В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cm0A00 ∨ ¬A01 ∨ · · · ∨ ¬A0kA000 ∨ ¬A001 ∨ · · · ∨ ¬A00rH HHHjA0 ∨ ¬A0 ∨ · · · ∨ ¬A0k ∨ ¬A001 ∨ · · · ∨ ¬A00rXX0 2XXXXXz?¬A02 ∨ · · · ∨ ¬A0k ∨ ¬A001 ∨ · · · ∨ ¬A00r ∨ ¬C20 ∨ · · · ∨ ¬Cm0а затем применяется к полученной резольвенте и запросу,ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты.

В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cm0A00 ∨ ¬A01 ∨ · · · ∨ ¬A0kA000 ∨ ¬A001 ∨ · · · ∨ ¬A00rHHHHHHj?H¬A01 ∨ ¬A02 ∨ · · · ∨ ¬A0k ∨ ¬C2 ∨ · · · ∨ ¬Cmто изменим порядок применения правилЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство леммы о вычислениях.Покажем, что этот вывод можно перестроить так, чтобы в немостались только SLD-резольвенты.

В этом выводе обязательноесть хотя бы одна SLD-резольвента (почему? ), потому чтопустой дизъюнкт — это всегда SLD-резольвента (почему? ).Тогда будем поступать так:¬C10 ∨ ¬C20 ∨ · · · ∨ ¬Cm0A00 ∨ ¬A01 ∨ · · · ∨ ¬A0kHHHA000 ∨ ¬A001 ∨ · · · ∨ ¬A00rHHHHHHHj?H00 ∨ · · · ∨ ¬A0 ∨ ¬C ∨ · · · ∨ ¬CH2mHH ¬A1 ∨ ¬A2kHjH¬A02 ∨ · · · ∨ ¬A0k ∨ ¬A001 ∨ · · · ∨ ¬A00r ∨ ¬C20 ∨ · · · ∨ Cm0и получим тот же самый результат,но уже только при помощи SLD-резолюции.ЛЕММА ОБ ОСНОВНЫХ ВЫЧИСЛЕНИЯХДоказательство.Будем применять этот прием, до тех пор пока в выводе неостанутся только правила SLD-резолюции.

Таким образом, витоге получим вывод пустого дизъюнкта из множествадизъюнктов{D1 , D2 , . . . , DN , ¬C10 ∨¬C2 ∨· · · ∨¬Cn0 }только при помощи правила SLD-резолюции.Это и есть успешное SLD-резолютивное вычисление основногозапроса G00 =?C10 , C20 , . . . Cn0 , обращенного к множеству основныхпримеров программных утверждений [P].Что и требовалось доказать.ЛЕММА О ПОДЪЕМЕЛемма о подъеме (для логических программ)Пусть G00 = G0 θ0 — основной пример запроса G0 с множествомцелевых переменных Y1 , .

. . , Ym , обращенный к хорновскойлогической программе P.Если запрос G00 , обращенный к множеству основных примеровпрограммных утверждений [P], имеет успешное вычисление,то исходный запрос G0 , обращенный к самой программе P,также имеет успешное вычисление с ответом η, которыйудовлетворяет равенствуθ0 = ηρ0для некоторой подстановки ρ0 .ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеРассмотрим SLD-резолютивное вычисление запроса G00 = G0 θ0с использованием основных примеров программныхутверждений из множества [P](D10 , ε, G10 ), (D20 , ε, G20 ), . .

. , (Dn0 , ε, )и покажем, что существует SLD-резолютивное вычислениезапроса G0 с использованием программы P(D1 , η1 , G1 ), (D2 , η2 , G2 ), . . . , (Dn , ηn , ),удовлетворяющее условиям леммы.ЛЕММА О ПОДЪЕМЕG0ЛЕММА О ПОДЪЕМЕG0θ0?G0 θ0ЛЕММА О ПОДЪЕМЕG0D1θ0?G0 θ0D2µ1Dnµ2D10?D20AAAµn?ε AAU G 01εAAU G0A2?Dn0qqq0Gn−1AεAA-AU ЛЕММА О ПОДЪЕМЕ- G1G0η1D1θ0?G0 θ0q- G2qqGn−1η2ηnD2µ1Dnµ2D10?D20AAAµn?ε AAU G 01- εAAU G0A2?Dn0qqq0Gn−1AεAA-AU ЛЕММА О ПОДЪЕМЕ- G1G0η1D1θ0?G0 θ0q- G2qqGn−1η2ηnD2µ1Dnµ2D10?D20AAAµn?ε AAU G 01- εAAU G0A2?Dn0qqq0Gn−1θ0 = (η1η2 . . .

ηn)|Y1,...,Ym ρ0AεAA-AU ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0D1θ00µ1?G00?= G0θ0D10@@@@R@G10= D1 µ1ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0D1@@@θ00η1µ1@R@?G00= G0θ0G1@@@@R@G10?D10= D1 µ1ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0D1@@@θ00η1µ1@R@?G00= G0θ0G1?D10= D1 µ1ρ1@@@@R?@G10 = G1 ρ1ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеВоспользуемся леммой о подъеме для обычных дизъюнктов.G0D1@@@θ00η1µ1@R@?G00= G0θ0G1?D10= D1 µ1ρ1@@@@R?@G10 = G1 ρ1И при этом верно равенство θ00 = (η1 ρ1 )|Y1 ,...,Ym .ЛЕММА О ПОДЪЕМЕДоказательство леммы о подъемеПоследовательно применяя этот прием на всех шагахвычисления запроса G00 , получаем SLD-резолютивноевычисление запроса G0 :(D1 , η1 , G1 ), (D2 , η1 , G2 ), . .

. , (Dn , ηn , )для которого выполняется система равенствθ0 = (η1 ρ1 )|Y1 ,...,Ymρ1 = (η2 ρ2 )|VarG1ρ2 = (η3 ρ3 )|VarG2...ρn = (ηn ρn )|VarGnИз этой системы следует равенство θ0 = (η1 η2 . . . ηn )|Y1 ,...,Ym ρ0для некоторой подстановки ρ0 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство теоремы полноты (завершение).Итак, у нас естьIправильный ответ θ0 на запрос G0 к хорновскойлогической программе P;Iподстановка λ = {Z1 /c1 , Z2 /c2 , . . .

, Zr /cr } «свежих»констант на место всех переменных Z1 , . . . , Zr из термовподстановки θ0 .Iосновной пример θ00 = θ0 λ правильного ответа θ.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство теоремы полноты (завершение).θ0 — правильный ответ на запрос G0 к хорновской логическойпрограмме P;⇓P |= G0 θ0 λ;⇓(по лемме об основных вычислениях )основной запрос G0 θ0 λ к множеству основных примеровпрограммных утверждений [P] имеет успешное вычисление;⇓(по лемме о подъеме для логических программ )запрос G0 к программе P имеет успешное вычисление свычисленным ответом η, для которого верно равенствоθ0 λ = ηρ0для некоторой подстановки ρ0 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство теоремы полноты (завершение).А теперь заменим в левой и правой частях равенстваθ0 λ = ηρ0все константы c1 , .

. . , cr на символы переменных Z1 , . . . , Zr .Поскольку константы c1 , . . . , cr не входят в состав запроса G0 ипрограммы P, эти константы не входят в состав термоввычисленного ответа η, и, значит, могут содержаться только вподстановке ρ0 .В левой части равенства подстановка λ = {Z1 /c1 , . . . , Zr /cr }превращается в пустую подстановку ε.В правой части равенства подстановка ρ0 превращается внекоторую новую подстановку ρ.В итоге равенство θ0 λ = ηρ0 превращается в равенствоθ0 = ηρПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИПоясняющий пример.Рассмотрим запрос ?P(U, V ) к логической программеP : P(f (X ), X ) ← R(X ); (1)R(Y ) ←;(2)Q(c) ←;(3)Легко видеть, что θ = {U/f (c), V /c} — это правильный ответна запрос к программе.Вместе с тем, единственный вычисленный ответ — этоη = {U/f (Y ), V /Y }.Все дело в том, что θ — это частный случай η: θ = η{Y /c}.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИИтак, любой правильный ответ на запрос к хорновскойлогической программе можно вычислить (возможно, собобщением) по правилу SLD-резолюции, и любойвычисленный ответ будет правильным.А как организовать вычисления логических программ, чтобывычислить ВСЕ ответы?КОНЕЦ ЛЕКЦИИ 13..