Решаема ли проблема остановки для чистых программ на идеальном компьютере?

25

Довольно просто понять, почему проблема остановки неразрешима для нечистых программ (т. Е. Программ, в которых ввод / вывод и / или состояния зависят от состояния машины); но интуитивно кажется, что остановка чистой программы на идеальном компьютере может быть решена, например, статическим анализом.

Это на самом деле так? Если нет, то какие контрпримеры или документы опровергают это утверждение?

Жюль
источник
35
Обратите внимание, что стандартные доказательства того, что проблема остановки неразрешима (например, описанная в википедии: en.wikipedia.org/wiki/Halting_problem#Sketch_of_proof ), все работают с моделями вычислений, которые даже не пытаются представлять ввод / вывод. И хотя, например, машины Тьюринга являются полноправными, их поведение формально определяется в терминах чистых функций. Таким образом, в некотором смысле «чистые программы на идеальном компьютере» на самом деле являются той установкой, в которой проблема остановки обычно оказывается неразрешимой.
Бен
1
Какие исследования вы провели? Погуглив "Проблема остановки", уже должен был ответить на этот вопрос для вас.
Джонатан Каст

Ответы:

38

Вот доказательство неразрешимости путем сокращения из проблемы Остановки.

Сокращение: при наличии машины M и ввода x создайте новую машину Тьюринга H которая не читает никаких входных данных, но записывает M и x на ленту и моделирует M на x пока M остановится.

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

Лиуве Винхуйзен
источник
2
Проблема остановки пустой ленты
Hendrik Jan
@HendrikJan Точно!
Лиуве Винхуйзен
16

Нет, это не так, и более того, это не зависит от ввода / вывода.

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

Зло
источник
18
Я не вижу смысла в этом ответе. То, что в настоящее время мы не знаем, существует ли такое число, не означает, что оно не существует, и что мы не можем в будущем написать статический анализатор, который сможет решить это. Лучшей альтернативой является использование известной неразрешимой проблемы. Например, известно, что не существует программы, способной решить все диофантовы уравнения, и решение такого уравнения аналогично задаче, показанной в ответе.
Бакуриу
2
Что ж, если бы проблема Остановки была разрешимой, то любая проблема была бы разрешима, если бы мы могли поместить ее в форму, в которой мы спрашиваем, останавливается ли программа или нет. Или любой вопрос формы: существует счетное множество, и я могу решить, есть ли какой-либо отдельный потенциальный элемент в наборе или нет. Набор пуст? Диофантовы уравнения имеют счетное множество потенциальных решений, и я могу проверить, является ли каждое отдельное потенциальное решение решением или нет. Если бы проблема Остановки была разрешима, то диофантовы уравнения были бы разрешимы.
gnasher729
10
@ gnasher729 Да, и так как они не являются проблемой, проблема с остановкой неразрешима. Это моя точка зрения. Хотя утверждение в этом ответе не имеет реального смысла: «Рассмотрим это математическое определение. В настоящее время мы не знаем, остановит ли программа, решившая это, или нет, но завтра парень может узнать, что это происходит, или нет, и этот ответ становится равным 100». % бессмысленно ".
Бакуриу
6
Разве это не похоже на случай, как можно решить, имеет ли π некоторую последовательность цифр? проблема остановки неразрешима с классами задач, а не с отдельными .
npostavs 13.09.16
2

Классическое доказательство диагонализацией является чистой машиной , не только чистой машиной Тьюринга, но и не опирается на «открытые проблемы».

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

Таким образом, гипотеза Коллатца уже может ответить на ваш вопрос (по крайней мере, временно), но она опирается на то, чего мы не знаем . Вместо этого классическое доказательство является решенной проблемой: мы уже знаем, что это неразрешимо .

Разработчик игр
источник
0

Просто отметим, что стандартное доказательство неразрешимости проблемы остановки основывается на той же идее, что и на языке quines: можно написать программу, подстроку которой соответствует исходный код всей программы. Затем, если бы была функция, haltsкоторая, учитывая исходный код программы, вернула True, если эта программа остановилась на всех входных данных, и False в противном случае, это была бы легальная программа:

prog() = if halts "prog" then prog() else ()

где "prog"будет какое-то выражение, которое оценивается для исходного кода prog; однако вы можете быстро увидеть, что он progостанавливается (для всех входов), если он не останавливается, что является противоречием. Ничто в этом доказательстве никак не зависит от ввода-вывода (нужен ли ввод-вывод для написания квин?).

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

Джонатан Каст
источник