2.4. Проблема разрешимости

Проблема нахождения эффективной процедуры (алгоритма) решения задач из данного класса задач (массовая проблема) называется проблемой разрешения этого класса. В интуитивном смысле массовая (алгоритмическая) проблема – это бесконечный класс родственных единичных конкретных проблем, каждая из которых требует ответа «да» или «нет», а метод разрешения массовой проблемы – это единый общий метод, дающий правильный ответ для каждой единичной проблемы. Фактически произвольную массовую проблему можно сформулировать как проблему распознавания некоторого свойства Е элементов данного бесконечного множества А; при этом единичные проблемы, составляющие эту массовую проблему, связываются с элементами множества А, и каждая из них состоит в том, что требуется узнать, обладает или нет свойством Е соответствующий элемент множества А.

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

Исчисление предикатов первого порядка – пример неразрешимой формальной системы. Впервые доказал существование неразрешимых алгоритмических проблем в 1936 г. американский логик Алонзо Черч. В доказанной им теореме говорится об отсутствии эффективной процедуры при решении вопроса относительно произвольной ППФ формальной системы, содержащей арифметику натуральных чисел, является ли эта ППФ теоремой. В доказательстве Черча были использованы идеи Геделя, оно было тесно связано с его знаменитой теоремой о неполноте, точнее, с двумя теоремами, доказанными им в 1931 г. Первая теорема тесно связана с явлением алгоритмической неразрешимости, вторая содержит более тонкое утверждение о формальных системах. Содержание первой теоремы о неполноте (если ограничиться натуральной арифметикой) заключается в следующем. Пусть FS – арифметическая формальная система, содержащая аксиомы Пеано. При этом предполагается, что FS корректно описывает арифметику, т.е., что все формулы, выводимые в FS, являются истинными утверждениями о натуральных числах. Для любой такой системы первая теорема Геделя утверждает, что не все истинные ППФ арифметики доказуемы в FS, т.е. в арифметике имеется некоторое утверждение. А, обладающее тем свойством, что ни А, ни ¬А не являются теоремами. Другими словами, понятие истинности ППФ арифметического языка шире, чем понятие доказуемости в любой формальной системе (если последняя корректна). Более того, если в арифметике имеются недоказуемые (неразрешимые) утверждения, то присоединение к такой теории неразрешимого утверждения в качестве аксиомы снова приводит к теории, являющейся формализацией арифметики, в которой по-прежнему имеются неразрешимые утверждения. Таким образом, теорема Геделя говорит не только о неполноте, но и о непополнимости формальной арифметики.

Во второй своей теореме Гедель показал невозможность доказательства непротиворечивости формальной теории, включающей формальную арифметику, конструктивными методами, формализуемыми в рамках самой этой теории.

Из геделевского доказательства неполноты арифметики, по существу, вытекала неразрешимость проблемы идентификации истинных утверждений элементарной арифметики.

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

Благодаря работам К. Геделя и А. Черча понятие алгоритмической неразрешимости было уточнено с привлечением понятий нумераций и частичной рекурсивности. Впоследствии английский математик А. Тьюринг предложил другое уточнение понятия неразрешимости, использовав понятие машины Тьюринга. Эти уточнения, как оказалось, приводят к равнообъемным понятиям неразрешимости. Известны и другие уточнения, дающие тот же результат: нормальные алгорифмы А.А. Маркова, формальные исчисления американского математика Э. Поста и другие.

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

А.А. Марков и Э. Пост построили полугруппы с неразрешимой проблемой тождества. Аналогичная проблема для групп – проблема тождества в группе – занимает важное место в теории групп. Советский математик П.С.Новиков в 1952 г. доказал алгоритмическую неразрешимость проблемы тождества теории групп, заключающуюся в невозможности распознавания эквивалентности слов для ассоциативных исчислений специального типа. Проблема эквивалентности слов для ассоциативных исчислений, т.е. исчислений, состоящих из совокупности слов в данном алфавите вместе с системой допустимых подстановок типа P_i ↔ Q_i , была впервые сформулирована еще в 1914 г. норвежским математиком Туэ. С тех пор предпринимались многие попытки построить такую общую эффективную процедуру, которая для любого ассоциативного исчисления и любой пары слов в нем позволила бы установить, эквивалентны эти слова или нет, т.е. существует ли или нет дедуктивная цепочка слов, ведущая как от одного слова к другому, так и обратно. Были построены конкретные примеры ассоциативных исчислений, для каждого из которых проблема эквивалентности слов оказалась неразрешимой. Была доказана также алгоритмическая неразрешимость ряда проблем в теориях полугрупп, групп, структур, колец, полей и других алгебраических систем.

