Agda.Utils.Graph.AdjacencyMap.Unidirectional

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.

Documentation

newtype Graph s t e

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

Fields

• graph :: Map s (Map t e)

  Forward edges.

Instances

(Ord r, Ord f) => SetToInfty f (ConGraph r f)

Methods

setToInfty :: [f] -> ConGraph r f -> ConGraph r f

Functor (Graph s t)

Methods

fmap :: (a -> b) -> Graph s t a -> Graph s t b

(<$) :: a -> Graph s t b -> Graph s t a

(Eq e, Eq t, Eq s) => Eq (Graph s t e)

Methods

(==) :: Graph s t e -> Graph s t e -> Bool

(/=) :: Graph s t e -> Graph s t e -> Bool

(Show e, Show t, Show s) => Show (Graph s t e)

Methods

showsPrec :: Int -> Graph s t e -> ShowS

show :: Graph s t e -> String

showList :: [Graph s t e] -> ShowS

(Ord r, Ord f, Negative a) => Negative (Graphs r f a)

Methods

negative :: Graphs r f a -> Bool

(Ord r, Ord f, Negative a) => Negative (Graph r f a)

A graph is negative if it contains a negative loop (diagonal edge). Makes sense on transitive graphs.

Methods

negative :: Graph r f a -> Bool

(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n n e)

Methods

prettyTCM :: Graph n n e -> TCM Doc

data Edge s t e

Constructors

Edge

Fields

• source :: s

  Outgoing node.

• target :: t

  Incoming node.

• label :: e

  Edge label (weight).

Instances

Eq f => SetToInfty f (Edge' r f a)

Methods

setToInfty :: [f] -> Edge' r f a -> Edge' r f a

Functor (Edge s t)

Methods

fmap :: (a -> b) -> Edge s t a -> Edge s t b

(<$) :: a -> Edge s t b -> Edge s t a

(Eq e, Eq t, Eq s) => Eq (Edge s t e)

Methods

(==) :: Edge s t e -> Edge s t e -> Bool

(/=) :: Edge s t e -> Edge s t e -> Bool

(Ord e, Ord t, Ord s) => Ord (Edge s t e)

Methods

compare :: Edge s t e -> Edge s t e -> Ordering

(<) :: Edge s t e -> Edge s t e -> Bool

(<=) :: Edge s t e -> Edge s t e -> Bool

(>) :: Edge s t e -> Edge s t e -> Bool

(>=) :: Edge s t e -> Edge s t e -> Bool

max :: Edge s t e -> Edge s t e -> Edge s t e

min :: Edge s t e -> Edge s t e -> Edge s t e

(Show e, Show t, Show s) => Show (Edge s t e)

Methods

showsPrec :: Int -> Edge s t e -> ShowS

show :: Edge s t e -> String

showList :: [Edge s t e] -> ShowS

(Ord r, Ord f, Dioid a) => Dioid (Edge' r f a)

Methods

compose :: Edge' r f a -> Edge' r f a -> Edge' r f a

unitCompose :: Edge' r f a

(Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a)

Methods

meet :: Edge' r f a -> Edge' r f a -> Edge' r f a

(Ord r, Ord f, Top a) => Top (Edge' r f a)

Methods

top :: Edge' r f a

isTop :: Edge' r f a -> Bool

Negative a => Negative (Edge' r f a)

An edge is negative if its label is.

Methods

negative :: Edge' r f a -> Bool

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

Reverse an edge.

edges :: Graph s t e -> [Edge s t e]

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

edgesFrom :: Ord s => Graph s t e -> [s] -> [Edge s t e]

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 t => Graph s t e -> [t] -> [Edge s t e]

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]

Get all self-loops.

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

Lookup label of an edge.

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

Get a list of outgoing edges with target.

neighboursMap :: Ord s => s -> Graph s t e -> Map t e

Get a list of outgoing edges with target.

sourceNodes :: Graph s t e -> Set s

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

targetNodes :: Ord t => Graph s t e -> Set t

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

data Nodes n

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

Fields

• srcNodes :: Set n
• tgtNodes :: Set n
• allNodes :: Set n

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

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

The set of all nodes (outgoing and incoming).

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

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

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

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

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

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

toList :: Graph s t e -> [Edge s t e]

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

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

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

clean :: Null e => Graph s t e -> Graph s t e

Removes Null edges (and empty Maps).

empty :: Graph s t e

Empty graph (no nodes, no edges).

singleton :: s -> t -> e -> Graph s t e

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

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

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

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

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

Left-biased union.

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

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

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

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

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

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

O((log n)^2).

filterEdges :: (e -> Bool) -> Graph s t e -> Graph s t e

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

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

Unzipping a graph (naive implementation using fmap).

mapWithEdge :: (Edge s t e -> e') -> Graph s t e -> Graph s t e'

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

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

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

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

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

data DAG n

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

DAG invariant.

oppositeDAG :: DAG n -> DAG n

The opposite DAG.

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

The nodes reachable from the given SCC.

sccDAG'

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

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

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

Returns True iff the graph is acyclic.

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

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.

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

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(e log n).

composeWith :: (Ord t, Ord u) => (c -> d -> e) -> (e -> e -> e) -> Graph s t c -> Graph t u d -> Graph s u e

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

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

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, [SCC n])

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.