<p>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.</p>
<p>The crucial approach to scaling such analyses is <em>modularity</em> which allows decomposing the problem into sub-problems. Indeed this usually consists in identifying cycle-like things, typically either cycles in the <strong>control flow graph</strong> or the <strong>call graph</strong>, and decomposing it along it's <strong>strongly connected components</strong> (SCCs). We have very efficient algorithms to do this. No algebraic topology really required here AFAIK.</p>
<p>This is the easy part. The hard part is then identifying <strong>variants</strong> 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 <a href="https://en.wikipedia.org/wiki/Linear_programming" rel="nofollow noreferrer">linear programing</a> and general combinatorial principles often related to <a href="https://en.wikipedia.org/wiki/Ramsey_theory" rel="nofollow noreferrer">Ramsey theory</a>. Again, I'm not sure whether algebraic topology really has a role to play.</p>
<hr />
<p>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 <strong>confluence</strong> 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).</p>
<p><a href="http://www.nue.ie.niigata-u.ac.jp/toyama/iwc2014/GHM.pdf" rel="nofollow noreferrer">Here's</a> some nice notes by Yves Guiraud, Eric Hoffbeck, and Philippe Malbos.</p>
<p>And <a href="https://gbaz.github.io/slides/pwl-homology-slides.pdf" rel="nofollow noreferrer">Here's</a> some really nice slides by Gershom Bazerman. Following the links to those papers should get you somewhere.</p>

CC BY-SA 4.0
2020-09-23T22:29:25.420Z
2020-09-23T22:29:25.420Z
cody
<p>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...</p>
<p>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:</p>
<ul>
<li><p>look at termination as the problem of finding loops in the code of the program.</p>
</li>
<li><p>look these loops as a fundamental group at some origin (a point in the source code)</p>
</li>
<li><p>test whether this fundamental group is simply connected (implying that this node is terminating)</p>
</li>
</ul>
<p>Of course both problems are undecidable (the second one being testing the simple connectedness) but it seems to me theoretically feasible.</p>
<p>Has this been done before? You find it is not feasible?</p>
<p><strong>Resources I find interesting (feel free to add)</strong></p>
<p><a href="https://books.google.ch/books?id=-pQ-m6sfE4gC&amp;pg=PA3&amp;dq=topology%20program%20termination&amp;hl=es&amp;sa=X&amp;ved=0ahUKEwiXgozevv_cAhXHJZoKHYzaBrAQ6AEIUzAG#v=onepage&amp;q&amp;f=false" rel="nofollow noreferrer">Progress Measures and Finite Arguments for Infinite Computations</a>, page 3.</p>
<p><a href="https://link.springer.com/chapter/10.1007/BFb0036946" rel="nofollow noreferrer">Power domains and predicate transformers: A topological view</a> (if I ever get access to it)</p>
<p><a href="https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&amp;arnumber=5128" rel="nofollow noreferrer">The topology of program termination.</a></p>
<p><a href="https://arxiv.org/pdf/1610.06341.pdf" rel="nofollow noreferrer">Scott approach distance on metric spaces</a></p>

CC BY-SA 4.0
2018-08-01T00:24:50.230Z
Have a look at [Eric Goubault](http://www.lix.polytechnique.fr/Labo/Eric.Goubault)'s work.
Martin Berger
CC BY-SA 4.0
2018-08-01T16:55:18.927Z
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.
Joshua Grochow
CC BY-SA 4.0
2018-08-04T23:18:00.160Z
@JoshuaGrochow do you think this is mitigated in the functional context (which is the one I am interested in)?
user1868607
CC BY-SA 4.0
2018-08-06T13:23:59.440Z
@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).
cody
CC BY-SA 4.0
2018-08-22T09:37:13.340Z
@Rodrigo If you are interested in the Smyth approach that you link to, consider [this introductory article](https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf) for background. I think it's quite different to what you have in mind.
Martin Berger
CC BY-SA 4.0
2018-08-22T10:06:33.973Z
thank you, @MartinBerger, the problem i see with Eric Goubault's work is that it is mostly related with concurrency. i guess i will need adapt techniques from other contexts. since i'm not an expert, i'm sure many references that i note may not be even remotely related for what i want....
user1868607
CC BY-SA 4.0
2018-08-22T10:19:59.703Z
@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.
Martin Berger
CC BY-SA 4.0
2020-09-23T11:25:39.663Z
I agree with @MartinBerger -- (a) termination is a liveness property, and (b) if you do any abstraction of the state space of a program at all, your abstraction of a sequential program will become a concurrent program.
Neel Krishnaswami
<reference-request><soft-question><formal-methods><algebraic-topology>
Algebraic topology for termination proofs
user1868607
# Algebraic topology for termination proofs

(Asked by: username_0 on 2018-08-01)

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](https://books.google.ch/books?id=-pQ-m6sfE4gC&pg=PA3&dq=topology%20program%20termination&hl=es&sa=X&ved=0ahUKEwiXgozevv_cAhXHJZoKHYzaBrAQ6AEIUzAG#v=onepage&q&f=false), page 3.

[Power domains and predicate transformers: A topological view](https://link.springer.com/chapter/10.1007/BFb0036946) (if I ever get access to it)

[The topology of program termination.](https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=5128)

[Scott approach distance on metric spaces](https://arxiv.org/pdf/1610.06341.pdf)

**Tags:** reference-request, soft-question, formal-methods, algebraic-topology
> **Comments:**
> **username_1**: Have a look at [Eric Goubault](http://www.lix.polytechnique.fr/Labo/Eric.Goubault)'s work.  
> **username_2**: 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.  
> **username_0**: @JoshuaGrochow do you think this is mitigated in the functional context (which is the one I am interested in)?  
> **username_3**: @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).  
> **username_1**: @Rodrigo If you are interested in the Smyth approach that you link to, consider [this introductory article](https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf) for background. I think it's quite different to what you have in mind.  
> **username_0**: thank you, @MartinBerger, the problem i see with Eric Goubault's work is that it is mostly related with concurrency. i guess i will need adapt techniques from other contexts. since i'm not an expert, i'm sure many references that i note may not be even remotely related for what i want....  
> **username_1**: @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.  
> **username_4**: I agree with @MartinBerger -- (a) termination is a liveness property, and (b) if you do any abstraction of the state space of a program at all, your abstraction of a sequential program will become a concurrent program.  

---

## 1 answers

### Answer by username_3 on 2020-09-23. Score: 4 | Accepted answer

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](https://en.wikipedia.org/wiki/Linear_programming) and general combinatorial principles often related to [Ramsey theory](https://en.wikipedia.org/wiki/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](http://www.nue.ie.niigata-u.ac.jp/toyama/iwc2014/GHM.pdf) some nice notes by Yves Guiraud, Eric Hoffbeck, and Philippe Malbos.

And [Here's](https://gbaz.github.io/slides/pwl-homology-slides.pdf) some really nice slides by Gershom Bazerman. Following the links to those papers should get you somewhere.


---

