The Immerman–Szelepcsényi Theorem is the statement that NL=coNL. 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 nondeterministic 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 nondeterministic algorithm. However, nondeterministic algorithms are hard to formalize in usual programming paradigms, since programmers do not (typically) wish to escape the comfortzone of real world deterministic models. However, the monadaware programmer can formalize such an algorithm by suitably defining a nondeterminism monad. See Wikipedia's page.
Informally speaking, the nondetermistic paradigm of computation is one where the computer is free to ("nondeterministically") choose an arbitrary path of computation at some points in a program.
To model this with haskell, we write nondeterminstic values of type a
as [a]
, in order to denote "a bunch of possibilities of a
". But, let us mask this and declare the following type synnonym:
1 

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

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 nondeterministically 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 

Calling 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
1 

We need to use Control.Monad.State
in order to use StateT
. The type NonDetState s a
denotes a nondeterministic 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.
The 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 NonDet
value.
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 nondeterministically.
1 2 3 4 

We leave getNextVertex
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 nondeterministic 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 target
with 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 nonempty 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 \(i\) steps by looking at the number of vertices reachable in \(i1\) steps.
1 2 3 4 5 6 7 

where
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 nonempty list if and only if target
is not reachable from source
.
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 nondeterministic 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 wellknown algorithm semiformal. 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.
Problem Loading...
Note Loading...
Set Loading...
Easy Math Editor
*italics*
or_italics_
**bold**
or__bold__
paragraph 1
paragraph 2
[example link](https://brilliant.org)
> This is a quote
2 \times 3
2^{34}
a_{i1}
\frac{2}{3}
\sqrt{2}
\sum_{i=1}^3
\sin \theta
\boxed{123}
Comments
There are no comments in this discussion.