Weak components of a digraph

Stream: Is there code for X?

[Niels Voss]

At Knuth's lecture on Thursday, he defined the weak components of a digraph to be the finest partition of its vertices such that for any two distinct weak components A and B, either there is a path from every element of A to every element of B but no path from any element of B to any element of A, or there is a path from every element of B to every element of A but no path from any element of A to any element of B. If the graph is acyclic, the definition simplifies to there being a path from every element of A to every element of B or vice versa. See page 11 here: https://cs.stanford.edu/~knuth/fasc12a+.pdf

The intuition is that when you take the strong components of a graph and contract each of them to a single vertex, you end up with a graph that is partially ordered by reachability. When you take the weak components of a graph and contract them to a single vertex, you end up with a graph that is linearly ordered by reachability. Knuth thinks that the common definition of weakly connected components is less useful than this new definition and should be renamed to "undirected components".

I was wondering if there way anything like this in mathlib? I can't even even find the strongly connected components of a diagraph in mathlib (unless you count Quivers as digraphs).

[Kyle Miller]

It's possible that strongly connected components exists somewhere for relations (the RflTransGen is partway there, and then you'd take a quotient to make it trichotomous), but digraphs are relatively new so it's not surprising it hasn't been defined yet for them.

[Niels Voss]

I don't see how taking a quotient of the strongly connected components will make it trichotomous. Doesn't that only get you an antisymmetric relation, not necessarily a trichotomous relation?

[Kyle Miller]

You're right, I meant antisymmetric.

[Kyle Miller]

(Unless I'm mistaken, taking ReflTransGen R and then quotient by fun x y : ReflTransGen R => x ≤ y ∧ y ≤ x gives a type whose terms are strongly connected components. I'm curious if this is already in mathlib somewhere. It seems plausible that there are cases where you start with an almost poset and then want to impose antisymmetry.)

[Niels Voss]

There is docs#AntisymmRel.setoid and docs#Antisymmetrization for preorders specifically, so I guess it is already in mathlib. However, I think strongly connected components are missing. Is this something that that there's interest in?

[Niels Voss]

I could see something similar for turning partial orders into total orders via Knuth's weak components, although I'm not sure what that's useful for

[Kyle Miller]

Yeah, I'd be interested in seeing the development of strongly connected components for digraphs.

(By the way, lean4#6189 paired with the unmerged lean4#6267 I hope will have an effect on the development of graph theory. These should make it possible to finally be able to have a generic HasAdj class and be able to write G.Adj with it, in addition to other generic constructions like paths and connected components.)

[Niels Voss]

What's the status of #4127? It seems that this PR has been around longer than Digraph has yet seems to contain more stuff than the current Digraph

[Kyle Miller]

There were a few obstructions:

• I didn't want to lose G.Adj v w, so I've been waiting on changes to core.
• It was unclear whether HasAdj should be dependent on the graph, or if that's just an unnecessary complication. It's conceivable that there are graph structures that would want the vertex type to be a field of the structure.
• There were some really bad simp failures. It's possible that simp has improved enough in the interim, but I haven't checked. These helper lemmas were necessary to get some obvious simps to go through, but they shouldn't be necessary: https://github.com/leanprover-community/mathlib4/pull/4127/files#diff-fe0532c2bbc700795928c8fe1cdb0a7a07bd69b3d8a97117c08f0f84b159b091R915-R917 https://github.com/leanprover-community/mathlib4/pull/4127/files#diff-fe0532c2bbc700795928c8fe1cdb0a7a07bd69b3d8a97117c08f0f84b159b091R1172-R1173

[Niels Voss]

Do you think there's any merit in trying to get the absolute most general definition of a graph into mathlib or should we just try to work at suitable levels of abstraction? The problem I see with this is that even Quiver isn't general enough to accommodate all types of graphs (it can't accommodate weighted graphs or mixed graphs) so anything that general would basically have to become a notation typeclass.

[Kyle Miller]

I doubt that there's a most general graph, and that's an idea behind #4127 — let's make it easy to define a structure for the combinatorics you want to do, and then give enough typeclass instances to hook in general theory and constructions that apply to the structure.

Even SimpleGraph isn't meant to be "the" simple graph by the way. It's the abstract interface to a simple graph, and for concrete applications you need to make a custom data structure with a function giving it a SimpleGraph view. (The bridges of Konigsberg proof in the Archive uses an edge list representation for example. There could be some more general constructions here so it doesn't need to be ad hoc.)

[Niels Voss]

What about making a DigraphLike typeclass, inspired by SetLike and FunLike? Or would this essentially be the same as HasAdj?

[Kyle Miller]

That's HasAdj, though feel free to be inspired on your own and see if something different comes out of it.

[Niels Voss]

Is there interest in trying to revive #4127?

[Kyle Miller]

Yes, I hope it's clear that I'm interested in it, even if there's been no obvious progress on #4127 itself for awhile now. For obstruction 1, the only thing remaining is a way to set which argument gets to be used for dot notation (lean4#6267), which will save a lot of unnecessary code churn.

For the other two obstructions, it would be helpful to know if simp has gotten better. This will take work to bring the PR up to date, which needs to be done anyway. If it's something you're interested in doing, feel free! I don't expect it to be straightforward unfortunately.

[Niels Voss]

I'll try to take a look at it after exams

[Niels Voss]

I'm going to try looking at #4127. Is lean4#6267 a hard dependency of #4127, or would it be possible to work on #4127 without having lean4#6267 merged, and just change the notation later?

An alternative to dot notation would be to define new notation for HasAdj.Adj, so that instead of writing G.Adj A B we could write something like A ~G~ B or G⇢ A B or A [G]⇢ B or something. This could potentially tie in to quiver syntax, so that A ⟶ B is the type of typeclass inferred quiver homs, and A [G]⟶ B or A ⟶ B [G] is the type of non-typeclass inferred quiver homs. This also leaves open the option to add symbols for bidirectional connections.