# Modelling Immerman–Szelepcsényi in Haskell

I am trying to model the proof of Immerman–Szelepcsényi Theorem with Haskell since it heavily uses non-determinism. An explanation of what the point of this is can be found here.

{-# LANGUAGE FlexibleContexts #-}

type NonDet a = [a]

type NonDetState s a = StateT s [] a

type Vertex = Int

-- represent the graph as an adjacency list
-- or equivalently, a nondeterministic computation
-- that returns the next vertex given the current
getNextVertex :: Vertex -> NonDet Vertex
getNextVertex = undefined

-- is there a path from source to target in bound 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 you knew the number of vertices reachable from the source -- use that to certify that target is not reachable 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 ()

-- figure out the number of vertices reachable from source
-- in steps 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) (0, 0, False)

-- figuring out how many vertices are reachable in (i+1) steps
-- given the number of vertices reachable in i steps
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

-- finally put all the methods together and show that
-- target is unreachable from source
certifyUnreach :: [Vertex] -> Vertex -> Vertex -> NonDet ()
certifyUnreach vertices source target = do
c <- countReachable vertices (length vertices) source
evalStateT (certifyUnreachAux vertices c source target) 0


I'd like general comments on how I could improve coding style. One particular thing is the awkward use of get and put to get the three counters but update one of them. I would like to know how this can be done more elegantly with lenses.

• guard (previousCount == previouslyReachable) <- did you mean to use the previousCount defined in the line after -- checked that v is a neighbor of u or u itself? Feb 8, 2019 at 15:52
• I meant to use the latest value of previousCount. So you are correct, I should have used a new get to get that value Feb 11, 2019 at 4:34

I'm not going to try to build/compile/test a full new version of your code, but I think I can still suggest ways to improve it.

You asked about using lenses to improve the get >>= put pattern you're using. I do think lenses have a place here (I'm not experienced with them), but they're not the first thing you need.

• Writing a expression of type State (Int, Int, Bool) is smelly. Tuples aren't bad, but they don't denote their own meaning. Which Int is which? What does the Bool represent? Also, for a triplet you can't use the convenient fst and snd. So: Introduce a record type for this state.
• Very often (I'm tempted to say "most of the time") one should use gets and modify instead of get and put. For example (in tuple syntax for now) instead of a get followed by a put, you would just write modify \(c1, c2, _) -> (c1, c2, True).

If you combine the above, you'll get something that's idiomatic and reads clearly without additional commentary. But it'll be a little verbose; you'll probably start getting warnings about line-length. This is where lenses help: You want a concise way to build the record-manipulating functions to pass to modify. Here's an example I found quickly, and there are lots of complete tutorials around.

All that said, I think some of your functions aren't really using (or don't need) the abstraction of the State monad (transformer). Notice how these functions start by writing their own state immediately, or they only write immediately before recursing, or when they're called, the resulting monadic value is immediately evaluated, or that none of your functions are using the same state type. I think guessPath and certifyUnreachAux should be re-written as stateless. countReachableInduct makes sense with a statefull body, but move the evaluation inside the function so the statefull-ness isn't part of the function's type (and save your self the initial put and terminal get using execState).

On the other hand, I think the abstraction of a global getNextVertex :: Vertex -> NonDet Vertex is highly suspicious. This implies that a single graph will be locked in at compile time? Looking at the Wikipedia page, that might be consistent with the intended proof, but if not then you might lift stuff into a Reader.

I was going to use lens, but everything worked out mundanely. :/

-- is there a path from source to target in bound steps
guessPath :: Int -> Vertex -> Vertex -> NonDet ()
guessPath bound source target = nonDeterministicWalk source bound where
nonDeterministicWalk v bound = do
guard $bound >= 0 unless (v == target)$ do
w <- getNextVertex v
nonDeterministicWalk w (bound - 1)

-- figure out the number of vertices reachable from source
-- in steps steps
countReachable :: [Vertex] -> Int -> Vertex -> NonDet Int
countReachable vertices steps source = if steps <= 0 then return 1 else do
previouslyReachable <- countReachable vertices (steps - 1) source
fmap sum $for vertices$ \v -> (evalStateT False) $do -- the state flag witnesses that -- v has at most distance 1 from u guard . (== previouslyReachable) . sum =<< vertices for \u -> -- guess if u reachable from the source in (steps - 1) steps return 0 <|> 1 <$ do -- if not, then we can move ahead to the next u
-- since we guessed that u is reachable, we should verify it
guessPath (steps - 1) source u
if u == v then put True
else do
neighbor <- lift $getNextVertex u when (u == neighbor)$ put True
-- if v is neither u nor a neighbor of u,
-- we just move to the second iteration
-- 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
gets $bool 0 1 -- finally put all the methods together and show that -- target is unreachable from source certifyUnreach :: [Vertex] -> Vertex -> Vertex -> NonDet () certifyUnreach vertices source target = do c <- countReachable vertices (length vertices) source guard . (== c) . sum =<< vertices for \v -> -- guess whether the vertex v is reachable and not the target return 0 <|> 1 <$ do
-- verify that the vertex is indeed reachable and not the target
guard \$ v /= target
guessPath (length vertices) source v