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.