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 '19 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 '19 at 4:34

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