Yes, I know it's uncomputable in the general case. What I want to know is what special cases have been solved, and if there is work ongoing on finding or developing more of them.
To be a little more explicit about the sort of thing I'm looking for, total functional language compilers have to approximate the halting problem, proving that your source code terminates or saying it can't thus prove it. Idris, as far as I can tell, just uses a "one argument must be structurally smaller on each recursive call" primitive-recursion checker*; Isabelle is more sophisticated, with
datatype rosetree = Rose "'a rosetree list" primrec rosemap :: "('a => 'b) => 'a rosetree => 'b rosetree" where "rosemap f (Rose as) = Rose (map (rosemap f) as)"
compiling fine despite the intermediate
map on the recursive calls. Isabelle's
fun mechanism seems even more powerful in terms of proving termination (although I can't think of a short, simple example for that off the top of my head).
Basically: how do these work? Are there papers or textbooks about the algorithms involved somewhere? Is finding heuristics for the halting problem a current research subject?
*If I'm wrong about this, please do let me know about that, too.