Алгоритм решения «проблемы остановки» Тьюринга

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

Могу ли я найти общий алгоритм для решения проблемы остановки для некоторых возможных пар ввода программы?

Могу ли я найти язык программирования (или языки), где я для каждой программы на этом языке могу решить, будет ли программа завершена или работать вечно?

Могу ли я найти общий алгоритм для решения проблемы остановки для некоторых возможных пар ввода программы?

Да, конечно. Например, вы могли бы написать алгоритм, который возвращает «Да, он завершается» для любой программы, которая не содержит ни циклов, ни рекурсии, и «Нет, он не завершается» для любой программы, которая содержит while(true)цикл, который обязательно будет достигнут и не содержит заявление о разрыве, и "Незнайка" для всего остального.

Могу ли я найти язык программирования (или языки), где я для каждой программы на этом языке могу решить, будет ли программа завершена или работать вечно?

Нет, если этот язык полон по Тьюрингу, нет.

Однако существуют полные языки, отличные от Тьюринга, такие как, например, Coq , Agda или Microsoft Dafny, для которых проблема остановки решаема (и фактически определяется их соответствующими системами типов, что делает их полными языками (то есть программа, которая может не завершиться, не будет компиляции)).

Я думаю, что все ответы здесь полностью и полностью упущены. Ответ на этот вопрос таков: если программа предназначена для остановки, тогда да, вам лучше показать, что она останавливается. Если вы не можете показать, что он легко останавливается, тогда программа должна считаться очень плохо написанной и отклоненной Контролем качества как таковой.

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

Если язык C ++, вы, вероятно, не сможете написать инструмент, на самом деле, вряд ли вы когда-нибудь запустите парсер, не говоря уже о том, чтобы доказать завершение работы. Для более структурированного языка вы должны быть в состоянии генерировать доказательство или, по крайней мере, делать это с определенными допущениями: в последнем случае инструмент должен выводить эти допущения. Аналогичный подход будет включать в себя завершение утверждений на языке и использовать их в сложных ситуациях, когда инструмент будет доверять утверждениям.

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

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

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

однако в информатике нет точного термина для «программ», которые «иногда» оказываются успешными. Слово «алгоритм» обычно зарезервировано для программ, которые всегда останавливаются.

концепция, кажется, явно отличается от вероятностных алгоритмов, где теоретики CS настаивают, что есть некоторая известная или вычислимая вероятность их успеха.

есть термин полуалгоритмы, который иногда используется, но, по-видимому, он является синонимом рекурсивно перечислимого или невычислимого.

поэтому для целей здесь, назовите их квазиалгоритмы . концепция отличается от разрешимой против неразрешимой.

$A$$X$$B$$Y$$X \subset Y$$X$$Y$$B$$A$

в CS эта «иерархия квазиалгоритмов», кажется, до сих пор изучалась в основном неформально.

это проявляется в исследовании занятых бобров [1] и в проблеме PCP [2]. фактически компьютерная атака на PCP на основе ДНК может рассматриваться как квазиалгоритм. [3] и это замечено в других областях, уже отмеченных, таких как доказательство теорем [4].

[1] Новая атака тысячелетия на проблему занятого бобра

[2] Решение проблемы с сообщениями Zhao (v2?)

[3] Использование ДНК для решения проблемы ограниченной почтовой корреспонденции . Kari et al.

[4] доказательство завершения программы Cook et al., Comm. ACM

(так что это на самом деле очень глубокий вопрос, который defn заслуживает того, чтобы быть на TCS.SE imho ... может быть, кто-то может переспросить его таким образом, чтобы он подходил и оставался)

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

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

Изменить: в свете комментариев, позвольте мне быть более явным: любой язык, который вы могли бы разработать, для которого вы могли бы решить проблему остановки, обязательно должен быть неполным по Тьюрингу. Это исключает любой язык, который содержит подходящий набор базовых ингредиентов (например, «переменные, условные выражения и переходы», или, как говорит @ sepp2k, универсальный «while» -loop).

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

$T$$T$

Это довольно тривиально. Если мы возьмем объединение любого подмножества ce прерывающих TM и любого подмножества ce не прерывающих TM, то результатом будет множество TM, для которых проблема остановки разрешима (запустите обе машины параллельно, если первая принимает TM) останавливается, если второй принимает, то машина не останавливается). Однако это не приведет к большому количеству интересных языков.

$\mathsf{ALogTime}$$c$$M$

Да, вы можете, но я сомневаюсь, что это будет полезно. Вам, вероятно, придется сделать это с помощью анализа случаев, и тогда вы сможете найти только наиболее очевидные случаи. Например, вы можете grep файл для кода while(true){}. Если файл имеет этот код, он никогда не завершится ^. В более общем смысле вы могли бы сказать, что программа без цикла или рекурсии всегда завершается, и есть несколько случаев, которые вы могли бы сделать, которые могли бы гарантировать, что программа будет или не прекратится, но даже для программы среднего размера это будет очень сложно и во многих случаях не сможет дать вам ответ.

tl; dr: Да, но вы не сможете использовать его для большинства полезных программ.

^ Да, технически, если этот код не находится в пути кода или есть другие потоки, он все еще может завершиться, но здесь я делаю общее замечание.