LectLog14 (Старые лекции, в целом тоже самое), страница 3

. , An )θ1 , (C2 , . . . , Cm )µ?qq θq 2Nq шаговqq θN?Так же, как и в базисе индукции,можно убедиться в том, чтоθ1 не влияет на C1 , . . . , Cm ,а µ не влияет на A0 , A1 , . . . , An .Поэтому C1 µ = A0 θ1 влечет C1 µθ1 = A0 µθ1 ,и (A1 , . . . , An )θ1 , (C2 , . . . , Cm )µ = (A1 , . . . , An , C2 , . . . , Cm )µθ1 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеИндуктивный переход. N → N + 1.?(C1 , .

. . , Cm )µ(A0 ← A1 , . . . , An )θ1ε??(A1 , . . . , An , C2 , . . . , Cm )µθ1?qq θq 2Nq шаговqq θN?Так же, как и в базисе индукции,можно убедиться в том, чтоθ1 не влияет на C1 , . . . , Cm ,а µ не влияет на A0 , A1 , . . . , An .Поэтому C1 µ = A0 θ1 влечет C1 µθ1 = A0 µθ1 ,и (A1 , . . . , An )θ1 , (C2 , . . . , Cm )µ = (A1 , . . . , An , C2 , .

. . , Cm )µθ1 .Т. к. C1 µθ1 = A0 µθ1 ,существует такая η1 ∈ НОУ(C1 , A0 ),что µθ1 = η1 ρ1 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеИндуктивный переход. N → N + 1.?C1 , . . . , CmA0 ← A1 , . . . , Anη1??(A1 , . . . , An , C2 , . . . , Cm )η1НОУ η1 порождает SLD-резольвентуG1 =?(A1 , . . . , An , C2 , . . . , Cm )η1запроса G0 =?C1 , .

. . , Cn иправила A0 ← A1 , . . . , An .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеИндуктивный переход. N → N + 1.?C1 , . . . , CmA0 ← A1 , . . . , Anη1??(A1 , . . . , An , C2 , . . . , Cm )η1НОУ η1 порождает SLD-резольвентуG1 =?(A1 , . . . , An , C2 , . . . , Cm )η1запроса G0 =?C1 , . . . , Cn иправила A0 ← A1 , . . . , An .Поскольку µθ1 = η1 ρ1 ,запрос G10 = (A1 , .

. . , An , C2 , . . . , Cm )µθ1является основным примеромзапроса G1 = (A1 , . . . , An , C2 , . . . , Cm )η1 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеИндуктивный переход. N → N + 1.?C1 , . . . , CmA0 ← A1 , . . . , Anη1??(A1 , . . . , An , C2 , . . . , Cm )η1?qq ηq 2Nq шаговqq ηN?НОУ η1 порождает SLD-резольвентуG1 =?(A1 , . . . , An , C2 , .

. . , Cm )η1запроса G0 =?C1 , . . . , Cn иправила A0 ← A1 , . . . , An .Поскольку µθ1 = η1 ρ1 ,запрос G10 = (A1 , . . . , An , C2 , . . . , Cm )µθ1является основным примеромзапроса G1 = (A1 , . . . , An , C2 , . . . , Cm )η1 .Тогда по индуктивной гипотезезапрос G1 = (A1 , . . . , An , C2 , . .

. , Cm )η1имеет успешное вычисление, и при этомρ1 θ2 . . . θN = η2 . . . ηN ρ .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеИндуктивный переход. N → N + 1.?C1 , . . . , CmA0 ← A1 , . . . , Anη1??(A1 , . . . , An , C2 , . . . , Cm )η1?qq ηq 2Nq шаговqq ηN?Итак, получаем, что запросG0 =?C1 , C2 , . . . , Cmимеет успешное вычислениес последовательностью подстановокη1 , η2 , . . . , ηNи при этомµθ1 = η1 ρ1 и ρ1 θ2 .

. . θN = η2 . . . ηN ρ .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеИндуктивный переход. N → N + 1.?C1 , . . . , CmA0 ← A1 , . . . , Anη1??(A1 , . . . , An , C2 , . . . , Cm )η1?qq ηq 2Nq шаговqq ηN?Итак, получаем, что запросG0 =?C1 , C2 , . . . , Cmимеет успешное вычислениес последовательностью подстановокη1 , η2 , . . . , ηNи при этомµθ1 = η1 ρ1 и ρ1 θ2 .

. . θN = η2 . . . ηN ρ .Таким образом,µθ1 θ2 . . . θN = η1 ρ1 θ2 . . . θN == η1 η2 . . . ηN ρ.Что и требовалось доказать.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛемма о подъеме для логических программ доказана, и вместес ней завершена 2-я часть доказательства теоремы.Таким образом, MP ⊆ SuccPСледствие 1.MP = SuccPСледствие 2.Пусть C1 , . . . , Cn — основные атомы, и P — хорновскаялогическая программа.Тогда P |= C1 & . .

. &Cn тогда и только тогда, когда запрос?C1 , . . . , Cn к программе P имеет успешное SLD-резолютивноевычисление.доказательство — самостоятельно.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИТеорема полноты (главная).Пусть θ — правильный ответ на запрос G к хорновскойлогической программе P.Тогда существует такой вычисленный ответ η на запрос G кпрограмме P, что θ = ηρ для некоторой подстановки ρ.Доказательство.Пусть θ = {y1 /t1 , . .

. , yk /tk } и пустьkSVarti = {z1 , . . . , zm }.i=1Выберем некоторое множество констант {c1 , . . . , cm }, несодержащихся в запросе G , в термах подстановки θ и впрограмме P, и рассмотрим подстановкуλ = {z1 /c1 , . . . , zm /cm }.Т. к. θ — правильный ответ, то P |= ∀z1 . . . ∀zm G θ.Поэтому G θλ — основной пример запроса G и P |= G θλ.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство.А раз G θλ — основной пример запроса G и P |= G θλ, то,согласно следствию 2 и лемме о подъеме для логическихпрограмм , запрос G имеет успешное SLD-резолютивноевычисление с таким вычисленным ответом η, чтоθλ = ηρ0для некоторой подстановки ρ0 .Т.

к. константы c1 , . . . , cm не входят в состав запроса G ипрограммы P, эти константы не входят в состав термоввычисленного ответа η, и, значит, могут содержаться только вподстановке ρ0 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство.А теперь заменим в левой и правой частях равенстваθλ = ηρ0все символы c1 , . . .

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