Довольно просто понять, почему проблема остановки неразрешима для нечистых программ (т. Е. Программ, в которых ввод / вывод и / или состояния зависят от состояния машины); но интуитивно кажется, что остановка чистой программы на идеальном компьютере может быть решена, например, статическим анализом.
Это на самом деле так? Если нет, то какие контрпримеры или документы опровергают это утверждение?
Ответы:
Вот доказательство неразрешимости путем сокращения из проблемы Остановки.
Сокращение: при наличии машиныM и ввода Икс создайте новую машину Тьюринга ЧАС которая не читает никаких входных данных, но записывает M и Икс на ленту и моделирует M на Икс пока M остановится.
Поведение этой новой машины не зависит от входной ленты, поэтому это чисто машина Тьюринга, к которой применим только статический анализ. Если бы статического анализа было достаточно, то он мог бы показать, останавливается ли , что показало бы, останавливается ли на , что решило бы проблему остановки для нечистых машин, которая, как мы знаем, неразрешима, и поэтому ваша проблема также неразрешима.H M xЧАС ЧАС M Икс
источник
Нет, это не так, и более того, это не зависит от ввода / вывода.
Простой контрпример: напишите программу для нахождения идеального нечетного числа (это открытая проблема: мы еще не знаем, существует ли она) - она не требует никакого ввода и не выполняет никаких нечистых задач; он может остановиться, когда найдет его, или может работать бесконечно (в случае, если такого числа не существует). Теперь, если статический анализ был достаточно мощным, чтобы определить случай остановки, он был бы использован для ответа на этот (и многие другие вопросы), где остановка означала бы положительное существование такого числа, а не остановка означала бы, что такого числа нет, но, к сожалению, статический анализ не такой мощный.
источник
Классическое доказательство диагонализацией является чистой машиной , не только чистой машиной Тьюринга, но и не опирается на «открытые проблемы».
Например, машина Тьюринга, которая выполняет гипотезу Коллатца, имеет неизвестный статус остановки, но она опирается на наше незнание о гипотезе Коллатца, однажды мы можем доказать, что Коллатц был прав, и тогда мы сможем решить, как остановить статус этой гипотезы. (Либо для некоторых входов не останавливается, либо Всегда останавливается).
Таким образом, гипотеза Коллатца уже может ответить на ваш вопрос (по крайней мере, временно), но она опирается на то, чего мы не знаем . Вместо этого классическое доказательство является решенной проблемой: мы уже знаем, что это неразрешимо .
источник
Просто отметим, что стандартное доказательство неразрешимости проблемы остановки основывается на той же идее, что и на языке quines: можно написать программу, подстроку которой соответствует исходный код всей программы. Затем, если бы была функция,
halts
которая, учитывая исходный код программы, вернула True, если эта программа остановилась на всех входных данных, и False в противном случае, это была бы легальная программа:где
"prog"
будет какое-то выражение, которое оценивается для исходного кодаprog
; однако вы можете быстро увидеть, что онprog
останавливается (для всех входов), если он не останавливается, что является противоречием. Ничто в этом доказательстве никак не зависит от ввода-вывода (нужен ли ввод-вывод для написания квин?).Кстати, вы можете захотеть заглянуть в «ввод-вывод на основе диалога», чтобы получить дополнительные доказательства того, что ввод-вывод совершенно не имеет отношения к вашей проблеме (в основном, программы, выполняющие ввод-вывод, могут быть сведены к программам, которые принимают ввод как (явные) функциональные аргументы и возвращают вывод в виде (явных) дополнительных результатов на ленивом языке). К сожалению, я не могу найти разумную, непредвзятую (или поддерживающую диалог) страницу в Интернете прямо сейчас.
источник