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

Description

Directed graphs (can of course simulate undirected graphs).

Represented as adjacency maps in direction from source to target.

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

This allows to get outgoing edges in O(log n) time where `n` is the number of nodes in the graph.

However, the set of incoming edges can only be obtained in `O(n log n)` or `O(e)` where `e` is the total number of edges.

Synopsis

# Documentation

newtype Graph s t e Source

`Graph s t e` is a directed graph with source nodes in `s` target nodes in `t` and edges in `e`.

Admits at most one edge between any two nodes. Several edges can be modeled by using a collection type for `e`.

Represented as "adjacency list", or rather, adjacency map. This allows to get all outgoing edges for a node in `O(log n)` time where `n` is the number of nodes of the graph.

Incoming edges can only be computed in `O(n + e)` time where `e` is the number of edges.

Constructors

 Graph Fieldsgraph :: Map s (Map t e)Forward edges.

Instances

 (Ord r, Ord f) => SetToInfty f (ConGraph r f) Source Functor (Graph s t) Source (Eq s, Eq t, Eq e) => Eq (Graph s t e) Source (Show s, Show t, Show e) => Show (Graph s t e) Source (Ord n, SemiRing e, Arbitrary n, Arbitrary e) => Arbitrary (Graph n n e) Source (Ord r, Ord f, Negative a) => Negative (Graphs r f a) 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. (PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n n e) Source

data Edge s t e Source

Constructors

 Edge Fieldssource :: sOutgoing node.target :: tIncoming node.label :: eEdge label (weight).

Instances

 Eq f => SetToInfty f (Edge' r f a) Source Functor (Edge s t) Source (Eq s, Eq t, Eq e) => Eq (Edge s t e) Source (Ord s, Ord t, Ord e) => Ord (Edge s t e) Source (Show s, Show t, Show e) => Show (Edge s t e) Source (CoArbitrary s, CoArbitrary t, CoArbitrary e) => CoArbitrary (Edge s t e) Source (Arbitrary s, Arbitrary t, Arbitrary e) => Arbitrary (Edge s t e) Source (Show r, Show f, Show a, Ord r, Ord f, Dioid a) => Dioid (Edge' r f a) Source (Show r, Show f, Show a, Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a) Source (Ord r, Ord f, Top a) => Top (Edge' r f a) Source Negative a => Negative (Edge' r f a) Source An edge is negative if its label is.

transposeEdge :: Edge s t e -> Edge t s e Source

Reverse an edge.

edges :: (Ord s, Ord t) => Graph s t e -> [Edge s t e] Source

Turn a graph into a list of edges. `O(n + e)`

edgesFrom :: (Ord s, Ord t) => Graph s t e -> [s] -> [Edge s t e] Source

All edges originating in the given nodes. (I.e., all outgoing edges for the given nodes.)

Roughly linear in the length of the result list `O(result)`.

edgesTo :: (Ord s, Ord t) => Graph s t e -> [t] -> [Edge s t e] Source

All edges ending in the given nodes. (I.e., all incoming edges for the given nodes.)

Expensive: `O(n * |ts| * log n)`.

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

Get all self-loops.

lookup :: (Ord s, Ord t) => s -> t -> Graph s t e -> Maybe e Source

Lookup label of an edge.

neighbours :: (Ord s, Ord t) => s -> Graph s t e -> [(t, e)] Source

Get a list of outgoing edges with target.

neighboursMap :: (Ord s, Ord t) => s -> Graph s t e -> Map t e Source

Get a list of outgoing edges with target.

sourceNodes :: (Ord s, Ord t) => Graph s t e -> Set s Source

Returns all the nodes with outgoing edges. `O(n)`.

targetNodes :: (Ord s, Ord t) => Graph s t e -> Set t Source

Returns all the nodes with incoming edges. Expensive! `O(e)`.

data Nodes n Source

For homogeneous graphs, `(s = t)` we can compute a set of all nodes.

Structure `Nodes` is for computing all nodes but also remembering which were incoming and which outgoing. This is mostly for efficiency reasons, to avoid recomputation when all three sets are needed.

Constructors

 Nodes FieldssrcNodes :: Set n tgtNodes :: Set n allNodes :: Set n

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

nodes :: Ord n => Graph n n e -> Set n Source

The set of all nodes (outgoing and incoming).

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

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

