Haskell Graph Stuff

GraphsAlgs.hs

module GraphsAlgs

where 

import List
import While
import Assert
import Reasoning (update,updates)

reachable :: Eq a => [(a,a)] -> a -> [a]
reachable g x = reachable' g [x] [x]

reachable' :: Eq a => [(a,a)] -> [a] -> [a] -> [a]
reachable' g = while2 
   (\ current _ -> not (null current))
   (\ current marked -> let 
     (y,rest) = (head current, tail current)
     newnodes = [ z  | (u,z) <- g, u == y, 
                        notElem z marked   ]
     current' = rest ++ newnodes
     marked'  = marked ++ newnodes 
  in 
     (current', marked'))

isConnected :: Eq a => [(a,a)] -> Bool
isConnected g = let 
    xs = map fst g `union` map snd g
  in 
    forall xs (\x -> forall xs (\ y -> 
       elem y (reachable g x)))

type Rel a = [(a,a)]

containedIn :: Eq a => [a] -> [a] -> Bool
containedIn xs ys = forall xs (\ x -> elem x ys) 

equalS :: Eq a => [a] -> [a] -> Bool
equalS xs ys = containedIn xs ys && containedIn ys xs 

infixr 5 @@

(@@) :: Eq a => Rel a -> Rel a -> Rel a
r @@ s = 
  nub [ (x,z) | (x,y) <- r, (w,z) <- s, y == w ]

lfp :: Eq a => (a -> a) -> a -> a
lfp f x | x == f x  = x
        | otherwise = lfp f (f x)

domain :: Eq a => Rel a -> [a]
domain r = nub (foldr (\ (x,y) -> ([x,y]++)) [] r)

rtc :: Eq a => Rel a -> Rel a
rtc r = let 
          xs = domain r 
          i  = [(x,x) | x <- xs ]
        in lfp (\ s -> (s `union` (r@@s))) i

tc :: Eq a => Rel a -> Rel a 
tc r = lfp (\ s -> (s `union` (r @@ s))) r

image :: Eq a => a -> Rel a -> [a]
image x r = [ y | (z,y) <- r, x == z ]

reachableA :: Eq a =>  [(a,a)] -> a -> [a]
reachableA = 
  assert2 (\ g x ys -> equalS ys (image x (rtc g)))
           reachable

type Vertex = Int 
type Edge = (Vertex,Vertex,Float)
type Graph = ([Vertex],[Edge]) 

mkproper :: [Edge] -> [Edge]
mkproper xs = let 
  ys = List.filter 
    (\ (x,y,w) -> x /= y && w > 0) xs
  zs = nubBy (\ (x,y,_) (x',y',_) -> 
    (x,y) == (x',y') || (x,y) == (y',x')) ys
  in foldr 
      (\ (x,y,w) us -> ((x,y,w):(y,x,w):us))
      [] zs

nodes :: (Eq a,Ord a) => [(a,a,b)] -> [a]
nodes = sort.nub.nds where 
  nds = foldr (\ (x,y,_) -> ([x,y]++)) [] 

mkGraph ::  [Edge] -> Graph
mkGraph es = let 
   new = mkproper es
   vs  = nodes new
 in (vs,new)

minim :: (Ord b) => (a -> b) -> [a] -> a
minim f = head . 
          (sortBy (\ x y -> compare (f x) (f y)))

prim :: [Edge] -> [Edge]
prim es = let 
   (v:vs) = nodes es
   vout   = vs 
   vin    = [v]
   tree   = []
 in prim' es vout vin tree

prim' :: [Edge] -> [Vertex] -> [Vertex] -> [Edge] 
      -> [Edge] 
prim' es = while3
   (\ vout _ _ -> not (null vout))
   (\ vout vin tree -> let
        links = [(x,y,w) | (x,y,w) <- es, 
                            elem x vin, elem y vout ]
        e@(x,y,w) = minim (\ (_, _, w) -> w) links 
      in 
        (vout\\[y],y:vin,e:tree))

