Gfrktyl

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.