Лекции В.А. Захарова (1157993), страница 23
Текст из файла (страница 23)
. , 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тупиковое вычислениеДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММКак видно из этого примера, выбор программных утвержденийиграет значительную роль.Программное утверждение — это способ (рецепт) решениязадачи (подцели).
Ясно, что некоторые способы решения могутбыть «хорошими», а некоторые — «плохими».Таким образом, чтобы вычислить все ответы на запрос (или,что то же само, гарантировать вычисление хотя бы одногоответа), нужно уметь просматривать все варианты выборапрограммных утверждений. И нужно правильно организоватьэтот перебор.ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММОпределениеДеревом SLD-резолютивных вычислений запроса G0 клогической программе P называется помеченное корневоедерево TG0 ,P , удовлетворяющее следующим требованиям:1. Корнем дерева является исходный запрос G0 ;2. Потомками каждой вершины G являются всевозможныеSLD-резольвенты запроса G (при фиксированномстандартном правиле выбора подцелей);3. Листовыми вершинами являются пустые запросы(завершающие успешные вычисления) и запросы, неимеющие SLD-резольвент (завершающие тупиковыевычисления).ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММИллюстрация?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) ←;(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.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}????ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММИтак, деревья вычислений логических программ бываютразные — конечные и бесконечные, с конечным илибесконечным множеством ветвей, и т.
п.Каждая ветвь дерева TG0 ,P соответствует одному извозможных вычислений запроса G0 к логической программе P.Некоторые из ветвей образуют успешное вычисление и даютответ на запрос.Возникает вопрос:Как нам обнаружить ветви успешных вычислений в деревеSLD-резолютивных вычислений программы?СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММОпределениеСтратегией вычисления запросов к логическим программамназывается алгоритм построения (обхода) дереваSLD-резолютивных вычислений TG0 ,P всякого запроса G0 кпроизвольной логической программе PСтратегия вычислений называется вычислительно полной ,если для любого запроса G0 и любой логической программы Pэта стратегия строит (обнаруживает) все успешныевычисления запроса G0 к программы PСТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММФактически, стратегия вычисления — это одна стратегийобхода корневого дерева.
Как известно, таких стратегийсуществует много, но среди них выделяются две наиболеехарактерные:Iстратегия обхода в ширину , при которой деревостроится (обходится) поярусно — вершина i-го нестроится, до тех пор пока не будут построены все вершины(i − 1)-го яруса;Iстратегия обхода в глубину с возвратом , при которойветви дерева обходятся поочередно — очередная ветвьдерева не обохдится, до тех пор пока не будут пройденывсе вершины текущей ветви.СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в ширину.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в ширину.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;?P(U,V ), R(U)tСТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в ширину.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СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в ширину.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 )@СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в ширину.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 )@СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в ширину.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)СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в ширину.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)СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в ширину.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СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в ширину.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?СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММСтратегия обхода в ширину является вычислительно полной,посколькуI каждый запрос имеет конечное число SLD-резольвент, ипоэтому в каждом ярусе дерева SLD-резолютивныхвычислений имеется конечное число вершин;I каждое успешное вычисление завершается на некоторомярусе;I и поэтому каждое успешное вычисление будет рано илипоздно полностью построено.Но строить интерпретатор логических программ на основестратегии обхода в ширину нецелесообразно.
При обходедерева в ширину нужно обязательно хранить в памяти всевершины очередного яруса. Это требует большого расходапамяти. Например, в 100-м ярусе двоичного дерева содержится299 вершин. Вычислительных ресурсов всего земного шара нехватит, чтобы хранить информацию обо всех этих вершинах.СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММСтратегия обхода в глубину с возвратом основана наследующих принципах:1. все программные утверждения упорядочиваются;2. на каждом шаге обхода из текущей вершины Gосуществляется переходIIлибо в новую вершину-потомок G 0 , которая являетсяSLD-резольвентой запроса G и первого по порядкупрограммного утверждения D, ранее не использованногодля этой цели;либо в ранее построенную родительскую вершину G 00(откат), если все программные утверждения уже былиопробованы для построения SLD-резольвент запроса G .СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;?P(U,V ), R(U)tСТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.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СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.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СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.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СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.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(3), ε?t??P(U,V ), R(U)tСТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.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) ?t6(3), ε?t??P(U,V ), R(U)tСТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.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}6?R(b) ?t6(3), ε?t??P(U,V ), R(U)tСТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.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)t6?Q(Y1 ), R(b) ?t(4), {Y1 /c}6?R(b) ?t6(3), ε?t?СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.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)t6?Q(Y1 ), R(b) ?t(4), {Y1 /c}6?R(b) ?t6(3), ε?t?СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.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}6?Q(Y1 ), R(b) ?t(4), {Y1 /c}6?R(b) ?t(3), ε6?t??P(U,V ), R(U)t@ (2), {U/X1 , V /X1 } @R t?Q(X1 ), R(X1 )@СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );?P(U,V ), R(U)tR(b) ←;@(1), {U/X1 , V /Y1 } @(2), {U/X1 , V /X1 }Q(c) ←;@ t?Q(X1 ), R(X1 )R?R(X1 ), Q(Y1 ), R(X1 ) t(3), {X1 /b}6?Q(Y1 ), R(b) ?t(4), {Y1 /c}6?R(b) ?t(3), ε6?t?(2), {X1 /c}?t?R(c)СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );?P(U,V ), R(U)tR(b) ←;@(1), {U/X1 , V /Y1 } @(2), {U/X1 , V /X1 }Q(c) ←;@ t?Q(X1 ), R(X1 )R?R(X1 ), Q(Y1 ), R(X1 ) t(3), {X1 /b}6?Q(Y1 ), R(b) ?t(4), {Y1 /c}6?R(b) ?t6(3), ε?t?6(2), {X1 /c}?t?R(c)failureСТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММПример обхода в глубину с возвратом.P : P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );?P(U,V ), R(U)tR(b) ←;@(1), {U/X1 , V /Y1 }(2), {U/X1 , V /X1 }@I@@Q(c) ←;R t?Q(X1 ), R(X1 )?R(X1 ), Q(Y1 ), R(X1 ) t@@(3), {X1 /b}6?Q(Y1 ), R(b) ?t(4), {Y1 /c}6?R(b) ?t6(3), ε?t?6(2), {X1 /c}?t?R(c)failureСТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММСтратегия обхода в глубину с возвратомIимеет эффективную реализацию: в памяти нужно хранитьлишь запросы той ветви, по которой идет обход, и каждыйзапрос должен вести учет использованных программныхутверждений;Iявляется, к сожалению, вычислительно неполной.ДЕРЕВЬЯ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММ.Обратимся к примеру 2.t?P(X Y ).P : P(X L) ← P(L), R(X );P(nil) ←;R(a) ←;R(c) ←;(1), {X1 /X , L1 /Y }(1), {Y /X2(1), {L2 /X3(1), {L3 /X4(1), {L4 /X5....?t?P(Y ), R(X )L2 }t?P(L2 ), R(X2 ), R(X )L3 }t?P(L3 ), R(X3 ), R(X2 ), R(X )L4 }t?P(L4 ), R(X4 ), R(X3 ), R(X2 ), R(X )L5 }∞ Обход дерева TG ,P уходит в глубинупо бесконечной ветви и не может возвратиться,чтобы обнаружить успешное вычисление.СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММСтратегия обхода в глубину с возвратом чувствительна кпорядку расположения программных утверждений в логическихпрограммах.