fromList :: (Ord s, Ord t) => [Edge s t e] -> Graph s t e Source

Constructs a graph from a list of edges. O(e log n)

Later edges overwrite earlier edges.

fromListWith :: (Ord s, Ord t) => (e -> e -> e) -> [Edge s t e] -> Graph s t e Source

Constructs a graph from a list of edges. O(e log n)

Later edges are combined with earlier edges using the supplied function.

toList :: (Ord s, Ord t) => Graph s t e -> [Edge s t e] Source

Convert a graph into a list of edges. O(e)

discrete :: Null e => Graph s t e -> Bool Source

Check whether the graph is discrete (no edges). This could be seen as an empty graph. Worst-case (is discrete): `O(e)`.

clean :: (Ord s, Ord t, Null e) => Graph s t e -> Graph s t e Source

Remove `Null` edges.

empty :: Graph s t e Source

Empty graph (no nodes, no edges).

singleton :: (Ord s, Ord t) => s -> t -> e -> Graph s t e Source

A graph with two nodes and a single connecting edge.

insert :: (Ord s, Ord t) => s -> t -> e -> Graph s t e -> Graph s t e Source

Insert an edge into the graph.

insertWith :: (Ord s, Ord t) => (e -> e -> e) -> s -> t -> e -> Graph s t e -> Graph s t e Source

Insert an edge, possibly combining `old` edge weight with `new` weight by given function `f` into `f new old`.

insertEdge :: (Ord s, Ord t) => Edge s t e -> Graph s t e -> Graph s t e Source

insertEdgeWith :: (Ord s, Ord t) => (e -> e -> e) -> Edge s t e -> Graph s t e -> Graph s t e Source

union :: (Ord s, Ord t) => Graph s t e -> Graph s t e -> Graph s t e Source

Left-biased union.

unionWith :: (Ord s, Ord t) => (e -> e -> e) -> Graph s t e -> Graph s t e -> Graph s t e Source

unions :: (Ord s, Ord t) => [Graph s t e] -> Graph s t e Source

unionsWith :: (Ord s, Ord t) => (e -> e -> e) -> [Graph s t e] -> Graph s t e Source

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

Removes the given node, be it source or target, and all corresponding edges, from the graph.

Expensive! `O(n log n)`.

removeEdge :: (Ord s, Ord t) => s -> t -> Graph s t e -> Graph s t e Source

`removeEdge s t g` removes the edge going from `s` to `t`, if any.

`O((log n)^2)`.

filterEdges :: (Ord s, Ord t) => (e -> Bool) -> Graph s t e -> Graph s t e Source

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

unzip :: Graph s t (e, e') -> (Graph s t e, Graph s t e') Source

Unzipping a graph (naive implementation using fmap).

mapWithEdge :: (Ord s, Ord t) => (Edge s t e -> e') -> Graph s t e -> Graph s t e' Source

Maps over a graph under availability of positional information, like `mapWithKey`.

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

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

sccs :: Ord n => Graph n 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 FieldsdagGraph :: 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.

Arguments

 :: Ord n => Graph n 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 n e -> DAG n Source

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

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

Returns `True` iff the graph is acyclic.

composeWith :: (Ord s, Ord t, Ord u) => (c -> d -> e) -> (e -> e -> e) -> Graph s t c -> Graph t u d -> Graph s u 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 lookup up all edges starting in with `t` in `g'`.

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

Transitive closure ported from Agda.Termination.CallGraph.

Relatively efficient, see Issue 1560.

gaussJordanFloydWarshallMcNaughtonYamadaReference :: forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n n e -> Graph n 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.

gaussJordanFloydWarshallMcNaughtonYamada :: forall n e. (Ord n, Eq e, StarSemiRing e) => Graph n n e -> Graph n 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 `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.

findPath :: (SemiRing e, Ord n) => (e -> Bool) -> n -> n -> Graph n n e -> Maybe e Source

Find a path from a source node to a target node.

The path must satisfy the given predicate `good :: e -> Bool`.

allPaths :: (SemiRing e, Ord n, Ord c) => (e -> c) -> n -> n -> Graph n n e -> [e] Source

`allPaths classify a b g` returns a list of pathes (accumulated edge weights) from node `a` to node `b` in `g`. Alternative intermediate pathes are only considered if they are distinguished by the `classify` function.