Проблема остановки и неразрешимость

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

Definition

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

Scope

Эта тема охватывает точную формулировку проблемы остановки, доказательство ее неразрешимости методом диагонализации, технику сведения «многие к одному» для переноса неразрешимости, теорему Райса о нетривиальных свойствах программ и классические неразрешимые проблемы, такие как проблема разрешения (Entscheidungsproblem) и проблема тождества для групп.

Core questions

• Почему не существует алгоритма, который определяет, останавливаются ли программы?
• Как используются сведения для доказательства неразрешимости одной проблемы из другой?
• Что говорит теорема Райса о разрешимости свойств программ?
• Какие известные математические проблемы оказались неразрешимыми?

Key theories

Неразрешимость проблемы остановки

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

Сведение и перенос неразрешимости

Если известная неразрешимая проблема сводится к целевой проблеме, то целевая проблема также неразрешима, что делает сведение стандартным инструментом для установления неразрешимости.

Теорема Райса

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

Clinical relevance

Результаты неразрешимости устанавливают жесткие ограничения на автоматизированное рассуждение и анализ программ: они показывают, что совершенные универсальные инструменты для проверки завершаемости или свойств программ не могут существовать, и объясняют, почему многие проблемы в логике, алгебре и теории чисел не имеют алгоритмического решения.

History

Тьюринг и Чёрч в 1936 году показали, что проблема разрешения (Entscheidungsproblem), вопрос об алгоритме, определяющем общезначимость формул логики первого порядка, неразрешима, при этом проблема остановки лежит в основе аргумента Тьюринга. Райс обобщил это явление в 1953 году, а неразрешимость впоследствии была установлена для конкретных проблем, таких как проблема тождества для групп Новиковым и десятая проблема Гильберта Матиясевичем.

Key figures

• Alan Turing
• Alonzo Church
• Henry Gordon Rice
• Pyotr Novikov

Seminal works

• sipser2013
• turing1936
• rogers1987

Frequently asked questions

Почему более быстрый компьютер не может решить проблему остановки?

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

Можем ли мы когда-нибудь сказать, остановится ли программа?

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