# A Haskell-Aware Explanation of Immerman–Szelepcsényi Theorem

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.

## Modelling Nondeterminism with the List Monad

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 as [a], in order to denote "a bunch of possibilities of a". But, let us mask this and declare the following type synnonym:

 1 type NonDet a = [a] 

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 type KnightPos = (Int, Int) 

Then, we try to see how we can represent the moves of the knight.

 1 2 3 4 5 6 7 8 moveKnight :: KnightPos -> NonDet KnightPos moveKnight (c, r) = do -- nondeterministically choose what the next move should be -- from the possible set of moves (c',r') <- [(c+2,r-1),(c+2,r+1),(c-2,r-1),(c-2,r+1) ,(c+1,r-2),(c+1,r+2),(c-1,r-2),(c-1,r+2) ] return (c',r') 

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 moveKnight :: KnightPos -> NonDet KnightPos moveKnight (c,r) = do (c',r') <- [(c+2,r-1),(c+2,r+1),(c-2,r-1),(c-2,r+1) ,(c+1,r-2),(c+1,r+2),(c-1,r-2),(c-1,r+2) ] guard (c' elem [1..8] && r' elem [1..8]) return (c',r') 

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 in3 :: KnightPos -> NonDet KnightPos in3 start = do first <- moveKnight start second <- moveKnight first moveKnight second 

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 :: (Bool -> Bool -> Bool -> Bool) -> NonDet (Bool, Bool, Bool) sat3 f = do var1 <- [True, False] var2 <- [True, False] var3 <- [True, False] guard (f var1 var2 var3 == True) return (var1, var2, var3) 

Calling sat3 f would give us a list of assignments which satisfy f and would be empty if there are none.

## Stateful Nondeterministic Machines

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 type NonDetState s a = StateT s [] a 

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.

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.

## Setting the Stage for Graphs

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 type Vertex = Int getNextVertex :: Vertex -> NonDet Vertex getNextVertex = undefined 

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 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 walkN :: Int -> NonDetState Vertex Vertex walkN n = do start <- get replicateM_ n $do u <- get v <- lift$ getNextVertex u put v current <- get return current 

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.

## On to the proof

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 guessPath :: Int -> Vertex -> Vertex -> NonDetState Vertex () guessPath bound source target = do put source nonDeterministicWalk bound where nonDeterministicWalk bound = do guard (bound >= 0) v <- get if v == target then return () else do w <- lift $getNextVertex v put w nonDeterministicWalk (bound - 1)  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 certifyUnreachAux :: [Vertex] -> Int -> Vertex -> Vertex -> NonDetState Int () certifyUnreachAux vertices c source target = do put 0 forM_ vertices$ \v -> do -- guess whether the vertex v is reachable or not guess <- lift [True, False] if (not guess || v == target) -- if the vertex v is not reachable or is the target -- then just move on to the next one then return () else do -- otherwise verify that the vertex is indeed reachable guessPath (length vertices) source v counter <- get put (counter + 1) counter <- get guard (counter == c) return () 

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 $i-1$ steps.

 1 2 3 4 5 6 7 countReachable :: [Vertex] -> Int -> Vertex -> NonDet Int countReachable vertices steps source = do if steps <= 0 then return 1 else do previouslyReachable <- countReachable vertices (steps - 1) source evalStateT (countReachableInduct vertices previouslyReachable steps source) undefine 

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 countReachableInduct :: [Vertex] -> Int -> Int -> Vertex -> NonDetState (Int, Int, Bool) Int countReachableInduct vertices previouslyReachable steps source = do -- initialize the counters to 0 put (0, 0, False) forM_ vertices $\v -> do -- set the first counter to 0 -- and unset the flag that says you have -- checked that v is a neighbor of u or u itself (previousCount, currentCount, b) <- get put (0, currentCount, False) forM_ vertices$ \u -> do -- guess if u reachable from the source in (steps - 1) steps guess <- lift [True, False] if not guess -- if not, then we can move ahead to the next u then return () else do -- since we guessed that u is reachable, -- we should verify it lift $evalStateT (guessPath (steps - 1) source u) 0 (previousCount, currentCount, b) <- get put ((previousCount + 1), currentCount, b) if (u == v) then do (previousCount, currentCount, _) <- get put (previousCount, currentCount, True) else do neighbor <- lift$ getNextVertex u if (u == neighbor) then do (previousCount, currentCount, _) <- get put (previousCount, currentCount, True) else -- if v is neither u nor a neighbor of u, -- we just move to the second iteration return () guard (previousCount == previouslyReachable) (previousCount, currentCount, b) <- get -- if v was at most distance 1 from u, which -- we verfied to be a vertex reachable in -- (steps - 1) steps, then v is reachable -- in steps steps put (previousCount, (currentCount + if b then 1 else 0), b) (_, currentCount, _) <- get return currentCount 

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 certifyUnreach :: [Vertex] -> Vertex -> Vertex -> NonDet () certifyUnreach vertices source target = do c <- countReachable vertices (length vertices) source evalStateT (certifyUnreachAux vertices c source target) 0 

