Documentation

A Graph has node elements a, and is just a relation between nodes.

Notation:

kvss : Graph a

(same as general dictionaries)

Property:

(v ↦ ks) ∈ graph-transpose(kvss) ⟺ ∀ (k ↦ vs) ∈ kvss. k ∈ ks ⟺ v ∈ vs

Run the Kosaraju algorithm, which computes strongly connected components. The algorithm computes a canonical node for each strongly connected component, and maps each node to the canonical node for strongly connected component in which it lives.

Definition:

strongly-connected ∈ ℘(Graph) strongly-connected(kvss) ≜ ∀ k₁,k₂ ∈ nodes(kvss). ∃ path(k₁,k₂) strongly-connected-components ∈ ℘(℘(Graph)) strongly-connected-components(kvsss) ≜ (∀ kvss ∈ kvsss. strongly-connected(kvss)) ∧ (∀ kvss₁,kvss₂ ∈ kvsss. ¬strongly-connected(kvss₁ ∪kvss₂))

Property:

∀ kvss. strongly-connected-components( values( graph-transpose( { k ↦ {v} | (k ↦ v) ∈ kosaraju(kvss) }

In the context of this function, we treat the element a like variables that have a definition/use structure. The first argument deps encodes dependencies from definitions of things to uses of things.

From a dependency relation, compute two elements: 1. The strongly connected components for the dependency relation, represented as a map from variables to a canonical SCC elements for its dependency group 2. A map from canonical SCC elements to: (a). All variables in its dependency group (i.e., the inverse of (1)) (b). All dependencies of all variables in the dependnecy group

1. is computed using kosaraju, but with an additional bit of information in the node representation that encodes def/use information, following these two semantic ideas: - *Use* of any variable x depends on the *definition* of that variable x - If `{x ↦ y}` appears in deps, this means that *definition* of variable x depends on *use* of variable y.

Compute strongly connected components following a dependency map, and process each component with a monadic action.

sccEachGroupM xs deps f

• xs represents a desired ordering in which to process variables (e.g., if definitions x and y do not depend on each other, and x comes before y in xs, then call f on the SCC group for x before doing the same for y.)
• deps represents dependency information. See sccGroups for how these are processed.
• `f b xs′` represents an action to perform on each SCC group. If the group is non-recursive, then b will be False and `|xs′| = 1`. If the group is recursive, then b will be True and `|xs′| ≥ 1`.

Similar to sccEachGroupM, but specialized to the identity monad.