Timeline for Implementing Tarjan's strongly connected components algorithm in a language without exceptions or undefined behavior
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 30, 2019 at 11:50 | comment | added | cody | Fair point, I guess there's a log factor in the time as well. | |
| Oct 29, 2019 at 23:18 | comment | added | isekaijin | This is done one time each time the node is the target of an edge, for a subtotal of $O(E)$ time. Furthermore, the edges are reached from their sources, for a total of $O(V + E)$ time. If the modification is performed in $O(\log V)$ time instead of $O(1)$ time, then the whole algorithm runs in $O(V + E \log V)$ time. 2/2 | |
| Oct 29, 2019 at 21:37 | comment | added | isekaijin | I don't see how the time complexity can be the same in an imperative and a purely functional implementation. The algorithm relies on the ability to modify information associated to an arbitrary node in $O(1)$ time, either by storing it in the node itself, or by using, say, a hash table. 1/2 | |
| Oct 29, 2019 at 20:31 | comment | added | cody | However, simply proving termination and completeness would be much easier than proving full correctness of such an algorithm, of course. | |
| Oct 29, 2019 at 20:30 | comment | added | cody | These really are implementations, though you may need to extract them in order to run them. Isabelle I think extracts to SML, and Coq to Ocaml (not sure about Why3). The implementation is functional, though I'm pretty sure that the time complexity is identical, and the space complexity is identical up to some log factor. They do mention in the conclusion that future work would be extending the proof to imperative implementations. | |
| Oct 27, 2019 at 18:59 | comment | added | isekaijin |
Are these really implementations, in the sense that you can run them and they have the specified complexity? I have only skimmed the paper, but I could not find any explicit uses of imperative mutation. While the Wikipedia article's presentation of the algorithm contains unnecessary imperative parts (e.g., after rewriting strongconnect to be tail recursive, we can afford to manage the auxiliary stack S in a purely functional manner), other parts are imperative in an essential way (e.g., updating the lowlink field of each node).
|
|
| Oct 27, 2019 at 15:56 | history | answered | cody | CC BY-SA 4.0 |