Теормин 2014 (avasite), страница 4

(Доказывается индукцией по длине вычисления)

Теорема полноты.

Пусть

1. P = {D1, D2, …, DN} — хорновская логическая программа,

2. G0 =?C1, C2, …, Cm — запрос с множеством целевых переменных Y1, Y2, …, Yk,

3. θ — правильный ответ на запрос G0 к хорновской логической программе P.

Тогда существует такой вычисленный ответ η на запрос G0 к программе P, что θ = ηρ для некоторой подстановки ρ.

(Теорема полноты гласит, что каждый правильный ответ — это пример (частный случай) некоторого вычисленного ответа).

(Рассмотрим любой частный случай нашего правильного ответа (запомним эту подстановку), для него примерим лемму об основных вычислениях, которая даст нам успешное SLD-резолютивное вычисление из множества основных примеров программных утверждений, а потом воспользуемся леммой о подъёме для хорновских дизъюнктов, которая даст нам вычисленный ответ, для которого правильный ответ и запомненная подстановка являются лишь частным случаем, а уже отсюда выведем нужную нам подстановку, являющуюся некоторым вычисленным ответом, применив трюк с подменой всех констант вставленных в используемой подстановке на символы переменных вместо которых они подставлялись)

Лемма об основных вычислениях.

Пусть

1. P = {D1, D2, …, DN} — хорновская логическая программа,

2. G₀’ = ?C₁’, C₂’, …, C_n’ — основной запрос,

и при этом верно P |= G₀’.

Тогда существует успешное SLD-резолютивное вычисление запроса G₀’, обращенного к множеству [P] основных примеров программных утверждений программы P.

(Множество дизъюнктов из утверждений программы и дизъюнкта, порождённого основным запросом – противоречиво, а значит можно выделить конечное противоречивое множество, а значит по теореме полноты резолюций выводим пустой дизъюнкт. Дальше докажем, что этот вывод является SLD-выводом. Разобьём все дизъюнкты на смешанные и негативные, тогда есть резольвенты 2-х типов - которые попадают в первое множество, или во второе, всегда в выводе найдётся хотя бы одна sld-резольвента (ибо таков пустой дизъюнкт), а потом нужно просто применить трюк, перегруппировав все резольвенты и заменив их на sld ((1+2)+3) == ((1+3)+2) )

Лемма о подъеме (для логических программ)

Пусть G₀’ = G₀θ’ — основной пример запроса G₀ с множеством целевых переменных Y1, …, Ym, обращенный к хорновской логической программе P. Если запрос G₀’, обращенный к множеству основных примеров программных утверждений [P], имеет успешное вычисление, то исходный запрос G₀, обращенный к самой программе P, также имеет успешное вычисление с ответом η, который удовлетворяет равенству θ'=ηρ’ для некоторой подстановки ρ'.

(Доказательство на основе обычной леммы о подъёме, которую применяют много раз подряд)

Лекция 14. Правила выбора подцелей. Деревья вычислений логических программ. Стратегии вычисления логических программ.

Определение.

Отображение R, которое сопоставляет каждому непустому запросу G: ?C1, C2, …, Cm одну из подцелей Ci=R(G) в этом запросе, называется правилом выбора подцелей.

Для заданного правила выбора подцелей R вычисление запроса G к логической программе P называется R-вычислением, если на каждом шаге вычисления очередная подцель в запросе выбирается по правилу R.

Ответ, полученный в результате успешного R-вычисления, называется R-вычисленным.

Переключательная лемма

Предположим, что запрос G₀ : ?C1, …, Ci, …, Cj, …, Cm к хорновской логической программе P имеет вычисление G0 : ?C1, …, Ci, …, Cj, …, Cm

{ D1: θ1 ∈ НОУ(Ci, D⁺₁) }

G₁’ : ?(C1, …, D⁻₁, … Cj, …, Cm)θ1

{ D2: θ2 ∈ НОУ(Cjθ1, D+2) }

G₂’ : ?(C1θ1, …, D−1θ1, . . . , D−2, . . . , Cmθ1)θ2

Тогда запрос G0 к программе P также имеет вычисление

(тут вычисление, как и выше, но в другом порядке)

