Разве решение проблемы остановки легче, чем думают люди?
Хотя общий случай неразрешим, многие люди все еще решают проблемы, которые достаточно хорошо подходят для повседневного использования.
В докторской диссертации Коэна о компьютерных вирусах он показал, что сканирование на вирусы эквивалентно проблеме остановки, но у нас есть целая индустрия, основанная на этой проблеме.
Я также видел проект терминатора Microsoft - http://research.microsoft.com/Terminator/
Что заставляет меня спросить - переоценивается ли проблема остановки - нужно ли нам беспокоиться об общем случае?
Будут ли типы тьюринг завершены с течением времени - зависимые типы кажутся хорошим развитием?
Или, если посмотреть по-другому, начнем ли мы использовать полные языки без тьюринга, чтобы получить преимущества статического анализа?
9 ответов
Разве решение проблемы остановки легче, чем думают люди?
Я думаю, что это так же сложно, как думают люди.
Будут ли типы тьюринга завершаться со временем?
зависимые типы кажутся хорошим развитием?
Даже очень.
Я думаю, что может быть рост в нетуринговых полных, но доказуемых языках. В течение достаточно долгого времени SQL находился в этой категории (его больше нет), но это не уменьшило его полезность. Я думаю, что есть место для таких систем.
Вау, это один запутанный вопрос.
Первое: проблема остановки не является "проблемой" в практическом смысле, как "проблема, которая должна быть решена". Это скорее утверждение о природе математики, аналогичное теореме Гёделя о неполноте.
Второе: тот факт, что создание совершенного антивирусного сканера трудно поддается (поскольку он эквивалентен проблеме остановки), является как раз причиной того, что "целая индустрия построена вокруг этой проблемы". Если бы можно было разработать алгоритм для идеального сканирования на вирусы, это было бы просто делом, когда кто-то делал бы это один раз, и тогда больше не было бы необходимости в отрасли. История окончена.
Третье: работа на языке Turing Complete не исключает "преимуществ статического анализа" - это просто означает, что существуют ограничения для статического анализа. Это нормально - есть ограничения практически на все, что мы делаем.
Наконец: если бы проблема остановки могла быть "решена" каким-либо образом, это определенно было бы "легче, чем думают люди", поскольку Тьюринг продемонстрировал, что она неразрешима. Общий случай - единственный релевантный случай с математической точки зрения. Конкретные случаи являются вопросами техники.
Есть много программ, для которых проблема остановки может быть решена, и множество этих программ полезно.
Если у вас был компилятор, который сообщал бы вам "Остановки", "Не останавливается" или "Не знаю", то он мог бы сказать вам, какая часть программы вызвала условие "Остановка" или "Не знаю", Если вы действительно хотели программу, которая определенно остановилась или не остановилась, то вы бы исправили эти блоки "не знаю" почти так же, как мы избавились бы от предупреждений компилятора. Я думаю, что мы все были бы удивлены тем, как часто попытка решить эту вообще невозможную проблему оказалась полезной.
Между прочим, я думаю, что полнота шаблонов по Тьюрингу показывает, что остановка переоценена. Большинство языков гарантируют, что их компиляторы остановятся; не так C++. Уменьшает ли это C++ как язык? Я так не думаю; у него много недостатков, но компиляции, которые не всегда останавливаются, не являются одним из них.
Как повседневный программист, я бы сказал, что стоит идти дальше по пути решения проблем стиля остановки, даже если вы только приближаетесь к этому пределу и никогда не достигаете его. Как вы указали, сканирование на вирусы оказывается полезным. Поиск в Google не претендует на абсолютный ответ "найди мне лучший X для Y", но он также особенно полезен. Если я запускаю новый вирус (muwahaha), это создает больший набор решений или просто проливает свет на существующую проблемную область? Независимо от технических различий, некоторые будут прагматично разрабатывать и взимать плату за последующие услуги "обнаружения и удаления".
Я с нетерпением жду реальных научных ответов на ваши другие вопросы...
Я не знаю, как тяжело люди думают, поэтому не могу сказать, проще ли. Тем не менее, вы правы в своем наблюдении, что неразрешимость проблемы (в целом) не означает, что все случаи этой проблемы неразрешимы. Например, я могу легко сказать, что такая программа, как while false do something завершается (при условии очевидной семантики while и false).
Такие проекты, как проект Terminator, о котором вы упоминали, очевидно, существуют (и, возможно, даже работают в некоторых случаях), поэтому ясно, что не все безнадежно. Существует также конкурс (я считаю, что каждый год) для инструментов, которые пытаются доказать завершение для систем перезаписи, которые в основном являются моделью вычислений. Но дело в том, что прекращение во многих случаях очень трудно доказать.
Проще всего взглянуть на это, возможно, увидеть неразрешимость как максимум сложности задач. Каждая инстанция находится где-то в масштабе от тривиального до этого максимума, и с более высоким максимумом вы обычно имеете, что инстанции также сложнее в среднем.
Проблема остановки действительно интересна, только если вы посмотрите на нее в общем случае, так как, если бы проблема остановки была разрешима, все другие неразрешимые проблемы также были бы разрешимы путем сокращения.
Итак, мое мнение по этому вопросу, нет, это не просто в тех случаях, которые имеют значение. Тем не менее, в реальном мире, это не может быть таким большим делом.
Смотрите также: http://en.wikipedia.org/wiki/Halting_problem
Тот факт, что проблема неразрешима, не означает, что она не интересна, а наоборот! Так что да, тот факт, что у нас нет эффективной и единой процедуры для решения проблемы завершения всех программ (а также многих других проблем с программным обеспечением), не означает, что не стоит искать частичные решения. В некотором смысле, именно поэтому мы нуждаемся в разработке программного обеспечения: потому что мы не можем просто делегировать задачу компьютерам.
Название вашего вопроса, однако, немного вводит в заблуждение. Я согласен с DrPizza: проблема терминации - такая же сложная, как думают люди. Более того, тот факт, что нам не обязательно беспокоиться об общем случае, не означает, что проблема завершения переоценена: стоит искать частичные решения, потому что мы знаем, что общее решение сложно.
Наконец, вопросы о зависимых типах и субрекурсивных языках, хотя они и частично связаны, на самом деле разные вопросы, и я не уверен, что вижу смысл смешивать их все вместе.
001 int D(int (*x)())
002 {
003 int Halt_Status = H(x, x);
004 if (Halt_Status)
005 HERE: goto HERE;
006 return Halt_Status;
007 }
008
009 int main()
010 {
011 Output("Input_Halts = ", H(D,D));
012 }
H правильно предсказывает, что D(D) никогда не остановится, пока H не прервет моделирование своего ввода.
(a) Если имитирующий блок принятия решения об остановке H правильно моделирует свой вход D до тех пор, пока H правильно не определит, что его моделируемый D не может достичь своего собственного оператора «возврата» за конечное число моделируемых шагов, тогда:
(b) H может прервать моделирование D и правильно сообщить, что D задает непрерывную последовательность конфигураций.
Когда понятно, что (b) является необходимым следствием (a), и мы можем видеть, что (a) было выполнено, мы понимаем, что H(D,D) может правильно определить статус остановки своего иначе «невозможного» входа. .
Моделирование принятия решения об остановке в применении к теореме об остановке
Вышеприведенный код является полностью рабочим кодом в операционной системе x86utm.
Поскольку H правильно определяет, что D, правильно смоделированный H, будет продолжать вызывать H(D,D), никогда не достигая своего собственного оператора «возврата», H прерывает моделирование D и возвращает 0 в main() в строке 011.
Наконец-то я достиг согласия по этому ключевому моменту:
H(D,D) правильно вычисляет отображение от своего входа к своему отклоненному состоянию на основании того, что H правильно предсказывает, что D, правильно смоделированный H, никогда не остановится.
Я оригинальный автор этой работы, и все, что вы найдете в Интернете по этому поводу, было написано мной.