Graph theory hierarchy

Stream: new members

[Jack Cheverton]

Hi,
I've been trying to do some work on graphs in Lean and further develop what is currently in the Mathlib library. The todo section in the Basic.lean file under simple graphs says:

"This is the simplest notion of an unoriented graph.  This should eventually fit into a more complete combinatorics hierarchy which includes multigraphs and directed graphs.  We begin with simple graphs in order to start learning what the combinatorics hierarchy should look like."

The current definition of the adjacency relation in a simple graph is:

Adj : V → V → Prop

If a larger graph hierarchy were to be made, is there any consensus on how to regard this as a multigraph?

[Philippe Duchon]

Actually the SimpleGraph structure includes the fact that the adjacency relation is both symmetric and irreflexive. If you remove the symmetry hypothesis, you get directed graphs (still without loops); if you remove the irreflexivity hypothesis, you allow loops.

I don't think multigraphs can fit into this. But if you want to add, say, directed simple graphs, my (neophyte) feeling is that SimpleGraph would have to extend SimpleDirectedGraph.

(My background is in a world where "graph" really means "finite graph", but of course Mathlib seems to make things as general as possible and as a consequence finiteness is always an added layer of complexity)

[Vincent Beffara]

There was a lot a discussion a year or so ago (here on Zulip in the graph theory channel) about refactoring the graph theory part of mathlib, with a view towards multigraphs, directed graphs, weighted graphs, hypergraphs and so on. I'm not sure what the current status of the refactor is.

As it is, it is indeed confusing that e.g. SimpleGraph is a basic object rather than a Graph that happens to isSimple.

One possible direction would be to reimplement the basic definitions using Serre's definition of a graph instead of an adjacency relation, it seems that building a hierarchy on top of that could be more feasible. That could be a fun project to try this out.

[Jon Bannon]

@Vincent Beffara : this is a very nice project idea. Interestingly, @Jack Cheverton found a rather large PR attempt trying to do just this. It was determined that there was too much overlap with the Quiver files in mathlib, and so the PR was closed unmerged. It seems funny that mathlib contains a definition of SimpleGraph and a definition of Quiver but nothing in between. Would it make sense to PR a file that defines Graph as an instance of Quiver that incorporates extra conditions? Is there a reason not to try this? It seems to me that if someone tries to Moogle Graph and finds nothing, that's strange. Is there some trouble with universes or something blocking this? (I am talking off-the-cuff here, since I don't know even if Quiver is a typeclass...)

[Jack Cheverton]

Can confirm what @Jon Bannon is saying.

[Kyle Miller]

Would it make sense to PR a file that defines Graph as an instance of Quiver that incorporates extra conditions?

An issue with Quiver for graph theory is that this is a typeclass whose instances associate edges to a given vertex type. This makes it awkward to talk about multiple graphs with the same vertex type, and in fact it makes it incorrect to do so since typeclass instances are supposed to be canonical.

I see talk in this thread about trying to make a hierarchy involving extending structures, but I don't think this will be workable (this is my opinion after thinking about how to do this for a few years). There are too many flavors of combinatorial objects, and a one-size-fits-all approach to try to come up with general structures is not possible.

In mathlib4#4127 I started a project to make a Digraph type and some graph interface typeclasses, and generalize SimpleGraph material to work with these typeclasses. I made some mistakes having these typeclasses involve types that are too dependent and ran into issues down the line with simp failing in some basic cases, but I think with some minor redesign it would be workable.

You can think about these typeclasses as being like a parameterized Quiver. Each graph object contains the data for how the vertices are connected, and you ought to supply that rather than leaving it implicit.

[Philippe Duchon]