и при этом запросы G₂' и G₂’’ являются вариантами друг друга, т. е. θ1θ2ρ’ = η1η2 и η1η2ρ''= θ1θ2 для некоторых ρ', ρ'' ∈ Subst.

(лемма говорит, что при изменении порядка выбора подцелей результат вычисления сохраняется (с точностью до переименования переменных))

(Доказательство в лоб – рассмотрением порядка одного и второго)

Теорема сильной полноты

Каково бы ни было правило выбора подцелей R, если θ — правильный ответ на запрос G₀ к хорновской логической программе P, то существует такой R-вычисленный ответ η, что равенство θ = ηρ выполняется для некоторой подстановки ρ.

(По теореме полноты – существует соответствующий вычисленный ответ, дальше итерационно – на первом шаге мы R-правило дало нам некоторую подцель, мы находим её в нашем вычислении и основываясь на переключательной теореме сдвигаем нужное вычисление вперёд. Остаётся проделать этот трюк лишь нужное число раз)

Деревом SLD-резолютивных вычислений запроса G0 к логической программе P называется помеченное корневое дерево T_G0,P, удовлетворяющее следующим требованиям:

1. Корнем дерева является исходный запрос G0

2. Потомками каждой вершины G являются всевозможные SLD-резольвенты запроса G (при фиксированном стандартном правиле выбора подцелей)

3. Листовыми вершинами являются пустые запросы (завершающие успешные вычисления) и запросы, не имеющие SLD-резольвент (завершающие тупиковые вычисления).

Стратегией вычисления запросов к логическим программам называется алгоритм построения (обхода) дерева SLD-резолютивных вычислений T_G0,P всякого запроса G0 к произвольной логической программе P.

Стратегия вычислений называется вычислительно полной, если для любого запроса G0 и любой логической программы P эта стратегия строит (обнаруживает) все успешные вычисления запроса G0 к программе P.

(Фактически, стратегия вычисления — это одна стратегий обхода корневого дерева. Как известно, таких стратегий существует много, но среди них выделяются две наиболее характерные: стратегия обхода в ширину и стратегия обхода в глубину с возвратом)

Стратегия обхода в ширину является вычислительно полной.

Стратегия обхода в глубину является вычислительно не полной.

Поскольку соображения эффективности превалируют над требованиями вычислительной полноты, в качестве стандартной стратегии вычисления логических программ была выбрана стратегия обхода в глубину с возвратом. (Программист должен сам позаботиться о надлежащем порядке расположения программных утверждений, чтобы стандартная стратегия вычисления позволяла отыскать все вычисленные ответы.)

Лекция 15. Алгоритмическая полнота логических программ. Моделирование машин Тьюринга логическими программами. Теорема Черча.

Тезис Черча

Класс эффективно (алгоритмически) вычислимых арифметических функций в точности совпадает с классом арифметических функций, вычислимых в каждой из перечисленных ниже моделей вычислений

1. машины Тьюринга—Поста,

2. λ-исчисление Черча—Клини,

3. системы равенств Эрбрана—Геделя,

4. алгорифмы Маркова,

5. системы Колмогорова—Шенхаге,

6. машины Минского,

7. ...

Модели вычислений такого вида называются алгоритмически полными.

Машина Тьюринга

Задан ленточный алфавит A = {a₀, a₁, a₂, …, a_n}, в котором особо выделена одна из букв a0 (пустой символ).

Ленточным словом называется всякое слово в алфавите A. Множество всех ленточных слов обозначим A*.

Для каждого слова w = z₁z₂ … z_n−1z_n будем использовать запись w⁻¹ для обозначения обратного слова z_nz_n−1…z₂z₁. Задан алфавит состояний Q = {q₀, q₁, q₂, …, q_m}, в котором особо выделено одно из состояний q₀ (начальное состояние).

Ленточной конфигурацией называется всякое слово вида w'q x w’’, где

1. q — состояние, q ∈ Q,

2. x — ленточная буква, x ∈ A,

3. w', w’’ — ленточные слова, w’, w’’ ∈ A*.

4. q — это то состояние, в котором находится МТ,

5. x — это буква, которая записана в той ячейке ленты, которую обозревает считывающая головка МТ,

