Вычислимость и сложность

вычислимость задача машина рекурсивный Задача считается вычислимой, если она может быть решена в принципе каким-либо вычислительным устройством. Гильберт верил в то, что все математические задачи вычислимы, но в 30-х годах прошлого века Гёдель, Тьюринг и Чёрч показали, что это не так. Были проведены обширные исследования вычислимости математических задач. В дополнение к этому, существует разделение вычислимых задач на классы сложности, в соответствии с тем, сколько времени — как функции от длины входа — требуется на вычисление ответа. Удивительно, насколько понятно, элегантно и точно классифицируются задачи.

Какие задачи являются вычислимыми? Введение и история.

В 1930;х, задолго до появления компьютеров, несколько математиков разных стран независимо ввели точные определения вычислимости. Алонзо Чёрч ввёл л-исчисление, Курт Гёдель определил рекурсивные функции, Стивен Клине определил формальные системы, Марков — то, что в последствии стало известным как алгоритмы Маркова, Эмиль Пост и Алан Тьюринг определили абстрактные машины, в настоящее время известные как машины Поста и машины Тьюринга.

Удивительно, но все эти модели в точности эквивалентны: все, вычислимое в л — исчислении вычислимо с помощью машины Тьюринга, то же выполняется и для остальных пар моделей вычисления. После того, как это было доказано, Чёрч предположил, что интуитивное понятие «вычислимости» совпадает с тем, которое было введено при помощи точных определений. Это предположение, называемое теперь «Тезисом Чёрча-Тьюринга», безоговорочно принимается математиками.

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

Как специальный случай проблемы разрешимости, Гильберт рассматривал задачу проверки общезначимости формул логики первого порядка. Логика первого порядка — математический язык, на котором может быть сформулировано большинство математических утверждений. Любое утверждение логики первого порядка имеет точное значение в каждой подходящей логической структуре, т. е. оно либо ложно, либо истинно в каждой такой структуре. Утверждения, истинные в любой структуре, называются общезначимыми. Утверждения, верные в какой-нибудь из структур, называются выполнимыми. Заметим, что формула общезначима, если ее отрицание,, выполнимо.

Гильберт называл задачу проверки общезначимости формул логики первого порядка entscheidungsproblem. В книге Гильберта и Аккермана Principles of Mathematical Logic авторы писали: «Задача проверки общезначимости формул логики первого порядка будет решена, если нам будет известна процедура, позволяющая по любому логическому выражению за конечное число шагов определить его выполнимость или общезначимость. Эта задача должна рассматриваться как основная задача математической логики» (Бергер, Грейдель и Гуревич 1997).

В 1930 году в своем тезисе Гёдель привел полную систему аксиом для логики первого порядка, основанной на Principia Mathematica Уайтхеда и Рассела (Гёдель 1930). Гёдель доказал теорему полноты, а именно, формула выводима из аксиом тогда и только тогда, когда она общезначима. Теорема полноты Гёделя стала шагом к решению entscheidungsproblem Гильберта.

В особенности, так как аксиомы и правила вывода очень просты, то существует алгоритм, который может выписать все доказательства. Заметим, что каждая строка в доказательстве является либо аксиомой, либо следует из предыдущих строк по одному из правил вывода. Для любой последовательности символов мы можем сказать, является ли она доказательством. Тем самым, можно по очереди выписывать все строки длины 1, 2, 3, и так далее, и проверять, является ли каждая из этих строк выводом какой-нибудь формулы. Если это так, то мы можем добавить последнюю строку вывода к нашему списку теорем (выводимых формул). Таким способом мы можем перечислить все теоремы, т. е. в точности все общезначимые формулы логики первого порядка, с помощью простого алгоритма. Более точно, множество общезначимых формул является областью значений вычислимой функции. Пользуясь современной терминологией, можно сказать, что множество общезначимых формул логики первого порядка рекурсивно перечислимо.

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

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

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

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