Почему не может быть программа, которая проверяет другую программу

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

Я помню, что мы учились на курсе вычислений, но теперь я просто не могу найти решение, и мне нужно объяснить это кому-то на моей работе.

Спасибо за помощь.

4 ответа

Решение

"Проверяет другую программу" очень широк. Фактически, некоторые функции программ могут быть проверены, например, проверяет ли тип программы Java. Тем не менее, проверка типов в Java-программе также отклонит некоторые программы, которые никогда не приведут к ошибке типа при запуске, например:

int foo() {
    if (true) return 5;
    else return null;
}

Этот метод никогда не вернет null, но средство проверки типов не может видеть это. Но разве мы не могли просто сделать систему более умного типа?

К сожалению, ответ - нет. Рассмотрим следующую программу:

int bar() {
    if (infiniteComputation()) return 5;
    else return null;
}

Тип проверки не может проверить, если infiniteComputation когда-нибудь вернет false, из-за проблемы остановки.

Другая связанная теорема - это теорема Райса, которая, вероятно, ближе к тому, о чем был ваш вопрос, чем к проблеме остановки.

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

Вы ищете проблему остановки.

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

Есть запись в Википедии об этом...

Но в основном, чтобы определить, может ли быть остановлена ​​какая-либо достаточно сложная программа, вам нужно запустить ее, чтобы отследить путь выполнения. Это означает, что вы вернулись к одной программе, на которой запущена другая программа, и если эта программа не останавливается, программа, которая ее просматривает, также не остановится.

Это все равно, что вычислять цифры для пи... это остановится? Как вы можете сказать, что оно бесконечно во время выполнения, в отличие от страдания от некоторых вычислительных проблем? Мы знаем, что эта конкретная проблема бесконечна, но другие подобные проблемы не были доказаны.

Ответ Байрона должен указать вам на важную информацию. Кроме того, вы можете иметь программу, которая проверяет конкретную программу. То, что вы не можете иметь, это программа, которая проверяет произвольность программы на правильность.

Другие вопросы по тегам