The Immerman–Szelepcsényi theorem is a proof 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 as [a], in order to denote "a bunch of possibilities of a". But, let us mask this and declare the following type synnonym:
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:
type KnightPos = (Int, Int)Then, we try to see how we can represent the moves of the knight.
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:
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.
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.
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.
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
type NonDetState s a = StateT s [] aWe 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.
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.
type Vertex = Int
getNextVertex :: Vertex -> NonDet Vertex
getNextVertex = undefinedWe 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.
walkN :: Int -> NonDetState Vertex Vertex
walkN n = do
start <- get
replicateM_ n $ do
u <- get
v <- lift $ getNextVertex u
put v
current <- get
return currentThis 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.
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.
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.
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) undefinewhere
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 currentCountNow, we can finally guess how many vertices are reachable from the start vertex and verify that target is indeed unreachable.
certifyUnreach :: [Vertex] -> Vertex -> Vertex -> NonDet ()
certifyUnreach vertices source target = do
c <- countReachable vertices (length vertices) source
evalStateT (certifyUnreachAux vertices c source target) 0This method would return a non-empty 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 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.