Algebra.Graph.AdjacencyMap.Algorithm

Alga is a library for algebraic construction and manipulation of graphs in Haskell. See this paper for the motivation behind the library, the underlying theory, and implementation details.

This module provides basic graph algorithms, such as depth-first search, implemented for the Algebra.Graph.AdjacencyMap data type.

Algorithms

dfsForest :: Ord a => AdjacencyMap a -> Forest a

Compute the depth-first search forest of a graph that corresponds to searching from each of the graph vertices in the Ord a order.

dfsForest empty                       == []
forest (dfsForest $ edge 1 1)         == vertex 1
forest (dfsForest $ edge 1 2)         == edge 1 2
forest (dfsForest $ edge 2 1)         == vertices [1,2]
isSubgraphOf (forest $ dfsForest x) x == True
isDfsForestOf (dfsForest x) x         == True
dfsForest . forest . dfsForest        == dfsForest
dfsForest (vertices vs)               == map (\v -> Node v []) (nub $ sort vs)
dfsForestFrom (vertexList x) x        == dfsForest x
dfsForest $ 3 * (1 + 4) * (1 + 5)     == [ Node { rootLabel = 1
                                                , subForest = [ Node { rootLabel = 5
                                                                     , subForest = [] }]}
                                         , Node { rootLabel = 3
                                                , subForest = [ Node { rootLabel = 4
                                                                     , subForest = [] }]}]

dfsForestFrom :: Ord a => [a] -> AdjacencyMap a -> Forest a

Compute the depth-first search forest of a graph, searching from each of the given vertices in order. Note that the resulting forest does not necessarily span the whole graph, as some vertices may be unreachable.

