Modelling Immerman–Szelepcsényi in Haskell

Question

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 #-}

import Control.Monad
import Control.Monad.State

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.

Answer 1

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.

Answer 2

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