Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Graph.AdjacencyMap.Unidirectional

Contents

- Graphs and edges
- Queries
- Construction
- Transformation
- Strongly connected components
- Reachability
- Transitive closure

Description

Directed graphs (can of course simulate undirected graphs).

Represented as adjacency maps in direction from source to target.

Each source node maps to an adjacency map of outgoing edges, which is a map from target nodes to edges.

Listed time complexities are for the worst case (and possibly amortised), with n standing for the number of nodes in the graph and e standing for the number of edges. Comparisons, predicates etc. are assumed to take constant time (unless otherwise stated).

Synopsis

- newtype Graph n e = Graph {
  - graph :: Map n (Map n e)
  }
- invariant :: Ord n => Graph n e -> Bool
- data Edge n e = Edge {
  - source :: n
  - target :: n
  - label :: e
  }
- lookup :: Ord n => n -> n -> Graph n e -> Maybe e
- edges :: Graph n e -> [Edge n e]
- neighbours :: Ord n => n -> Graph n e -> [(n, e)]
- neighboursMap :: Ord n => n -> Graph n e -> Map n e
- edgesFrom :: Ord n => Graph n e -> [n] -> [Edge n e]
- edgesTo :: Ord n => Graph n e -> [n] -> [Edge n e]
- diagonal :: Ord n => Graph n e -> [Edge n e]
- nodes :: Graph n e -> Set n
- sourceNodes :: Graph n e -> Set n
- targetNodes :: Ord n => Graph n e -> Set n
- isolatedNodes :: Ord n => Graph n e -> Set n
- data Nodes n = Nodes {
  - srcNodes :: Set n
  - tgtNodes :: Set n
  - allNodes :: Set n
  }
