Теорема Черча

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

История

Предпосылки

В начале XX века в рамках программы Гильберта по обоснованию математики возникла задача формализации всех математических рассуждений. Предполагалось, что для любой математической истины можно построить формальное доказательство, которое будет проверяться механически. Однако в 1931 году Курт Гёдель опубликовал теоремы о неполноте, показав, что в любой достаточно мощной формальной системе существуют истинные, но недоказуемые утверждения. Это подорвало оптимизм программы Гильберта, но оставило открытым вопрос о существовании алгоритма, который мог бы решать, является ли данное утверждение доказуемым (или, что эквивалентно, является ли данная формула общезначимой).

Формулировка Черча

В 1936 году Алонзо Чёрч, работая над формализацией понятия алгоритма через λ-исчисление, опубликовал статью «A note on the Entscheidungsproblem» (Заметка о проблеме разрешения). В ней он доказал, что проблема разрешения (Entscheidungsproblem) для логики первого порядка неразрешима. Иными словами, не существует общего алгоритма, который для любой формулы логики первого порядка определял бы, является ли она общезначимой (истинной во всех интерпретациях). Это доказательство опиралось на понятие рекурсивной функции (формализация вычислимости, предложенная Чёрчем и Клини). Чёрч показал, что если бы проблема разрешения была разрешима, то можно было бы построить алгоритм решения проблемы остановки, которая, как он доказал, неразрешима.

Связь с тезисом Чёрча — Тьюринга

Параллельно с Чёрчем, в 1936 году Алан Тьюринг опубликовал работу «On Computable Numbers, with an Application to the Entscheidungsproblem», в которой ввёл формальную модель вычислителя — машину Тьюринга. Тьюринг независимо доказал неразрешимость проблемы остановки, а затем и проблемы разрешения. Чёрч и Тьюринг пришли к одному и тому же выводу: класс алгоритмически разрешимых задач совпадает с классом задач, вычислимых на машине Тьюринга (или, что эквивалентно, с классом рекурсивных функций). Этот принцип получил название тезис Чёрча — Тьюринга. Теорема Черча, таким образом, является первым строгим доказательством существования алгоритмически неразрешимой задачи, основанным на формальном определении вычислимости.

Формулировка

Существует несколько эквивалентных формулировок теоремы Черча. Наиболее распространённые:

1. Проблема разрешения для логики первого порядка неразрешима. Не существует алгоритма, который для любой замкнутой формулы логики первого порядка за конечное число шагов давал бы ответ «да», если формула общезначима, и «нет» в противном случае.
2. Проблема тождества слов для полугрупп неразрешима. Не существует алгоритма, который для произвольной полугруппы, заданной образующими и соотношениями, и двух произвольных слов в её алфавите определял бы, равны ли эти слова в данной полугруппе.
3. Проблема остановки неразрешима. Не существует общего алгоритма, который для любой программы (или машины Тьюринга) и любых входных данных определял бы, завершится ли выполнение программы или будет работать бесконечно.

Доказательство (идея)

Доказательство теоремы Черча базируется на сведении проблемы остановки к проблеме разрешения. Основная идея:

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

Следствия

Теорема Черча имеет фундаментальные последствия для математики, логики и информатики:

• Ограничения формальных систем. Она показывает, что не существует полной и непротиворечивой формальной системы, в которой можно было бы доказать или опровергнуть любое истинное утверждение. Это является усилением теорем Гёделя о неполноте.
• Практические ограничения программирования. Теорема доказывает, что невозможно создать универсальный анализатор программ, который бы определял, завершится ли программа, не возникнет ли в ней ошибка, или будет ли она выполнять определённые действия. Это имеет прямое отношение к проблемам верификации программ, статического анализа кода и автоматического тестирования.
• Развитие теории вычислимости. Теорема Черча стала отправной точкой для развития теории алгоритмов, теории сложности вычислений и теории рекурсии. Она определила границы того, что можно вычислить, и стимулировала поиск алгоритмов для задач, которые всё же разрешимы, но требуют больших вычислительных ресурсов.

Критика и уточнения

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

Источники

• Church, A. (1936). A note on the Entscheidungsproblem. The Journal of Symbolic Logic, 1(1), 40-41.
• Turing, A. M. (1936). On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 2(1), 230-265.
• Клини, С. К. (1952). Введение в метаматематику. Иностранная литература.
• Мендельсон, Э. (1964). Введение в математическую логику. Наука.
• Роджерс, Х. (1967). Теория рекурсивных функций и эффективная вычислимость. Мир.