<< Пред. стр.

стр. 4
(общее количество: 5)

ОГЛАВЛЕНИЕ

След. стр. >>

Лемма 5.3 Предыдущая лемма верна и в P A|= .
Запишем все формулы арифметики. Каждой формуле будем соотносить некоторый
номер – число Геделя формулы (например номер формулы при записи в лексикографи-
ческом порядке). n? – число Геделя для ? ? L?ar .
Замечание 5.3 Если ? N D ?, и, кроме того ? разрешимо, то любое Q выразимое в
? является разрешимым и любая F выразимая в P hi – вычислима.
Обозначим универсально выражающие множества как Repr?.
Теорема 5.2 ReprT h(N) и ReprP A|= .
Доказательство: Приведем лишь идею доказательства. Нужно по любому Q по-
строить разрешающую формулу. Разрешающую программу нужно описать формулой.
Тогда у нас будет формула, разрешающая множество (выразительную силу языка счи-
таем достаточной)

5.1 Теорема о неподвижной точке
Теорема 5.3 О неподвижной точке
Пусть задано ? ? L?ar , в котором выразимо любое разрешимое множество и любая
выполнимая функция. Тогда для любой ? ? L?ar , #f ree(?) = 1 существует ?, такое
что ? |= ? - ?(n? ).
Доказательство: Определим функцию F : NxN > N.
Если n = n? , где ? – формула с одной свободной переменнрой, то F (n, m) := n?((m)) .
В противном случае F (n, m) := 0.
F является вычислимой, а следовательно и выразимой, тогда существует выража-
ющая ее формула ?(?0 , ?1 , ?3 ).
Для заданой ? с одной свободной переменной построим формулы ? := ?z(?(x, x, z) >
?(z)) и ? := (?(n? , n? , z) > ?(z)), т. е. ? = ?[n? /x].
Докажем, что ? |= ? - ?(n? ), или ? ? - ?(n? ), или ? ? > ?(n? ), или
? ? > ?.
30 Формальные теории


