Решить проблему остановки проще, чем думают?

Решить проблему остановки проще, чем думают?

Я думаю, что это именно так сложно, как думают люди.

Станут ли типы со временем полными по Тьюрингу?

Дорогой, они уже есть!

зависимые типы кажутся хорошим развитием?

Даже очень.

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

Вау, это один запутанный вопрос.

Во-первых: проблема остановки — это не «проблема» в практическом смысле, а «проблема, которую необходимо решить». Это скорее утверждение о природе математики, аналогичное теореме Гёделя о неполноте.

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

Третье: работа на языке Turing Complete не устраняет «преимуществ статического анализа» — это просто означает, что у статического анализа есть ограничения. Все в порядке, в любом случае почти все, что мы делаем, имеет пределы.

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

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

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

Как повседневный программист, я бы сказал, что стоит продолжать идти по пути к решению проблем в стиле остановки, даже если вы только приближаетесь к этому пределу и никогда не достигаете его. Как вы указали, сканирование на вирусы оказывается ценным. Поиск Google не претендует на то, чтобы быть абсолютным ответом на вопрос «найди мне лучшее X вместо Y», но он также очень полезен. Если я выпущу новый вирус (мувахаха), создаст ли это более широкий набор решений или просто прольет свет на существующую проблемную область? Независимо от технических различий, некоторые из них будут прагматично разрабатывать и взимать плату за последующие услуги «обнаружения и удаления».

Я с нетерпением жду реальных научных ответов на другие ваши вопросы...

Между прочим, я думаю, что полнота шаблонов по Тьюрингу показывает, что остановку переоценивают. Большинство языков гарантируют, что их компиляторы остановятся; не так С++. Принижает ли это С++ как язык? я так не думаю; у него много недостатков, но компиляция, которая не всегда останавливается, не является одним из них.

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

Итак, мое мнение по этому вопросу таково: нет, в важных случаях это непросто. Тем не менее, в реальном мире это может быть не так уж и важно.

См. также: http://en.wikipedia.org/wiki/Halting_problem#Importance_and_consequences

Я не знаю, как люди думают, что это сложно, поэтому я не могу сказать, легче ли это. Однако вы правы в своем наблюдении, что неразрешимость проблемы (вообще) не означает, что все экземпляры этой проблемы неразрешимы. Например, я могу легко сказать вам, что такая программа, как while false do something, завершается (предполагая очевидную семантику while и false).

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

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

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

Однако название вашего вопроса немного вводит в заблуждение. Я согласен с DrPizza: проблема терминации настолько сложна, насколько люди думают. Кроме того, тот факт, что нам не обязательно беспокоиться об общем случае, не означает, что проблема завершения переоценена: стоит искать частные решения, потому что мы знаем, что общее решение трудно .

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