Лекции В.А. Захарова (1157993), страница 25
Текст из файла (страница 25)
. zn будет представлено спискомlist(w ) = z1 z2 . . . zn nil... ..Каждая ленточная конфигурация α = u q z v будетпредставлена парой списков left(α), right(α), гдеleft(α) = list(u −1 ),right(α) = q z list(v )...Например,left(0111q1 1011110) = 1 1 1 0 nil,right(0111q1 1011110) = q1 1 0 1 1 1 1 0 nil.............МОДЕЛИРОВАНИЕ МАШИН ТЬЮРИНГАЛОГИЧЕСКИМИ ПРОГРАММАМИКаждой команде K = q b c q 0 L сопоставим пару программныхутверждений D1 (K ), D2 (K ):. ..... ...
..D1 (K ) : P(Z X , q b Y , X 0 , Y 0 ) ← P(X , q 0 Z c Y , X 0 , Y 0 );D1 (K ) : P(nil, q b Y , X 0 , Y 0 )← P(nil, q 0 a0 c Y , X 0 , Y 0 );Каждой команде K = q b c q 0 R сопоставим пару программныхутверждений D1 (K ), D2 (K ):..
.... ... . .D1 (K ) : P(X , q b Z Y , X 0 , Y 0 ) ← P(c X , q 0 Z Y , X 0 , Y 0 );D1 (K ) : P(X , q b nil, X 0 , Y 0 )← P(c X , q 0 a0 nil, X 0 , Y 0 );МОДЕЛИРОВАНИЕ МАШИН ТЬЮРИНГАЛОГИЧЕСКИМИ ПРОГРАММАМИКроме того, для каждой пары q, z, где q ∈ Q, z ∈ A, введемфакт Dq,z :....Dq,z : P(X , q z Y , X , q z Y ) ←;Теперь для каждой машины Тьюринга π = {K1 , K2 , .
. . , KN }выделим множество Tπ всех пар qx, которые не являютсяначалами ни одной из команд программы π...и построим хорновскую логическую программу[Pπ = {D1 (K ), D2 (K ) : K ∈ π} ∪Dqx .(qx∈Tπ )Можно надеяться, что логическая программа Pπвоспроизводит все вычисления машины Тьюринга π.МОДЕЛИРОВАНИЕ МАШИН ТЬЮРИНГАЛОГИЧЕСКИМИ ПРОГРАММАМИПримерПустьK1 =K2 =K3 =A = {0, 1} и пусть π = {K1 , K2 , K3 }, гдеq0 0 1 q1 R,q1 0 1 q0 L,q1 1 1 q1 R.Машина Тьюринга c программой π транслируется влогическую программу Pπ .МОДЕЛИРОВАНИЕ МАШИН ТЬЮРИНГАЛОГИЧЕСКИМИ ПРОГРАММАМИПримерЛогическая программа Pπ :.. ...P(Z .X , q .0.Y , X , Y )P(nil, q .0.Y , X , Y )P(X , q .1.Z .Y , X , Y )P(X , q .1.nil, X , Y )P(X , q .1.Z , X , q .1.Z )P(X , q0 0 Z Y , X 0 , Y 0 )P(X , q0 0 nil, X 0 , Y 0 )01100110000000.
... ..P(X , q .Z .1.Y , X , Y );P(nil, q .0.1.Y , X , Y );P(1.X , q .Z .Y , X , Y );P(1.X , q .0.nil, X , Y );← P(1 X , q1 Z Y , X 0 , Y 0 );← P(1 X , q1 0 nil, X 0 , Y 0 );←←←←← ;001100000000МОДЕЛИРОВАНИЕ МАШИН ТЬЮРИНГАЛОГИЧЕСКИМИ ПРОГРАММАМИЛемма 1Для любой пары ленточных конфигураций α, β ∈ Conf икоманды K отношение перехода α →K β выполняется тогда итолько тогда, когда запросGα : ?P(left(α), right(α), X , Y )и одно из программных утверждений D1 (K ), D2 (K )имеют SLD-резольвенту Gβ :?P(left(β), right(β), X , Y ).ДоказательствоСамостоятельно.МОДЕЛИРОВАНИЕ МАШИН ТЬЮРИНГАЛОГИЧЕСКИМИ ПРОГРАММАМИЛемма 2Ленточная конфигурация α ∈ Conf является заключительнойдля машины Тьюринга π тогда и только тогда, когда запросGα : ?P(left(α), right(α), X , Y )Sи одно из программных утверждений множестваDqx(qx∈Tπ )имеют пустой дизъюнкт в качестве SLD-резольвенты.ДоказательствоСамостоятельно.МОДЕЛИРОВАНИЕ МАШИН ТЬЮРИНГАЛОГИЧЕСКИМИ ПРОГРАММАМИТеорема (о моделировании МТ логическимипрограммами)Каковы бы ни были машина Тьюринга π и начальнаяконфигурация α0 , вычислениеα0 →π α1 →π α2 →π · · · →π αNзавершается заключительной конфигурацией αN тогда итолько тогда, когда запросGα0 : ?R(left(α0 ), right(α0 ), X , Y )к хорновской логической программе Pπ имеет успешноевычисление с вычисленным ответомθ = {X /left(αN ), Y /right(αN )}.ДоказательствоСледует из лемм 1 и 2.МОДЕЛИРОВАНИЕ МАШИН ТЬЮРИНГАЛОГИЧЕСКИМИ ПРОГРАММАМИТаким образом, хорновские логические программы обладаютне меньшими вычислительными воможностями, чем машиныТьюринга.
Значит, логическое программирование — этоуниверсальная модель вычислений, позволяющая вычислятьвсе эффективно вычислимые функции.Но это также означает, что логическому программированиюприсущи все те трудности анализа поведения программ,которые присущи и другим универсальным моделямвычислений. Речь идет об алгоритмически неразрешмыхзадачах.Например, интересен вопрос о том, можно ли по заданномузапросу G к логической программе P выяснить, имеет ли этотзапрос хотя бы одно успешное вычисление.
Тогда не пришлосьбесполезно тратить время на построение дереваSLD-резолютивных вычислений.ТЕОРЕМА ЧЕРЧАТеорема Тьюринга об алгоритмическойнеразрешимости проблемы остановаПроблема останова машин Тьюринга алгоритмическинеразрешима, т. е. не существует алгоритма (машиныТьюринга), способного вычислить следующую функцию1, если x — это начальная ленточная конфигурация,если y — это список команд МТ π,F (x, y ) =и вычисление π(x) конечно;0 в противном случае.ДоказательствоИзвестно каждому первокурснику.ТЕОРЕМА ЧЕРЧАИз теоремы о моделировании машин Тьюринга логическимипрограммами и теоремы об алгоритмической неразрешимостипроблемы останова машин Тьюринга получаем нескольковажных следствийСледствие 1.Не существует алгоритма, способного определить по заданномузапросу G к хорновской логической программе P,Iявляется ли дерево SLD-резолютивных вычисленийзапроса G конечным;Iсодержит ли дерево SLD-резолютивных вычисленийзапроса G хотя бы одно успешное вычисление;Iявляется ли заданная подстановка θ вычисленным ответомна запрос G .ТЕОРЕМА ЧЕРЧАСледствие 2 (Теорема Черча).Не существует алгоритма, способного определить позаданной замкнутой формуле логики предикатов ϕ,является ли эта формула общезначимой, т.
е. проблемаобщезначимости "|= ϕ ?"алгоритмически неразрешима.ДоказательствоПусть G : ?C1 , . . . , Cm произвольный запрос к произвольнойлогической программе P = {D1 , . . . , DN }.Тогда...ТЕОРЕМА ЧЕРЧАДоказательствоЗапрос G к программе P имеет хотя бы одно успешноеSLD-резолютивное вычисление⇐⇒(теоремы корректности и полноты)Запрос G к программе P имеет хоть один правильный ответ θ⇐⇒(определение правильного ответа){D1 , . . .
, DN } |= ∀z1 . . . ∀zk (C1 & . . . &Cm )θ⇐⇒(теорема о логическом следовании)|= D1 & . . . &DN }∀z1 . . . ∀zk (C1 & . . . &Cm )θ.ТЕОРЕМА ЧЕРЧАТеорема Черча об алгоритмической неразрешимости проблемыобщезначимости показывает, что ни одна системаавтоматического доказательства теорем не можетгарантировать решение следующих вопросов для произвольныхформул:Iявляется ли заданная формула ϕ общезначимой?Iявляется ли заданная формула ϕ выполнимой?Iявляется ли заданная формула ϕ логическим следствиемзаданного множества формул Γ?КОНЕЦ ЛЕКЦИИ 15.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 16.Управление вычислениямилогических программ.Оператор отсечения.УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИВопросы:А как организовано вычислениелогических программ накомпьютере?Как устроен интерпретаторлогических программ?УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПростейший способ организации работы логических программна основе стандартной стратегии обхода дереваSLD-резолютивных вычислений в глубину с возвратом — эторабота со стеком (или магазином ).В каждом элементе Sn стека содержится следующаяинформация:IТекущее целевое утверждение (запрос) Gn ;IКомпозиция всех ранее вычисленных унификаторовηn = (θ1 .
. . θn )|целев.перем ;IСчетчик использованных программных утвержденийcountn ;IСпециальные пометки (о некоторых из них будетрассказано далее).УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?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:η = ε;P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;Протокол:Унификация(1)(2)(3)(4)count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?P(U, V ), R(U)Программа P:η = ε;P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;Протокол:SLD-резолюцияНОУ = {X1 /U, Y1 /V }(1)(2)(3)(4)count = 1?R(U), Q(V ), R(U)η = ε;count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:SLD-резолюцияНОУ = {U/b}count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:Нет унификатораcount = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:Нет унификатораcount = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:Нет унификатораcount = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:Унификацияcount = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)SLD-резолюцияη = {U/b, V /c}; count = 1НОУ = {V /c}УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Нет унификатораη = {U/b, V /c}; count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Нет унификатораη = {U/b, V /c}; count = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Унификацияη = {U/b, V /c}; count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)SLD-резолюцияη = {U/b, V /c}; count = 3НОУ = εη = {U/b, V /c}УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Успех: η = {U/b, V /c}η = {U/b, V /c}; count = 3η = {U/b, V /c}УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Откатη = {U/b, V /c}; count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};count = 4Протокол:?R(b)Нет унификатораη = {U/b, V /c}; count = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3?Q(V ), R(b)η = {U/b};Протокол:Откатcount = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1?R(U), Q(V ), R(U)η = ε;count = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?P(U, V ), R(U)Программа P:η = ε;P(X , Y ) ← R(X ), Q(Y );P(X , X ) ← Q(X );R(b) ←;Q(c) ←;Протокол:SLD-резолюцияНОУ = {U/X1 , V /X1 }(1)(2)(3)(4)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 1УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4?R(c)η = {U/c, V /c}; count = 1Протокол:SLD-резолюцияНОУ = {X1 /c}УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4?R(c)η = {U/c, V /c}; count = 1Протокол:Нет унификатораУПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4?R(c)η = {U/c, V /c}; count = 2Протокол:Нет унификатораУПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4?R(c)η = {U/c, V /c}; count = 3Протокол:Нет унификатораУПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4?R(c)η = {U/c, V /c}; count = 4Протокол:Нет унификатораУПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2?Q(X1 ), R(X1 )η = {U/X1 ,V /X1 };count = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 2УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 3УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?P(U, V ), R(U)?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)count = 4УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?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)УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИД.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
