Лекции 12-23. Математическая логика (после колка) (1161871), страница 6

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 6)

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

. , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙПереключательная лемма.Тогда запрос G0 к программе P также имеет вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD2η1 ∈ НОУ(Cj , D2+ )9?G100 :?(C1 , . . . , Ci , . . . , D2− , . . . , Cm )η1D1 η2 ∈ НОУ(Ci η1 , D1+ )9?G200 :?(C1 η1 , . . . , D1− , . . . , D2− η1 . . . , Cm η1 )η2и при этом запросы G20 и G200 являются вариантами друг друга,т. е. θ1 θ2 ρ0 = η1 η2 и η1 η2 ρ00 = θ1 θ2 для некоторых ρ0 , ρ00 ∈ Subst.ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙПереключательная лемма говорит о том, что при изменениипорядка выбора подцелей результат вычисления сохраняется (сточностью до переименования переменных).ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , .

. . , Ci , . . . , Cj , . . . , CmD1 θ ∈ НОУ(C , D + )19?i1G10 :?(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?iСогласно определениюSLD-резолютивного вычисленияDomθ1 ∩ VarD2 = ∅.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Согласно определениюSLD-резолютивного вычисленияDomθ1 ∩ VarD2 = ∅.Поэтому D2+ θ2 = D2+ θ1 θ2 .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 , . . . , CmD1 θ ∈ НОУ(C , D + )9?1i1Согласно определениюSLD-резолютивного вычисленияDomθ1 ∩ VarD2 = ∅.Поэтому D2+ θ2 = D2+ θ1 θ2 .G10 :?(C1 , . . . , D1− , . . . , Cj , . . . , Cm )θ1D29?θ ∈ НОУ(C θ2+j 1 , D2 )Следовательно,Cj θ1 θ2 = D2+ θ2 = D2+ θ1 θ2 ,т. е.

Cj и D2+ унифицируемы.G20 :?(C1 θ1 , . . . , D1− θ1 , . . . , D2− , . . . , Cm θ1 )θ2ПРАВИЛА ВЫБОРА ПОДЦЕЛЕЙДоказательство (переключательной леммы).Рассмотрим первое вычислениеG0 :?C1 , . . . , Ci , . . . , Cj , . . . , CmD1 θ ∈ НОУ(C , D + )19?iА раз Cj и D2+ унифицируемы,существует η1 ∈ НОУ(Cj , D2+ ),и при этом θ1 θ2 = η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 + )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(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тупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММКак видно из этого примера, выбор программных утвержденийиграет значительную роль.Программное утверждение — это способ (рецепт) решениязадачи (подцели).

Характеристики

Список файлов лекций