про "гарантированноую завершаемость" исчо;
Там срачик все продожается - меня уверяют что это "первое приближение к решению задачи". А типа что "неразрешимые задачи решаются" это "переформулирвали задачу чтобы обойти ограничение".
По мне так - это вообще не приближение - а скорее приличный шаг в сторону от реальной постановки задачи в большинстве случаев. И в подавляющем большинстве случаев решения неразрешимых алгоритмически задач ничего не "переформулируют", а просто на вопрос разрешимости забивают - поскольку он изначально в формулировку задачи не входил и его добавление только усложняет дело без всякой пользы.
Потому как реально почти всегда нужна не "программа, которая когда-нибудь (сколь угодно когда-нибудь) гарантировано решит задачу во всех случаях", а "программа котороая скорее всего решит задачу за разумное время в большинстве практически интересных случаев" (есть и довольно распространенные исключения в заменой "скорее всего для большинства случаев" на "может быть когда-нибудь решит хоть для какого-то" (многие схемотехнические компиляторы кстати именно так себя раньше вели) или "гарантированно хоть что-то выдаст за разумное время для всех случаев"*
Задач в которых прямо востребована наука про разрешимость практически не бывает. Вот как раз про сложность (но там обычно уже квадратичная малоприемлема) - очень даже востребована.
Вообще задачи про доказательство "хороших свойств" программ - наука неплохо разработанная. Вот только завершаемость там идет с приоритетом не очень большим - скорее потому что частичная функция обычно значит ошибку в коде. Полезная диагностика, которую программиста полезно заставить оверрайдить явно - если он действительно этого хотел**.
*) Последнее на вид близко к "разрешимости" - но на практике копается как раз в развитии науки как программировать реальные задачи на тьюринговски-неполных языках - вполне тоже можно кстати. Вот там да - приходится переделывать - но не под "разрешимость", а под "верифицируемую автоматически разрешимость"
**) При этом, замечу, что автоматическая верификация кода на завершаемость представляет вариацию на тему "проблемы остановки" - коя тоже формально неразрешима ;)))
По мне так - это вообще не приближение - а скорее приличный шаг в сторону от реальной постановки задачи в большинстве случаев. И в подавляющем большинстве случаев решения неразрешимых алгоритмически задач ничего не "переформулируют", а просто на вопрос разрешимости забивают - поскольку он изначально в формулировку задачи не входил и его добавление только усложняет дело без всякой пользы.
Потому как реально почти всегда нужна не "программа, которая когда-нибудь (сколь угодно когда-нибудь) гарантировано решит задачу во всех случаях", а "программа котороая скорее всего решит задачу за разумное время в большинстве практически интересных случаев" (есть и довольно распространенные исключения в заменой "скорее всего для большинства случаев" на "может быть когда-нибудь решит хоть для какого-то" (многие схемотехнические компиляторы кстати именно так себя раньше вели) или "гарантированно хоть что-то выдаст за разумное время для всех случаев"*
Задач в которых прямо востребована наука про разрешимость практически не бывает. Вот как раз про сложность (но там обычно уже квадратичная малоприемлема) - очень даже востребована.
Вообще задачи про доказательство "хороших свойств" программ - наука неплохо разработанная. Вот только завершаемость там идет с приоритетом не очень большим - скорее потому что частичная функция обычно значит ошибку в коде. Полезная диагностика, которую программиста полезно заставить оверрайдить явно - если он действительно этого хотел**.
*) Последнее на вид близко к "разрешимости" - но на практике копается как раз в развитии науки как программировать реальные задачи на тьюринговски-неполных языках - вполне тоже можно кстати. Вот там да - приходится переделывать - но не под "разрешимость", а под "верифицируемую автоматически разрешимость"
**) При этом, замечу, что автоматическая верификация кода на завершаемость представляет вариацию на тему "проблемы остановки" - коя тоже формально неразрешима ;)))