I am not a graph theorist, but those I talk to on a regular basis tend to manipulate various flavors of graphs (simple or multi, unoriented or not, weighted or not - also planar or not, but that is probably another matter) according to the problem at hand - but I have never heard any of them talk of a quiver (and I don't know what it is either). So if graphs are defined in terms of quivers, my feeling is that the interface for "just graphs" had better be really transparent, or getting them interested in formalizing their results will be even harder.

[Kyle Miller]

@Philippe Duchon A quiver is a directed multigraph (with distinguishable edges -- sometimes multigraphs are defined to be a function V -> V -> Nat with indistinguishable edges, so it's worth mentioning this). The word comes from representation theory or category theory, and it's so-named because a quiver in archery is a collection of arrows (the edges, but with a category theory point of view).

[Jon Bannon]

@Jack Cheverton is my undergrad research student, and is interested in working toward being able to contribute some basic things to mathlib. @Kyle Miller , is there a specific few definitions where the dependent type hell is concentrated that I could try to think about fixing with Jack, for experience's sake? If not, we will step through the main file and look at your design.

[Kyle Miller]

It's been awhile and I don't remember the exact details, but for example this technical lemma was there to put something into the correct form so that a simp lemma was applicable.

This is all for the sake of making a uniform interface. To some degree I think it's also fine to move forward and define various graph objects and try to unify later.

In case it's helpful, there's a Digraph type at https://github.com/kmill/msri2023_graphs/tree/main/GraphProjects from taking much of the SimpleGraph material and adapting it.

[Jon Bannon]

@Kyle Miller : Thanks for pointing us to the lemma. We will look at these and perhaps to try to make some small contributions, awaiting the later unification effort. Will try to stay close to what you have designed thus far.

[Jack Cheverton]

@Kyle Miller Would it be alright if I worked on porting what you've done into Mathlib? I'm looking to get some practice into going through the PR process and I think trying to submit this would be useful. Plus, it seems like this is the most well thought out attempt of designing digraphs currently available.

[Kyle Miller]

@Jack Cheverton Sure (and Zulip tip: the syntax to ping someone is @**Jack Cheverton** with the asterisks).

How about this:

1. Take a chunk of Digraph.lean (100-300 lines) and create Mathlib/Combinatorics/Digraph/Basic.lean
2. Carefully compare this to what's in Mathlib/Combinatorics/SimpleGraph/Basic.lean to see if anything has changed for SimpleGraph in the meantime (you can look at the file history to help with this)
3. Create the PR and request my review.

Something I think I'm going to try to organize this summer is a group project to get graph theory moving, with a goal being to finally have all the basic graph types. Be sure to join the #graph theory channel!

[Jack Cheverton]

@Kyle Miller May I have permission to push branches up to Mathlib? My GitHub username is jt18chev

[Jireh Loreaux]

@Jack Cheverton please see https://github.com/leanprover-community/mathlib4/invitations

[Jack Cheverton]

@Kyle Miller Question for you about credit and the PR process: would there be any issue with me listing you as an author in the Digraph file and you reviewing that same file? It seems to me like there could be a potential conflict of interest. If that would be an issue, do you have any ideas of how to cleanly go about doing this?

[Kyle Miller]

@Jack Cheverton There's no problem with that. The "authors" list is meant to be "who would be good people to talk to about this file?"

[Jireh Loreaux]

Kyle can always ask for a second set of eyes from other maintainers if he feels he has contributed too much to the code. This happens regularly.

[Jack Cheverton]

@Kyle Miller I submitted a PR for the Digraph file and set you as a reviewer. However, I just found a major issue with the file. It previously allowed for vertices to connect into themselves, but this would make it into a directed multigraph rather than just a standard digraph. So for the time being you can ignore that PR and I'll ping you when it's ready.

[Jack Cheverton]

Actually, it might be better to have the standard Digraph allow loops and then define some sort of Simple Digraph later that doesn't. So that PR should actually be ready for review now. Sorry for the confusion!

[Kevin Buzzard]

If you want the PR to be ignored you can just close it with an explanation there, that will definitely do the trick! You can reopen it later if you decide to fix it up.

[Jon Bannon]

Hi all, for the record, @Jack Cheverton 's PR #14091 is no longer buggy (in fact, there was no major issue). I will review it, but am not an expert on the graph theory design choices so probably will need some backup!

(I imagine announcing this here is bad form for some reason I am not aware of...if this is the case then my apologies!)

[Kevin Buzzard]

Announcing it here is fine but there's also a channel #PR reviews where you can feel free to talk about other people's PRs.