6. w’ — это ленточное слово, составленное из символов, записанных слева от обозреваемой ячейки,

7. w’’ — это ленточное слово, составленное из символов, записанных справа от обозреваемой ячейки.

По умолчанию считается, что во всех остальных ячейках ленты записаны пустые символы.

Ленточная конфигурация вида uq₀xv называется начальной конфигурацией.

Множество всех конфигураций обозначим Conf_A,Q.

Множество всех начальных конфигураций обозначим Conf⁰_A,Q.

Командой называется всякая пятерка вида q x y q’ D, где

1. q, q’ — состояния, q, q’ ∈ Q,

2. x , y — ленточные буквы, x , y ∈ A,

3. D — направление сдвига головки, D ∈ {L, R}.

Эту команду нужно понимать так: если МТ находится в состоянии q и обозревает символ x, то записать в обозреваемую ячейку символ y, перейти в состояние q’ и сдвинуть считывающую головку на одну ячейку в направлении D.

Каждая команда K задает отношение перехода →_K на множестве ленточных конфигураций α →_K β

Оно определяется так:

1. если α = uzqxv и K = qxyq’L, то β = uq'zyv ,

2. если α = qxv и K = qxyq’L, то β = q’a₀yv ,

3. если α = uqxzv и K = qxyq’R , то β = uyq’zv ,

4. если α = uqx и K = qxyq’R , то β = uyq’a₀.

Программа машины Тьюринга — это произвольное множество команд π = {K₁, K₂, …, K_N}. Программа π называется детерминированной, если для любых двух команд этой программы

K_i = q_i xyq_i’D_i , K_j = q_j ztq_j’D_j, выполняется хотя бы одно из двух условий q_i ≠ q_j, x ≠ z.

Программа π задает отношение переходов на множестве ленточных конфигураций →_π = . Конфигурация α называется заключительной для программы π, если не существует никакой конфигурации β, для которых выполняется α →_π β. Это означает, что α = uqxv, и в программе π нет ни одной команды K = qx…

Вычислением машины Тьюринга с программой π на начальной конфигурации α₀, α₀ ∈ Conf⁰ называется последовательность конфигураций π(α₀) = α₀, α₁, α₂, …, α_i, α_i+1, … удовлетворяющая следующим условиям:

1. для любого i, i ≥ 0, верно αi →_π α_i+1;

2. последовательность π(α₀) либо является бесконечной, либо заканчивается заключительной конфигурацией α_N.

В последнем случае α_N называется результатом вычисления. Результат бесконечного вычисления считается неопределенным. Ясно, что вычисление π(α₀) детерминированной машины Тьюринга однозначно определяется начальной конфигурацией α₀ и программой π.

Лемма 1

Для любой пары ленточных конфигураций α, β ∈ Conf и команды K отношение перехода α →_K β выполняется тогда и только тогда, когда запрос Gα: ?P (left (α), right (α), X, Y) и одно из программных утверждений D1 (K), D2 (K) имеют SLD-резольвенту Gβ: ?P (left (β), right (β), X, Y).

(типо очевидно – если есть резольвента – т.е. есть соответствующий НОУ, который описывает лево и право и дальше по построению следует, что выполняется отношение перехода в машине Тьюринга, и наоборот – если выполняется отношение перехода, то мы можем выписать НОУ совершить SLD-резолютивный переход)

Лемма 2

Ленточная конфигурация α ∈ Conf является заключительной для машины Тьюринга π тогда и только тогда, когда запрос Gα: ?P (left (α), right (α), X, Y) и одно из программных утверждений множества имеют пустой дизъюнкт □ в качестве SLD-резольвенты.

(типо так же очевидно как и в предыдущей лемме)

Теорема (о моделировании МТ логическими программами)

Каковы бы ни были машина Тьюринга π и начальная конфигурация α₀, вычисление α₀ →_π α₁ →_π α₂ →_π … →_π α_N завершается заключительной конфигурацией α_N тогда и только тогда, когда запрос Gα₀: ?R (left (α0), right (α0), X, Y) к хорновской логической программе Pπ имеет успешное вычисление с вычисленным ответом θ = {X/left (α_N), Y/right (α_N)}.