13
$\begingroup$

I'm reading about various ways in which termination proofs of software verifiers are built: ad-hoc methods that detect recursions, term-rewriting, synthesis of lexicographic orderings...

From the ad-hoc methods I came with the following intuitive idea. Is it possible to formalize termination with algebraic topology? The idea would be:

  • look at termination as the problem of finding loops in the code of the program.

  • look these loops as a fundamental group at some origin (a point in the source code)

  • test whether this fundamental group is simply connected (implying that this node is terminating)

Of course both problems are undecidable (the second one being testing the simple connectedness) but it seems to me theoretically feasible.

Has this been done before? You find it is not feasible?

Resources I find interesting (feel free to add)

Progress Measures and Finite Arguments for Infinite Computations, page 3.

Power domains and predicate transformers: A topological view (if I ever get access to it)

$\endgroup$
  • 3
    $\begingroup$ Have a look at Eric Goubault's work. $\endgroup$ – Martin Berger Aug 1 '18 at 0:24
  • 1
    $\begingroup$ One issue to keep in mind is that a returning to the same line of code only implies an infinite loop if the state of the memory is the same both times. One of the tricky things about detecting non-halting behavior is that it can occur even when the state of the memory itself never loops. Whether or not this kind of behavior occurs in practice is, of course, a separate question. $\endgroup$ – Joshua Grochow Aug 1 '18 at 16:55
  • $\begingroup$ @JoshuaGrochow do you think this is mitigated in the functional context (which is the one I am interested in)? $\endgroup$ – Javier Aug 4 '18 at 23:18
  • 1
    $\begingroup$ @Rodrigo: no, it is not, since in the functional context the "state of the memory" is simply the values of the arguments of the recursive calls, which in many cases will never be identical in a non-terminating sequence (imagine a definition of factorial without a base case). $\endgroup$ – cody Aug 6 '18 at 13:23
  • $\begingroup$ @Rodrigo If you are interested in the Smyth approach that you link to, consider this introductory article for background. I think it's quite different to what you have in mind. $\endgroup$ – Martin Berger Aug 22 '18 at 9:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.