Войти
В теории вычислимости, проблема остановки - это проблема определения на основе описания произвольной компьютерной программы и входных данных, завершит ли программа выполнение или продолжит выполнение бесконечно. Алан Тьюринг доказал в 1936 году, что общий алгоритм для решения проблемы остановки для всех возможных пар программа-ввод не может существовать.
Для любой программы f, которая может определить, останавливаются ли программы, «патологическая» программа g, вызываемая с некоторым входом, может передать свой собственный источник и свой вход в f, а затем конкретно сделать противоположное тому, что f предсказывает g. Сделаю. Не может существовать f, который занимается этим делом. Ключевой частью доказательства является математическое определение компьютера и программы, которое известно как машина Тьюринга ; проблема остановки неразрешима по машинам Тьюринга. Это один из первых случаев проблем с решением, которые оказались неразрешимыми. Это доказательство важно для практических вычислений, поскольку определяет класс приложений, которые никакое изобретение в области программирования не может выполнять идеально.
Джек Коупленд (2004) связывает введение термина «проблема остановки» с работой Мартина Дэвиса в 1950-х.
Проблема остановки - это проблема решения о свойствах компьютерных программ на фиксированной полной по Тьюрингу модели вычислений, т.е. программы, которые могут быть написаны на некотором заданном языке программирования, который является достаточно общим, чтобы быть эквивалентным машине Тьюринга. Проблема состоит в том, чтобы определить, учитывая программу и ввод в программу, остановится ли программа в конечном итоге при запуске с этим вводом. В этой абстрактной структуре нет ограничений по ресурсам на объем памяти или время, необходимое для выполнения программы; это может занять произвольно много времени и использовать произвольный объем памяти перед остановкой. Вопрос просто в том, остановится ли данная программа на определенном входе.
Например, в псевдокоде программа
не останавливается; скорее, это продолжается бесконечно в бесконечном цикле. С другой стороны, программа
останавливается.
Хотя решить, останавливать ли эти программы просто, более сложные программы оказываются проблематичными. Один из подходов к решению проблемы может заключаться в том, чтобы запустить программу, сделав некоторое количество шагов, и проверить, не останавливается ли она. Но если программа не останавливается, неизвестно, остановится ли программа в конечном итоге или будет работать вечно. Тьюринг доказал, что не существует алгоритма, который всегда правильно решает, останавливается ли программа для данной произвольной программы и ввода при запуске с этим вводом. Суть доказательства Тьюринга состоит в том, что любой такой алгоритм может противоречить самому себе и, следовательно, не может быть правильным.
Некоторые бесконечные циклы могут быть весьма полезными. Например, циклы событий обычно кодируются как бесконечные циклы. Однако большинство подпрограмм предназначены для завершения (остановки). В частности, при жестких вычислениях в реальном времени программисты пытаются писать подпрограммы, которые не только гарантированно завершатся (остановятся), но также гарантированно завершатся до заданного крайнего срока.
Иногда эти программисты используют какой-то универсальный (полный по Тьюрингу) язык программирования, но пытаются писать в ограниченном стиле, таком как MISRA C или SPARK, что позволяет легко доказать, что итоговые подпрограммы завершаются до указанного крайнего срока.
В других случаях эти программисты применяют правило наименьшей мощности - они намеренно используют компьютерный язык, который не является полностью полным по Тьюрингу. Часто это языки, которые гарантируют завершение всех подпрограмм, например Coq.
Сложность проблемы остановки заключается в требовании, чтобы процедура принятия решения работала для всех программ и входных данных. Конкретная программа либо останавливается на заданном входе, либо не останавливается. Рассмотрим один алгоритм, который всегда отвечает «останавливается», а другой - «не останавливается». Для любой конкретной программы и ввода один из этих двух алгоритмов отвечает правильно, даже если никто не знает, какой именно. Однако ни один алгоритм не решает проблему остановки в целом.
Существуют программы (интерпретаторы ), которые имитируют выполнение любого исходного кода, который им предоставлен. Такие программы могут продемонстрировать, что программа действительно останавливается, если это так: сам интерпретатор в конечном итоге останавливает свое моделирование, что показывает, что исходная программа остановилась. Однако интерпретатор не остановится, если его программа ввода не остановится, поэтому этот подход не может решить проблему остановки, как указано; он не отвечает успешно "не останавливается" для программ, которые не останавливаются.
Проблема остановки теоретически разрешима для линейных ограниченных автоматов (LBA) или детерминированных машин с конечной памятью. Машина с конечной памятью имеет конечное число конфигураций, и, следовательно, любая детерминированная программа на ней должна в конечном итоге либо остановиться, либо повторить предыдущую конфигурацию:
Однако Мински отмечает, что компьютер с миллионом мелких деталей, каждая из которых имеет два состояния имели бы по крайней мере 2 возможных состояния:
Мински утверждает, что хотя машина может быть конечной, конечные автоматы «имеют ряд теоретических ограничений»:
Также может быть автоматически решено, останавливается ли недетерминированная машина с конечной памятью ни на одной, некоторых или всех возможных последовательностях недетерминированных решений, путем перечисления состояний после каждого возможного решения.
Проблема остановки исторически важна, потому что это была одна из первых проблем, которая была доказана неразрешимой. (Доказательство Тьюринга было опубликовано в мае 1936 года, тогда как доказательство Алонзо Черча неразрешимости проблемы в лямбда-исчислении было опубликовано уже в апреле 1936 года [Church, 1936].) Впоследствии были описаны многие другие неразрешимые проблемы.
В своем первоначальном доказательстве Тьюринг формализовал концепцию алгоритма, представив машины Тьюринга. Однако результат никоим образом не специфичен для них; он в равной степени применяется к любой другой модели вычислений, эквивалентной по своей вычислительной мощности машинам Тьюринга, таким как алгоритмы Маркова, лямбда-исчисление, Post системы, регистровые машины или системы тегов.
Важно то, что формализация позволяет напрямую отображать алгоритмы на некоторый тип данных, который алгоритм может работать. Например, если формализм позволяет алгоритмам определять функции над строками (такими как машины Тьюринга), тогда должно быть отображение этих алгоритмов на строки, и если формализм позволяет алгоритмам определять функции над натуральными числами (такими как вычислимые функции ), тогда должно быть отображение алгоритмов в натуральные числа. Сопоставление со строками обычно является наиболее простым, но строки в алфавите с n символами также могут быть сопоставлены с числами, интерпретируя их как числа в n-арном числе. система.
Традиционное представление задач решения - это совокупность объектов, обладающих рассматриваемым свойством. Множество остановки
представляет проблему остановки.
Этот набор рекурсивно перечислим, что означает, что существует вычислимая функция, которая перечисляет все пары (i, x), которые он содержит. Однако дополнение этого набора не является рекурсивным перечислимым.
Существует много эквивалентных формулировок проблемы остановки; любой набор, степень Тьюринга равняется таковой для задачи остановки. Примеры таких наборов включают:
Доказательство того, что проблема остановки не разрешима, - это доказательство от противоречия. Чтобы проиллюстрировать концепцию доказательства, предположим, что существует вычисляемая функция total halts (f), которая возвращает true, если подпрограмма f останавливается (при запуске без входов) и возвращает false в противном случае. Теперь рассмотрим следующую подпрограмму:
def g (): if halts (g): loop_forever ()
halts (g) должен либо возвращать true, либо false, потому что предполагалось, что halts составляет total. Если halts (g) возвращает true, тогда g вызовет loop_forever и никогда не остановится, что является противоречием. Если halts (g) возвращает false, тогда g остановится, потому что он не будет вызывать loop_forever; это тоже противоречие. В целом, halts (g) не может возвращать значение истинности, которое согласуется с тем, останавливается ли g. Следовательно, исходное предположение о том, что halts - это полностью вычислимая функция, должно быть ложным.
Метод, использованный в доказательстве, называется диагонализацией - g делает противоположное тому, что, по словам останова, должно делать g. Разница между этим наброском и фактическим доказательством состоит в том, что в фактическом доказательстве вычислимая остановка функции не принимает непосредственно подпрограмму в качестве аргумента; вместо этого он берет исходный код программы. Фактическое доказательство требует дополнительной работы для решения этой проблемы. Более того, фактическое доказательство избегает прямого использования рекурсии, показанной в определении g.
Вышеупомянутая концепция показывает общий метод доказательства; в этом разделе будут представлены дополнительные сведения. Общая цель - показать, что не существует total вычислимой функции, которая решает, останавливается ли произвольная программа i на произвольном входе x; то есть следующая функция h не вычислима (Penrose 1990, p. 57–63):
Здесь программа i относится к i-й программе в перечислении всех программ фиксированной полной по Тьюрингу модели вычисление.
| f (i, j) | i | ||||||
| 1 | 2 | 3 | 4 | 5 | 6 | ||
| j | 1 | 1 | 0 | 0 | 1 | 0 | 1 |
| 2 | 0 | 0 | 0 | 1 | 0 | 0 | |
| 3 | 0 | 1 | 0 | 1 | 0 | 1 | |
| 4 | 1 | 0 | 0 | 1 | 0 | 0 | |
| 5 | 0 | 0 | 0 | 1 | 1 | 1 | |
| 6 | 1 | 1 | 0 | 0 | 1 | 0 | |
| f (i, i) | 1 | 0 | 0 | 1 | 1 | 0 | |
| g (i) | U | 0 | 0 | U | U | 0 | |
Возможные значения для общей вычислимой функции f, расположенные в двумерном массиве. Оранжевые клетки - диагональ. Значения f (i, i) и g (i) показаны внизу; U указывает, что функция g не определена для конкретного входного значения.
Доказательство продолжается путем непосредственного установления того, что никакая общая вычислимая функция с двумя аргументами не может быть требуемой функцией h. Как и в наброске концепции, для любой полной вычислимой двоичной функции f следующая частичная функция g также вычисляется некоторой программой e:
Проверка вычислимости g основана на следующих конструкциях (или их эквивалентах):
Следующий псевдокод иллюстрирует простой способ вычисления g:
процедура compute_g (i): если f (i, i) == 0, тогда вернуть 0 цикл else навсегда
Поскольку g частично вычислим, должна быть программа e, которая вычисляет g, предположение, что модель вычислений является полной по Тьюрингу. Эта программа - одна из всех программ, в которых определена функция остановки h. Следующий шаг доказательства показывает, что h (e, e) не будет иметь того же значения, что и f (e, e).
Из определения g следует, что должен выполняться ровно один из следующих двух случаев:
В любом случае f не может быть той же функцией, что и h. Поскольку f была произвольной полной вычислимой функцией с двумя аргументами, все такие функции должны отличаться от h.
Это доказательство аналогично диагональному аргументу Кантора. Можно визуализировать двумерный массив с одним столбцом и одной строкой для каждого натурального числа, как указано в таблице выше. Значение f (i, j) помещается в столбец i, строку j. Поскольку предполагается, что f является общей вычислимой функцией, любой элемент массива может быть вычислен с помощью f. Построение функции g можно визуализировать с помощью главной диагонали этого массива. Если массив имеет 0 в позиции (i, i), тогда g (i) равно 0. В противном случае g (i) не определено. Противоречие происходит из-за того, что существует некоторый столбец e массива, соответствующий самому g. Теперь предположим, что f была функцией остановки h, если g (e) определена (в данном случае g (e) = 0), g (e) останавливается, поэтому f (e, e) = 1. Но g (e) = 0 только тогда, когда f (e, e) = 0, что противоречит f (e, e) = 1. Аналогично, если g (e) не определен, то функция остановки f (e, e) = 0, что приводит к g (e) = 0 по построению g. Это противоречит предположению, что g (e) не определено. В обоих случаях возникает противоречие. Следовательно, любая вычислимая функция f не может быть функцией остановки h.
Типичным методом доказательства неразрешимости проблемы является метод редукции. Для этого достаточно показать, что если решение новой проблемы было найдено, его можно было бы использовать для решения неразрешимой проблемы путем преобразования экземпляров неразрешимой проблемы в экземпляры новой проблемы. Поскольку мы уже знаем, что никакой метод не может решить старую проблему, никакой метод не может решить и новую проблему. Часто новая проблема сводится к решению проблемы остановки. (Тот же метод используется для демонстрации того, что проблема NP complete, только в этом случае вместо демонстрации отсутствия решения он демонстрирует отсутствие решения за полиномиальное время, предполагая, что P ≠ NP.)
Например, одним из таких последствий неразрешимости проблемы остановки является то, что не может быть общего алгоритма, который решает, будет ли данное утверждение о натуральных числах верно или неверно. Причина этого в том, что предложение о том, что определенная программа остановится при определенных входных данных, может быть преобразовано в эквивалентное утверждение о натуральных числах. Если бы у нас был алгоритм, который мог бы найти значение истинности каждого утверждения о натуральных числах, он определенно мог бы найти значение истинности этого утверждения; но от этого будет зависеть, остановится ли исходная программа, что невозможно, поскольку проблема остановки неразрешима.
Теорема Райса обобщает теорему о неразрешимости проблемы остановки. В нем говорится, что для любого нетривиального свойства не существует общей процедуры принятия решения, которая для всех программ решала бы, обладает ли частичная функция, реализованная входной программой, этим свойством. (Частичная функция - это функция, которая не всегда может давать результат, и поэтому используется для моделирования программ, которые могут либо давать результаты, либо не останавливаться.) Например, свойство «остановка для входа 0» неразрешимо. Здесь «нетривиальный» означает, что набор частичных функций, удовлетворяющих этому свойству, не является ни пустым набором, ни набором всех частичных функций. Например, «останавливается или не останавливается на входе 0» явно верно для всех частичных функций, поэтому это тривиальное свойство, и его можно определить с помощью алгоритма, который просто сообщает «истина». Кроме того, эта теорема верна только для свойств частичной функции, реализованной программой; Теорема Райса не распространяется на свойства самой программы. Например, «остановка на входе 0 в пределах 100 шагов» не является свойством частичной функции, которая реализуется программой - это свойство программы, реализующей частичную функцию, и очень разрешимо.
Грегори Чейтин определил вероятность остановки, представленную символом Ω, тип действительного числа, которое, как неформально считается, представляет вероятность что случайно созданная программа останавливается. Эти числа имеют ту же степень Тьюринга, что и проблема остановки. Это нормальное и трансцендентное число, которое может быть определено, но не может быть полностью вычислено. Это означает, что можно доказать, что не существует алгоритма , который выдает цифры Ω, хотя его первые несколько цифр можно вычислить в простых случаях.
Хотя доказательство Тьюринга показывает, что не может быть общего метода или алгоритма для определения того, останавливаются ли алгоритмы, отдельные экземпляры этой проблемы вполне могут быть уязвимы для атаки. Имея конкретный алгоритм, часто можно показать, что он должен останавливаться при любом вводе, и на самом деле компьютерщики часто делают это как часть доказательства правильности. Но каждое доказательство должно разрабатываться специально для рассматриваемого алгоритма; не существует общего механического способа определить, останавливаются ли алгоритмы на машине Тьюринга. Однако есть некоторые эвристики , которые можно использовать в автоматическом режиме, чтобы попытаться построить доказательство, которое часто оказывается успешным в типичных программах. Эта область исследований известна как автоматизированный анализ завершения.
. Поскольку отрицательный ответ на проблему остановки показывает, что существуют проблемы, которые не могут быть решены машиной Тьюринга, тезис Черча – Тьюринга ограничивает чего можно достичь на любой машине, реализующей эффективные методы. Однако не все машины, которые можно представить человеческому воображению, подчиняются тезису Чёрча – Тьюринга (например, машины-оракулы ). Остается открытым вопрос, могут ли существовать реальные детерминированные физические процессы, которые в конечном итоге ускользают от моделирования машиной Тьюринга, и, в частности, можно ли с пользой использовать какой-либо такой гипотетический процесс в форме вычислительная машина (гиперкомпьютер ), которая могла бы, среди прочего, решить проблему остановки для машины Тьюринга. Также остается открытым вопрос, участвуют ли такие неизвестные физические процессы в работе человеческого мозга и могут ли люди решить проблему остановки (Copeland 2004, p. 15).
Концепции, возникающие в теоремах Гёделя о неполноте, очень похожи на те, которые возникают в связи с проблемой остановки, и доказательства очень похожи. Фактически, более слабая форма Первой теоремы о неполноте является простым следствием неразрешимости проблемы остановки. Эта более слабая форма отличается от стандартной формулировки теоремы о неполноте тем, что утверждает, что аксиоматизация натуральных чисел, которая одновременно является полной и звуковой, невозможна. «Правильная» часть - это ослабление: это означает, что мы требуем, чтобы рассматриваемая аксиоматическая система доказывала только истинные утверждения о натуральных числах. Поскольку разумность подразумевает согласованность, эту более слабую форму можно рассматривать как следствие сильной формы. Важно отметить, что утверждение стандартной формы первой теоремы Гёделя о неполноте совершенно не связано с истинностью утверждения, а касается только вопроса о том, возможно ли его найти с помощью математического доказательства.
Более слабая форма теоремы может быть доказана из неразрешимости проблемы остановки следующим образом. Предположим, что у нас есть обоснованная (и, следовательно, непротиворечивая) и полная аксиоматизация всех истинных логических утверждений о натуральных числах. Затем мы можем построить алгоритм, который перечислит все эти утверждения. Это означает, что существует алгоритм N (n), который, учитывая натуральное число n, вычисляет истинное логическое утверждение первого порядка о натуральных числах, и что для всех истинных утверждений существует по крайней мере одно n такое, что N (n) дает это заявление. Теперь предположим, что мы хотим решить, останавливается ли алгоритм с представлением a на входе i. Мы знаем, что это утверждение может быть выражено с помощью логического оператора первого порядка, скажем, H (a, i). Поскольку аксиоматизация завершена, то либо существует n такое, что N (n) = H (a, i), либо существует n 'такое, что N (n') = ¬ H (a, i). Таким образом, если мы перебираем по всем n, пока не найдем H (a, i) или его отрицание, мы всегда остановимся, и, более того, ответ, который он нам даст, будет истинным (по разумности). Это означает, что это дает нам алгоритм для решения проблемы остановки. Поскольку мы знаем, что такого алгоритма быть не может, отсюда следует, что предположение о том, что существует непротиворечивая и полная аксиоматизация всех истинных логических утверждений первого порядка о натуральных числах, должно быть ложным.
Многие варианты проблемы остановки можно найти в учебниках по вычислимости (например, Sipser 2006, Davis 1958, Minsky 1967, Hopcroft and Ullman 1979, Börger 1989). Обычно их неразрешимость следует за уменьшением стандартной задачи остановки. Однако некоторые из них имеют более высокую степень неразрешимости. Следующие два примера типичны.
Универсальная проблема остановки, также известная (в теории рекурсии ) как совокупность, - это проблема определения, остановится ли данная компьютерная программа для каждого входа (совокупность имени происходит от эквивалентного вопроса о том, является ли вычисленная функция итого ). Эта проблема не только неразрешима, как проблема остановки, но и весьма неразрешима. С точки зрения арифметической иерархии, это 
Это, в частности, означает, что проблема остановки не может быть решена даже с помощью oracle.
Существует множество программ, которые для некоторых входных данных возвращают правильный ответ на проблему остановки, в то время как для других входных данных они не возвращают ответ вообще. Однако проблема «данная программа p является ли она решателем частичной остановки» (в описанном смысле) по крайней мере так же сложна, как и проблема остановки. Чтобы убедиться в этом, предположим, что для этого существует алгоритм PHSR («распознаватель решателя частичной остановки»). Затем его можно использовать для решения проблемы остановки следующим образом: чтобы проверить, останавливается ли входная программа x на y, создайте программу p, которая на входе (x, y) сообщает истину и расходится на всех других входах. Затем проверьте p с помощью PHSR.
Приведенный выше аргумент является сокращением проблемы остановки до распознавания PHS, и таким же образом могут быть уменьшены более сложные проблемы, такие как остановка всех входных данных, подразумевая, что распознавание PHS не только неразрешимый, но и более высокий в арифметической иерархии, а именно
Машина Тьюринга с потерями - это машина Тьюринга, в которой часть ленты может недетерминированно исчезнуть. Проблема остановки разрешима для машины Тьюринга с потерями, но не примитивно-рекурсивной.
Машина с оракулом для проблемы остановки может определить, остановятся ли определенные машины Тьюринга на определенных входах, но они не могут определить, в целом, остановятся ли машины, эквивалентные им самим.