- computeNodes :: Ord n => Graph n e -> Nodes n
- discrete :: Null e => Graph n e -> Bool
- acyclic :: Ord n => Graph n e -> Bool
- fromNodes :: Ord n => [n] -> Graph n e
- fromNodeSet :: Ord n => Set n -> Graph n e
- fromEdges :: Ord n => [Edge n e] -> Graph n e
- fromEdgesWith :: Ord n => (e -> e -> e) -> [Edge n e] -> Graph n e
- empty :: Graph n e
- singleton :: Ord n => n -> n -> e -> Graph n e
- insert :: Ord n => n -> n -> e -> Graph n e -> Graph n e
- insertWith :: Ord n => (e -> e -> e) -> n -> n -> e -> Graph n e -> Graph n e
- insertEdge :: Ord n => Edge n e -> Graph n e -> Graph n e
- insertEdgeWith :: Ord n => (e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
- union :: Ord n => Graph n e -> Graph n e -> Graph n e
- unionWith :: Ord n => (e -> e -> e) -> Graph n e -> Graph n e -> Graph n e
- unions :: Ord n => [Graph n e] -> Graph n e
- unionsWith :: Ord n => (e -> e -> e) -> [Graph n e] -> Graph n e
- mapWithEdge :: (Edge n e -> e') -> Graph n e -> Graph n e'
- transposeEdge :: Edge n e -> Edge n e
- transpose :: Ord n => Graph n e -> Graph n e
- clean :: Null e => Graph n e -> Graph n e
- removeNode :: Ord n => n -> Graph n e -> Graph n e
- removeNodes :: Ord n => Set n -> Graph n e -> Graph n e
- removeEdge :: Ord n => n -> n -> Graph n e -> Graph n e
- filterEdges :: (Edge n e -> Bool) -> Graph n e -> Graph n e
- unzip :: Graph n (e, e') -> (Graph n e, Graph n e')
- composeWith :: Ord n => (c -> d -> e) -> (e -> e -> e) -> Graph n c -> Graph n d -> Graph n e
- sccs' :: Ord n => Graph n e -> [SCC n]
- sccs :: Ord n => Graph n e -> [[n]]
- data DAG n = DAG {
  - dagGraph :: Graph
  - dagComponentMap :: IntMap (SCC n)
  - dagNodeMap :: Map n Int
  }
- dagInvariant :: Ord n => DAG n -> Bool
- oppositeDAG :: DAG n -> DAG n
- reachable :: Ord n => DAG n -> SCC n -> [n]
- sccDAG' :: forall n e. Ord n => Graph n e -> [SCC n] -> DAG n
- sccDAG :: Ord n => Graph n e -> DAG n
- reachableFrom :: Ord n => Graph n e -> n -> Map n (Int, [Edge n e])
- reachableFromSet :: Ord n => Graph n e -> Set n -> Set n
- walkSatisfying :: Ord n => (Edge n e -> Bool) -> (Edge n e -> Bool) -> Graph n e -> n -> n -> Maybe [Edge n e]
- gaussJordanFloydWarshallMcNaughtonYamada :: forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n e -> (Graph n e, [SCC n])
- gaussJordanFloydWarshallMcNaughtonYamadaReference :: forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n e -> Graph n e
- complete :: (Eq e, Null e, SemiRing e, Ord n) => Graph n e -> Graph n e
- completeIter :: (Eq e, Null e, SemiRing e, Ord n) => Graph n e -> [(Graph n e, Graph n e)]

# Graphs and edges

newtype Graph n e Source #

`Graph n e` is a type of directed graphs with nodes in `n` and edges in `e`.

At most one edge is allowed between any two nodes. Multigraphs can be simulated by letting the edge type `e` be a collection type.

The graphs are represented as adjacency maps (adjacency lists, but using finite maps instead of arrays and lists). This makes it possible to compute a node's outgoing edges in logarithmic time (O(log n)). However, computing the incoming edges may be more expensive.

Note that neither the number of nodes nor the number of edges may exceed ``maxBound` :: `Int``.

Constructors

Graph |

Fields

- graph :: Map n (Map n e)

  Forward edges.

Instances

(Ord r, Ord f) => SetToInfty f (ConGraph r f) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods setToInfty :: [f] -> ConGraph r f -> ConGraph r f Source #
Functor (Graph n) Source # |
Instance details Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional Methods fmap :: (a -> b) -> Graph n a -> Graph n b Source # (<$) :: a -> Graph n b -> Graph n a Source #
(Eq n, Eq e) => Eq (Graph n e) Source # |
Instance details Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional Methods (==) :: Graph n e -> Graph n e -> Bool Source # (/=) :: Graph n e -> Graph n e -> Bool Source #
(Ord n, Show n, Show e) => Show (Graph n e) Source # |
Instance details Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional Methods showsPrec :: Int -> Graph n e -> ShowS Source # show :: Graph n e -> String Source # showList :: [Graph n e] -> ShowS Source #
(Ord n, Pretty n, Pretty e) => Pretty (Graph n e) Source # |
Instance details Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional Methods pretty :: Graph n e -> Doc Source # prettyPrec :: Int -> Graph n e -> Doc Source # prettyList :: [Graph n e] -> Doc Source #
(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e) Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Graph n e -> TCM Doc Source #
(Ord r, Ord f, Negative a) => Negative (Graphs r f a) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods negative :: Graphs r f a -> Bool Source #
(Ord r, Ord f, Negative a) => Negative (Graph r f a) Source # | A graph is `negative` if it contains a negative loop (diagonal edge). Makes sense on transitive graphs.
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods negative :: Graph r f a -> Bool Source #

invariant :: Ord n => Graph n e -> Bool Source #

Internal invariant.

data Edge n e Source #

Edges.

Constructors

Edge |

Fields

- source :: n

  Outgoing node.

- target :: n

  Incoming node.

- label :: e

  Edge label (weight).

Instances

Eq f => SetToInfty f (Edge' r f a) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods setToInfty :: [f] -> Edge' r f a -> Edge' r f a Source #
Functor (Edge n) Source # |
Instance details Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional Methods fmap :: (a -> b) -> Edge n a -> Edge n b Source # (<$) :: a -> Edge n b -> Edge n a Source #
(Eq n, Eq e) => Eq (Edge n e) Source # |
Instance details Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional Methods (==) :: Edge n e -> Edge n e -> Bool Source # (/=) :: Edge n e -> Edge n e -> Bool Source #
(Ord n, Ord e) => Ord (Edge n e) Source # |

Instance details

Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional

Methods

compare :: Edge n e -> Edge n e -> Ordering Source #

(<) :: Edge n e -> Edge n e -> Bool Source #

(<=) :: Edge n e -> Edge n e -> Bool Source #

(>) :: Edge n e -> Edge n e -> Bool Source #

(>=) :: Edge n e -> Edge n e -> Bool Source #

max :: Edge n e -> Edge n e -> Edge n e Source #

min :: Edge n e -> Edge n e -> Edge n e Source #

(Show n, Show e) => Show (Edge n e) Source # |
Instance details Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional Methods showsPrec :: Int -> Edge n e -> ShowS Source # show :: Edge n e -> String Source # showList :: [Edge n e] -> ShowS Source #
(Pretty n, Pretty e) => Pretty (Edge n e) Source # |
Instance details Defined in Agda.Utils.Graph.AdjacencyMap.Unidirectional Methods pretty :: Edge n e -> Doc Source # prettyPrec :: Int -> Edge n e -> Doc Source # prettyList :: [Edge n e] -> Doc Source #
(Ord r, Ord f, Dioid a) => Dioid (Edge' r f a) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods compose :: Edge' r f a -> Edge' r f a -> Edge' r f a Source # unitCompose :: Edge' r f a Source #
(Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods meet :: Edge' r f a -> Edge' r f a -> Edge' r f a Source #
(Ord r, Ord f, Top a) => Top (Edge' r f a) Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods top :: Edge' r f a Source # isTop :: Edge' r f a -> Bool Source #
Negative a => Negative (Edge' r f a) Source # | An edge is negative if its label is.
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods negative :: Edge' r f a -> Bool Source #

# Queries

lookup :: Ord n => n -> n -> Graph n e -> Maybe e Source #

If there is an edge from `s` to `t`, then `lookup s t g` is ``Just` e`, where `e` is the edge's label. O(log n).

edges :: Graph n e -> [Edge n e] Source #

The graph's edges. O(n + e).

neighbours :: Ord n => n -> Graph n e -> [(n, e)] Source #

`neighbours u g` consists of all nodes `v` for which there is an edge from `u` to `v` in `g`, along with the corresponding edge labels. O(log n + |`neighbours u g`|).

neighboursMap :: Ord n => n -> Graph n e -> Map n e Source #

`neighboursMap u g` consists of all nodes `v` for which there is an edge from `u` to `v` in `g`, along with the corresponding edge labels. O(log n).

edgesFrom :: Ord n => Graph n e -> [n] -> [Edge n e] Source #

`edgesFrom g ns` is a list containing all edges originating in the given nodes (i.e., all outgoing edges for the given nodes). If `ns` does not contain duplicates, then the resulting list does not contain duplicates. O(|`ns`| log |`n`| + |`edgesFrom g ns`|).

edgesTo :: Ord n => Graph n e -> [n] -> [Edge n e] Source #

`edgesTo g ns` is a list containing all edges ending in the given nodes (i.e., all incoming edges for the given nodes). If `ns` does not contain duplicates, then the resulting list does not contain duplicates. O(|`ns`| n log n).

diagonal :: Ord n => Graph n e -> [Edge n e] Source #

All self-loops. O(n log n).

nodes :: Graph n e -> Set n Source #

All nodes. O(n).

sourceNodes :: Graph n e -> Set n Source #

Nodes with outgoing edges. O(n).

targetNodes :: Ord n => Graph n e -> Set n Source #

Nodes with incoming edges. O(n + e log n).

isolatedNodes :: Ord n => Graph n e -> Set n Source #

Nodes without incoming or outgoing edges. O(n + e log n).

data Nodes n Source #

Various kinds of nodes.

Constructors

Nodes |

Fields

- srcNodes :: Set n

  Nodes with outgoing edges.

- tgtNodes :: Set n

  Nodes with incoming edges.

- allNodes :: Set n

  All nodes, with or without edges.

computeNodes :: Ord n => Graph n e -> Nodes n Source #

Constructs a `Nodes` structure. O(n + e log n).

discrete :: Null e => Graph n e -> Bool Source #

Checks whether the graph is discrete (containing no edges other than `null` edges). O(n + e).

acyclic :: Ord n => Graph n e -> Bool Source #

Returns `True` iff the graph is acyclic.

# Construction

fromNodes :: Ord n => [n] -> Graph n e Source #

Constructs a completely disconnected graph containing the given nodes. O(n log n).

fromNodeSet :: Ord n => Set n -> Graph n e Source #

Constructs a completely disconnected graph containing the given nodes. O(n).

fromEdges :: Ord n => [Edge n e] -> Graph n e Source #

`fromEdges es` is a graph containing the edges in `es`, with the caveat that later edges overwrite earlier edges. O(|`es`| log n).

fromEdgesWith :: Ord n => (e -> e -> e) -> [Edge n e] -> Graph n e Source #

`fromEdgesWith f es` is a graph containing the edges in `es`. Later edges are combined with earlier edges using the supplied function. O(|`es`| log n).

empty :: Graph n e Source #

Empty graph (no nodes, no edges). O(1).

singleton :: Ord n => n -> n -> e -> Graph n e Source #

A graph with two nodes and a single connecting edge. O(1).

insert :: Ord n => n -> n -> e -> Graph n e -> Graph n e Source #

Inserts an edge into the graph. O(log n).

insertWith :: Ord n => (e -> e -> e) -> n -> n -> e -> Graph n e -> Graph n e Source #

`insertWith f s t new` inserts an edge from `s` to `t` into the graph. If there is already an edge from `s` to `t` with label `old`, then this edge gets replaced by an edge with label `f new old`, and otherwise the edge's label is `new`. O(log n).

insertEdge :: Ord n => Edge n e -> Graph n e -> Graph n e Source #

Inserts an edge into the graph. O(log n).

insertEdgeWith :: Ord n => (e -> e -> e) -> Edge n e -> Graph n e -> Graph n e Source #

A variant of `insertWith`. O(log n).

union :: Ord n => Graph n e -> Graph n e -> Graph n e Source #

Left-biased union.

Time complexity: See `unionWith`.

unionWith :: Ord n => (e -> e -> e) -> Graph n e -> Graph n e -> Graph n e Source #

Union. The function is used to combine edge labels for edges that occur in both graphs (labels from the first graph are given as the first argument to the function).

Time complexity: O(n₁ log (n₂n₁ + 1) + e₁ log e₂, where n₁/ is the number of nodes in the graph with the smallest number of nodes and n₂ is the number of nodes in the other graph, and e₁ is the number of edges in the graph with the smallest number of edges and e₂ is the number of edges in the other graph.

Less complicated time complexity: O((n + e) log n (where n and e refer to the resulting graph).

unions :: Ord n => [Graph n e] -> Graph n e Source #

Union. O((n + e) log n (where n and e refer to the resulting graph).

unionsWith :: Ord n => (e -> e -> e) -> [Graph n e] -> Graph n e Source #

Union. The function is used to combine edge labels for edges that occur in several graphs. O((n + e) log n (where n and e refer to the resulting graph).

# Transformation

mapWithEdge :: (Edge n e -> e') -> Graph n e -> Graph n e' Source #

A variant of `fmap` that provides extra information to the function argument. O(n + e).

transposeEdge :: Edge n e -> Edge n e Source #

Reverses an edge. O(1).

transpose :: Ord n => Graph n e -> Graph n e Source #

The opposite graph (with all edges reversed). O((n + e) log n).

clean :: Null e => Graph n e -> Graph n e Source #

Removes `null` edges. O(n + e).

removeNode :: Ord n => n -> Graph n e -> Graph n e Source #

`removeNode n g` removes the node `n` (and all corresponding edges) from `g`. O(n + e).

removeNodes :: Ord n => Set n -> Graph n e -> Graph n e Source #

`removeNodes ns g` removes the nodes in `ns` (and all corresponding edges) from `g`. O((n + e) log |`ns`|).

removeEdge :: Ord n => n -> n -> Graph n e -> Graph n e Source #

`removeEdge s t g` removes the edge going from `s` to `t`, if any. O(log n).

filterEdges :: (Edge n e -> Bool) -> Graph n e -> Graph n e Source #

Keep only the edges that satisfy the predicate. O(n + e).

unzip :: Graph n (e, e') -> (Graph n e, Graph n e') Source #

Unzips the graph. O(n + e).

composeWith :: Ord n => (c -> d -> e) -> (e -> e -> e) -> Graph n c -> Graph n d -> Graph n e Source #

`composeWith times plus g g'` finds all edges `s --c_i--> t_i --d_i--> u` and constructs the result graph from `edge(s,u) = sum_i (c_i times d_i)`.

Complexity: For each edge `s --> t` in `g` we look up all edges starting with `t` in `g'`.

Precondition: The two graphs must have exactly the same nodes.

# Strongly connected components

sccs' :: Ord n => Graph n e -> [SCC n] Source #

The graph's strongly connected components, in reverse topological order.

sccs :: Ord n => Graph n e -> [[n]] Source #

The graph's strongly connected components, in reverse topological order.

data DAG n Source #

SCC DAGs.

The maps map SCC indices to and from SCCs/nodes.

Constructors

DAG |

Fields

- dagGraph :: Graph
- dagComponentMap :: IntMap (SCC n)
- dagNodeMap :: Map n Int

dagInvariant :: Ord n => DAG n -> Bool Source #

`DAG` invariant.

oppositeDAG :: DAG n -> DAG n Source #

The opposite DAG.

reachable :: Ord n => DAG n -> SCC n -> [n] Source #

The nodes reachable from the given SCC.

sccDAG' Source #

Arguments

:: Ord n |
=> Graph n e |
-> [SCC n] | The graph's strongly connected components.
-> DAG n |

Constructs a DAG containing the graph's strongly connected components.

sccDAG :: Ord n => Graph n e -> DAG n Source #

Constructs a DAG containing the graph's strongly connected components.

# Reachability

reachableFrom :: Ord n => Graph n e -> n -> Map n (Int, [Edge n e]) Source #

`reachableFrom g n` is a map containing all nodes reachable from `n` in `g`. For each node a simple path to the node is given, along with its length (the number of edges). The paths are as short as possible (in terms of the number of edges).

Precondition: `n` must be a node in `g`. The number of nodes in the graph must not be larger than ``maxBound` :: `Int``.

Amortised time complexity (assuming that comparisons take constant time): O(e log n), if the lists are not inspected. Inspection of a prefix of a list is linear in the length of the prefix.

reachableFromSet :: Ord n => Graph n e -> Set n -> Set n Source #

`reachableFromSet g ns` is a set containing all nodes reachable from `ns` in `g`.

Precondition: Every node in `ns` must be a node in `g`. The number of nodes in the graph must not be larger than ``maxBound` :: `Int``.

Amortised time complexity (assuming that comparisons take constant time): O((|`ns`| + e) log n).

walkSatisfying :: Ord n => (Edge n e -> Bool) -> (Edge n e -> Bool) -> Graph n e -> n -> n -> Maybe [Edge n e] Source #

`walkSatisfying every some g from to` determines if there is a walk from `from` to `to` in `g`, in which every edge satisfies the predicate `every`, and some edge satisfies the predicate `some`. If there are several such walks, then a shortest one (in terms of the number of edges) is returned.

Precondition: `from` and `to` must be nodes in `g`. The number of nodes in the graph must not be larger than ``maxBound` :: `Int``.

Amortised time complexity (assuming that comparisons and the predicates take constant time to compute): O(n + e log n).

# Transitive closure

gaussJordanFloydWarshallMcNaughtonYamada :: forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n e -> (Graph n e, [SCC n]) Source #

Computes the transitive closure of the graph.

Uses the Gauss-Jordan-Floyd-Warshall-McNaughton-Yamada algorithm (as described by Russell O'Connor in "A Very General Method of Computing Shortest Paths" http://r6.ca/blog/20110808T035622Z.html), implemented using `Graph`, and with some shortcuts:

- Zero edge differences are not added to the graph, thus avoiding some zero edges.
- Strongly connected components are used to avoid computing some zero edges.

The graph's strongly connected components (in reverse topological order) are returned along with the transitive closure.

gaussJordanFloydWarshallMcNaughtonYamadaReference :: forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n e -> Graph n e Source #

Computes the transitive closure of the graph.

Uses the Gauss-Jordan-Floyd-Warshall-McNaughton-Yamada algorithm (as described by Russell O'Connor in "A Very General Method of Computing Shortest Paths" http://r6.ca/blog/20110808T035622Z.html), implemented using matrices.

The resulting graph does not contain any zero edges.

This algorithm should be seen as a reference implementation. In practice `gaussJordanFloydWarshallMcNaughtonYamada` is likely to be more efficient.

complete :: (Eq e, Null e, SemiRing e, Ord n) => Graph n e -> Graph n e Source #

Transitive closure ported from Agda.Termination.CallGraph.

Relatively efficient, see Issue 1560.

completeIter :: (Eq e, Null e, SemiRing e, Ord n) => Graph n e -> [(Graph n e, Graph n e)] Source #

Version of `complete` that produces a list of intermediate results paired to the left with a difference that lead to the new intermediat result.

The last element in the list is the transitive closure, paired with the empty graph.

    complete g = snd $ last $ completeIter g