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.

  • 4
    $\begingroup$ 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? $\endgroup$ – Raphael Jun 27 '18 at 20:35
  • $\begingroup$ @Raphael My apologies. What should I do, then? Edit to a more focused question, make a new question, close it in sorrow? $\endgroup$ – Zyzzyva Jun 28 '18 at 14:55
  • $\begingroup$ If you can make your question more focused, definitely edit! $\endgroup$ – Raphael Jun 28 '18 at 16:09

The question as asked is indeed very broad. I give a brief answer here: What are some comparative studies on program termination verification tools?, but that really barely scratches the surface.

I do have several remarks:

  • In general, once must distinguish between whole program analyses, which are powerful, but do not scale very well for realistic development, and modular analyses which are weaker, but have hope of being integrated in a development environment. Isabelle and Idris both take this approach. As a side note, I'm not sure if this Fuhs et al paper corresponds to the "out of the box" termination check for Isabelle, but it might be enlightening in terms of what the state of the art is.

  • Termination of higher-order typed programs is difficult, because it involves subtle interactions between the type system features, the inductive types involved, and the "guard condition" required for function definitions. The more complicated the termination check, the less trustworthy the system, since consistency depends on it! These slides by Barras go into some of the nasty details for the Coq system.

  • Termination for higher-order systems with side effects (references) is particularly nasty. In particular, types are not enough anymore, even in the absence of recursion, see e.g. Landin's knot.


Not the answer you're looking for? Browse other questions tagged or ask your own question.