Почти все разделы математики изобилуют массовыми проблемами. Долго не поддавалась решению десятая проблема Гильберта, суть которой состоит в следующем: требуется найти эффективную процедуру, позволяющую для любого диофантового уравнения выяснить, имеет ли оно целочисленное решение. Напомним, что диофантовым называется уравнение вида P = 0, где P – многочлен с целочисленными коэффициентами. Для частного случая диофантова уравнения с одним неизвестным такой алгоритм известен, и он сводится к тому, что если уравнение с целочисленными коэффициентами имеет целый корень x₀, то обязательно свободный член в этом уравнении делится на x₀. Что касается общего случая для множества целочисленных многочленов от произвольного числа неизвестных, то вплоть до 1969 г. эта проблема, хотя над ней работали многие выдающиеся математики современности, не была решена. И только в конце 1969 г. советскому математику Ю.В. Матиясевичу удалось доказать, что эта проблема алгоритмически неразрешима.

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

Известны два способа доказательства алгоритмической неразрешимости: прямой, основанный на так называемом «диагональном» методе, и косвенный, использующий сводимость к данной проблеме другой массовой проблемы, неразрешимость которой была доказана раньше. Идею прямого метода доказательства алгоритмической неразрешимости поясним на примере так называемой проблемы остановки машины Тьюринга. Эта проблема заключается в нахождении алгоритма, который позволял бы по любой машине Тьюринга и любой конфигурации ленты узнать, остановится или нет машина, начав работу с этой конфигурации. Выберем какую-либо эффективную нумерацию всех машин Тьюринга и обозначим через M_x ту машину, которая получает номер x. Пронумеруем все конфигурации ленты, причем так, чтобы каждое натуральное число являлось номером некоторой конфигурации. Обозначим через K_x конфигурацию с номером x.

Перейдем теперь к неформальному доказательству того, что не существует алгоритма распознавания остановки произвольной машины Тьюринга для произвольной начальной конфигурации ленты. Предположим, что такой алгоритм есть. Тогда, очевидно, частично рекурсивной будет функция f(x), определенная следующим образом: f(x) не определено, если x не является номером никакой машины; f(x) равно 1 или 0 в зависимости от того, остановится или нет машина M_x, начав работу с конфигурации K_x. Значит, существует машина Тьюринга, вычисляющая функцию f(x). Эту машину легко переделать в другую машину, отличающуюся от первой только тем, что когда первая машина в качестве результата вычисления дает 1, вторая попадает в цикл. Пусть y – номер второй машины. Запустим машину M_y с конфигурации K_y. Если машина остановится, то, по самому определению машины M_y, должно быть f(y) = 0, и, следовательно, по определению функции f машина M_y не остановится. Если машина M_y не остановится, то, поскольку f определена в y, f(y) = 1 и, следовательно, по определению функции f, машина M_y остановится. Полученное противоречие является доказательством неразрешимой алгоритмической проблемой остановки машины Тьюринга.

Косвенный метод доказательства алгоритмической неразрешимости разъясним на примере так называемой m-сводимости. Пусть имеются две массовые проблемы. Первая заключается в распознавании свойства E элементов множества A, вторая – в распознавании свойства F элементов множества B. Говорят, что первая массовая проблема m-сводима ко второй, если существует эффективное отображение φ множества A в множество B такое, что для любого a  A утверждения: «a обладает свойством E» и «φ(a) обладает свойством F» одновременно истинны или ложны. Легко видеть, что, если одна массовая проблема m-сводима к другой и первая проблема алгоритмически неразрешима, то вторая проблема также будет алгоритмически неразрешимой.

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

В заключение отметим, что понятие эффективной процедуры является метаматематическим понятием. Что это значит? Язык, на котором дается описание какой-либо формальной системы, называется метаязыком в отличие от предметного языка или языка – объекта, который используется для высказываний внутри самой формальной системы. Таким образом, если мы возьмем высказывание типа «Исчисление предикатов первого порядка непротиворечиво», то это есть высказывание, сделанное на метаязыке. В свою очередь, высказывание типа x(A(x) → B(x)) → (x A(x) → x B(x)) есть высказывание, записанное на предметном языке.

Отсюда понятие теоремы (выводимой ППФ) самой формальной системы нельзя путать с теоремой, описывающей какие-либо свойства формальной системы, последняя есть метатеорема. Вышеприведенное высказывание, записанное на русском языке о непротиворечивости исчисления предикатов первого порядка, есть метатеорема, высказывание же, записанное в терминах , , →, ¬, &, , ( ) есть теорема исчисления предикатов.