Ещё одни лекции В.А. Захарова, страница 23

ЗахаровЛекция 14.Правила выбора подцелей.Деревья вычислений логическихпрограмм.Стратегии вычисления логическихпрограмм.ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙSLD-резолютивное вычисление запроса ?G к логическойпрограмме P определяется неоднозначно.Рассмотрим запрос ?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(X , Y ) ← R(X ), Q(Y ); (1)P(X , X ) ← Q(X );(2)P(X , Y ) ← R(X ), Q(Y ); (1)P(X , X ) ← Q(X );(2)ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙРассмотрим два вычисления запроса ?P(U, V ), R(U)?P(U, V ), R(U)?P(U, V ), R(U)R(b) ←P(X1 , Y1 ) ← R(X1 ), Q(Y1 )θ1 = {U/X1 , V /Y1 }??R(X1 ), Q(Y1 ), R(X1 )η1 = {U/b}??P(b, V )R(b) ←θ2 = {X1 /b}P(X1 , Y1 ) ← R(X1 ), Q(Y1 )??Q(Y1 ), R(b)Q(c) ←η2 = {X1 /b, V /Y1 }??R(b), Q(Y1 )Q(c) ←θ3 = {Y1 /c}??R(b)R(b) ←η3 = {Y1 /c}??R(b)R(b) ←??θ4 = ε??θ = θ1 θ2 θ3 θ4 |{U,V } = {U/b, V /c}η = η1 η2 η3 η4 |{U,V } = {U/b, V /c}η4 = εПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙКак видите, мы получаем одинаковые вычисленные ответы вобоих вычислениях независимо от порядка выбора подцелей вцелевых утверждениях.Это случайность или так бывает всегда?С точки зрения операционной семантики программ, запрос —это список задач, которые нужно решить.Для решения запроса нужно решить все подцели запроса.Значит, результат вычисления не зависит от того порядка,в котором решаются задачи (выбираются подцели).Решение одной задачи может помочь решить другую.Значит, правильно выбранный порядок решения задачсущественно влияет на эффективность вычислениязапроса.Покажем, что верно первое предположение.ПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИОпределение.Отображение R, которое сопоставляет каждому непустомузапросу G : ?C1 , C2 , .

. . , Cm одну из подцелей Ci = R(G ) в этомзапросе, называется правилом выбора подцелей .Для заданного правила выбора подцелей R вычислениезапроса G к логической программе P называетсяR-вычислением , если на каждом шаге вычисления очереднаяподцель в запросе выбирается по правилу R.Ответ, полученный в результате успешного R-вычисления,называется R-вычисленным .Возникает вопрос:При каком правиле выбора подцелей R каждый вычисленныйответ оказывется R-вычисленным?ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДля каждого программного утвержденияD : A0 ← A1 , A2 , .

. . , An условимся использовать запись D +для обозначения атома A0 , а запись D − — для обозначениясписка атомов A1 , A2 , . . . , An . В частности, если D — это фактA0 ←, то D − — это пустой список.Выбор обозначений обусловлен тем, что утверждениеD : A0 ← A1 , A2 , . . . , An соответствует дизъюнктуположительная литераA0∨ ¬A1 ∨ ¬A2 ∨ · · · ∨ ¬Anотрицательные литерыПОЛНОТА ОПЕРАЦИОННОЙ СЕМАНТИКИПереключательная лемма.Предположим, что запрос G0 :?C1 , . .

. , Ci , . . . , Cj , . . . , Cm кхорновской логической программе P имеет вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1θ1 ∈ НОУ(Ci , D1+ )9?G1 :?(C1 , . . . , D1− , . . . , Cj , . . . , Cm )θ1D2 θ2 ∈ НОУ(Cj θ1 , D2+ )9?G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . .

. , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙПереключательная лемма.Тогда запрос G0 к программе P также имеет вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD2η1 ∈ НОУ(Cj , D2+ )9?G1 :?(C1 , . . . , Ci , . . . , D2− , . . . , Cm )η1D1 η2 ∈ НОУ(Ci η1 , D1+ )9?G2 :?(C1 η1 , . . . , D1− , .

. . , D2− η1 . . . , Cm η1 )η2и при этом запросы G2 и G2 являются вариантами друг друга,т. е. θ1 θ2 ρ = η1 η2 и η1 η2 ρ = θ1 θ2 для некоторых ρ , ρ ∈ Subst.ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙПереключательная лемма говорит о том, что при изменениипорядка выбора подцелей результат вычисления сохраняется (сточностью до переименования переменных).ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , .

. . , Ci , . . . , Cj , . . . , CmD1 θ1 ∈ НОУ(Ci , D1+ )9?G1 :?(C1 , . . . , D1− , . . . , Cj , . . . , Cm )θ1D2 θ2 ∈ НОУ(Cj θ1 , D2+ )9?G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ1 ∈ НОУ(Ci , D1+ )9?Согласно определениюSLD-резолютивного вычисленияDomθ1 ∩ VarD2 = ∅.G1 :?(C1 , . .

. , D1− , . . . , Cj , . . . , Cm )θ1D2 θ2 ∈ НОУ(Cj θ1 , D2+ )9?G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ1 ∈ НОУ(Ci , D1+ )9?Согласно определениюSLD-резолютивного вычисленияDomθ1 ∩ VarD2 = ∅.Поэтому D2+ θ2 = D2+ θ1 θ2 .G1 :?(C1 , . . .

, D1− , . . . , Cj , . . . , Cm )θ1D2 θ2 ∈ НОУ(Cj θ1 , D2+ )9?G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ1 ∈ НОУ(Ci , D1+ )9?Согласно определениюSLD-резолютивного вычисленияDomθ1 ∩ VarD2 = ∅.Поэтому D2+ θ2 = D2+ θ1 θ2 .G1 :?(C1 , .

. . , D1− , . . . , Cj , . . . , Cm )θ1D2θ ∈ НОУ(C θ , D + )2j 129?Следовательно,Cj θ1 θ2 = D2+ θ2 = D2+ θ1 θ2 ,т. е. Cj и D2+ унифицируемы.G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ1 ∈ НОУ(Ci , D1+ )9?А раз Cj и D2+ унифицируемы,существует η1 ∈ НОУ(Cj , D2+ ),и при этом θ1 θ2 = η1 λ.G1 :?(C1 , .

. . , D1− , . . . , Cj , . . . , Cm )θ1D2 θ2 ∈ НОУ(Cj θ1 , D2+ )9?G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ1 ∈ НОУ(Ci , D1+ )9?Далее, заметим,что Ci θ1 θ2 = D1+ θ1 θ2 ,и поэтому Ci η1 λ = D1+ η1 λ.G1 :?(C1 , . . . , D1− , . . . , Cj , .

. . , Cm )θ1D2 θ2 ∈ НОУ(Cj θ1 , D2+ )9?G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ1 ∈ НОУ(Ci , D1+ )9?Далее, заметим,что Ci θ1 θ2 = D1+ θ1 θ2 ,и поэтому Ci η1 λ = D1+ η1 λ.Т. к. Domη1 ∩ VarD1 = ∅,++G1 :?(C1 , . . . , D1− , . .

. , Cj , . . . , Cm )θ1 верно D1 η1 = D1 .D2 θ2 ∈ НОУ(Cj θ1 , D2+ )9?G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ1 ∈ НОУ(Ci , D1+ )9?Далее, заметим,что Ci θ1 θ2 = D1+ θ1 θ2 ,и поэтому Ci η1 λ = D1+ η1 λ.Т. к. Domη1 ∩ VarD1 = ∅,++G1 :?(C1 , . . . , D1− , . .

. , Cj , . . . , Cm )θ1 верно D1 η1 = D1 .Значит, Ci η1 λ = D1+ λ,D2т. е. Ci η1 и D1+ унифицируемы.θ2 ∈ НОУ(Cj θ1 , D2+ )9?G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , .

