Как уже многие люди ответили, проблема ур, которую невозможно решить, является проблемой остановки: напишите программу H
, которая принимает программу P
в качестве входных данных и отвечает, собирается ли программа ввода P
Зацикливаться вечно или нет. Обратите внимание, что наша программа H
может отвечать правильно для многих входных программ, задача состоит в том, чтобы написать программу, которая может ответить на это для всех программ.
Почему проблема остановки неразрешима? Доказательство довольно простое и довольно забавное:
Предположим, что мы можем написать программу H
, которая решает проблему остановки. (Цель состоит в том, чтобы показать, что, предполагая это, мы получим результаты, которые являются просто бессмысленными, следовательно, наше предположение неверно.) Теперь создайте программу EVIL
, которая использует H
в качестве подпрограммы. Мы можем написать EVIL
так:
EVIL p = if H p then loop
else false
Краткое пояснение приведено по порядку. EVIL
берет программу, и если эта программа останавливается, то EVIL
зацикливается. Если входная программа зацикливается вечно, EVIL
возвращает false.
Следующий шаг действительно крут: примените EVIL
к себе! Вопрос в том, каким будет ответ EVIL EVIL
? Это явно зависит от того, будет ли EVIL
зацикливаться вечно или нет. Давайте рассмотрим две альтернативы:
Предположим, что EVIL
циклы навсегда. Но затем, когда мы передаем в качестве входной программы саму себя, она должна вернуть false
, поскольку H
обнаружил, что она будет зацикливаться вечно. Но возвращение false
противоречит тому, что мы впервые сказали, что EVIL
зацикливается навсегда, так что это явно не может быть.
Хорошо, так что EVIL
не зацикливается. Что ж, когда мы передадим EVIL
себе, он просто зациклится, потому что H
вернул true
. Таким образом, у нас есть противоречие и здесь.
Облом! Обе альтернативы (EVIL
циклы или нет) приводят к противоречиям. Таким образом, наши предположения должны быть ошибочными. Не существует такой программы, как H
, которая могла бы решить, останавливать функцию или нет.
Существует много интересных неисчислимых проблем, связанных с проблемой остановки. Некоторые из моих любимых приходят от технологии компилятора. Например: найти наименьшую эквивалентную программу.
Еще одно: учитывая, что вы аннотировали вашу программу утверждениями, напишите программу, которая проверяет, будет ли какое-либо из утверждений нарушено во время выполнения. Такая программа иногда называется средством проверки моделей, и они могут быть действительно полезными, но они никогда не могут быть завершены, то есть им иногда приходится отвечать «я не знаю», когда проблема становится слишком сложной.