Сводка определений и основных фактов, страница 5

выполняется равенство

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

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

Определение. Ленточный алфавит

- это множество допустимых значений ячеек памяти (символ называется пустым). Слово в алфавите А называется ленточным словом.

Определение. Алфавит состояний - это множество состояний, причем состояние называется заключительным, а состояние - начальным.

О

п

р

е

д

е

л

е

н

и

е

.

Л

е

н

т

о

ч

н

а

я

к

о

н

ф

и

г

у

р

а

ц

и

я

–

э

т

о

т

р

о

й

к

а

, где - ленточное слово, которое является содержимым ленты слева от обозреваемой ячейки, - текущее состояние машины Тьюринга, - слово, состоящее из самой ячейки и содержимого ленты справа от нее.

Определение. Команда машины Тьюринга – это пятерка

, где q и q' – состояния, a, b – символы из алфавита А,

.

Определение. Машиной Тьюринга называется тройка

, где А – ленточный алфавит, Q_T – конечное подмножество множества состояний, П_Т – множество команд. Важное ограничение: для любого состояния, отличного от заключительного, и символа из ленточного алфавита существует единственная команда.

Определение. Отношением непосредственного перехода называется отношение

, где

- состояния машины Тьюринга. Обозначим

транзитивное замыкание отношения непосредственного перехода.

Для каждой машины Тьюринга определим функцию , причем если

- начальная конфигурация, то

тогда и только тогда, когда

- заключительная конфигурация, и

.

Тезис Чёрча: Для любой функции

существует алгоритм вычисления этой функции тогда и только тогда, когда

для некоторой машины Тьюринга.

Введем дополнительные обозначения: nil – 0-местный функциональный символ (константа), • - 2-местный функциональный символ, и введем отображение множества машин Тьюринга на множество логических программ:

Теорема. Пусто Т – машина Тьюринга,

- логическая программа. Тогда для любой начальной конфигурации

существует заключительная конфигурация

, такая, что

, тогда и только тогда, когда запрос имеет успешное SLD-резолютивное вычисление с ответом

.

Теорема (Чёрча; о неразрешимости проблемы общезначимости для классической логики предикатов): Не существует алгоритма, который для любой формулы

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

общезначима, и 0 в противном случае.

Определение. Правилом выбора подцелей называется отображение

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

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

О

п

р

е

д

е

л

е

н

и

е

.

В

ы

ч

и

с

л

е

н

н

ы

й

о

т

в

е

т

,

п

о

л

у

ч

е

н

н

ы

й

в

р

е

з

у

л

ь

т

а

т

е

R-

в

ы

ч

и

с

л

е

н

и

я

н

а

з

ы

в

а

е

т

с

я

R-

в

ы

ч

и

с

л

е

н

н

ы

м

о

т

в

е

т

о

м

.

Лемма (переключательная): Пусть Р – хорновская логическая программа, - запрос к ней, пусть также имеется SLD-резолютивное вычисление

, причем и - этапы SLD-резолютивного вычисления, на которых i-ая подцель была раскрыта по правилу и соответственно. Тогда существует SLD-резолютивное вычисление

, такое, что на этапе раскрытие происходило по правилу , а на этапе - по правилу , при этом для вычисленных ответов

и

существуют конечные подстановки

и

, такие, что

,

.

Теорема: Пусть Р – хорновская логическая программа, G – запрос к ней, R и R' – различные правила выбора. Тогда если

- R-вычислимый ответ на G к Р, то существует такой R'-вычислимый ответ

, такой, что

и

для некоторых конечных перестановок (переименований)

и

.

Теорема (сильной полноты): Пусть G – запрос к хорновской логической программе Р, R – правило выбора,

- правильный ответ на G к Р. Тогда существует R-вычислимый ответ

, такой, что

, где

- конечная подстановка (переименование).

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

1) каждой вершине приписан запрос;

2) корню дерева приписан запрос G;

3) из каждой вершины, помеченной запросом , исходят дуги, помеченные натуральными числами , где N – количество программных утверждений в Р, и идущие в вершины, помеченные в том и только в том случае, когда запрос получен из запроса G путем применения программного утверждения и при этом других SLD-резольвент, инцидентных , нет.

Таким образом, каждая ветвь такого дерева будет соответствовать вычислению ответа на запрос G к логической программе Р.

Определение. Стратегией вычисления называется стратегия обхода дерева SLD-резолютивных вычислений:

• стратегия обхода в ширину: поярусное построение дерева. Как только в одной из ветвей обнаруживается , то ответ вычисляется путем «сбора» всех подстановок на данной ветви;

• стратегия обхода в глубину с возвратом – построение дерева по ветвям (на каждом этапе выбирается самая левая из непройденных ветвей)

Определение. Стратегия вычисления (обхода дерева SLD-резолютивных вычислений) называется полной, если для любого запроса G к логической программе Р все вычисленные ответы будут построены.

Т

е

о

р

е

м

а

.

С

т

р

а

т

е

г

и

я

о

б

х

о

д

а

в

ш

и

р

и

н

у

–

п

о

л

н

а

я

,

с

т

р

а

т

е

г

и

я

о

б

х

о

д

а

в

г

л

у

б

и

н

у

с

в

о

з

в

р

а

т

о

м

–

н

е

п

о

л

н

а

я

.

Определение. Оператор отсечения (саt) – это 0-местный предикат со следующей операционной семантикой:

Пусть в логической программе Р имеется программной утверждение

, G - запрос к этой программе. Строим дерево SLD-резолютивных вычислений.

- это парная метка, которая означает, омента ее появления интересует только одна альтернатива. Соответственно, после второго появления * ветвление снова разрешается.

Откат при этом производится в вершину, предшествующую первому появлению *.

Теорема полноты для SLD-резолютивного вычисления с операцией отсечения не выполняется.

Определение. Оператор отрицания (not) – это оператор логического программирования со следующей операционной семантикой:

Пусть Р – логическая программа, а G – запрос вида not(A). Тогда реакция интерпретатора на данный запрос будет следующей:

1) если существует успешное SLD-резолютивное вычисление на запрос , то результатом вычисления будет fail;

2) если SLD-резолютивное дерево вычислений для запроса представляет собой конечное число неудачных ветвей, то запрос G имеет успешное вычисление;

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

∞.

Таким образом, оператор not работает на основе «почти трехзначной» логики, что дает эффект немонотонности вывода.

4. Обзор разделов математической логики

4.1. Исчисление предикатов и элементарная теория

Исчисление предикатов состоит из системы аксиом и правил вывода. Существует много разных систем аксиом.

Система аксиом:

- закон сложного силлогизма

- свойства конъюнкции

- свойства дизъюнкции

- законы противоречия

- закон исключенного третьего

, где х свободна для t в

.

Правила вывода:

1.

- правило отделения (modus ponens); следствие импликации отделяется от посылки.

2.

- правило обобщения.

Определение. Логическим выводом в исчислении предикатов из множества формул Г называется конечная последовательность формул

, такая, что для любого

- либо

;

- либо

- одна из 15 аксиом;

- либо

получается из предшествующих формул по правилу отделения или обобщения.

Логический вывод – формализация понятия математического доказательства.

Последняя формула

из последовательности логического вывода называется выводимой из Г и обозначается как