Module Graph.WeakTopological
Weak topological ordering of the vertices of a graph, as described by François Bourdoncle.
Weak topological ordering is an extension of topological ordering for potentially cyclic graphs.
A hierarchical ordering of a set is a well-parenthesized permutation of its elements with no consecutive (. The elements between two parentheses are called a component, and the first elements of a component is called the head. A weak topological ordering of a graph is a hierarchical ordering of its vertices such that for every edge u -> v of the graph, either u comes (strictly) before v, or v is the head of a component containing u.
One may notice that :
- For an acyclic graph, every topological ordering is also a weak topological ordering.
- For any graph with the vertices
v1, ..., vN, the following trivial weak topological ordering is valid :(v1 (v2 (... (vN))...)).
Weak topological ordering are useful for fixpoint computation (see ChaoticIteration). This module aims at computing weak topological orderings which improve the precision and the convergence speed of these analyses.
- author
- Thibault Suzanne
- see Efficient chaotic iteration strategies with widenings
, François Bourdoncle, Formal Methods in Programming and their Applications, Springer Berlin Heidelberg, 1993
module type G = sig ... endMinimal graph signature for the algorithm
type 'a element=|Vertex of 'a|Component of 'a * 'a tThe type of the elements of a weak topological ordering over a set of
'a.Vertex vrepresents a single vertex.Component (head, cs)is a component of the wto, that is a sequence of elements between two parentheses.headis the head of the component, that is the first element, which is guaranteed to be a vertex by definition.csis the rest of the component.
and 'a tThe type of a sequence of outermost elements in a weak topological ordering. This is also the type of a weak topological ordering over a set of
'a.
val fold_left : ('a -> 'b element -> 'a) -> 'a -> 'b t -> 'aFolding over the elements of a weak topological ordering. They are given to the accumulating function according to their order.
Note that as
elements present in an ordering of typetcan contain values of typetitself due to theComponentvariant, this function should be used by defining a recursive functionf, which will callfold_leftwithfused to define the first parameter.