История изменений
Исправление quasimoto, (текущая версия) :
шутить изволите?
Вполне серьёзно.
Если ты видел — IDEA для скалы рисует спирали для рекурсивных функций и кружки для хвостовой рекурсии. У меня как-то был баг — JVM падала в SO, так как в рекурсивный вызов не то передавалось и функция зависала вплоть до SO (а ведь может и просто повиснуть). Вот пусть рисует что-нибудь для гарантированно завершаемых функций без исключений :)
Касательно проблемы останова — есть класс функций для которых она разрешима (где-то между PR и R), в этом классе достаточно много практически-полезных функций (ещё нужно вспомнить что циклы можно видеть как сахар над рекурсией, так что их анализ сводится к тому же анализу последней), в остальном — false negatives, то есть функция вне этого класса может быть тотальной, но такой разрешимый алгоритм этого знать не может (так как в общем случае для R это неразрешимая проблема), поэтому просто отбрасывает её вместе с остальными незавершаемыми функциями.
Кроме того, если помогать компилятору, то можно доказать завершаемость чего-угодно из R, уже без false negatives (well-founded recursion).
Исходная версия quasimoto, :
шутить изволите?
Вполне серьёзно.
Если ты видел — IDEA для скалы рисует спирали для рекурсивных функций и кружки для хвостовой рекурсии. У меня как-то был баг — JVM падала в SO, так как в рекурсивный вызов не то передавалось и функция зависала вплоть до SO (а ведь может и просто повиснуть). Вот пусть рисует что-нибудь для гарантированно завершаемых функций без исключений :)
Касательно проблемы останова — есть класс функций для которых она разрешима (где-то между PR и R), в этом классе достаточно много практически-полезных функций (ещё нужно вспомнить что циклы можно видеть как сахар над рекурсией, так что их анализ сводится к тому же анализу последней), в остальном — false negatives, то есть функция вне этого класса может быть тотальной, но такой разрешимый алгоритм этого знать не может (так как в общем случае для R это неразрешимая проблема), поэтому просто отбрасывает её вместе с остальными незавершаемыми функциями.