Я перехожу к доказательству проблемы остановки в Intro к теории вычислений Sipser, и моя главная забота заключается в следующем:
Если TM M не знает, когда он зацикливается (он не может принять или отклонить, почему TM является Тьюрингом, распознаваемым для всех строк), тогда как мог бы решающий H решить, может ли M быть в цикле? Эта же проблема будет продолжаться, когда TM D выполняет свою обработку.
Это "доказательство противоречия", редукция ad absurdum. (Латинские фразы всегда хороши в теоретических классах... если они имеют смысл, конечно.)
Эта программа H - это просто программа с двумя входами: строка, представляющая собой программу для некоторой машины, и ввод. В целях доказательства вы просто предполагаете, что программа H правильная: она просто остановится и примет, если M принимает с w. Вам не нужно думать о том, как это будет сделано; на самом деле, мы собираемся доказать, что это не может, что никакая такая программа H не может существовать,...
Поскольку
если бы такая программа существовала, мы могли бы немедленно построить другую программу H ', которую H не мог решить. Но, по предположению, такой программы нет: H может решить все. Таким образом, мы вынуждены заключить, что никакая программа, определенная так, как мы определили H, не возможна.
Кстати, метод доказательства reductio является более противоречивым, чем вы могли ожидать, учитывая, как часто его используют, особенно в области компьютерных наук. Вы не должны смущаться, чтобы найти это немного странным. Магический термин "неконструктивный", и если вы чувствуете себя очень амбициозным, спросите одного из ваших профессоров о критике Эретта Бишопа неконструктивной математики.
После прочтения этого и попытки визуализации доказательства я придумал этот код, который является упрощенной версией кода в этом ответе, на соответствующий вопрос:
function halts(func) {
// Insert code here that returns "true" if "func" halts and "false" otherwise.
}
function deceiver() {
if(halts(deceiver))
while(true) { }
}
Если halts(deceiver) возвращает true, deceiver будет выполняться вечно, и если он вернет false, deceiver остановится, что противоречит определению halts. Следовательно, функция halts невозможна.