2
\$\begingroup\$

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.

\$\endgroup\$
  • \$\begingroup\$ 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? \$\endgroup\$ – Gurkenglas Feb 8 at 15:52
  • \$\begingroup\$ I meant to use the latest value of previousCount. So you are correct, I should have used a new get to get that value \$\endgroup\$ – Agnishom Chattopadhyay Feb 11 at 4:34
0
\$\begingroup\$

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
  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
\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.