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

Например, TP монотонен.Лемма (о монотонности TP )I ⊆ J ⇒ TP (I ) ⊆ TP (J)Доказательство:Пусть A0 ∈ TP (I ). Тогда по определению оператора TPсуществует такой основной пример программного утвержденияD = A0 ← A1 , . . . , An ∈ [P], что {A1 , . . . , An } ⊆ I .Поскольку I ⊆ J, верно {A1 , . . . , An } ⊆ J, и поэтомуA0 ∈ TP (J).ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯУсловимся n-кратную композицию операторанепосредственного следования обозначать TPn , т. е.TPn (I ) = TP (TP (. . . TP (I ) . .

. )).|{z}n разТеорема (об устройстве MP )Для любой хорновской логической программы P верноравенство∞[MP =TPi (∅) .i=0ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯДоказательство:Вначале покажем, что справедливы следующие включения:TP0 (∅) ⊆ TP1 (∅) ⊆ TP2 (∅) ⊆ · · · ⊆ TPi (∅) ⊆ TPi+1 (∅) ⊆ . . .Это можно показать по индукции.Базис индукции. TP0 (∅) = ∅ ⊆ TP1 (∅).Индуктивный переход. Если TPi−1 (∅) ⊆ TPi (∅), то, согласнолемме о монотонности оператора TP , получаемTPi (∅) = TP (TPi−1 (∅)) ⊆ TP (TPi (∅)) = TPi+1 (∅).ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯДоказательство: 1.

Покажем MP ⊇∞STPi (∅).i=0Индукцией по i покажем, что MP ⊇ TPi (∅).Базис индукции. TP0 (∅) = ∅ ⊆ MP .Индуктивный переход. Допустим A0 ∈ TPi+1 (∅). Поопределению оператора TP это означает, что существует такойосновной пример программного утвержденияD = A0 ← A1 , . . . , An ∈ [P], что {A1 , .

. . , An } ⊆ TPi (∅).Согласно индуктивному предположению {A1 , . . . , An } ⊆ MP .Тогда, согласно лемме о модели для логической программы,получаем A0 ∈ MP .ОПЕРАТОР НЕПОСРЕДСТВЕННОГОСЛЕДОВАНИЯДоказательство: 2. Покажем MP ⊆∞STPi (∅).i=0Для этого достаточно показать, что∞Si=0TPi (∅) — одна измоделей программы P (почему этого достаточно? ).Воспользуемся леммой о модели для логической программы.Пусть D = A0 ← A1 , . . . , An — произвольный пример∞Sпрограммного утверждения из [P] и {A1 , . . . , An } ⊆TPi (∅).i=0Тогда, согласно свойству оператора TP , существует такое m,что {A1 , . . .

, An } ⊆ TPm (∅) (почему это так? ).Тогда, согласно определению оператора TP , верно∞SA0 ∈ TPm+1 (∅), и, поэтому, A0 ∈TPi (∅).Значит,∞Si=0i=0TPi (∅)— модель для P. MP ⊆∞Si=0TPi (∅).ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИТеперь мы знаем, что наименьшая эрбрановская модель MPимеет слоистое устройство.'$MP'$TPn (∅)rrrC0'(∅)TP3'TP2(∅)TP1 (∅)&&&&$$%%%%И это поможет нам доказать индукцией по числу слоев, чтодля каждого основного атома C0 ∈ MP запрос ?C0 имеетуспешное вычисление.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИТеорема полноты (первая)MP ⊆ SuccPДоказательство проведем в два этапаЭтап 1. Покажем, что если C0 ∈ MP , то запрос ?C0 клогической программе [P], состоящей из всех возможныхосновных примеров программы P, имеет успешноевычисление.Этап 2.

Покажем, что если основной запрос ?C0 к логическойпрограмме [P] имеет успешное вычисление, то и запрос ?C0 клогической программе P также имеет успешное вычисление.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство (Этап 1)Пусть C0 ∈ MP . По теореме об устройстве наименьшей∞STPi (∅), и поэтомумодели, верно равенство MP =i=0существует такое m, что C0 ∈ TPm (∅).Доказательство существования успешного вычисленияпроведем индукцией по m: C0 ∈ TPm (∅).Базис индукции.

m = 1. Если C0 ∈ TP (∅), то в программе [P]существует факт C0 ←. Значит, запрос ?C0 к программе [P]имеет успешное вычисление (C0 ←, ε, ).ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство (Этап 1)Индуктивный переход. m → m + 1. Пусть C0 ∈ TPm+1 (∅).Тогда в программе [P] существует такое утверждениеD0 = C0 ← C1 , C2 , . . . , Cn , что {C1 , . . . , Cn } ⊆ TPm (∅).ТогдаIЗапрос ?C0 к программе [P] имеет SLD-резольвенту?C1 , C2 , . . . , Cn ;IСогласно индуктивному предположению, каждый запрос?Ci , где 1 ≤ i ≤ n, имеет успешное SLD-резолютивноевычисление(Di1 , ε, Gi1 ), .

. . , (Diki , ε, ).почему в качестве унификаторов здесь стоит пустаяподстановка ε?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство (Этап 1)Индуктивный переход. Учитывая, что подцели C1 , C2 , . . . , Cn— это основные атомы, и, следовательно, они не изменяются врезультате применения к ним любых подстановок, получаемуспешное вычисление запроса ?C0 к программе [P]:?C0D0 : C0 ← C1 , C2 , . . . , Cn??C1 , C2 , .

. . , Cn?C0D0 : C0 ← C1 , C2 , . . . , Cn??C1 , C2 , . . . , Cn?C1D11?G11D12r?rrqqq?CnGn1Dn2r?rrD1k1?Dn1?Dnkn??C0?C0D0?D0 : C0 ← C1 , C2 , . . . , Cn?C1 , C2 , . . . , Cn D11??C1 , C2 , . . . , Cn?G11 , C2 , . . . , Cn?C1D11?G11D12r?rrqqq?CnDn1?Gn1Dn2r?rrD1k1?rrrDnkn?D1k1??Cq 2 , . . . , Cnqq?CnDn1?Gn1rrrDnkn?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство (Этап 1)Индуктивный переход. Учитывая, что подцели C1 , C2 , . .

. , Cn— это основные атомы, и, следовательно, они не изменяются врезультате применения к ним любых подстановок, получаемуспешное вычисление запроса ?C0 к программе [P]:И этим завершается построение успешного вычисления запроса?C0 к программе [P].Конец 1-го этапа док-ва.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство (Этап 2)Теперь необходимо показать, что если основной запрос ?C0 кпрограмме [P] имеет успешное вычисление, то этот же запрос?C0 к программе P также имеет успешное вычисление.Мы докажем, на самом деле, более общее утверждение,которое сформулируем в виде отдельной леммы.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛемма о подъеме (для логических программ)Пусть G0 — запрос к логической программе P, y1 , .

. . , yk —целевые переменные, t1 , . . . , tk — основные термы.Пусть запрос G00 = G0 {y1 /t1 , . . . , yk /tk } к логическойпрограмме [P] имеет успешное вычислениеcomp 0 = (D10 , ε, G10 ), (D20 , ε, G20 ), . . . , (DN0 , ε, ),в котором каждое программное утверждение Di0 ∈ [P] являетсяосновным примером Di0 = Di θi некоторого утвержденияпрограммы P.Тогда запрос G0 к логической программе P также имеетуспешное вычислениеcomp = (D1 , η1 , G1 ), (D2 , η2 , G2 ), . . . , (DN , ηN , ),и при этом существует подстановка ρ, для которой верноравенство {y1 /t1 , .

. . , yk /tk }θ1 θ2 . . . θN = η1 η2 . . . ηN ρ.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛемма о подъеме (для логических программ)G0ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛемма о подъеме (для логических программ)G0µ?G0 µПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛемма о подъеме (для логических программ)G0D1µD2θ1?G0 µθ2??D1 θ 1D2 θ 2AADNθN?DN θ NAε AAU G 01εAAU G0A2qqqGN0AεAA-AU ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛемма о подъеме (для логических программ)G0- G1η1D1µG0 µqqGNθ1ηNDNθ2??D1 θ 1D2 θ 2θN?DN θ NAε AAU G 01- η2D2AA?q- G2εAAU G0A2qqqGN0AεAA-AU ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИЛемма о подъеме (для логических программ)G0- G1η1D1µG0 µqqGN- η2ηND2θ1DNθ2??D1 θ 1D2 θ 2AA?q- G2θN?DN θ NAε AAU G 01εAAU G0A2qqqGN0µθ1θ2 . .

. θN = η1η2 . . . ηNρAεAA-AU ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство (Этап 2)Для нужд доказываемой теоремы достаточно использовать тотвариант леммы о подъеме, когда запрос G0 состоит изодной-единственной подцели.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеВоспользуемся индукцией по длине успешного вычисления.Обозначим символом µ подстановку {y1 /t1 , . . . , yk /tk }.Тогда G00 = G0 µ.Базис индукции. N = 1.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеБазис индукции.

N = 1.G00D10ε?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеБазис индукции. N = 1.Это возможно, если?C0 µA0 θ1 ←ε?запрос G00 состоит из одной подцели,т. е. G0 = C0 , G00 = C0 µ,а программное утверждение D10 — это факт,т. е. D1 = A0 ←, D00 = A0 θ1 ←,и при этом C0 µ = A0 θ1 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеБазис индукции. N = 1.Итак, G0 = C0 , D1 = A0 ←, C0 µ = A0 θ1 .?C0 µA0 θ1 ←ε?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеБазис индукции. N = 1.Итак, G0 = C0 , D1 = A0 ←, C0 µ = A0 θ1 .?C0 µA0 θ1 ←ε?Но при этом VarG0 ∩ VarD1 = ∅ (почему? ),и VarC0 µ = ∅ (почему? ).ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеБазис индукции.

N = 1.Итак, G0 = C0 , D1 = A0 ←, C0 µ = A0 θ1 .?C0 µA0 θ1 ←ε?Но при этом VarG0 ∩ VarD1 = ∅ (почему? ),и VarC0 µ = ∅ (почему? ).Значит, подстановка µ не влияет на A0 ,и подстановка θ1 не влияет на C0 µ.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеБазис индукции.

N = 1.Итак, G0 = C0 , D1 = A0 ←, C0 µ = A0 θ1 .?C0 µA0 θ1 ←ε?Но при этом VarG0 ∩ VarD1 = ∅ (почему? ),и VarC0 µ = ∅ (почему? ).Значит, подстановка µ не влияет на A0 ,и подстановка θ1 не влияет на C0 µ.Значит, C0 µθ1 = C0 µ = A0 θ1 = A0 µθ1 ,т. е. атомы C0 и A0 имеют унификатор µθ1 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеБазис индукции. N = 1.Итак, G0 = C0 , D1 = A0 ← и C0 µθ1 = A0 µθ1 .?C0 µA0 θ1 ←ε?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеБазис индукции.

N = 1.Итак, G0 = C0 , D1 = A0 ← и C0 µθ1 = A0 µθ1 .?C0A0 ←η1?Значит, атомы C0 и A0 имеют НОУ η1 ,и тогда запрос G0 =?C0 и факт A0 ←порождают SLD-резольвенту при помощи η1 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеБазис индукции. N = 1.Итак, G0 = C0 , D1 = A0 ← и C0 µθ1 = A0 µθ1 .?C0A0 ←η1?Значит, атомы C0 и A0 имеют НОУ η1 ,и тогда запрос G0 =?C0 и факт A0 ←порождают SLD-резольвенту при помощи η1 .Получаем успешное вычисление запроса G0 =?C0к программе P.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеБазис индукции. N = 1.Итак, G0 = C0 , D1 = A0 ← и C0 µθ1 = A0 µθ1 .?C0A0 ←η1?Значит, атомы C0 и A0 имеют НОУ η1 ,и тогда запрос G0 =?C0 и факт A0 ←порождают SLD-резольвенту при помощи η1 .Получаем успешное вычисление запроса G0 =?C0к программе P.η1 ∈ НОУ(C0 , A0 ), а µθ1 — унификатор C0 и A0 .Значит, µθ1 = η1 ρ для некоторой подстановки ρ.Базис индукции доказан.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеИндуктивный переход.

N → N + 1.G00D10ε?G10?qq θq 2Nq шаговqq θN?ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеИндуктивный переход. N → N + 1.?C10 , . . . , Cm0A00 ← A01 , . . . , A0nε??A01 , . . . , A0n , C20 , . . . , Cm0?qq θq 2Nq шаговqq θN?Чтобы сделать 1-ый шаг вычисления,нужно, чтобыG00 = C10 , . . . , Cm0 ,D10 = A00 ← A01 , . . . , A0n ,и при этом C10 = A00 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеИндуктивный переход. N → N + 1.Чтобы сделать 1-ый шаг вычисления,нужно, чтобы(A0 ← A1 , . . .

, An )θ1G00 = C10 , . . . , Cm0 ,εD10 = A00 ← A01 , . . . , A0n ,??(A1 , . . . , An )θ1 , (C2 , . . . , Cm )µ и при этом C10 = A00 .?(C1 , . . . , Cm )µ?qq θq 2Nq шаговqq θN?Значит,G0 = C1 , . . . , Cm , D1 = A0 ← A1 , . . . , An ,и при этомC10 , . . . , Cm0 = (C1 , . . . , Cm )µ,A00 ← A01 . . . , A0n = (A0 ← A1 , . . . , An )θ1 иC1 µ = A0 θ1 .ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИДоказательство леммы о подъемеИндуктивный переход.

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