mst :: [Edge] -> [Edge] -> Bool
mst _ [] = True
mst g [e] = elem e g
mst g (e@(x,y,w):es) = let 
    vs = nodes es 
  in 
     elem e g 
     && mst g es 
     && elem x vs
     && notElem y vs
     && forall g  (\ (x',y',w') -> 
          (elem x' vs && notElem y' vs) ==> w <= w')

primA :: [Edge] -> [Edge]
primA = assert1 mst prim

prim'' :: [Edge] -> [Vertex] -> [Vertex] -> [Edge] 
       -> [Edge] 
prim'' es = while3
   (\ vout _ _ -> not (null vout))
   (invar3 (\ _ _ tree -> mst es tree)
   (\ vout vin tree -> let
        links = [(x,y,w) | (x,y,w) <- es, 
                            elem x vin, elem y vout ]
        e@(x,y,w) = minim (\ (_, _, w) -> w) links 
      in 
        (vout\\[y],y:vin,e:tree)))

bfs :: Eq a => [(a,a)] -> a -> a -> Int
bfs g s = let 
    d = update (\_ -> undefined) (s,0) 
  in bfs' g [s] [s] d

bfs' :: Eq a => [(a,a)] -> [a] -> [a] 
             -> (a -> Int) -> a -> Int
bfs' g = while3 (\ q _ _ -> not (null q))
                (\ (u:q) t d -> let 
                    new = [ y | (x,y) <- g, 
                                 x == u, notElem y t ]
                    q' = q ++ new
                    t' = t `union` new
                    pairs = [(v, d u + 1) | v <- new ]
                    d' = updates d pairs 
                  in (q',t',d'))

exampleG = mkproper
           [(0,1,5),(0,5,3),(1,2,2),(1,6,3),(2,3,6),
            (2,7,10),(3,4,3),(4,5,8),(5,6,7),(6,7,2)]

dijkstra :: [Edge] -> Vertex -> Vertex -> Float 
dijkstra es s = let 
    t = [s]
    p = []
    d = (\ x -> if x == s then 0 else undefined)
  in 
    dijkstra' es t p d

dijkstra' :: [Edge] -> [Vertex] -> [Vertex] 
          -> (Vertex -> Float) -> Vertex -> Float
dijkstra' es = while3 
  (\ t _ _ -> not (null t))
  (\ t p d -> let 
      v = minim (\ x -> d x) t
      pairs = [(u,w)| (x,u,w) <- es, x == v]
      old   = [(u, min (d u) (d v + w)) | 
                    (u,w) <- pairs, elem u t ]
      new   = [(u, d v + w) | (u,w) <- pairs, 
                      notElem u t, notElem u p ]
      d'    = updates d (old ++ new)
      t'    = (t \\ [v]) `union` (map fst new)
    in (t',v:p,d'))

definedOn :: (Num b,Ord b) => [a] -> (a -> b) -> Bool
definedOn xs f = and (map (triv.f) xs)
  where triv = (\ x -> x >= 0)

dijkstraA :: [Edge] -> Vertex -> Vertex -> Float 
dijkstraA es s = let 
    t = [s]
    p = []
    d = (\ x -> if x == s then 0 else undefined)
  in 
    dijkstraA' es t p d

dijkstraA' :: [Edge] -> [Vertex] -> [Vertex] 
          -> (Vertex -> Float) -> Vertex -> Float
dijkstraA' es = while3 
  (\ t _ _ -> not (null t))
  (invar3 (\ t p d -> definedOn (t `union` p) d)
  (\ t p d -> let 
       v = minim (\ x -> d x) t
       pairs = [(u,w)| (x,u,w) <- es, x == v]
       old   = [(u, min (d u) (d v + w)) | 
                    (u,w) <- pairs, elem u t ]
       new   = [(u, d v + w) | (u,w) <- pairs, 
                       notElem u t, notElem u p ]
       d'    = updates d (old ++ new)
       t'    = (t \\ [v]) `union` (map fst new)
     in (t',v:p,d')))

edges2fct :: [(Int, Int, Float)] 
          -> Int -> Int -> Float
edges2fct es i j = let 
   links = filter (\ (x,y,w) -> x == i && y == j) es
   ws = map (\ (_,_,w) -> w) links 
  in
   if null ws then 0 else head ws

fct2edges :: Int -> (Int->Int->Float) 
          -> [(Int, Int, Float)]
fct2edges n f = 
  [(x,y,f x y) | x <- [0..n-1], y <- [0..n-1], 
                 f x y > 0 ]

infty :: Float
infty = 1/0

fw :: Int -> (Int -> Int -> Float) 
   -> Int -> Int -> Float
fw n f = let 
    init = \ i j -> 
             if f i j > 0 then f i j else infty 
 in 
    fw' n init 

update2 :: (Eq a,Eq b) => (a -> b -> c) -> (a,b,c) 
        -> a -> b -> c
update2 f (u,v,w) x y = 
    if u == x && v == y then w else f x y

fw' ::  Int -> (Int -> Int -> Float) 
            -> Int -> Int -> Float
fw' n = let 
    nodes = [0..n-1]
    pairs = [(i,j) | i <- nodes, j <- nodes]
  in
    for pairs (\ (i,j) -> 
       for nodes (\ k d -> let 
          k' = k-1 
        in 
          update2 d 
              (i,j,min (d i j) (d i k' + d k' j))))

isShortest :: Int -> (Int -> Int -> Float) 
           -> Int -> Int -> Float -> Bool
isShortest n f i j w = let 
    g = fct2edges n f 
  in  
    w == dijkstra g i j

fwA = assert4 isShortest fw

exampleF :: Int -> Int -> Float
exampleF = edges2fct exampleG

mfw :: Int -> (Int -> Int -> Float) -> 
       Int -> Int -> (Float, Int)
mfw n f = let 
  init = \ i j -> 
            (if f i j > 0 then f i j else infty, -1)
 in 
    mfw' n init 

mfw' ::  Int -> (Int -> Int -> (Float, Int))
              -> Int -> Int -> (Float, Int)
mfw' n = let 
    nodes = [0..n-1]
    pairs = [(i,j) | i <- nodes, j <- nodes]
  in
    for pairs (\ (i,j) -> 
       for nodes (\ k d -> let 
           k' = k-1 
           f  = \ x y -> fst (d x y)
         in 
           if f i k' + f k' j < f i j then 
             update2 d (i,j,(f i k' + f k' j, k'))
           else d))

getPath :: (Int -> Int -> (Float, Int))
        -> Int -> Int -> [Int]
getPath d i j = let 
    dist = fst (d i j)
    k    = snd (d i j)
  in 
    if dist == infty then error "no path"
    else if k == -1 then []
    else getPath d i k ++ [k] ++ getPath d k j 

warshall :: Int -> (Int->Int->Bool) 
         -> Int -> Int -> Bool
warshall n = let 
    nodes = [0..n-1]
    pairs = [(i,j) | i <- nodes, j <- nodes]
  in 
    for pairs (\ (i,j) -> 
       for nodes (\ k t -> let 
         k' = k-1 
       in 
         update2 t 
            (i,j, t i j || (t i k' && t k' j))))

isTC :: Int -> (Int->Int->Bool) -> (Int->Int->Bool) 
     -> Bool
isTC n r t = let 
    r' = [(i,j)| i <- [0..n-1], j <- [0..n-1], r i j ]
    t' = [(i,j)| i <- [0..n-1], j <- [0..n-1], t i j ]
  in 
    equalS t' (tc r')

warshallA :: Int -> (Int->Int->Bool) -> Int -> Int 
          -> Bool
warshallA = assert2 isTC warshall

bfInit :: Vertex -> [Edge] 
       -> (Vertex -> Float,Vertex -> Vertex)
bfInit s es = let 
    d  = update (\ _ -> infty) (s,0)
    p  = \ _ -> undefined
  in 
    (d,p)

bfLoop ::  [Edge] 
       -> (Vertex -> Float,Vertex -> Vertex)
       -> (Vertex -> Float,Vertex -> Vertex)
bfLoop es = let 
    ns = nodes es
    is = [1..length(ns) - 1]
  in 
    for is (\ _ (d,p) -> let 
          us    = 
             filter (\ (u,v,w) -> d(u) + w < d(v)) es
          pairs = map (\ (u,v,w) -> (v,d(u) + w)) us 
          vs    = map (\ (u,v,_) -> (v,u)) us
       in 
          (updates d pairs, updates p vs))

bf :: Vertex -> [Edge] -> 
               (Vertex -> Float,Vertex -> Vertex)
bf s es = bfLoop es (bfInit s es)

infixl 2 ##

(##) :: a -> (a -> b) -> b 
x ## f = f x

belmanFord :: Vertex -> [Edge] -> 
              (Vertex -> Float,Vertex -> Vertex)
belmanFord s es = bfInit s es ## bfLoop es

traceBack :: (Vertex -> Vertex) 
          -> Vertex ->  Vertex -> [Vertex]
traceBack p s t = 
   if s == t then [s]
   else t : traceBack p s (p t)

bfCheck :: [Edge] -> (Vertex -> Float) -> Bool
bfCheck es d = 
  forall es (\ (u,v,w) -> d u + w >= d v)

bfLoopA ::  [Edge] 
        -> (Vertex -> Float,Vertex -> Vertex)
        -> (Vertex -> Float,Vertex -> Vertex)
bfLoopA = 
    assert2 (\ es _ (d,_) -> bfCheck es d) bfLoop

bfA :: [Edge] -> Vertex 
    -> (Vertex -> Float,Vertex -> Vertex)
bfA es s = bfLoopA es (bfInit s es)