The Immerman–Szelepcsényi Theorem is the statement that NL=co-NL. To make a long story short, saying that a problem is in NL is to say that the problem is equivalent (logspace reducible) to figuring out whether there is a path in a directed graph from one node to another. It is easy to see that a non-deterministic machine can easily guess a path from one node to another if there is one, simply by walking along adjacent vertices. Also, this walk only requires the algorithm to remember only the current vertex (and also a count of how many steps it has proceeded). But, can something similar be done to check the absence of a path? The answer is yes, and this is what we will show in this note.
To demonstrate how this is possible, one needs to produce a non-deterministic algorithm. However, non-deterministic algorithms are hard to formalize in usual programming paradigms, since programmers do not (typically) wish to escape the comfort-zone of real world deterministic models. However, the monad-aware programmer can formalize such an algorithm by suitably defining a nondeterminism monad. See Wikipedia's page.
Informally speaking, the non-determistic paradigm of computation is one where the computer is free to ("non-deterministically") choose an arbitrary path of computation at some points in a program.
To model this with haskell, we write non-determinstic values of type
[a], in order to denote "a bunch of possibilities of
a". But, let us mask this and declare the following type synnonym:
To steal an example from Learn You a Haskell, let us try to model where a possible chess player could take his knight to. First, we will denote their position on the board by the following:
Then, we try to see how we can represent the moves of the knight.
1 2 3 4 5 6 7 8
But, let us also impose the restriction that
(c', r') must also be a position on the chessboard. To do so, we import
guard :: Alternative f => Bool -> f () from
Control.Monad. For our purposes, the
guard is a way to reject a computation path which we deem to be illegal. (A more comprehensive explanation can be found in the Haskell Wikibook). We will indeed use this quiet liberally in our actual proof in order to block computation paths which do not witness what we are looking for. Getting back to the
moveKnight example, we modify the above code to say:
1 2 3 4 5 6 7
We should note that the real power of this notation is that we may compose nondeterministic computations sequentially to form larger nondeterministic computations. Here is how we can non-deterministically calculate where the knight would be in 3 moves.
1 2 3 4 5
To demonstrate this idea further, let us see how we can nondeterministically find a satisfying assignment for boolean functions. For simplicity, let us look at the case where there are only three variables in the function.
1 2 3 4 5 6 7
sat3 f would give us a list of assignments which satisfy
f and would be empty if there are none.
To model the proof of Immerman–Szelepcsényi theorem, we would want to think of machines with several integer counters which can be updated, incremented and read from. This sort of programs are known as stateful programs because updates of the states are not immediately functional operations. We model them with the following type
We need to use
Control.Monad.State in order to use
StateT. The type
NonDetState s a denotes a non-deterministic state machine which has a state of type
s and an output of type
a. We will not explain the internal mechanics of
StateT but we will discuss how to use it.
NonDetState s monad supports a method
get which gives the current state of the machine and a method
put which updates the current state. Furthermore, we can use
lift to convert values of type
NonDet a to values of type
NonDetState s. And, we may use
evalStateT to run a given nondeterministic machine with a particular initial state and get a
We will assume that the graph is given to us in the form of an adjacency list, or equivalently a function that given a vertex provides a neighbour non-deterministically.
1 2 3 4
undefined, but for the purpose of testing, the reader can substitute any reasonable function. Note that for the purpose of complexity arguments, we require the graph to be finite.
To demonstrate how we are going to use this object, let us see how we can write a non-deterministic state machine that walks along a given vertex to an arbitrary vertex for a given number of steps.
1 2 3 4 5 6 7 8 9
This state machine, which starts with an initial state
start, walks for
n steps nondeterministically, updating the current vertex each time. In the type
NonDetState Vertex Vertex, the first
Vertex denotes that the machine internally remembers a specific vertex, and the second
Vertex denotes that the machine outputs a vertex.
First, we define how to guess a path from a
source to a
bound number of steps.
1 2 3 4 5 6 7 8 9 10 11 12 13 14
If a particular branch of the computation is able to guess a path, then it returns
(). Otherwise, the
guard ensures that the branch dies. Thus, a non-empty number of values are produced iff it is possible to guess a path.
Now, the magic begins. Suppose we knew how many vertices are reachable from the
start vertex. In that case, we can run through all the vertices and increment a counter for each vertex that we have verified is reachable. We make sure we do not do this for the vertex
target. If we see that the number of vertices we have counted is actually the known count, then we are sure that
target is indeed unreachable.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
But, how can we compute the number of reachable vertices? We do this inductively by calculating the number of vertices which are reachable in steps by looking at the number of vertices reachable in steps.
1 2 3 4 5 6 7
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
Now, we can finally guess how many vertices are reachable from the
start vertex and verify that
target is indeed unreachable.
1 2 3 4
This method would return a non-empty list if and only if
target is not reachable from
The theoretical exercise that spurs this discussion is whether we could certify the abasence of a path in logspace. Indeed, if we analyze any run of the non-deterministic computation, we are only storing a constant number of counters and vertices. Storing information about such things would require only logarithmically many bits in the size of the graph.
This was an exercising in making an well-known algorithm semi-formal. Some possible further steps would be to actually prove its correctness in a proof assistant like Coq or Agda. Also, if research projects like Resource Aware ML succeed, then we could have the compiler itself reason about space complexity. I'd also be interested in suggestions on coding style.