2
$\begingroup$

I asked this question on Stack Overflow, but I have not obtained an actual answer to the question.


Tarjan's strongly connected components algorithm is stunningly beautiful, and inexpressible in a literal way in any programming language that I know of.

Allow me to refer to the pseudocode in the Wikipedia article. The problem is with the code that pops the strongly connected component we just found from the auxiliary stack:

// If v is a root node, pop the stack and generate an SCC
if (v.lowlink = v.index) then
  start a new strongly connected component
  repeat
    w := S.pop()
    w.onStack := false
    add w to current strongly connected component
  while (w != v)
  output the current strongly connected component
end if

The instruction w := S.pop() is unsafe, because, as far as the programming language's static semantics knows or cares, S could be empty. (Of course, a human programmer can easily tell that S will not be empty, because we are only popping S until we find v, which is initially contained in S.) Hence, a compiler for a memory safe language will emit code that

  1. Checks whether S is empty.
  2. Raises an exception if the stack is empty.
  3. Pops and returns the stack's top element otherwise.

I am not too worried about the (negligible) performance impact of the useless test of emptiness. (Thus, “rewrite it in a memory-unsafe language” is not an answer.) However, I am concerned with the fact I cannot communicate an important invariant in a way that the compiler can treat as actionable information.

My questions are:

  1. Am I overlooking some way in which I can communicate to the compiler the fact that S contains v?

  2. If the answer to the first question is negative, is there a proof that I can't communicate this fact to the compiler?


EDIT: I am starting to suspect that the key to solving this conundrum is to use the same tricks I used to work around the lack of polymorphic recursion in SML without introducing redundant safety checks, but I need to properly write this down.

$\endgroup$
  • $\begingroup$ Have you considered headMay :: [a] -> Maybe a in language such as Haskell? $\endgroup$ – Apiwat Chantawibul Oct 25 '19 at 14:59
  • $\begingroup$ @ApiwatChantawibul: How exactly does that help? $\endgroup$ – pyon Oct 25 '19 at 16:04
  • 2
    $\begingroup$ I think I initially misunderstand your question. Let me try again. So, it's not that you want to communicate to compiler the possibility of pop failing --- a situation which Maybe type would help. Rather, you want to communicate to compiler that using pop in that situation actually has no possibility of failing. $\endgroup$ – Apiwat Chantawibul Oct 25 '19 at 16:35
  • $\begingroup$ How about defining a new stack data type which can not become empty then? OR if that doesn't help, look into dependent type which allows for stack type depending on an integer value denoting its size? $\endgroup$ – Apiwat Chantawibul Oct 25 '19 at 16:54
  • 2
    $\begingroup$ Perhaps this is useful: Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle $\endgroup$ – rici Oct 27 '19 at 4:45
4
$\begingroup$

There will always be situations where we can see there is a complex invariant but the compiler cannot derive it. Type systems are sound but not complete: not all invariants can be expressed in the type system. So this isn't something specific to Tarjan's algorithm; it is a general fact of life when working in a type system -- sometimes the compiler will insert type checks that the programmer can tell won't be necessary, and similarly, as a programmer you might need to insert type checks that you can tell won't be necessary.

$\endgroup$
  • $\begingroup$ This is a perfectly fine engineering answer. But, as a mathematician, I'd like to determine formally the limits of the type system's expressive power. So I want a proof that this invariant is inexpressible in a conventional type system, like Java's or ML's or Haskell's. Unfortunately, as a rather traditional mathematician, I'm not proficient enough in type theory to carry out the proof myself, so perhaps a computer scientist could help me? $\endgroup$ – pyon Oct 25 '19 at 17:17
  • $\begingroup$ I'm wondering about this myself. There is probably a formal proof out there along the lines of "We could let compiler check any (propositions/types) at compile time, but that would make type-checker turing complete". $\endgroup$ – Apiwat Chantawibul Oct 26 '19 at 0:42
  • 1
    $\begingroup$ @ApiwatChantawibul: In formal logic, there are results like “formal system S is not strong enough to prove theorem T”. Results like “type system S cannot verify invariant T” should be completely analogous. (Note, however, that I do not want to verify everything about Tarjan's SCC algorithm. I want to verify just enough to elide the redundant nonemptiness check.) $\endgroup$ – pyon Oct 26 '19 at 4:26
3
$\begingroup$

By a happy coincidence, people (Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz and Laurent Thery) have completed formally verified implementations of Tarjan's algorithm in various formal systems!

The paper, titled "Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle", can be found, e.g. here.

One step of proving correctness in these systems is necessarily excluding the exceptions and undefined behavior you mention, so the article should be very relevant!

The Why3 implementation is probably the closest one to the Wikipedia pseudo-code.

$\endgroup$
  • $\begingroup$ 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). $\endgroup$ – pyon Oct 27 '19 at 18:59
  • 1
    $\begingroup$ 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. $\endgroup$ – cody Oct 29 '19 at 20:30
  • 1
    $\begingroup$ However, simply proving termination and completeness would be much easier than proving full correctness of such an algorithm, of course. $\endgroup$ – cody Oct 29 '19 at 20:31
  • $\begingroup$ 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 $\endgroup$ – pyon Oct 29 '19 at 21:37
  • 1
    $\begingroup$ 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 $\endgroup$ – pyon Oct 29 '19 at 23:18

Your Answer

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

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