План лекций (очень подробный), страница 8

множество ответов.

Стандартная стратегия обхода (или построения) sld-дерева: подхо-

дящие С1,...,Сl упорядочиваются (слева направо) в соответствии с их

порядком (сверху вниз) в программе; обход дерева осуществляется

"вглубь" (спуск по крайней левой еще не пройденной ветви до конца, за-

тем возврат на ближайшую снизу развилку, и т.д.).

Замечания. 1) Стандартная стратегия корректна, но не полна: попав

на бесконечную ветвь, никогда не дойдем до более правых ветвей. Поэто-

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

ности, и при этом могут перечисляться как все, так и не все ответы. 2)

Пусть q±,...,bn - текущий запрос. Тогда каждый атом Вi - его под-

цель. Подцель называется успешной, если существует sld-вывод программы

<p,bi>, и неуспешной в противном случае. Если подцель bi успешна, то

следующей рассматривается подцель bi+1, а если неуспешна, происходит

поиск другого вывода для подцели bi-1.

Операторы Пролога fail, ! (cut) и not не имеют удовлетворительной

декларативной семантики в терминах классической логики, но имеют про-

цедурную семантику в терминах построения sld-дерева.

А именно: fail есть всегда неуспешная подцель.

Если в теле некоторого программного утверждения С содержится опе-

ратор !(сut), и голова этого программного утверждения унифицируется с

атомом текущего запроса, приписанного вершине r1, то ниже этой вершины

может встретиться вершина r2 с текущим запросом !,.... В таком случае

! - успешная подцель, но при возврате переход из r2 осуществляется

сразу в вершину r0, непосредственно предшествующую r1 (если r0 нет,

вычисление заканчивается).

Подцель not(В) успешна, если неуспешна В, и наоборот. Поэтому

оператор not в Прологе носит название "отрицание как неудача". Декла-

ративная семантика этого оператора соответствует принятию "гипотезы

замкнутости мира". А именно, "мир", описываемый программными утвержде-

ниями p, считается "замкнутым" в том смысле, что те суждения, которые

не являются в нем истинными, полагаются ложными. Пусть для некоторого

атома a верно: p|=a. Тогда не верно, что Р|=їА. Но если для атома b не

верно, что Р|=В, то Р|=їВ также не верно (последнее отношение равно-

сильно отношению Р,В|=Б, которое не выполнено в силу непротиворечивос-

ти любого множества хорновских дизъюнктов). Поэтому для построения ма-

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

от классического ї) отрицание ~: p|=~b <=> не верно, что p|=b. Отрица-

ние как неудача соответствует отрицанию ~ в полном sld-дереве, но в

случае применения стандартной стратегии построения этого дерева отно-

шение p|=b может оказаться не установленным (при попадании на беско-

нечную ветвь). Поэтому процедурная семантика not корректна по отноше-

нию к декларативной, но не полна.

$6. Дедуктивный поиск ответов на вопросы. Окончание.

t29 (о конструктивности классической логики по отношению к прог-

раммам). Если <p,q> - программа, и p|=e.q (где e.q - замыкание формулы

q кванторами существования), то существует подстановка б, такая что

p|=qб. Д. аналогично доказательству Т22 и Т23.

Можно ли найти эту подстановку методом резолюций?

Преобразуем p|=e.q в |=a.p>e.q, а затем в a.p & a.їq |=Б. Если

q±&...&bm, то їq эквивалентно їb1v...vїbm. Приведение к скулемовской

нормальной форме не изменяет формулу a.p & a.їq. Т.к. p|=qб, существу-

ет sld-вывод, вычисляющий б.

Если представить хорновские дизъюнкты из p в дизъюнктивной форме,

а запрос q±&...&bm - в виде q'=їb1v...vїbm, то sld-вывод программы

<p,q> превратится в вывод методом резолюций для множества дизъюнктов

pu{q'}, так что sld-резолюцию можно рассматривать как стратегия метода

резолюций, полную на множестве программ.

Следствия: 1) программы - это как раз те задачи, для которых воз-

можен дедуктивный поиск ответов на вопросы (в частности - методом ре-

золюций); 2) программа <p,q> имеет хотя бы один ответ <=> формула

a.p>e.q является общезначимой.

Ключевые слова к $$1-6: дедуктивный поиск ответов на вопросы,

конструктивность, хорновский дизъюнкт, наименьшая эрбрановская модель,

sld-резолюция, sld-последовательность/вывод/дерево, правило выбора

подцели, наиболее общий унификатор, алгоритм унификации, декларатив-

ная/процедурная семантика, стандартная стратегия вычисления, гипотеза

замкнутости мира.

$7. Алгоритмическая полнота чистого Пролога.

Неформальное понятие алгоритма (решает массовую проблему; состоит

из элементарных шагов: однозначно ясно, как его выполнить, что являет-

ся результатом и какой шаг следующий). Функция называется интуитивно

вычислимой, если ее вычисляет некоторый алгоритм. Функция называется

вычислимой, если ее вычисляет некоторая машина Тьюринга.

Тезис Черча: множество интуитивно вычислимых функций совпадает с

множеством вычислимых.

Алгоритмический язык (в частности, язык программирования) называ-

ется алгоритмически полным, если для любой вычислимой функции сущест-

вует программа на этом языке, ее вычисляющая.

Пролог-программа <p,q(x,y)> вычисляет (не всюду определенную)

функцию f(x) <=> для любых a и b, таких что f(a)=b, sld-дерево

<p,q(a,y)> конечно и содержит единственный вывод, вычисляющий подста-

новку {y:=b}, а для любого c, такого что значение f(c) не определено,

sld-дерево <p,q(с,y)> бесконечно и не содержит выводов.

t30 (об алгоритмической полноте Пролога). Если функция f(x) (не

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

га, то существует Пролог-программа, вычисляющая эту же функцию. Д.:

моделирование программы машины Тьюринга Пролог-программой.

$8. Проблема общезначимости в логике предикатов.

(Массовая) проблема называется разрешимой, если существует всюду

определенный алгоритм, ее решающий. В частности, разрешимость проблемы

общезначимости формул логики предикатов означает существование алго-

ритма, по любой формуле однозначно определяющего: общезначима эта фор-

мула или нет.

Сопоставим программе <p,q> формулу a.p > e.q .

t31. Проблема общезначимости формул, соответствующих программам,

не разрешима. Д.: сведение к проблеме остановки. Если всегда можно ус-

тановить общезначимость формулы a.p > e.q, то всегда можно установить,

имеет ли хотя бы один ответ программа <p,q>. Но это означает возмож-

ность установить, закончит ли работу произвольная машину Тьюринга

(т.к. ее можно смоделировать в виде Пролог-программы). Последнее про-

тиворечит неразрешимости проблемы остановки.

Следствие. Не существует алгоритма, по тексту Пролог-программы

определяющего: 1) имеет ли она ответы; 2) заканчивает ли она работу.

t32. (Теорема Черча о неразрешимости логики предикатов). Проблема

общезначимости формул логики предикатов не разрешима. Д. доказательст-

во следует из Т31.

Ключевые слова к $$7-8: алгоритм; алгоритмическая полнота; машина

Тьюринга; тезис Черча; разрешимость массовой проблемы; проблема общез-

начимости.