Directed Graphs

Small directed graph module providing the core graph-theoretic mechanisms used by the generalization linter.

---

Main definitions

• Digraph: Implemented as an adjacency list.
• Condensation: Condensation of digraph into DAG of SCCs.
• minCommonAncestors: Find the least upper bounds.

---

References

• [A. J. Best. 2023. Automatically Generalizing Theorems Using Typeclasses.][best2023automaticallyGeneralizingTheorems]
• [D. J. King, J. Launchbury. 1995. Structuring depth-first search algorithms in Haskell.][10.1145/199448.199530]

structure GeneralizationLinter.Digraph (V : Type u) [BEq V] [Hashable V] : Type u

Directed graph with vertices of type V, implemented through an adjacency list adj.

• adj : Std.HashMap V (Array V)

  Adjacency list of the directed graph.

  Given a vertex a, adj[a] is the array of immediate successors of a.

  Default: {}

  ---

  Example

  1 → 2 ─┐
  ↓   ↑  │    5
  3   4 ←┘
  

  For the graph shown above (where the 5 is an isolated vertex), we'd have:

  • adj[1] = [2, 3]
  • adj[2] = [4]
  • adj[3] = []
  • adj[4] = [2]
  • adj[5] = []

  ---

  Implementation Notes

  Storing the successors as an Array instead of a List is more efficient for our purposes. Conceptually, either one would work.

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedDigraph {a✝ : Type u_1} {a✝¹ : BEq a✝} {a✝² : Hashable a✝} : Inhabited (Digraph a✝)

Equations

• GeneralizationLinter.instInhabitedDigraph = { default := GeneralizationLinter.instInhabitedDigraph.default }

