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

Значит, логическое программирование — этоуниверсальная модель вычислений, позволяющая вычислятьвсе эффективно вычислимые функции.Но это также означает, что логическому программированиюприсущи все те трудности анализа поведения программ,которые присущи и другим универсальным моделямвычислений. Речь идет об алгоритмически неразрешмыхзадачах.Например, интересен вопрос о том, можно ли по заданномузапросу G к логической программе P выяснить, имеет ли этотзапрос хотя бы одно успешное вычисление. Тогда не пришлосьбесполезно тратить время на построение дереваSLD-резолютивных вычислений.ТЕОРЕМА ЧЕРЧАТеорема Тьюринга об алгоритмическойнеразрешимости проблемы остановаПроблема останова машин Тьюринга алгоритмическинеразрешима, т.

е. не существует алгоритма (машиныТьюринга), способного вычислить следующую функцию⎧1, если x — это начальная ленточная конфигурация,⎪⎪⎨если y — это список команд МТ π,F (x, y ) =и вычисление π(x) конечно;⎪⎪⎩0 в противном случае.ДоказательствоИзвестно каждому первокурснику.ТЕОРЕМА ЧЕРЧАИз теоремы о моделировании машин Тьюринга логическимипрограммами и теоремы об алгоритмической неразрешимостипроблемы останова машин Тьюринга получаем нескольковажных следствийСледствие 1.Не существует алгоритма, способного определить по заданномузапросу G к хорновской логической программе P,является ли дерево SLD-резолютивных вычисленийзапроса G конечным;содержит ли дерево SLD-резолютивных вычисленийзапроса G хотя бы одно успешное вычисление;является ли заданная подстановка θ вычисленным ответомна запрос 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 )θ.ТЕОРЕМА ЧЕРЧАТеорема Черча об алгоритмической неразрешимости проблемыобщезначимости показывает, что ни одна системаавтоматического доказательства теорем не можетгарантировать решение следующих вопросов для произвольныхформул:является ли заданная формула ϕ общезначимой?является ли заданная формула ϕ выполнимой?является ли заданная формула ϕ логическим следствиемзаданного множества формул Γ?КОНЕЦ ЛЕКЦИИ 15.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 16.Управление вычислениямилогических программ.Оператор отсечения.УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИВопросы:А как организовано вычислениелогических программ накомпьютере?Как устроен интерпретаторлогических программ?УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПростейший способ организации работы логических программна основе стандартной стратегии обхода дереваSLD-резолютивных вычислений в глубину с возвратом — эторабота со стеком (или магазином ).В каждом элементе Sn стека содержится следующаяинформация:Текущее целевое утверждение (запрос) Gn ;Композиция всех ранее вычисленных унификаторовηn = (θ1 .

. . θn )|целев.перем ;Счетчик использованных программных утвержденийcountn ;Специальные пометки (о некоторых из них будетрассказано далее).УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИПример стекового вычисления логическихпрограммЗапрос: ?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)УПРАВЛЕНИЕ ВЫЧИСЛЕНИЯМИД.