Кратко и по делу.
Определения (формально через языки и машины Тьюринга):
- Решаемая (разрешимая) задача: пусть алфавит $\Sigma$ и язык $L\subseteq {\Sigma }^{\ast }$. Язык $L$ разрешим, если существует машина Тьюринга $M$ такая, что для любого входа $x\in {\Sigma }^{\ast }$ $M$ останавливается и
$$M\text{принимает}x⟺x\in L.$$ То есть алгоритм всегда завершает работу и правильно отвечает «да/нет».
- Полуразрешимая (рекурсивно перечислимая, r.e.) задача: язык $L$ полуразрешим, если существует машина Тьюринга $M$, которая для любого $x\in L$ останавливается и принимает $x$, а для $x\notin L$ либо отвергает, либо никогда не останавливается. Формально:
$$\exists M\forall x(x\in L\Rightarrow M\text{останавливается и принимает}x).$$ Полуразрешимые языки можно перечислять (генерировать все элементы).
- Неразрешимая задача: язык $L$ неразрешим, если не существует машины Тьюринга, решающей его во всех случаях (т.е. не выполняется определение разрешимости). Отношения между классами:
$$\{\text{разрешимые}\}\subseteq \{\text{полуразрешимые}\},$$ и
$$L\text{разрешим}⟺L\text{и}\overline{L}\text{полуразрешимы}.$$
Классический пример неразрешимой задачи — задача останова (Halting problem). Определим
$$\mathrm{HALT}=\{⟨M,x⟩\mid \text{машина}M\text{останавливается на входе}x\}.$$ - $\mathrm{HALT}$ полуразрешима: симулируя $M$ на $x$ пошагово, если симуляция останавливается — принимаем.
- $\mathrm{HALT}$ неразрешима: классическое доказательство диагонализацией / редукцией. Например, если бы существовал решатель для множества ${\mathrm{A}}_{TM}=\{⟨M,w⟩\mid M\text{принимает}w\}$, то можно было бы сконструировать машину, создающую логическое противоречие при подаче на себя самой (стандартная диагональная конструкция), значит такого решателя нет; из этого вытекает неразрешимость $\mathrm{HALT}$.
Практические последствия для разработчиков ПО (кратко):
- Нельзя написать универсальный инструмент, который для любого входного программы и любого свойства всегда за конечное время даст правильный ответ (например, «закончится ли программа», «эквивалентны ли две произвольные программы», «имеется ли ошибка во всех выполнениях»).
- На практике используют приближения и ограничения:
- статический анализ с пере- или недоопределениями: sound (без ложных отрицаний, но много ложных срабатываний) или incomplete (может пропустить ошибки);
- ограничение класса программ (декартова глубина раскладывания, ограничение памяти/циклов, язык с ограниченной семантикой), где проблемы становятся разрешимыми;
- эвристики, таймауты, символьное исполнение и bounded model checking (проверка в пределах заданной глубины);
- ночная/выполняемая проверка и мониторинг в рантайме;
- использование формальных методов и интерактивных доказательных помощников для конкретных критичных модулей.
- Теорема Райса: любое нетривиальное семантическое свойство программ («имеет ли программа свойство P, зависящее только от её поведения») неразрешимо в общем случае — поэтому автоматические проверки таких свойств всегда требуют приближений или ограничений.
Вывод: различие — в требовании прекращения работы и точности ответа; многие полезные вопросы о программах в общем виде неразрешимы, потому инструменты анализа ПО строятся на приближениях, ограничениях или интерактивной верификации.