1. ? ?(n? , n? , n? ) > ?(n? ).
Если F (n? , n? ) = n? , то ? ?(n? , n? , n? ). Верно, что ? ?(n? , n? , n? ) > ?(n? ) и
? ?((n? , n? , n? ).
Отсюда ?, ? ?(n? ) или ? ? > ?(n? ).
2. F (n? , n? ) = n?(n? ) = n?

? ?!z?(n? , n? , z)
? ?(n? , n? , n? )

P hi ?z(?(n? , n? , z) > z = n? )
P hi ?(n? ) > ?z(?(n? , n? , z) > z = n? )
P hi ?(n? ) > ?z(?(n? , n? , z) > ?(z))
?

Таким образом ? |= ?(n? ) > ?
Сформулируем данную теорему для программ.
Теорема 5.4 Для f : N > N – отображения между номерами Геделя программ
найдется программа ? такая что n? = nf (n? ) .
Данная теорема позволяет, в частности, утверждать, что для любого языка про-
граммирования существует программа, печатающая свой текст.

5.2 Теорема Тарского
Определение 5.8 Пусть ? – система аксиом L?ar . Тогда ?(? ) – множество след-
ствий из ?. Будем говорить, что оно выразимо в ?, если множество соответству-
ющих номеров Геделя выразимо в ?.

Теорема 5.5 Пусть ? совместное и в нем выразимы все разрешимые множества
векторов и выполнимые функции на N. Если ?|= выразимо в ?, то существует ? ?
L?ar , такая что ? ? ?|= , ¬? ? ?|= .

Доказательство: ?|= выразимо в ?, следовательно выразимо множество номеров
Геделя, т. е. натуральных чисел. Тогда ?(r0 ) выражает свойство быть исчислимым, т. е.
для ? ? L?ar ? |= ? и ? ? равносильно ? |= ?(n? ) и ? ?(n? ) соответственно.
Рассмотрим ? := ¬?. По теореме о неподвижной точке можем построить ?, такую
что ? ? - ?(n? ), т. е. ? ? - ¬?(n? ).
Докажем, что ? ? (? ? ? ). Пусть ? ?, тогда ? ¬?(n? ). Отсюда (по опреде-
лению ?) ? ¬?, но это противоречит совместности ?.
Докажем, что ? ¬? (¬? ? ? ). Пусть ? ¬?, тогда ? ?(n? . Отсюда (по
определению ?) ? ?, а это противоречит совместности ?.
Таким образом ? ? ? и ¬? ? ? .
5.3 Вторая теорема Геделя 31


Теорема 5.6 Тарского о невыразимости истины.
Пусть в L?ar ? L? ? – достаточно богатое множество формул (выразимы все
разрешимые множества векторов над N и все вычислимые формулы на N) на языке
содержащем язык арифметики ? – совместно, ?|= – выразимо в ? и ?|= не является
полной.

Доказательство: Докажем от противного. Если теория модели выразима, достаточно
богата, совместна, тогда она бы не была полной, но теория модели всегда полна.
Тогда теория стандартной модели арифметики не выразима в себе самой.

Следствие 5.1 Существует абсолютно невычислимая функция.

Доказательство:
Определим f : N > {0, 1} следующим образом:
f (n) := 0, если n – номер Геделя теоремы теории чисел и f (n) = 1, если n – не номер
Геделя.
0, n = n? , ?? ? T h(N)
f (n) =
1, n = n? , ?? ? T h(N)
Приведенный пример доказывает существование абсолютно невычислимой функции.

Заметим, что в достаточно богатых языках логики первого порядка можно записы-
вать утверждения о совмесности теорий формулами языка, но эти утверждения “почти”
никогда не выводятся из теории. Почти, означает, что данный язык должен содержать
арифметику.

Теорема 5.7 (Геделя о неполноте). Пусть L? содержит арифметику Пеано. Пусть
? ? L? совместное, разрешимое, достаточно богатое множество формул. Тогда
можно конкретно выписать предложение этого языка ?, для которого ? ?, ? ¬?.

Доказательство: Пусть это не так. Тогда T h(N) полна так как она регистрово ак-
сиоматезируема (потому что ? – регистрово разрешима), а так как все регистрово-
разрешимые множества выразимы в ?), то и ?|= выразима в ?. Следовательно теория
выразима.

5.3 Вторая теорема Геделя
В этой части положим ?ar ? ?, если не оговорено обратное.
Фиксируем теорию в достаточно богатом языке ?ar ? ?, ? ? L? – система аксиом.
? – регистрово разрешима, тогда T h(?) – регистрово аксиоматезируема.
Можно занумеровать все выводы из ?(? ), проверяя каждый раз принадлежат ли
листья ?. В зависимости от этого выводим на печать.
H ? NxN (m, n) ? H, если m-й вывод в этой нумерации приводит к формуле
? с номером n. Так как ? – регистрово-разрешимо, то и H – регистрово разрешимо.
Выражение ? ? равносильно выражению ?m ? N (m, n? ) ? H
32 Формальные теории


?H (?0 , ?1 ) ? L? выражает H – конкретная формула
Рассмотрим формулу Der? (x) ? L? , такую что Der? (x) = ?y?H (y, x) (формулу х
можно вывести из ?).
Тогда существует ?, такая что она не выводима из ? (?? : ? ? - ¬Deg? (n? )).


Лемма 5.4 Пусть ? – совместно (|= ?). Тогда ? ?.


Доказательство: Пусть ? ?, тогда ?m ? N (m, n? ) ? H, откуда ? ?H (m, n? )
(т.к. ?n выражает H). А следовательно ? ?y ?H (y, n? ), но ? - ¬Der? (n? ), занчит
Der? (n? )
? ¬?. Значит ? несовместно(невыразимо), сто противоречит условию.
Запишем утверждение о совместности ?: Con? ? L? . Con? := ¬Der? (n0 = s(0)) –
? совместно если из него не выводится, что 0 = s(0).
Если P A|= ? ?, то ? Con? - ¬Der? (n? ), где ? та самая неподвижная точка.
(доказательство аналогично теореме о неподвижной точке).


Теорема 5.8 Вторая теорема Геделя о неполноте.
Пусть ?– регистрово-разрешимое совместное множество формул из L? , доста-
точно богатое, P A|= ? ?. Тогда ? Con? .


Доказательство: Докажем от противного. Пусть ? Con? . Тогда P hi ¬Der? (n? ),
но тогда ? ?. Получили противоречие с только что доказаным утверждением. .
Возьмем в качестве L? язык теории множеств. Из аксиом ZF выводится арифме-
тика. Пользуясь только аксиомами ZF, мы не можем доказать ее непротиворечивость.
Средствами математики нельзя доказать непротиворечивость математики. Кроме то-
го, никакое нетривиальное семантическое свойство программ не является разрешимым
(тривиальные свойства – те которым удовлетворяют все программы, или которым не
удовлетворяют программы вообще).
В некоторых случаях одна теория способна доказать непротиворечивость другой
(“более слабой”). Так, в теории множеств ZF можно доказать непротиворечивость Th(N).
Формула Con(Th(N)) недоказуема в Th(N) (если эта теория непротиворечива), однако
перевод ее в язык теории множеств можно доказать с помощью аксиом ZF. Формула
Con(Th(N)) - замкнутая формула теории Th(N), т.е. вполне определенное утверждение
о свойствах натуральных чисел. Это утверждение в Th(N) недоказуемо, но его можно
доказать в теории множеств. Эта несколько стложная для интуитиывного понимания
фраза означает в точности следующее: некоторые утверждения о свойствах натураль-
ных чисел, требующие для своей формулировки только понятие натурального числа
(и, казалось бы, касающиеся только этих чисел), требуют для своего доказательства
сложные понятия, не укладывающиеся в рамки Th(N).
33


6 Язык Пролог
Пусть есть некая система аксиом ? и некоторая теорема P. Нужно проверить, является
ли она семантическим следствием ? или не является. Иными словами выполняется ли
такое:
? |= P.
Семантическое следствие заменим на выводимость формальную, а для формальной вы-
водимости мы построим соответствующую формальную систему. Формальная система
будет называться формальной системой опровержения. Будем обознаяать выводимость
методом опровержений таким образом:

? P.
R


Понятно, что сама по себе задача является алгоритмически неразрешимой. Мак-
симум, на что можно надеятся – это на “половину” решения: если действительно P
является семантическим следствием, то тогда рано или поздно такое доказательство
мы найдем, но если P не является семантическим следствием, то не бедет никакой
возможности выяснить, появится ли доказательство через годы или оно не появиться
никогда. На большее расситывать даже в принципе не следует.
Теперь будем строить эту систему.

Определение 6.1 Подстановкой называется запись вида:

? = t1/x1 , t2/x2 . . . tn/xn ,

где x1 , x2 . . . xn – символы предметных переменных, а t1 , t2 . . . tn – это термы.

Если E – либо терм, либо атомная формула, либо отрицание атомной формулы, то
тогда результат подстановки ? в E будем обозначать как E? .

Определение 6.2 Если E – это либо терм, либо атомная формула, либо отрицание
отомной формы, то E будем называть выражением.

Определение 6.3 Атомную форму или ее отрицание будем еще называть литера-
лом.

Пример 6.1 Если E – литерал: E = A (x, f (y) , z), а

? = c/x, g (b)/y , a/z ,

то тогда
E? = A (c, f (g (b)) , a) .
34 Язык Пролог


Определение 6.4 Если ? и ? – две подстановки:

? = t1/x1 , t2/x2 . . . tn/xn ,


? = v1/y1 , v2/y2 . . . vn/yk
Определим композицию подстановок ? и ? следующим образом:

? ? ? = t1 ?/x1 , t2 ?/x2 . . . tn ?/xn , v1/y1 , v2/y2 . . . vk/yk

Вычеркнем все замены вида [x/x]; если среди y1 , y2 , . . . , yk есть переменные из множе-
ства {x1 , x2 , . . . , xn }, соответствующая подстановка также удаляется. Результирующая
подстановка и будет являться композицией подстановок ? и ?: ? ? ?.

Пример 6.2

? = f (c)/x, b/y , y/z , ? = c/u, a/y , b/z ?
? ? ? = f (c)/x, b/y , a/z , c/u, a/y , b/z = f (c)/x, b/y , a/z , c/u

Упражнение 6.1 Рассмотрим пустую подстановку ? := {}. Доказать:

1. ?? (? ? ? = ? ? ? = ?);

2. Для любого выражения E верно: (E?1 ) ?2 = E (?1 ? ?2 );

3. Порядок применения композиций несущественен: (?1 ? ?2 ) ? ?3 = ?1 ? (?2 ? ?3 ).

Определение 6.5 Подстановка ? называется унификатором (uni?er) множества вы-
ражений {E1 , E2 , . . . , En }, если E1 ? = E2 ? = . . . = En ?.

Пример 6.3 E1 = A (x, c), E2 = A (y, c), ? = z/x, z/y ; ? унификатор, так как E1 ? =
E2 ? = A (z, c).

Замечание 6.1 Теория унификаторов была разработана в 60-х годах 20 в. Джулией
Робинсон (J. Robinson).

Определение 6.6 Унификатор ? множества выражений {E1 , E2 , . . . , En } называет-
ся самым общим унификатором (most general uni?er) этого множества, если для лю-
бого другого унификатора ? этого множества верно ? = ? ? ?, причем ? = ?.

Определение 6.7 Множество выражений называется унифицируемым, если у него
есть хотя бы один унификатор.
6.1 Формальная Система Опровержения 35


Теорема 6.1 Любое унифицируемое множество выражений имеет самый общий уни-
фикатор, причем единственный с точностью до переобозначения переменных.

Доказательство: Докажем существование самого общего унификатора. Представим
алгоритм его нахождения и рассмотрим работу этого алгоритма на примере.

1. Запишем выражения из множества E = {E1 , E2 , . . . , En } в столбик, используя
символы с постоянной шириной, то есть, чтобы i-ые символы разных строк были
записаны один под другим. Например:
E1 = A (x,f (u))
E2 = A (g (y) ,f (h (z)))

2. Составим disagreement set множество несовпадений D следующим образом: бу-
дем сканировать записанные выражения вертикальными линиями. Пропустив
k столбцов, состоящих из одинаковых символов, внесем в множество D все термы,
попадающие в k + 1-ый столбец. В нашем случае D (E) = {x, g (y)};

3. Построим унификатор ?1 для множества D (?1 = g (y)/x ) и применим его к вы-
ражениям: E1 ?1 = A (g (y) , f (u)) , E2 ?1 = A (g (y) , f (h (z))); в дальнейшем будем
работать уже с этими выражениями.
4. Если множество E еще не унифицировано, перейдем к шагу 1, работая уже с
множеством E = {E1 ?1 , E2 ?1 }

Очевидно, что, в соответствии с алгоритмом, рано или поздно множество E будет
унифицировано (в нашем случае на втором шаге, ?2 = h (z)/u ), причем полученный
унификатор ? = ?1 ? ?2 ? . . . ? ?n будет самым общим. В случае, если множество неуни-
фицируемо (например, разные выражения содержат различные константы), алгоритм
будет выполняться бесконечно, однако такая ситуация невозможна по условию теоремы
(множество выражений унифицируемо).
Трудоемкость данного алгоритма является не почти линейной, как может показать-
ся вначале, а экспоненциальной вследствие действия под названием occur check , то
есть “проверка вхождения”: ? (x ? Var, t ? Ter) : x ? t. Она предотвращает зациклива-
/
ние алгоритма, гарантируя, что disagreement set содержит только те термы, которым
не принадлежит некоторая входящая в него переменная, то есть, позволяет избежать
циклических замен вида [f (x)/x] для множества D = {x, f (x)}.

6.1 Формальная Система Опровержения
Нормальная форма Скулема. Любая формула языка логики первого порядка может
быть приведена к нормальной форме Скулема (Skolem) к виду

?x1 ?x2 ?x3 . . . ?xn (C1 ? C2 ? C3 ? . . . ? Cn )
36 Язык Пролог


где Ci фразы, конечные дизъюнкции литералов. Все кванторы всеобщности (?) выно-
сятся вперед, кванторы существования (?) недопустимы. В скобках находится выраже-
ние в конъюнктной нормальной форме (КНФ) конъюнкции элементарных дизъюнк-
ций.

Замечание 6.2 Литерал атомная формула или ее отрицание.

Процесс приведения выражения к нормальной форме Скулема состоит из следую-
щих этапов: сначала с помощью семантических эквивалентностей осуществляется пе-
реход к КНФ, после чего все кванторы выносятся за скобки и исключаются кванторы
существования.
Проиллюстрируем исключение квантора существования на примерах. Для исклю-
чения ’?x’ из ?x?y (A (x, y)) внесем в сигнатуру языка новую константу c и запишем:
?y (A (c, y)). В случае другого расположения кванторов, например, ?y?x (A (x, y)), необ-
ходимо ввести в сигнатуру уже новую унарную функцию f : ?y (A (f (y) , y)); приведение
?y?z?x (A (x, y, z)) требует введения бинарной функции: ?y?z (A (g (y, z) , y, z)).
В дальнейшем мы будем работать только с формулами в нормальной форме Ску-
лема. Это не сужает круг рассматриваемых формул, так как любая формула языка
логики первого порядка может быть записана в таком виде. Будем писать для крат-
кости: P = {C1 , C2 , C3 , . . . , Cn } вместо P = ?x1 ?x2 ?x3 . . . ?xn (C1 ? C2 ? C3 ? . . . ? Cn ).
Информация о наличии кванторов всеобщности не теряется, так как здесь мы имеем
дело только с замкнутыми формулами и для переменных всеобщность следует автома-
тически.
Введем правила вывода. Пусть C1 , C2 , Q некоторые фразы. Будем говорить, что
C1 и C2 выводят Q в формальной системе опровержения R и записывать C1 , C2 |=R Q,
если:

• Существуют такие подстановки ?1 , ?2 , что C1 ?1 и C2 ?2 не имеют общих имен
переменных;

• Существуют такие множества литералов {L1 , L2 , L3 , . . . , Ln } ? C1 ?1 и {L1 , L2 , L3 , . . . , Ln } ?
C2 ?2 , где литералы второго множества являются отрицаниями литералов первого,
что объединенное множество со снятыми отрицаниями {L1 , L2 , L3 , . . . , Ln , L1 , L2 , L3 , . . . , Ln }
унифицируемо, его самый общий унификатор ?;

• Формула Q имеет вид:

((C1 ?1 \ {L1 , L2 , L3 , . . . , Ln }) ? (C2 ?2 \ {L1 , L2 , L3 , . . . , Ln })) ?

Пример 6.4 C1 = {A (z) ? ¬B (y) ? A (g (x))}, C2 = {¬A (x) ? ¬C (x)}. Переименуем
переменные в соответствии с правилом 1: ?1 = ? (пустая замена), ?2 = {u/x}. Да-
лее, рассматривая множества литералов, получим ? = g (x)/z , x/u . Здесь наличие
6.1 Формальная Система Опровержения 37


множеств {Li } и Lj позволяет избавиться от не унифицируемых литералов, вхо-
дящих в одну формулу в положительном, а в другую в отрицательном виде. Замена
переменных позволяет избежать неунифицируемых множеств вида {x, f (x)}. Напри-
мер, {¬x, f (x)} |=R ?, так как в процессе редукции (удаления литералов, ведущих к
лжи) остается пустое множество, которое семантически эквивалентно лжи.

Теорема 6.2 Пусть множество фраз S невыполнимо, тогда S выводит пустую фра-
зу в этой формальной системе опровержения (S |=R ).

Эту теорему можно назвать теоремой о “полноте наоборот”: тогда как полнота в
обычном понимании означает, что, если некое выражение семантически истинно, то
оно истинно и синтаксически, эта теорема утверждает о том, что семантическая ложь
выводит пустой литерал.
Рассмотрим алгоритм проверки выполнимости множества фраз:

REPEAT {S := Res (S)} UNTIL { ? S} : PRINT ’S невыполнимо’

Здесь Res (S) множество резольвентов, то есть всех возможных выводов из пар фраз,
принадлежащих S. Если множество выполнимо, данный алгоритм будет работать бес-
конечно.

Пример 6.5 Запишем формулировку Парадокса Брадобрея:

?x?y (B (x) ? ¬S (y, y) > S (x, y)) ? ?x?y (B (x) ? S (y, y) > ¬S (x, y))

Мы хотим доказать, что ¬?xB (x), или, что то же самое, что ?B (x) |= ?, то
есть, существование семантического противоречия.
Представим данную формулу (а также цель) в виде множества фраз в нормаль-
ной форме Скулема: {¬B (x) , S (y, y) , ¬S (x, y)}, {¬B (x) , ¬S (y, y) , ¬S (x, y)}, {B (c)}.
Выведем из двух первых фраз новую: {¬B (x)}, и получим новую систему: {¬B (x)},
{B (c)}, из которой выводится пустое множество .

Алгоритм представляет каждую формулу в виде набора фраз и, совмещая каждую
с каждой, пытается сократить результат с учетом унификации до получения пустой
фразы на выходе.
Можно оптимизировать алгоритм путем ввода правил, ограничивающих полный пе-
ребор. Таким образом, получаем два класса стратегий, которых придерживаются алго-
ритмы: полные стратегии, которые для противоречивого набора входных фраз всегда
рано или поздно получают на выходе ложь, и неполные, позволяющие оптимально об-
рабатывать некоторый класс задач, но допускающие невозможность найти ответ для
других (грубо говоря, алгоритм зацикливается при некоторых корректных входных
данных).
38 Язык Пролог


Рассмотрим структуру PROLOG-программы. Автоматический доказатель язы-
ка PROLOG основан на схожих принципах и использует неполную стратегию, ко-
торая заключается в следующем: рассматриваются первые две фразы; затем к вы-
водам из них добавляется третья и рассматриваются выводы уже из этого набора
и так далее. Неполноту этой стратегии можно продемонстрировать на примере: из
(A ? B) ? (A ? ¬B) ? (¬A ? B) ? (¬A ? ¬B) никогда не будет получена ложь. Одна-
ко, при некоторых ограничениях на входные фразы данная стратегия является полной,
а именно, если программа состоит только из фраз Хорна (Hoarn).

Определение 6.8 Фразы Хорна – это фразы, содержащие не более одной положи-
тельной атомной формулы.

Например, A ? ¬B, ¬A ? B и ¬A ? ¬B – фразы Хорна, а A ? B нет; фразы Хорна
также записываются следующим образом: A0 ? ¬A1 ? ¬A2 ? ¬A3 = A0 < A1 , A2 , A3 ,
на языке PROLOG A0 : ? ? A1, A2, A3.; фраза Хорна, не содержащая положительных
литералов, называется целью: < A1 , A2 , A3 = : ? ? A1 , A2 , A3 ..
Таким образом, PROLOG-программа состоит из набора фраз Хорна и цели.

<< Пред. стр.

стр. 4
(общее количество: 5)

ОГЛАВЛЕНИЕ

След. стр. >>