dfsForestFrom vs empty                           == []
forest (dfsForestFrom [1]   $ edge 1 1)          == vertex 1
forest (dfsForestFrom [1]   $ edge 1 2)          == edge 1 2
forest (dfsForestFrom [2]   $ edge 1 2)          == vertex 2
forest (dfsForestFrom [3]   $ edge 1 2)          == empty
forest (dfsForestFrom [2,1] $ edge 1 2)          == vertices [1,2]
isSubgraphOf (forest $ dfsForestFrom vs x) x     == True
isDfsForestOf (dfsForestFrom (vertexList x) x) x == True
dfsForestFrom (vertexList x) x                   == dfsForest x
dfsForestFrom vs             (vertices vs)       == map (\v -> Node v []) (nub vs)
dfsForestFrom []             x                   == []
dfsForestFrom [1,4] $ 3 * (1 + 4) * (1 + 5)      == [ Node { rootLabel = 1
                                                           , subForest = [ Node { rootLabel = 5
                                                                                , subForest = [] }
                                                    , Node { rootLabel = 4
                                                           , subForest = [] }]

dfs :: Ord a => [a] -> AdjacencyMap a -> [a]

Compute the list of vertices visited by the depth-first search in a graph, when searching from each of the given vertices in order.

dfs vs    $ empty                    == []
dfs [1]   $ edge 1 1                 == [1]
dfs [1]   $ edge 1 2                 == [1,2]
dfs [2]   $ edge 1 2                 == [2]
dfs [3]   $ edge 1 2                 == []
dfs [1,2] $ edge 1 2                 == [1,2]
dfs [2,1] $ edge 1 2                 == [2,1]
dfs []    $ x                        == []
dfs [1,4] $ 3 * (1 + 4) * (1 + 5)    == [1,5,4]
isSubgraphOf (vertices $ dfs vs x) x == True

reachable :: Ord a => a -> AdjacencyMap a -> [a]

Compute the list of vertices that are reachable from a given source vertex in a graph. The vertices in the resulting list appear in the depth-first order.

reachable x $ empty                       == []
reachable 1 $ vertex 1                    == [1]
reachable 1 $ vertex 2                    == []
reachable 1 $ edge 1 1                    == [1]
reachable 1 $ edge 1 2                    == [1,2]
reachable 4 $ path    [1..8]              == [4..8]
reachable 4 $ circuit [1..8]              == [4..8] ++ [1..3]
reachable 8 $ clique  [8,7..1]            == [8] ++ [1..7]
isSubgraphOf (vertices $ reachable x y) y == True

topSort :: Ord a => AdjacencyMap a -> Maybe [a]

Compute the topological sort of a graph or return Nothing if the graph is cyclic.

topSort (1 * 2 + 3 * 1)               == Just [3,1,2]
topSort (1 * 2 + 2 * 1)               == Nothing
fmap (flip isTopSortOf x) (topSort x) /= Just False
isJust . topSort                      == isAcyclic

isAcyclic :: Ord a => AdjacencyMap a -> Bool

Check if a given graph is acyclic.

isAcyclic (1 * 2 + 3 * 1) == True
isAcyclic (1 * 2 + 2 * 1) == False
isAcyclic . circuit       == null
isAcyclic                 == isJust . topSort

scc :: Ord a => AdjacencyMap a -> AdjacencyMap (AdjacencyMap a)

Compute the condensation of a graph, where each vertex corresponds to a strongly-connected component of the original graph. Note that component graphs are non-empty, and are therefore of type Algebra.Graph.NonEmpty.AdjacencyMap.

scc empty               == empty
scc (vertex x)          == vertex (NonEmpty.vertex x)
scc (edge 1 1)          == vertex (NonEmpty.edge 1 1)
scc (edge 1 2)          == edge   (NonEmpty.vertex 1) (NonEmpty.vertex 2)
scc (circuit (1:xs))    == vertex (NonEmpty.circuit1 (1 :| xs))
scc (3 * 1 * 4 * 1 * 5) == edges  [ (NonEmpty.vertex  3      , NonEmpty.vertex  5      )
                                  , (NonEmpty.vertex  3      , NonEmpty.clique1 [1,4,1])
                                  , (NonEmpty.clique1 [1,4,1], NonEmpty.vertex  5      ) ]
isAcyclic . scc == const True
isAcyclic x     == (scc x == gmap NonEmpty.vertex x)

Correctness properties

isDfsForestOf :: Ord a => Forest a -> AdjacencyMap a -> Bool

Check if a given forest is a correct depth-first search forest of a graph. The implementation is based on the paper "Depth-First Search and Strong Connectivity in Coq" by François Pottier.

isDfsForestOf []                              empty            == True
isDfsForestOf []                              (vertex 1)       == False
isDfsForestOf [Node 1 []]                     (vertex 1)       == True
isDfsForestOf [Node 1 []]                     (vertex 2)       == False
isDfsForestOf [Node 1 [], Node 1 []]          (vertex 1)       == False
isDfsForestOf [Node 1 []]                     (edge 1 1)       == True
isDfsForestOf [Node 1 []]                     (edge 1 2)       == False
isDfsForestOf [Node 1 [], Node 2 []]          (edge 1 2)       == False
isDfsForestOf [Node 2 [], Node 1 []]          (edge 1 2)       == True
isDfsForestOf [Node 1 [Node 2 []]]            (edge 1 2)       == True
isDfsForestOf [Node 1 [], Node 2 []]          (vertices [1,2]) == True
isDfsForestOf [Node 2 [], Node 1 []]          (vertices [1,2]) == True
isDfsForestOf [Node 1 [Node 2 []]]            (vertices [1,2]) == False
isDfsForestOf [Node 1 [Node 2 [Node 3 []]]]   (path [1,2,3])   == True
isDfsForestOf [Node 1 [Node 3 [Node 2 []]]]   (path [1,2,3])   == False
isDfsForestOf [Node 3 [], Node 1 [Node 2 []]] (path [1,2,3])   == True
isDfsForestOf [Node 2 [Node 3 []], Node 1 []] (path [1,2,3])   == True
isDfsForestOf [Node 1 [], Node 2 [Node 3 []]] (path [1,2,3])   == False

isTopSortOf :: Ord a => [a] -> AdjacencyMap a -> Bool

Check if a given list of vertices is a correct topological sort of a graph.

isTopSortOf [3,1,2] (1 * 2 + 3 * 1) == True
isTopSortOf [1,2,3] (1 * 2 + 3 * 1) == False
isTopSortOf []      (1 * 2 + 3 * 1) == False
isTopSortOf []      empty           == True
isTopSortOf [x]     (vertex x)      == True
isTopSortOf [x]     (edge x x)      == False