Игошин Математическая логика и теория алгоритмов (1019110), страница 93

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 93)

Последнее означает следующее. Поскольку функции уи и 8 вычислимы, то мы для каждого номера х можем выяснить, определено значение Цх) или нет. Это, в свою очередь, означает, что построена разрешающая функция ум о я для проблемы самоприменимости алгоритма, что невозможно. Если рассмотреть случай, когда ),' я С, то нужно выбрать|; а С. Проведя аналогичные рассуждения, придем к следующей разрешающей функции для проблемы самоприменимости 1 — уи(я(х)), что также противоречит доказанной ранее неразрешимости этой алгоритмической проблемы. Теорема доказана.

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

Дело в том, что мы пытаемся создать единый алгоритм„который имеет дело с функциями. Но что значит иметь дело с функцией? Функция должна быть как-то задана. В данном случае функциями; задается вычисляющим ее алгоритмом А„(мы помним, что каждая функция может вычисляться множеством алгоритмов). Разыскиваемый нами единый алгоритм как раз и имеет дело с алгоритмами, вычисляющими функции. Так вот, смысл теоремы Райса состоит в том, что 374 „о описанию алгоритма, вычисляющего функцию, ничего нельзя дать о свойствах функции, которую он вычисляет. Еще раз подчеркнем — не существует единого алгоритма, применимого к опи, ниям всех вычисляющих алгоритмов. В частности, оказывается неразрешимой проблема эквивалентности алгоритмов (упоминавшаяся нами в в 33): по двум заданць1м алгоритмам нельзя узнать, вычисляют они одну и ту же функцию или нет.

Каждый, кто имел дело с программированием (написанием компьютерных программ), знает, что по тексту сколько-нибудь сложной программы, не запуская ее в работу, трудно понять, что она делает (какую функцию вычисляет). Если это понимание и приходит, то каждый раз по-своему; единого метода здесь не существует. Это своего рода практическое проявление теоремы Райса. Мы уже обсуждали проблемы синтаксиса и семантики языка лри рассмотрении формальных теорий. В теории алгоритмов появляется еще один аспект этой проблемы.

Синтаксические свойства алгоритма — это свойства описывающих его текстов, т.е. свойства конечных слов в фиксированном алфавите. Семантические (или смысловые) свойства алгоритма связаны с тем, что он делает. Хорошо известно, что в процессе отладки программ синтаксические ошибки отыскиваются довольно легко (этому, в частности, способствуют и дополнительные программы-алгоритмы). Главные неприятности связаны именно с анализом семантики неотлаженной программы, т.е. с попытками установить, что же она делает вместо того, чтобы делать то, что мы хотим (и здесь нам уже никакие дополнительные программы помочь не могут). Образно выражаясь, можно сказать, что теорема Райса звучит так: по синтаксису алгоритма ничего нельзя узнать о его семантике. Другие примеры влгоркпиической неразрешимости.

В начале 9 23 отмечалось, что не существует алгоритма, позволяющего для каждой формулы логики предикатов определить, будет ли формула выполнимой или общезначимой. Это означает, что массовые проблемы разрешения для общезначимости и выполнимости формул логики предикатов алгоритмически не разрешимы. Одной из наиболее знаменитых алгоритмических проблем математики являлась 10-я проблема Гильберта, поставленная им в числе других в 1901 г. на Международном математическом кон"рессе в Париже. Требовалось найти алгоритм, определяющий для любого диафантова уравнения, имеет ли оно целочисленное реше"ие. Диафантово уравнение есть уравнение вида г(х, у, ..., г) = О, "де р(х, у, ..., г) — многочлен с целыми показателями степеней и с целыми коэффициентами.

В общем случае эта проблема долго оставалась нерешенной, и только в 1970 г. советский математик )О В. Матиясевич доказал ее неразрешимость. 375 Существует множество и других алгоритмических проблем, от носительно которых установлена их неразрешимость. Среди них ряд алгебраических проблем, приводящих к различным вариан там проблемы слов, которые исследовались советскими математи ками А.А.

Марковым, П. С. Новиковым, А. И. Мальцевым. В заключение еще раз отметим, что алгоритмическая неразре шимость означает лишь отсутствие единого способа для решения всех единичных задач данной бесконечной серии, в то время ках каждая индивидуальная задача серии вполне может быть решена своим индивидуальным способом. Более того, может оказаться разрешимой (своим индивидуальным методом) не только каждая отдельная задача этого класса, но и целые подклассы задач этого класса. Поэтому, если проблема неразрешима в общем случае, нужно искать ее разрешимые частные случаи.

Задача в более общей постановке имеет больше шансов оказаться неразрешимой, Так, несмотря на отсутствие единого алгоритма, позволяющего для каждой формулы логики предикатов определить, является ли она выполнимой или общезначимой, мы в 5 21 ответили на этот вопрос применительно к конкретным индивидуальным формулам, а в 5 23 сумели даже отыскать алгоритмы решения данной задачи для целых классов формул некоторых специальных видов.

Аналогична ситуация с диафантовыми уравнениями. Например, для частного случая диафантова уравнения а„х" + а„,х" ' + . + а,х+ ао — — О хорошо известно, что все его целые корни следует искать среди делителей свободного члена ае В то же время понимание сути проблемы алгоритмической неразрешимости и знание основных алгоритмических неразрешимостей является одним из важных элементов современной математической и логической культуры, особенно для тех, кто имеет профессиональные дела, связанные с компьютерами, программированием и информатикой. $37.Теорема Геделя о неполноте формальной арифметики Эта теорема, уже неоднократно встречавшаяся нам, утверждает, что любая непротиворечивая формальная аксиоматическая теория, формализующая арифметику натуральных чисел, не является (абсолютно) полной.

В настоящем параграфе дается доказательство этой теоремы, опирающееся на идеи и методы теории алгоритмов. Тем самым будет еще раз продемонстрирована на самом высоком уровне теснейшая связь математической логики И теории алгоритмов — двух математических дисциплин, образующих фунламент всей современной математики. Наше изложени~ 376 будет основываться на доказательстве, разработанном М.АрбибОМ [10.1]. После доказательства теоремы 35.7 о том, что существует перечислимое, но неразрешимое множество натуралъных чисел, было заявлено, что она фактически включает в себя в неявном виде теорему Геделя о неполноте формальной арифметики.

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

При этом утверждение теоремы 35.7 о существовании перечислимого, но неразрешимого множества натуральных чисел будет основополагающей предпосылкой для доказательства теоремы Геделя, которую мы докажем в следующей формулировке: «Каждая адекватная ьз-непротиворечивая формальная арифметика неполна».

Далее, мы поясним, что будем понимать под формальной арифметикой, а также определим и разъясним те понятия, которые участвуют в приведенной формулировке теоремы Геделя. Начнем с формальных аксиоматических теорий. Формальные аксиоматические теории и натуральные числа. В э 28, и. 1, определено понятие формальной аксиоматической теории.

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

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

Следовательно, каждое из этих множеств перечислимо. Понятия вывода и теоремы в формальной аксиоматической теории даны в определении 28.2. Все теоремы, приводимые в настоящем параграфе, в соответствии с нашей терминологией являются фактически метатеоре- 377 мами, т.е. теоремами о свойствах (формальных) аксиоматических теорий. Но поскольку здесь никакой конкретной аксиоматичес. кой теории мы не рассматриваем, никаких теорем такой теории не доказываем, т.е. никаких теорем, кроме метатеорем, здесь не будет, то мы метатеоремы будем называть просто теоремами. Теорема 37.1.

Характеристики

Список файлов книги