This method would return a non-empty list if and only if target is not reachable from source.

## On Space Complexity

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.

## Further Thoughts

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.

2 years, 5 months ago

This discussion board is a place to discuss our Daily Challenges and the math and science related to those challenges. Explanations are more than just a solution — they should explain the steps and thinking strategies that you used to obtain the solution. Comments should further the discussion of math and science.

When posting on Brilliant:

• Use the emojis to react to an explanation, whether you're congratulating a job well done , or just really confused .
• Ask specific questions about the challenge or the steps in somebody's explanation. Well-posed questions can add a lot to the discussion, but posting "I don't understand!" doesn't help anyone.
• Try to contribute something new to the discussion, whether it is an extension, generalization or other idea related to the challenge.

MarkdownAppears as
*italics* or _italics_ italics
**bold** or __bold__ bold
- bulleted- list
• bulleted
• list
1. numbered2. list
1. numbered
2. list
Note: you must add a full line of space before and after lists for them to show up correctly
paragraph 1paragraph 2

paragraph 1

paragraph 2

[example link](https://brilliant.org)example link
> This is a quote
This is a quote
    # I indented these lines
# 4 spaces, and now they show
# up as a code block.

print "hello world"
# I indented these lines
# 4 spaces, and now they show
# up as a code block.

print "hello world"
MathAppears as
Remember to wrap math in $$ ... $$ or $ ... $ to ensure proper formatting.
2 \times 3 $2 \times 3$
2^{34} $2^{34}$
a_{i-1} $a_{i-1}$
\frac{2}{3} $\frac{2}{3}$
\sqrt{2} $\sqrt{2}$
\sum_{i=1}^3 $\sum_{i=1}^3$
\sin \theta $\sin \theta$
\boxed{123} $\boxed{123}$

Sort by:

Hey Agnishom! I think this was a well-written piece! Learned something new today, so thank you! :) However, I had a few suggestions about the code. Please consider them with a pinch of salt. I came up with these after briefly reading the code. I'd have to implement it all to be sure.

1. In the places where you're doing this:
haskell if v == target then return () else do...  you could try using something like unless and when from Control.Monad.

2. Instead of using forM_ you could try using map or any of the fold methods. It's a functional language so yeah using such methods would make the code more in-line with the idiomatic approach.

3. In many places I think using the >>= operator would suffice over the do. Also, I think you could have leveraged the >=> (the left-to-right Kleisli-Composition Operator alongside replicate.

Overall, you could use a linter like hlint to aid you in writing more idiomatic code in case you'd be interested.

- 9 months, 2 weeks ago

Thank you Sameer! These are interesting comments. I would generally agree that using the monadic bind >>= is a better idea than explicit do, I feel that in this case do makes the presentation clearer. Also, good to know about unless and when. I did not know about these combinators!

- 7 months, 1 week ago