1
$\begingroup$

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 -> bar is hereditarily terminating if, for every hereditarily terminating x : foo, evaluating the expression f x always terminates and the final result is a hereditarily terminating value of type bar.

Remarks:

  • 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:

  1. What kind of proof techniques would be necessary to prove the above conjecture?

  2. 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.

$\endgroup$
  • 2
    $\begingroup$ Can't you just have the case where the stack is empty return a nonsense value? This case would never be reached so the program is still a correct implementation of Tarjan's algorithm. $\endgroup$ – Aaron Rotenberg Dec 29 '19 at 20:50
  • $\begingroup$ @AaronRotenberg Then the caller of the function has to handle the nonsensical value, even though it can't happen. Your suggestion is literally the nonsolution described in my final remark. $\endgroup$ – pyon Dec 29 '19 at 20:54
  • 2
    $\begingroup$ Why? You aren't proving correctness, just total termination, right? So your unreachable branch just has to return any value of the same type as the reachable branch, i.e. scc list with no option. You could return a list of a single SCC containing every vertex—it doesn't matter since it's unreachable. That would only be an issue if you also needed to return a proof object showing that the algorithm correctly computes the SCCs. $\endgroup$ – Aaron Rotenberg Dec 29 '19 at 23:56
  • 2
    $\begingroup$ If you're trying to do total functional programming with correctness proofs, you might want to just switch to a dependently typed language like Agda. Then you can prove that the unused branch really doesn't happen, within the syntax of the language. $\endgroup$ – Aaron Rotenberg Dec 30 '19 at 4:19
  • 1
    $\begingroup$ Agda has IO and state monads that are similar to Haskell's. Don't ask me for more details though, I've never actually used Agda. But if you know how Haskell monads work, I would start by Googling for the Agda equivalents. $\endgroup$ – Aaron Rotenberg Dec 30 '19 at 7:28

Your Answer

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

Browse other questions tagged or ask your own question.