dfs package:algebraic-graphs

Return the list vertices visited by the depth-first search in a graph, starting from the given seed vertices. Adjacent vertices are explored in the increasing order. Complexity: O((L + m) * log n) time and O(n) space, where L is the number of seed vertices.

dfs empty      vs    == []
dfs (edge 1 1) [1]   == [1]
dfs (edge 1 2) [0]   == []
dfs (edge 1 2) [1]   == [1,2]
dfs (edge 1 2) [2]   == [2]
dfs (edge 1 2) [1,2] == [1,2]
dfs (edge 1 2) [2,1] == [2,1]
dfs x          []    == []

and [ hasVertex v x | v <- dfs x vs ]       == True
dfs (3 * (1 + 4) * (1 + 5)) [1,4]           == [1,5,4]
dfs (circuit [1..5] + circuit [5,4..1]) [3] == [3,2,1,5,4]

Return the list vertices visited by the depth-first search in a graph, starting from the given seed vertices. Adjacent vertices are explored in the increasing order according to their Ord instance. Complexity: O((L + m) * log n) time and O(n) space, where L is the number of seed vertices.

dfs empty      vs    == []
dfs (edge 1 1) [1]   == [1]
dfs (edge 1 2) [0]   == []
dfs (edge 1 2) [1]   == [1,2]
dfs (edge 1 2) [2]   == [2]
dfs (edge 1 2) [1,2] == [1,2]
dfs (edge 1 2) [2,1] == [2,1]
dfs x          []    == []

and [ hasVertex v x | v <- dfs x vs ]       == True
dfs (3 * (1 + 4) * (1 + 5)) [1,4]           == [1,5,4]
dfs (circuit [1..5] + circuit [5,4..1]) [3] == [3,2,1,5,4]

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 == Algebra.Graph.AdjacencyMap.dfs . toAdjacencyMap

Compute the list of vertices visited by the depth-first search in a graph, when searching from each of the given vertices in order. In the following examples we will use the helper function:

(%) :: Ord a => (GraphKL a -> b) -> AdjacencyMap a -> b
f % x = f (fromAdjacencyMap x)

for greater clarity.

dfs % edge 1 1 $ [1]   == [1]
dfs % edge 1 2 $ [0]   == []
dfs % edge 1 2 $ [1]   == [1,2]
dfs % edge 1 2 $ [2]   == [2]
dfs % edge 1 2 $ [1,2] == [1,2]
dfs % edge 1 2 $ [2,1] == [2,1]
dfs % x        $ []    == []

dfs % (3 * (1 + 4) * (1 + 5)) $ [1,4]     == [1,5,4]
and [ hasVertex v x | v <- dfs % x $ vs ] == True

Compute the depth-first search forest of a graph, where adjacent vertices are explored in the increasing order. Complexity: O((n + m) * min(n,W)) time and O(n) space.

forest $ dfsForest empty              == 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)
dfsForest $ 3 * (1 + 4) * (1 + 5)     == [ Node { rootLabel = 1
, subForest = [ Node { rootLabel = 5
, subForest = [] }]}
, Node { rootLabel = 3
, subForest = [ Node { rootLabel = 4
, subForest = [] }]}]
forest (dfsForest $ circuit [1..5] + circuit [5,4..1]) == path [1,2,3,4,5]

Compute the depth-first search forest of a graph starting from the given seed vertices, where adjacent vertices are explored in the increasing order. Note that the resulting forest does not necessarily span the whole graph, as some vertices may be unreachable. The seed vertices which do not belong to the graph are ignored. Complexity: O((L + m) * log n) time and O(n) space, where L is the number of seed vertices.

