Есть ли разумное понятие алгоритма аппроксимации для неразрешимой задачи?

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

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

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

В случае проблемы остановки ответ «еще нет». Причина заключается в том, что стандартный логический метод для определения того, насколько трудным является доказательство завершения программы (например, порядковый анализ), имеет тенденцию терять слишком много комбинаторной и / или теоретико-числовой структуры.

Уровень техники в практическом анализе завершения императивных программ - это то, что называется «синтезом ранговых функций» (у Байрона Кука есть готовящаяся книга «Проверка завершения программы» на эту тему из CUP). Идея состоит в том, чтобы вычислить линейную функцию значений переменных программы сейчас и на предыдущем шаге, которая служит метрикой завершения. (Одна из замечательных особенностей этого метода заключается в том, что он использует лемму Фаркаша, которая дает четкую геометрическую точку зрения на происходящее.) Интересно то, что инструменты, построенные на этом подходе, могут делать такие вещи, как показ завершения функции Аккермана (который не является примитивно-рекурсивным), но вы можете создавать не вложенные циклы while, которые могут их победить (для которых требуется чтобы показать завершение).$\omega$

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

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

Из запоминающегося разговора человека, который реализовал алгоритм, который решает неразрешимую проблему: «На все входы, которые я пробовал, уходит 2-3 секунды».

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

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

Учитывая оптимальную машину и целое число , можете ли вы дать правильный ответ на проблему остановки для всех программ размером , за исключением дроби , для сколь угодно малых ? В 70-х Линч доказал, что нет, вы не можете . Несколько лет назад мы с коллегами доказали более сильную версию этого результата, позволяя алгоритму совершать ошибки или не останавливаться на небольшой части входных данных или требуя только вероятностного приближения с вероятностью (позволяя алгоритму подбрасывать монеты).n < n ϵ ϵ p > $M$$n$$\lt n$$\epsilon$$\epsilon$$p\gt 0$

Попутно мы доказали кучу интересных вещей о свойствах последовательности , где - это соотношение программ размера которые останавливаются (оказывается, эта последовательность очень странная ). Если приведенный выше документ слишком плотный, вы можете посмотреть мои слайды, когда мы представили результаты на ICALP.ρ n < $\rho_n$$\rho_n$$<n$