# What is the current state of the art in solving the halting problem? [closed]

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?

## closed as too broad by rici, Evil, Pål GD, Discrete lizard♦, vonbrandJul 6 '18 at 15:16

Please edit the question to limit it to a specific problem with enough detail to identify an adequate answer. Avoid asking multiple distinct questions at once. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• Your titular question is way too broad. The more narrow inquiry in the question body still is, imho: you are asking for a literature survey. Community votes, please: too broad? – Raphael Jun 27 '18 at 20:35
• @Raphael My apologies. What should I do, then? Edit to a more focused question, make a new question, close it in sorrow? – Zyzzyva Jun 28 '18 at 14:55
• If you can make your question more focused, definitely edit! – Raphael Jun 28 '18 at 16:09