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
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
- Checks whether
- Raises an exception if the stack is empty.
- 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:
Am I overlooking some way in which I can communicate to the compiler the fact that
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.