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

Question

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

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

Я также видел проект терминатора Microsoft - http://research.microsoft.com/Terminator/

Что заставляет меня спросить - переоценивается ли проблема остановки - нужно ли нам беспокоиться об общем случае?

Будут ли типы тьюринг завершены с течением времени - зависимые типы кажутся хорошим развитием?

Или, если посмотреть по-другому, начнем ли мы использовать полные языки без тьюринга, чтобы получить преимущества статического анализа?

Answer 1

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

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

Будут ли типы тьюринг завершены со временем?

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

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

Очень сильно.

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

Answer 2

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

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

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

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

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

Answer 3

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

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

Answer 4

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

Answer 5

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

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

Answer 6

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

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

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

Answer 7

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

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

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

Answer 8

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

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

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