14
$\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)

The topology of program termination.

Scott approach distance on metric spaces

Improve this question
$\endgroup$
8
  • 3
    $\begingroup$ Have a look at Eric Goubault's work. $\endgroup$
    – Martin Berger
    Commented Aug 1, 2018 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
    Commented Aug 1, 2018 at 16:55
  • $\begingroup$ @JoshuaGrochow do you think this is mitigated in the functional context (which is the one I am interested in)? $\endgroup$
    – user1868607
    Commented Aug 4, 2018 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
    Commented Aug 6, 2018 at 13:23
  • 1
    $\begingroup$ @Rodrigo It's true, Eric's work is mostly about concurrency. His key intuition is that deadlocks in concurrency correspond to holes in algebraic topology. But one needs to generalise algebraic topology to directed algebraic topology in order to make this work. I think the need for directedness doesn't go away in a purely sequential setting. Also: sequential computation is a special case of concurrency. $\endgroup$
    – Martin Berger
    Commented Aug 22, 2018 at 10:19

1 Answer 1

Reset to default
3
$\begingroup$

As someone somewhat familiar with termination analysis, I'd say that the techniques are only as ad-hoc as the programs they aim to prove termination of, which is to say very ad-hoc indeed.

The crucial approach to scaling such analyses is modularity which allows decomposing the problem into sub-problems. Indeed this usually consists in identifying cycle-like things, typically either cycles in the control flow graph or the call graph, and decomposing it along it's strongly connected components (SCCs). We have very efficient algorithms to do this. No algebraic topology really required here AFAIK.

This is the easy part. The hard part is then identifying variants for each SCC. Here again you can do things in a modular manner, but it's more subtle. The most relevant fields as far as I can tell are constraint solving, and in particular linear programing and general combinatorial principles often related to Ramsey theory. Again, I'm not sure whether algebraic topology really has a role to play.

I will mention a connection between algebraic topology and rewrite theory though, if that can sate your curiosity: there is a strong analogy between homological algebra and confluence of rewrite systems. In particular, there is a connection between simply connected spaces, and (nice) rewrite systems in which every critical pair is closed (which implies confluence).

Here's some nice notes by Yves Guiraud, Eric Hoffbeck, and Philippe Malbos.

And Here's some really nice slides by Gershom Bazerman. Following the links to those papers should get you somewhere.

Improve this answer
$\endgroup$

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