. . , Ci , . . . , Cj , . . . , CmD1 θ1 ∈ НОУ(Ci , D1+ )9?А раз Ci η1 и D1+ унифицируемы,существует η2 ∈ НОУ(Ci η1 , D1+ ),и при этом λ = η2 ρ .G1 :?(C1 , . . . , D1− , . . . , Cj , . . . , Cm )θ1D2 θ2 ∈ НОУ(Cj θ1 , D2+ )9?G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . .

. , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ1 ∈ НОУ(Ci , D1+ )9?Итак, получаемη1 ∈ НОУ(Cj , D2+ ),η2 ∈ НОУ(Ci η1 , D1+ ),θ1 θ2 = η1 λ = η1 η2 ρ .G1 :?(C1 , . . . , D1− , .

. . , Cj , . . . , Cm )θ1D2 θ2 ∈ НОУ(Cj θ1 , D2+ )9?G2 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Получаем другое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD2 η1 ∈ НОУ(Cj , D2+ )9?Итак, получаемη1 ∈ НОУ(Cj , D2+ ),η2 ∈ НОУ(Ci η1 , D1+ ),θ1 θ2 = η1 λ = η1 η2 ρ .G1 :?(C1 , .

. . , Ci , . . . , D2− , . . . , Cm )η1D1η ∈ НОУ(C η , D + )2i 119?Значит, запрос G0 имеети другое вычисление.G2 :?(C1 η1 , . . . , D1− , . . . , D2− η1 . . . , Cm η1 )η2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).G0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD2η1 ∈ НОУ(Cj , D2+ )9?Применяя те же рассужденияк построенному вычислениюполучим η1 η2 = θ1 θ2 ρ .G1 :?(C1 , . . . , Ci , .

. . , D2− , . . . , Cm )η1D1 η2 ∈ НОУ(Ci η1 , D1+ )9?G2 :?(C1 η1 , . . . , D1− , . . . , D2− η1 . . . , Cm η1 )η2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).G0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD 2η∈НОУ(Cj , D2+ )19?Применяя те же рассужденияк построенному вычислениюполучим η1 η2 = θ1 θ2 ρ .G1 :?(C1 , . .

. , Ci , . . . , D2− , . . . , Cm )η1D1η ∈ НОУ(C η , D + )2i 119?G2 :?(C1 η1 , . . . , D1− , . . . , D2− η1 . . . , Cm η1 )η2Равенства θ1 θ2 = η1 η2 ρ , η1 η2 = θ1 θ2 ρ означают, чтоподстановки η1 η2 и θ1 θ2 , а также запросы G2 и G2 являютсявариантами друг друга.ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙТеорема сильной полнотыКаково бы ни было правило выбора подцелей R, если θ —правильный ответ на запрос G0 к хорновской логическойпрограмме P, то существует такой R-вычисленный ответ η,что равенствоθ = ηρвыполняется для некоторой подстановки ρ.ДоказательствоПо теореме полноты существут такой вычисленный ответ η ,что θ = η ρ .

Рассмотрим соответствующее этому ответууспешное вычисление запроса G, ),comp = (D1 , η1 , G1 ), . . . , (DN , ηN .в котором η = η1 . . . ηNПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательствоПредположим, что R(G0 ) = Ci . Поскольку comp — этоуспешное вычисление, существует ki , что подцель Ci впервыевыбирается на ki -ом шаге вычисления comp . Применяяпоследовательно ki раз переключательную лемму, можнополучить успешное вычисление, ),comp = (Dik , η1 , G1 ), (D1 , η2 , G1 ), .

. . , (DN , ηNв котором на первом шаге выбирается подцель Ci = R(G0 ), но — это вариантпри этом вычисленный результат η = η1 . . . ηNвычисленного ответа η = η1 . . . ηN , и значит θ = η ρ .Повторяя этот трюк 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(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)R(b) ←??θ4 = εP(X1 , X1 ) ← Q(X1 );η1 = {U/X1 , V /X1 }??Q(X1 ), R(X1 )Q(c) ←??R(c)failureη2 = {X1 /c}тупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММКак видно из этого примера, выбор программных утвержденийиграет значительную роль.Программное утверждение — это способ (рецепт) решениязадачи (подцели).