Существует ли “достаточно хорошее” решение для проблемы остановки?
Известно, что проблема остановки не может иметь определенного решения, то, которое a) возвращает true <==>, программа действительно останавливается и b) обрабатывает любой вход, но я задавался вопросом, существуют ли достаточно хорошие решения проблемы, которые могут, возможно, обработать определенные типы процессов выполнения программы отлично, или могут определить, когда это не может правильно решить проблему или ту, которая является правильной высокий процент времен и так далее....
Если так, насколько хороший они, и на какие идеи/ограничения они полагаются?
6 ответов
Обычный подход состоит в том, чтобы ограничить поведение программы эффективно вычисляемым ] алгоритм. Например, просто типизированное лямбда-исчисление можно использовать для определения того, что алгоритм всегда останавливается. Это означает, что просто типизированное лямбда-исчисление не является полным по Тьюрингу, но все же достаточно мощно, чтобы представлять множество интересных алгоритмов.
Один из способов доказать остановку цикла - определить некоторую целочисленную переменную (не обязательно явно в программе), которая всегда уменьшается при каждом выполнении цикла, и что как только эта переменная станет меньше нуля, цикл завершится. Мы можем назвать эту переменную вариантом цикла.
Рассмотрим следующий небольшой фрагмент:
var x := 20;
while (x >= 0) {
x := x - 1
}
Здесь мы видим, что x уменьшается каждый раз при выполнении цикла, и что цикл завершится, когда x <0 (очевидно, это не очень строго, но вы получаете идея). Следовательно, мы можем использовать x как вариант.
А как насчет более сложного примера? Рассмотрим конечный список целых чисел L = [L [0], L [1], ..., L [n]]. in (L, x) истинно, если x является членом L. Теперь рассмотрим следующую программу:
var x := 0;
while (in(L, x)) {
x := x + 1
}
Она будет искать натуральные числа (0, 1, 2, ...), и остановиться, как только он обнаружит значение для x, которого нет в L. Итак, как мы докажем, что это завершается? В L должно быть максимальное значение - назовем его max (L). Затем мы можем определить наш вариант как max (L) - x . Чтобы доказать прекращение, мы сначала должны доказать, что max (L) - x всегда убывает - это не слишком сложно, поскольку мы можем доказать, что x всегда увеличивается. Затем мы должны доказать, что цикл завершится, когда max (L) - x <0 . Если max (L) - x <0 , то max (L)
те, которые могут отлично обрабатывать определенные типы программных потоков
Это легко, и чем легче, тем более узкими являются ваши «определенные типы». Примитивный пример: решите, завершается ли следующий фрагмент кода для произвольных начальных значений x:
void run(int x)
{
while(x != 0)
{
x = x > 0 ? x-2 : x+2;
}
}
Решение короче, чем сам код.
или способны определить, когда это не может правильно решить проблему
Опять же просто: возьмите программу выше,заставьте его ответить «нет», когда программа не соответствует фиксированной узкой схеме.
или тот, который является правильным в высоком проценте раз
Как вы определяете «высокий» процент над бесконечным набором возможных входов?
См. статьи, связанные с проектом Terminator:
http://research.microsoft.com/en-us/um/cambridge/projects/terminator/
Иногда очевидно, остановится машина или нет, даже если он очень большой. Как только вы определите шаблон, например наличие переменной «обратный отсчет», вы можете написать небольшую машину, которая будет работать на любой машине, у которой она есть. Это бесконечное семейство, но ничтожно малая часть всех возможных машин. Большинство машин, написанных человеком, имеют очень простое поведение для своего размера, поэтому меня не слишком удивит, если многие из них могут быть решены в практическом времени / пространстве, но я понятия не имею, как это измерить.
Чтобы дать вам представление о том, насколько сложна проблема «насколько они хороши», вот вопрос, представляющий большой теоретический интерес: для данного размера N, сколько машин размера N останавливаются? Это невычислимо (потому что машина, которая могла бы вычислить, могла бы использоваться для решения проблемы остановки) и неизвестна для N> 4.
Да, просто сделайте пространство состояний конечным, и это (теоретически) возможно для всех входов. (Просто переберите все возможности.)
Теоретически это возможно для любой программы, работающей на реальном компьютере. (Возможно, вам придется использовать компьютер с большим объемом ОЗУ, чем тот, на котором должна выполняться программа, для проведения анализа. И, конечно, анализ займет невероятно много времени.)
Возможно, вы захотите что-то более практичное. В этом случае подумайте о языках. Проблема синтаксической правильности / неправильности может быть решена довольно быстро (в зависимости от типа языка и длины ввода), хотя существует бесконечно много программ, которые вы можете предоставить в качестве ввода. ( Примечание: Мы не говорим о выполнении входной программы, а просто определяем, синтаксически она правильна или нет.)