forest $ dfsForestFrom empty      vs             == empty
forest $ dfsForestFrom (edge 1 1) [1]            == vertex 1
forest $ dfsForestFrom (edge 1 2) [0]            == empty
forest $ dfsForestFrom (edge 1 2) [1]            == edge 1 2
forest $ dfsForestFrom (edge 1 2) [2]            == vertex 2
forest $ dfsForestFrom (edge 1 2) [1,2]          == edge 1 2
forest $ dfsForestFrom (edge 1 2) [2,1]          == vertices [1,2]
isSubgraphOf (forest $ dfsForestFrom x vs) x     == True
isDfsForestOf (dfsForestFrom x (vertexList x)) x == True
dfsForestFrom x (vertexList x)                   == dfsForest x
dfsForestFrom x []                               == []
dfsForestFrom (3 * (1 + 4) * (1 + 5)) [1,4]      == [ Node { rootLabel = 1
, subForest = [ Node { rootLabel = 5
, subForest = [] }
, Node { rootLabel = 4
, subForest = [] }]
forest $ dfsForestFrom (circuit [1..5] + circuit [5,4..1]) [3] == path [3,2,1,5,4]

Compute the depth-first search forest of a graph, where adjacent vertices are explored in the increasing order according to their Ord instance. Complexity: O((n + m) * min(n,W)) time and O(n) space.

forest $ dfsForest empty              == 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)
dfsForest $ 3 * (1 + 4) * (1 + 5)     == [ Node { rootLabel = 1
, subForest = [ Node { rootLabel = 5
, subForest = [] }]}
, Node { rootLabel = 3
, subForest = [ Node { rootLabel = 4
, subForest = [] }]}]
forest (dfsForest $ circuit [1..5] + circuit [5,4..1]) == path [1,2,3,4,5]

Compute the depth-first search forest of a graph starting from the given seed vertices, where adjacent vertices are explored in the increasing order according to their Ord instance. Note that the resulting forest does not necessarily span the whole graph, as some vertices may be unreachable. The seed vertices which do not belong to the graph are ignored. Complexity: O((L + m) * log n) time and O(n) space, where L is the number of seed vertices.

forest $ dfsForestFrom empty      vs             == empty
forest $ dfsForestFrom (edge 1 1) [1]            == vertex 1
forest $ dfsForestFrom (edge 1 2) [0]            == empty
forest $ dfsForestFrom (edge 1 2) [1]            == edge 1 2
forest $ dfsForestFrom (edge 1 2) [2]            == vertex 2
forest $ dfsForestFrom (edge 1 2) [1,2]          == edge 1 2
forest $ dfsForestFrom (edge 1 2) [2,1]          == vertices [1,2]
isSubgraphOf (forest $ dfsForestFrom x vs) x     == True
isDfsForestOf (dfsForestFrom x (vertexList x)) x == True
dfsForestFrom x (vertexList x)                   == dfsForest x
dfsForestFrom x []                               == []
dfsForestFrom (3 * (1 + 4) * (1 + 5)) [1,4]      == [ Node { rootLabel = 1
, subForest = [ Node { rootLabel = 5
, subForest = [] }
, Node { rootLabel = 4
, subForest = [] }]
forest $ dfsForestFrom (circuit [1..5] + circuit [5,4..1]) [3] == path [3,2,1,5,4]

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 == Algebra.Graph.AdjacencyMap.dfsForest . toAdjacencyMap

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 == Algebra.Graph.AdjacencyMap.dfsForestFrom . toAdjacencyMap

Compute the depth-first search forest of a graph. In the following examples we will use the helper function:

(%) :: Ord a => (GraphKL a -> b) -> AdjacencyMap a -> b
f % x = f (fromAdjacencyMap x)

for greater clarity.

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
dfsForest % forest (dfsForest % x)      == dfsForest % x
dfsForest % vertices vs                 == map (\v -> Node v []) (nub $ sort vs)
dfsForest % (3 * (1 + 4) * (1 + 5))     == [ Node { rootLabel = 1
, subForest = [ Node { rootLabel = 5
, subForest = [] }]}
, Node { rootLabel = 3
, subForest = [ Node { rootLabel = 4
, subForest = [] }]}]

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. In the following examples we will use the helper function:

(%) :: Ord a => (GraphKL a -> b) -> AdjacencyMap a -> b
f % x = f (fromAdjacencyMap x)

for greater clarity.

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

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

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

Check if a given forest is a valid depth-first search forest of a graph.

isDfsForestOf f == Algebra.Graph.AdjacencyMap.isDfsForestOf f . toAdjacencyMap