I am taking my question here from there. Consider the following scenario:
You are given a fixed programming language with no nonlocal control flow constructs. In particular, the language does not have
- Exceptions, first-class continuations, etc.
- Assertions, in the sense of “runtime tests that crash the program if they fail”.
Remark: An example of such a language could be Standard ML, minus the ability to raise exceptions. Inexhaustive pattern matching implicitly raises the
Match exception, so it is also ruled out.
Moreover, you are forced to program using only hereditarily terminating values. Inductively, we define hereditarily terminating values as follows:
- Data constructors (including numeric and string literals) are hereditarily terminating.
- Applications of data constructors to hereditarily terminating arguments are hereditarily terminating.
- A procedure
f : foo -> baris hereditarily terminating if, for every hereditarily terminating
x : foo, evaluating the expression
f xalways terminates and the final result is a hereditarily terminating value of type
Hereditarily terminating procedures need not be pure. In particular, they may read from or write to a mutable store.
A procedure is more than just the function it computes. In particular, functions do not have an intrinsic asymptotic time or space complexity, but procedures do.
Hereditarily terminating procedures formalize my intuitive idea of “program that is amenable to local reasoning”. Thus, I am interested in what useful programs one can write using only hereditarily terminating procedures. At the most basic level, programs are built out of algorithms, so I want to investigate what algorithms are expressible using only hereditarily terminating procedures.
Unfortunately, I have hit an expressiveness ceiling much earlier than I expected. No matter how hard I tried, I could not implement Tarjan's algorithm for finding the strongly connected components of a directed graph.
Recall that Tarjan's algorithm performs a depth-first search of the graph. In addition to the usual depth-first search stack, the algorithm uses an auxiliary stack to store the nodes whose strongly connected components have not been completely explored yet. Eventually, every node in the current strongly connected component will be explored, and we will have to pop them from the auxiliary stack. This is the step I am having trouble with: The loop that pops the nodes from the stack terminates when a given reference node has been found. But, as far as the type checker can tell, the reference node could not be in the stack at all! This results in an extra control flow path in which the stack is empty after popping everything from it and still not finding the reference node. At this point, the only thing the algorithm can do is fail.
This leads to the following...
Conjecture: Tarjan's algorithm cannot be implemented in Standard ML using only hereditarily terminating procedures.
My questions are:
What kind of proof techniques would be necessary to prove the above conjecture?
What is the bare minimum type system in which Tarjan's algorithm can be expressed as a hereditarily terminating program? That is, what is the bare minimum type system that can “understand” that the auxiliary stack is guaranteed to contain the reference node, and thus will not add a control flow path in which the auxiliary stack is empty before the reference node has been found?
Final remark: It is possible to rewrite this program inside a partiality monad. Then every procedure would be a Kleisli arrow. Instead of
val tarjan : graph -> scc list
we would have something like
val tarjan : graph -> scc list option
But, obviously, this defeats the point of the exercise, which is precisely to take out the procedure out of the implicit partiality monad present in most programming languages. So this does not count as a solution.