Data.Graph.Indexed.Subgraph

Definitions

0 NodeMap : Nat -> Nat -> Type

  A mapping from indices in one array (or graph) to indices in another.

Totality: total
Visibility: public export

nodeMap : IArray k (Fin m) -> NodeMap m k

  Computes a node map from an array of indices.

Totality: total
Visibility: export

adjAssocList : NodeMap k m -> AssocList k e -> AssocList m e

  Adjust an assoc list (a list of edges) according to a mapping from
  old nodes to new nodes.

Totality: total
Visibility: export

0 ISubgraph : Nat -> Nat -> Type -> Type -> Type

  An indexed graph that represents a subgraph on another one.
  
  Every node is linked to the node in the original graph.

Totality: total
Visibility: public export

0 Subgraph : Nat -> Type -> Type -> Type

  An graph that represents a subgraph on another one.
  
  Every node is linked to the node in the original graph.

Totality: total
Visibility: public export

subgraph : IGraph m e n -> IArray k (Fin m) -> ISubgraph k m e n

  Computes a subgraph of a graph containing the given nodes.
  Runs in O(k * log (k)) for sparse graphs.

Totality: total
Visibility: export

subgraphL : IGraph m e n -> List (Fin m) -> Subgraph m e n

  Computes a subgraph of a graph containing the given nodes.
  Runs in O(k * log (k)) for sparse graphs.

Totality: total
Visibility: export

connectedComponents : IGraph k e n -> List (Subgraph k e n)

  Extracts the connected components of a potentially disconnected
  graph.
  
  Runs in O(k * log(k)) for sparse graphs.

Totality: total
Visibility: export

origin : ISubgraph k m e n -> Fin k -> Fin m

  Converts the node of a subgraph to the corresponding node in the
  original graph.

Totality: total
Visibility: export

originEdge : ISubgraph k m e n -> Edge k e -> Maybe (Edge m e)

  Converts the edge of a subgraph to the corresponding edge in the
  original graph.
  
  This comes with the potential of failure, since we cannot prove that
  the subgraph is injective, that is, distinct nodes in the subgraph
  point at distinct nodes in the original graph.

Totality: total
Visibility: export

biconnectedComponents : IGraph k e n -> List (Subgraph k e n)

  Extracts the biconnected components of a graph (Hopcroft/Tarjan algorithm).
  
  A graph is "biconnected" or "2-connected" if at least two of
  its edges need to be removed to get to a disconnected graph.
  
  Biconnected subgraphs only consist of cyclic vertices and edges.
  When analyzing the cycles in a graph, for instance, when computing
  the relevant cycles or a minimal cycle basis, it is always sufficient
  - and often much more efficient - to inspect the biconnected
  components in isolation.

Totality: total
Visibility: export