LectLog15 (1158008), страница 2
Текст из файла (страница 2)
, D1− , . . . , Cj , . . . , Cm )θ1D2 θ ∈ НОУ(C θ9?2+j 1 , D2 )G20 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ ∈ НОУ(C , D + )19?iДалее, заметим,что Ci θ1 θ2 = D1+ θ1 θ2 ,и поэтому Ci η1 λ = D1+ η1 λ.1G10 :?(C1 , . .
. , D1− , . . . , Cj , . . . , Cm )θ1D2 θ ∈ НОУ(C θ9?2+j 1 , D2 )G20 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ ∈ НОУ(C , D + )Далее, заметим,что Ci θ1 θ2 = D1+ θ1 θ2 ,и поэтому Ci η1 λ = D1+ η1 λ.Т. к. Domη1 ∩ VarD1 = ∅,верноD1+ η1 = D1+ .G10 :?(C1 , . . . , D1− , .
. . , Cj , . . . , Cm )θ119?i1D2 θ ∈ НОУ(C θ9?2+j 1 , D2 )G20 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ ∈ НОУ(C , D + )Далее, заметим,что Ci θ1 θ2 = D1+ θ1 θ2 ,и поэтому Ci η1 λ = D1+ η1 λ.Т. к. Domη1 ∩ VarD1 = ∅,верноD1+ η1 = D1+ .G10 :?(C1 , .
. . , D1− , . . . , Cj , . . . , Cm )θ1Значит, Ci η1 λ = D1+ λ,D2т. е. Ci η1 и D1+ унифицируемы.9?9?1θ2i1∈ НОУ(Cj θ1 , D2+ )G20 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , .
. . , Ci , . . . , Cj , . . . , CmD1 θ ∈ НОУ(C , D + )19?iА раз Ci η1 и D1+ унифицируемы,существует η2 ∈ НОУ(Ci η1 , D1+ ),и при этом λ = η2 ρ0 .1G10 :?(C1 , . . . , D1− , . . . , Cj , . . . , Cm )θ1D2 θ ∈ НОУ(C θ9?2+j 1 , D2 )G20 :?(C1 θ1 , . . . , D1− θ1 , . . .
, D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ ∈ НОУ(C , D + )19?i1Итак, получаемη1 ∈ НОУ(Cj , D2+ ),η2 ∈ НОУ(Ci η1 , D1+ ),θ1 θ2 = η1 λ = η1 η2 ρ0 .G10 :?(C1 , . . . , D1− , .
. . , Cj , . . . , Cm )θ1D2 θ ∈ НОУ(C θ9?2+j 1 , D2 )G20 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Получаем другое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD2 η ∈ НОУ(C , D + )9?1j2Итак, получаемη1 ∈ НОУ(Cj , D2+ ),η2 ∈ НОУ(Ci η1 , D1+ ),θ1 θ2 = η1 λ = η1 η2 ρ0 .G100 :?(C1 , . . . , Ci , .
. . , D2− , . . . , Cm )η1D19?η ∈ НОУ(C η2Значит, запрос G0 имеети другое вычисление.+i 1 , D1 )G200 :?(C1 η1 , . . . , D1− , . . . , D2− η1 . . . , Cm η1 )η2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).G0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD2η1 ∈ НОУ(Cj , D2+ )9?Применяя те же рассужденияк построенному вычислениюполучим η1 η2 = θ1 θ2 ρ00 .G100 :?(C1 , . .
. , Ci , . . . , D2− , . . . , Cm )η1D1 η2 ∈ НОУ(Ci η1 , D1+ )9?G200 :?(C1 η1 , . . . , D1− , . . . , D2− η1 . . . , Cm η1 )η2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).G0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD2η ∈ НОУ(C , D + )9?1jПрименяя те же рассужденияк построенному вычислениюполучим η1 η2 = θ1 θ2 ρ00 .2G100 :?(C1 , . . . , Ci , . .
. , D2− , . . . , Cm )η1D1η2 ∈ НОУ(Ci η1 , D1+ )9?G200 :?(C1 η1 , . . . , D1− , . . . , D2− η1 . . . , Cm η1 )η2Равенства θ1 θ2 = η1 η2 ρ0 , η1 η2 = θ1 θ2 ρ00 означают, чтоподстановки η1 η2 и θ1 θ2 , а также запросы G20 и G200 являютсявариантами друг друга.ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙТеорема сильной полнотыКаково бы ни было правило выбора подцелей R, если θ —правильный ответ на запрос G0 к хорновской логическойпрограмме P, то существует такой R-вычисленный ответ η,что равенствоθ = ηρвыполняется для некоторой подстановки ρ.ДоказательствоПо теореме полноты существут такой вычисленный ответ η 0 ,что θ = η 0 ρ0 .
Рассмотрим соответствующее этому ответууспешное вычисление запроса G0comp 0 = (D1 , η10 , G1 ), . . . , (DN , ηN, ),0 .в котором η 0 = η10 . . . ηNПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательствоПредположим, что R(G0 ) = Ci . Поскольку comp 0 — этоуспешное вычисление, существует ki , что подцель Ci впервыевыбирается на ki -ом шаге вычисления comp 0 . Применяяпоследовательно ki раз переключательную лемму, можнополучить успешное вычисление00comp 00 = (Dik , η100 , G100 ), (D1 , η200 , G100 ), .
. . , (DN , ηN, ),в котором на первом шаге выбирается подцель Ci = R(G0 ), но00 — это вариантпри этом вычисленный результат η 00 = η100 . . . ηN000вычисленного ответа η = η1 . . . ηN , и значит θ = η 00 ρ00 .Повторяя этот трюк N раз, получим требуемое успешноеR-вычисление.Полное и строгое доказательство требует примененияматематической индукции. Провести самостоятельно.ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙТеорема сильной полноты говорит о том, что правило выбораподцелей не играет существенной роли при вычислении ответа:любое правило выбора подцелей позволяет получить всевычисленные ответы.Поэтому для единообразной организации вычисленийлогических программ всегда используется стандартноеправило выбора : в каждом запросе всегда выбирается самаяпервая (левая) подцель.Теперь займемся вопросом о том, какую роль играет выборподходящих программных утверждений.ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММОбратимся снова к запросу ?P(U, V ), R(U) к логическойпрограммеP : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;(1)(2)(3)(4)и будем применять стандартное правило выбора подцелей.ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММТогда возможны следующие два вычисления запроса?P(U, V ), R(U)?P(U, V ), R(U)?P(U, V ), R(U)тупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММТогда возможны следующие два вычисления запроса?P(U, V ), R(U)?P(U, V ), R(U)?P(U, V ), R(U)P(X1 , Y1 ) ← R(X1 ), Q(Y1 )θ1 = {U/X1 , V /Y1 }??R(X1 ), Q(Y1 ), R(X1 )тупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММТогда возможны следующие два вычисления запроса?P(U, V ), R(U)?P(U, V ), R(U)?P(U, V ), R(U)P(X1 , Y1 ) ← R(X1 ), Q(Y1 )θ1 = {U/X1 , V /Y1 }??R(X1 ), Q(Y1 ), R(X1 )R(b) ←θ2 = {X1 /b}??Q(Y1 ), R(b)тупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММТогда возможны следующие два вычисления запроса?P(U, V ), R(U)?P(U, V ), R(U)?P(U, V ), R(U)P(X1 , Y1 ) ← R(X1 ), Q(Y1 )θ1 = {U/X1 , V /Y1 }??R(X1 ), Q(Y1 ), R(X1 )R(b) ←θ2 = {X1 /b}??Q(Y1 ), R(b)Q(c) ←θ3 = {Y1 /c}??R(b)тупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММТогда возможны следующие два вычисления запроса?P(U, V ), R(U)?P(U, V ), R(U)?P(U, V ), R(U)P(X1 , Y1 ) ← R(X1 ), Q(Y1 )θ1 = {U/X1 , V /Y1 }??R(X1 ), Q(Y1 ), R(X1 )R(b) ←θ2 = {X1 /b}??Q(Y1 ), R(b)Q(c) ←θ = {Y1 /c}3??R(b)R(b) ←θ4 = ε??тупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММТогда возможны следующие два вычисления запроса?P(U, V ), R(U)?P(U, V ), R(U)?P(U, V ), R(U)P(X1 , Y1 ) ← R(X1 ), Q(Y1 )θ1 = {U/X1 , V /Y1 }??R(X1 ), Q(Y1 ), R(X1 )R(b) ←θ2 = {X1 /b}??Q(Y1 ), R(b)Q(c) ←θ = {Y1 /c}3??R(b)R(b) ←θ4 = ε??тупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММТогда возможны следующие два вычисления запроса?P(U, V ), R(U)?P(U, V ), R(U)?P(U, V ), R(U)P(X1 , Y1 ) ← R(X1 ), Q(Y1 )θ1 = {U/X1 , V /Y1 }??R(X1 ), Q(Y1 ), R(X1 )P(X1 , X1 ) ← Q(X1 );η1 = {U/X1 , V /X1 }??Q(X1 ), R(X1 )R(b) ←θ2 = {X1 /b}??Q(Y1 ), R(b)Q(c) ←θ = {Y1 /c}3??R(b)R(b) ←θ4 = ε??тупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММТогда возможны следующие два вычисления запроса?P(U, V ), R(U)?P(U, V ), R(U)?P(U, V ), R(U)P(X1 , Y1 ) ← R(X1 ), Q(Y1 )θ1 = {U/X1 , V /Y1 }??R(X1 ), Q(Y1 ), R(X1 )R(b) ←P(X1 , X1 ) ← Q(X1 );η1 = {U/X1 , V /X1 }??Q(X1 ), R(X1 )Q(c) ←η2 = {X1 /c}θ2 = {X1 /b}??Q(Y1 ), R(b)Q(c) ←θ = {Y1 /c}3??R(b)R(b) ←θ4 = ε????R(c)failureтупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММКак видно из этого примера, выбор программных утвержденийиграет значительную роль.Программное утверждение — это способ (рецепт) решениязадачи (подцели).
Ясно, что некоторые способы решения могутбыть «хорошими», а некоторые — «плохими».Таким образом, чтобы вычислить все ответы на запрос (или,что то же само, гарантировать вычисление хотя бы одногоответа), нужно уметь просматривать все варианты выборапрограммных утверждений. И нужно правильно организоватьэтот перебор.ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММОпределениеДеревом SLD-резолютивных вычислений запроса G0 клогической программе P называется помеченное корневоедерево TG0 ,P , удовлетворяющее следующим требованиям:1. Корнем дерева является исходный запрос G0 ;2. Потомками каждой вершины G являются всевозможныеSLD-резольвенты запроса G (при фиксированномстандартном правиле выбора подцелей);3.
Листовыми вершинами являются пустые запросы(завершающие успешные вычисления) и запросы, неимеющие SLD-резольвент (завершающие тупиковыевычисления).ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММИллюстрация'TG0 ,P&?Gt 0P)@PPqR@?$%ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММИллюстрация?Gt 0P)@PPqR@?'TG0 ,P$?GitPq t ?Gi0vt) @PPqqq@R t 000@?G 00 t?G?Gi0i&i%ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММИллюстрация?Gt 0P)@PPqR@?'TG0 ,P?GitPq t ?Gi0vt) @PPqqq@R t 000@?G 00 t?G?Gi0ii$?Gt j?t?&%ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример 1.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример 1.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;?P(U,V ), R(U)tДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример 1.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;(1), {U/X1 , V /Y1 }Q(c) ←;?R(X1 ), Q(Y1 ), R(X1 ) t?P(U,V ), R(U)t@ (2), {U/X1 , V /X1 }@R t?Q(X1 ), R(X1 )@ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример 1.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;(1), {U/X1 , V /Y1 }Q(c) ←;?R(X1 ), Q(Y1 ), R(X1 ) t(3), {X1 /b}?Q(Y1 ), R(b) t??P(U,V ), R(U)t@ (2), {U/X1 , V /X1 }@R t?Q(X1 ), R(X1 )@(2), {X1 /c}?t?R(c)ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример 1.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;(1), {U/X1 , V /Y1 }Q(c) ←;?R(X1 ), Q(Y1 ), R(X1 ) t(3), {X1 /b}?Q(Y1 ), R(b) t?(4), {Y1 /c}?R(b) ?t?P(U,V ), R(U)t@ (2), {U/X1 , V /X1 }@R t?Q(X1 ), R(X1 )@(2), {X1 /c}?t?R(c)failureДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример 1.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;(1), {U/X1 , V /Y1 }Q(c) ←;?R(X1 ), Q(Y1 ), R(X1 ) t(3), {X1 /b}?P(U,V ), R(U)t@ (2), {U/X1 , V /X1 }@R t?Q(X1 ), R(X1 )@(2), {X1 /c}?Q(Y1 ), R(b) t??t?R(c)failure(4), {Y1 /c}?R(b) ?t(3), ε?t?ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример 2..P : P(X L) ← P(L), R(X );P(nil) ←;R(a) ←;R(c) ←;.t?P(X Y )ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММ.Пример 2..P : P(X L) ← P(L), R(X );P(nil) ←;R(a) ←;R(c) ←;t?P(X Y )(1), {X1 /X , L1 /Y }?t?P(Y ), R(X )ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММ.Пример 2.t?P(X Y ).P : P(X L) ← P(L), R(X );(1), {X1 /X , L1 /Y }P(nil) ←;?t?P(Y ), R(X )R(a) ←;@ (2), {Y /nil}(1), {Y /X2 L2 }@R(c) ←;R t?R(X )@?P(L2 ), R(X2 ), R(X ) t.ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММ.Пример 2.t?P(X Y ).P : P(X L) ← P(L), R(X );(1), {X1 /X , L1 /Y }P(nil) ←;?t?P(Y ), R(X )R(a) ←;@ (2), {Y /nil}(1), {Y /X2 L2 }@R(c) ←;R t?R(X )@?P(L2 ), R(X2 ), R(X )t.(1), {L2 /X3?P(L3 ), R(X3 ),R(X2 ), R(X ).L3 }(3), {X /a} @ (4), {X /c}@(2), {L2 /nil}?) ?R(X2 ), R(X ) tt?Rtt @??ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММ.Пример 2.t?P(X Y ).P : P(X L) ← P(L), R(X );(1), {X1 /X , L1 /Y }P(nil) ←;?t?P(Y ), R(X )R(a) ←;@ (2), {Y /nil}(1), {Y /X2 L2 }@R(c) ←;R t?R(X )@?P(L2 ), R(X2 ), R(X )t.(1), {L2 /X3.L3 }(3), {X /a} @ (4), {X /c}@(2), {L2 /nil}?P(L3 ), R(X3 ),?) ?R(X2 ), R(X ) ttR(X2 ), R(X )@∞(2), {L3 /nil}@(3), {X1 /a}?Rt?R(X )@t?R(X )(3), {X1 /a})?t?R(X3 ), R(X2 ), R(X )?Rtt @?ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММ.Пример 2.t?P(X Y ).P : P(X L) ← P(L), R(X );(1), {X1 /X , L1 /Y }P(nil) ←;?t?P(Y ), R(X )R(a) ←;@ (2), {Y /nil}(1), {Y /X2 L2 }@R(c) ←;R t?R(X )@?P(L2 ), R(X2 ), R(X )t.(1), {L2 /X3.L3 }(3), {X /a} @ (4), {X /c}@(2), {L2 /nil}?P(L3 ), R(X3 ),?) ?R(X2 ), R(X ) ttR(X2 ), R(X )@?@(3), {X1 /a}??Rt?R(X )@tt?R(X )@@ (4), {X /c}(4),{X/c}?R(X3 ), R(X2 ), R(X )(3), {X /a} @ (3), {X /a} @?Rt?Rtt @t @)∞?Rtt @(2), {L3 /nil}(3), {X1 /a}????ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММИтак, деревья вычислений логических программ бываютразные — конечные и бесконечные, с конечным илибесконечным множеством ветвей, и т.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