def GeneralizationLinter.Digraph.vertices {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Array V

Returns an array of the vertices of G in some order.

Equations

• G.vertices = G.adj.keysArray

def GeneralizationLinter.Digraph.contains {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (v : V) : Bool

Returns true iff G contains the vertex v.

Equations

• G.contains v = G.adj.contains v

def GeneralizationLinter.Digraph.succs {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (v : V) : Array V

Returns the immediate successors of v in G.

Warning: If v is not in G, this will silently return the empty array.

Equations

• G.succs v = G.adj.getD v #[]

def GeneralizationLinter.Digraph.insertVertex {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (v : V) : Digraph V

Inserts vertex v into G, and returns updated G.

Equations

• G.insertVertex v = if G.contains v = true then G else { adj := G.adj.insert v #[] }

def GeneralizationLinter.Digraph.insertEdge {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (s t : V) : Digraph V

Inserts edge s → t into G, and returns updated G. (s stands for "source vertex" and t stands for "target vertex" of the edge to be inserted.)

Equations

• One or more equations did not get rendered due to their size.

Reachability

partial def GeneralizationLinter.Digraph.dfs {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (v : V) (acc : Array V) (vis : Std.HashSet V) : Array V × Std.HashSet V

Depth-first search to compute transitive closure of v under G.

• acc is an array that will eventually contain all vertices reachable from v, including v itself. If G is acyclic, this list will be returned in postorder.
• vis is the set of visited vertices. It will eventually also contain all vertices reachable from v, including v itself.

def GeneralizationLinter.Digraph.downSet {V : Type u} [BEq V] [Hashable V] (G : Digraph V) (v : V) : Std.HashSet V

Returns the set of vertices of G reachable from v.

Equations

• G.downSet v = (G.dfs v #[] ∅).snd

def GeneralizationLinter.Digraph.downSets {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Std.HashMap V (Std.HashSet V)

Returns map from vertices to the set of vertices that each can reach.

Equations

• G.downSets = Std.HashMap.fold (fun (sets : Std.HashMap V (Std.HashSet V)) (v : V) (x : Array V) => sets.insert v (G.downSet v)) ∅ G.adj

def GeneralizationLinter.Digraph.postorder {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Array V

Equations

• G.postorder = (Array.foldl (fun (x : Array V × Std.HashSet V) (v : V) => match x with | (acc, vis) => G.dfs v acc vis) (#[], ∅) G.vertices).fst

def GeneralizationLinter.Digraph.transpose {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Digraph V

Returns transpose of G.

Equations

• One or more equations did not get rendered due to their size.

Condensation

def GeneralizationLinter.Digraph.sccs {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Array (Array V)

Strongly-connected components of G, computed with Kosaraju–Sharir's algorithm.

Equations

• One or more equations did not get rendered due to their size.

structure GeneralizationLinter.Digraph.Condensation (V : Type u) [BEq V] [Hashable V] : Type u

• graph : Digraph Nat

  Digraph of indices. Guaranteed to be a DAG.

• members : Std.HashMap Nat (Array V)

  Maps an index to the array of vertices contained in the SCC corresponding to the index.

• componentsMap : Std.HashMap V Nat

  Maps a vertex to the index of its parent SCC.

• downSetsByIndex : Std.HashMap Nat (Std.HashSet Nat)

  Maps an index to its corresponding down-set.

• vertices : Array Nat

  graph.vertices, cached inside condense.

def GeneralizationLinter.Digraph.condense {V : Type u} [BEq V] [Hashable V] (G : Digraph V) : Condensation V

Condense digraph G into DAG of SCCs of G and return the result as a Condensation structure.

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.Digraph.Condensation.indicesOf {V : Type u} [BEq V] [Hashable V] (c : Condensation V) (vs : Std.HashSet V) : Std.HashSet Nat

Returns indices of SCCs containing the vertices vs.

Equations

• c.indicesOf vs = Std.HashSet.fold (fun (indices : Std.HashSet Nat) (v : V) => match c.componentsMap[v]? with | some idx => indices.insert idx | none => indices) ∅ vs

Least Upper Bounds

inductive GeneralizationLinter.Digraph.Condensation.AbsencePolicy : Type

Establishes how minCommonAncestors should handle inputs that are unexpectedly not vertices of the given condensation.

• failClosed : AbsencePolicy

  Return an empty array. (Default.)

• failOpenGuarded : AbsencePolicy

  Filter out bad inputs and proceed as usual.

@[implicit_reducible]

instance GeneralizationLinter.Digraph.Condensation.instBEqAbsencePolicy : BEq AbsencePolicy

Equations

• GeneralizationLinter.Digraph.Condensation.instBEqAbsencePolicy = { beq := GeneralizationLinter.Digraph.Condensation.instBEqAbsencePolicy.beq }

def GeneralizationLinter.Digraph.Condensation.instBEqAbsencePolicy.beq : AbsencePolicy → AbsencePolicy → Bool

Equations

• GeneralizationLinter.Digraph.Condensation.instBEqAbsencePolicy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def GeneralizationLinter.Digraph.Condensation.instReprAbsencePolicy.repr : AbsencePolicy → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GeneralizationLinter.Digraph.Condensation.instReprAbsencePolicy : Repr AbsencePolicy

Equations

• GeneralizationLinter.Digraph.Condensation.instReprAbsencePolicy = { reprPrec := GeneralizationLinter.Digraph.Condensation.instReprAbsencePolicy.repr }

def GeneralizationLinter.Digraph.Condensation.minCommonAncestors {V : Type u} [BEq V] [Hashable V] (c : Condensation V) (reqs : Array (Std.HashSet V)) (ap : AbsencePolicy := AbsencePolicy.failClosed) : Array (Array V)

Idea: Given the set of classes that a theorem uses, find the minimal common ancestor of that set in the class DAG, i.e., the weakest common ancestor of the elements of the set (i.e., their meet), if a unique one exists. The class DAG is not a lattice, however, so the meet is not guaranteed to exist. In those cases, an antichain of incomparable answers is returned.

---

Implementation notes

The set of used classes is given as an array (requirements) of smaller sets. Currently, these smaller sets are usually singletons, except for used classes that are not universe polymorphic. In those cases, the corresponding smaller set consists of the used class with the specific universe level, and the universe-polymorphic version of the used class.

The idea is that the array of smaller sets communicates the requirements as a general AND of ORs. Let's call each smaller set a set of witnesses. The question then becomes:

Find a class that is a common ancestor to at least one witness of each requirement (i.e., a common ancestor of at least one transversal of the sets of witnesses).

The answer is returned as an array of arrays. Any element of any of the inner arrays is a class which satisfies, on its own, all the given requirements. The structure within which the classes are given encodes the relationships between all of these classes:

• All classes within each inner array are mutually equipotent. Each inner array therefore represents a single SCC of the class graph pre-condensation (or, equivalently, a single vertex in the class DAG, i.e., in the condensation of the class graph).
• The SCCs listed in the outer array are pairwise unreachable in the class graph. Alternatively, roughly speaking, the outer array represents the antichain of vertices of the class DAG which satisfy the requirements. More precisely, each of these vertices is a bona-fide minimal common ancestor; it's just that minimality doesn't generally imply uniqueness in our case, since the class DAG is not a lattice.

---

Examples

• Unique minimal common ancestor: Sometimes, there is exactly one minimal common ancestor.

  minCommonAncestors #[{Monoid}, {CommSemigroup}] = #[#[CommMonoid]]
  

• No common ancestors: Quite often, there may not exist any class which satisfies all the given requirements.

  minCommonAncestors #[{Inv}, {SDiff}] = #[]
  

• Minimal common ancestors of single classes: Within an SCC of the class graph (pre-condensation), all classes are pairwise equipotent. This means that any element of the SCC is a minimal common ancestor of any other element or subset of the SCC. Note that the vast majority of the SCCs of the class graph (pre-condensation) are singletons.

  minCommonAncestors #[{Nonempty}] = #[#[Inhabited, Nonempty]]
  minCommonAncestors #[{Monoid}] = #[#[Monoid]]
  

• Multiple non-equipotent minimal common ancestors: Rarely, requirements may have multiple non-equipotent minimal common ancestors.

  minCommonAncestors #[{Add}, {Mul}] = #[
    #[FirstOrder.Language.Structure]
    #[Lean.Grind.Semiring],
    #[Distrib],
  ]
  

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.Digraph.Condensation.reaches {V : Type u} [BEq V] [Hashable V] (c : Condensation V) (s t : V) : Bool

Given the condensation of a graph and two vertices s and t of the graph (pre-condensation), returns whether s reaches t in the graph (pre-condensation).

Equations

• c.reaches s t = match c.componentsMap[s]?, c.componentsMap[t]? with | some s_idx, some t_idx => (c.downSetsByIndex.getD s_idx ∅).contains t_idx | x, x_1 => false

def GeneralizationLinter.Digraph.Condensation.coalesceWith {α : Type u_1} [Inhabited α] (fuse : α → α → α) (connected : α → α → Bool) (xs : Array α) : Array α

Given an array xs and methods

• fuse to merge two elements of the array and
• connected to query whether two elements of the array should be merged,

returns an array in which no two elements should be merged anymore.

We require the following preconditions:

• connected must be a symmetric relation.
• For any a b c : α, connected a c implies connected (fuse a b) c.

---

Examples:

coalesceWith (·.append ·) (fun x y : List Nat => x.any y.contains)
  #[[1], [1, 2], [3], [2, 4], [5, 6]] = #[[1, 1, 2, 2, 4], [3], [5, 6]]
coalesceWith (·.union ·) (fun x y : HashSet Nat => !(x.inter y).isEmpty)
  #[{1}, {1, 2}, {3}, {2, 4}, {5, 6}] = #[{1, 2, 4}, {3}, {5, 6}]

Equations

• GeneralizationLinter.Digraph.Condensation.coalesceWith fuse connected xs = GeneralizationLinter.Digraph.Condensation.coalesceWith.loop✝ fuse connected xs (xs.size * xs.size + 1)

def GeneralizationLinter.Digraph.Condensation.partitionByDesc {V : Type u} [BEq V] [Hashable V] (used : Std.HashSet V) (conn : V → V → Bool) : Array (Std.HashSet V)

Partitions used into subsets whose down-sets are disconnected according to conn.

---

Example

Roughly speaking, in our use-case, if partitionByDesc was called on {Semigroup, MulOneClass, IsPreorder, IsTotal}, it would return [{Semigroup, MulOneClass}, {IsPreorder}, {IsTotal}]. Refer to the examples documented for sharesDataDesc for more information.

Equations

• One or more equations did not get rendered due to their size.