Is it safe to interpret `Quiver` as a digraph?

Stream: new members

[Jihoon Hyun]

Of course, quiver is clearly another way of calling a directed graph, but I'm wondering if there were some thoughts about distinguishing them when defining docs#Quiver . (For instance, quiver is defined as a typeclass, but docs#SimpleGraph is defined as a structure.)

[Niels Voss]

One thing to note about Quiver is that it lets you have an arbitrary type as your set of edges between any two vertices, so it's more like a multidigraph. According to the documentation of Quiver, you can use Quiver.{0} V if you want to prevent repeated edges.

One important thing to note about quivers is that they form the backbone of the category theory library in mathlib, so you'll see a lot of category theory specific notation and terminology (less so when you aren't using it as a typeclass though)

[Niels Voss]

If you wanted to use a digraph, I would either use the Digraph type directly or just a V -> V -> Prop (in classical math, a digraph is a set + a relation on that set, but in Lean types are usually decoupled from the structures on them, so in Lean a digraph is just a relation)

[Niels Voss]

If you'd like, you can think of making an instance of Quiver as basically a way to overload the the a ⟶ b notation, which intuitively represents the set of morphisms between two objects (not to be confused with the A → B notation which is the type of functions from A to B)

[Jihoon Hyun]

Then why is Digraph not designed to accept multiple edges? I don't think people are only interested in digraphs without multiple edges.

[Niels Voss]

But some people are interested in graphs without multiple edges, so there needs to be a type for those that doesn't require passing around "there is at most one edge between any pair of vertices" as a hypothesis to several theorems

[Niels Voss]

That being said, Digraph doesn't need to be the only digraph type, it's possible that in the future we might add a Multidigraph type

[Jihoon Hyun]

Niels Voss 말함:

That being said, Digraph doesn't need to be the only digraph type, it's possible that in the future we might add a Multidigraph type

And maybe MultiGraph, too. Would you also be happy if there is a definition for both?

[Niels Voss]

I think this is the point we start running into issues. There's really no such thing as a "graph" in math, since there are dozens of different types of graphs. If we wanted a type for every sort of graph, we would need

• Simple Graphs
• Digraphs
• Digraphs without loops
• Multidigraphs
• Multigraphs
• Undirected graphs (i.e. Simple Graphs but they can include loops)
• Weighted graphs
• Mixed graphs
• Hypergraphs
• Digraphs where the edges have their own identity

[Niels Voss]

If we did this naively, this would be bad, because we would need to keep reproving the same facts for different types of graphs. So, we clearly need an a priori approach to adding different types of graphs

[Niels Voss]

unfortunately, there doesn't seem to be one yet, although this is something multiple people have spent some time thinking about. For example, a while back @Kyle Miller had worked on #4127, which should hopefully be a step in the right direction

[Niels Voss]

There's the also the issue of what you actually mean by a multigraph. If you look at https://en.wikipedia.org/wiki/Multigraph, then you'll notice there are two different definitions of undirected multigraphs. Let's assume you want the latter.

In classical math, a simple (non-multi) graph is a set of vertices along with a subset of the pairs of vertices. Technically, in classical math, you are not allowed to talk about the set of all graphs, because from there you could get the set of all sets, which leads to Russell's paradox. However, given a set of vertices, you can talk about the set of simple (non-multi) graphs on those set of vertices. That is, instead of talking about graphs in general, we talk about graphs on V, where V is a fixed set of vertices. This is what Lean does, so there's no issue.

If you instead choose to define a multigraph as a set V along with for every pair of vertices, a set of edges between them, then you can't even talk about the set of multigraphs on V, because you hit Russell's paradox right away. In Lean, this problem manifests itself by the fact that Quiver requires you to increase the universe level by 1, which can make some things ugly.

[Niels Voss]

All of this is to say that the reason we don't have MultiGraph yet is that we haven't yet figured out a good way to add it.

[Jihoon Hyun]

Thanks for the brief overview!
It seems like we might need a new definition of multiset with infinite cardinality in consideration, and HasAdj in #4127 to be extended to accept more or less than two vertices (by multiset described earlier).
Also to consider weights, we may also define HasWeightedAdj typeclass extended from HasAdj.

Something like def MultiSet (\a : Type*) : \a \to Sort _ and class HasAdj (Γ : Type _) (V : outParam (Γ → Type _)) where Adj (G : Γ) : MultiSet (V G) → Prop may work for example, but we probably need more discussion for these.

[Niels Voss]

The Multiset in mathlib is more of a data structure than a practically usable type; that is why it only allows finite cardinality. For infinite Multisets, the definition you'd want would be

def InfMultiset (A : Type u) : Type u := A -> Nat

although at that point I'm not even sure its worth having this as its own type.

[Niels Voss]

Out of curiosity, do you have a specific thing you plan to do with digraphs or multigraphs? If you're interested in them just because, then that's totally fine, but if you're trying to accomplish something there might be an easier way that doesn't require resolving the hard problem of getting good graph theory definitions

[Jihoon Hyun]

Niels Voss 말함:

The Multiset in mathlib is more of a data structure than a practically usable type; that is why it only allows finite cardinality. For infinite Multisets, the definition you'd want would be

def InfMultiset (A : Type u) : Type u := A -> Nat

although at that point I'm not even sure its worth having this as its own type.

I'm aware of Multiset. The definition you suggested might not work for types with more diverse cardinality.

Niels Voss 말함:

Out of curiosity, do you have a specific thing you plan to do with digraphs or multigraphs? If you're interested in them just because, then that's totally fine, but if you're trying to accomplish something there might be an easier way that doesn't require resolving the hard problem of getting good graph theory definitions

Actually, no, Digraph is enough for my case. Since Quiver has more APIs to use than Digraph, I was just wondering why Quiver is defined (again, aside from Digraph) in Mathlib, and has more theorems than Digraphs.

[Niels Voss]

Oh right, I completely forgot that infinite multisets might allow infinite cardinality. In that case, maybe A -> Cardinal might work, although there might be a more elegant way to define it. Plus this requires a universe bump, so it's not like it's any better than Quiver.

The documentation at the top of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Digraph/Basic.html describes why we aren't just using Quiver.{0}. To be fair, I'm not completely sure myself why we couldn't have used Quiver.{0} despite the fact that it is a class, but the Digraph here is definitely clearer.

[Niels Voss]

Eventually, we might want Digraph to as much API as Quiver, although that might be blocked behind #4127, which is in turn blocked behind lean4#6489

[Niels Voss]

What sort of API is present in Quiver that you need that's missing from Digraph?

[Jihoon Hyun]

Well, that's what I have to figure out, but I searched for connected components and that's definitely not implemented for digraphs.
Aside from APIs from quiver, I probably need orientation of a graph, which is not implemented yet. I'll fill in the TODOs when I need them.

[Niels Voss]

Maybe you can ask in "Is there code for X?" I'm not super familiar with every part of mathlib, so there might be people there who can tell you whether or not such a thing exists, or if there's something similar for relations that can easily be translated to graphs (e.g. a clever way to combine existing things like transitive closures and antisymmetrizations to get a setoid).

Also, if you're looking for ways to contribute to mathlib, these might be valuable things to add! You'd probably need to discuss how graph theory development should be handled right now with someone more knowledgeable than I am

[Philippe Duchon]

Niels Voss said:

I think this is the point we start running into issues. There's really no such thing as a "graph" in math, since there are dozens of different types of graphs. If we wanted a type for every sort of graph, we would need

• Simple Graphs
• Digraphs
• Digraphs without loops
• Multidigraphs
• Multigraphs
• Undirected graphs (i.e. Simple Graphs but they can include loops)
• Weighted graphs
• Mixed graphs
• Hypergraphs
• Digraphs where the edges have their own identity

That's very true, unfortunately - and it's only the tip of the iceberg. Once you've picked your graphs, you have to agree on what constitutes a path, or a cycle.

I'm very interested in seeing how the graph part of the library evolves, including what tricks can be used to accomodate variants of the notions without duplicating lots of code. My naive view would be that the "right" way would be to have maximal generality (something like, multidigraphs with labelled edges and vertices) and make it as simple as possible to specialize, but it's very possible that there are good design reasons not to pick that as a solution.

[Niels Voss]

The "multidigraphs with labeled edges and vertices" approach you mentioned is basically Quiver, but it requires a universe bump so maybe we shouldn't use it everywhere. Plus, this isn't actually full generality: it doesn't accommodate weighted graphs, mixed graphs, hypergraphs, etc. (arguably hypergraphs barely count as graphs, and maybe shouldn't need to fit into the standard graph hierarchy).

Additionally, it's not clear it can easily be specialized. Suppose you want multigraphs where the edges have no identity and there must be a finite number of them between two vertices. You can't actually express this as a subtype of Quiver. Quiver lets you pick any type between two given vertices to act as your set of edges, and it's very hard to force it to be finite or to remove the identity between edges.

[Niels Voss]

It seems what we would need is an extra layer of abstraction on top of Quiver to specify the acceptable type of Homs. Something like:

def GeneralizedQuiver.{v,u} (C : Type v) (V : Type u) where
    Hom : V -> V -> C

and then Quiver.{v,u} becomes GeneralizedQuiver (Sort v), and a weighted graph becomes GeneralizedQuiver Real, and a multidigraph with finite edge counts and no identity becomes GeneralizedQuiver Nat. Digraph is either Quvier.{0} or GeneralizedQuiver Prop, and SimpleGraph would be a subtype of Digraph. I'm not sure how to do mixed graphs (maybe like GeneralizedQuiver (Fin 3) + some symmetry property?), and hypergraphs seem hopeless.

Now that I think about it, effectively, all GeneralizedQuiver is is operator overloading for the Hom operator.

Maybe this doesn't actually make any sense (it's really late for me, so I'm not thinking straight) but I can't think of any other way to do it. I also have no idea where typeclasses should be involved.

[Jihoon Hyun]

Maybe you can ask in "Is there code for X?"

I was about to ask there, but I accidently posted the question here.

[Philippe Duchon]

Niels Voss said:

The "multidigraphs with labeled edges and vertices" approach you mentioned is basically Quiver, but it requires a universe bump so maybe we shouldn't use it everywhere. Plus, this isn't actually full generality: it doesn't accommodate weighted graphs, mixed graphs, hypergraphs, etc. (arguably hypergraphs barely count as graphs, and maybe shouldn't need to fit into the standard graph hierarchy).

In my mind, once you have identities on vertices and edges you can add weights as a mapping from vertices/edges to wherever your weights should live in. It would probably feel better to have them in the graph structure itself, but it's something that would become partly transparent with implicit arguments.

One other thing that would make graph theorists (at least, those that I know) very confused would be if it was difficult to state that their graphs are finite. This is very often an unstated (because it's so obvious) assumption in some areas, but in others it would make the notion next to to useless.

As an example, recently some colleagues (working with Coq instead of Lean, but the problems are similar) wanted to use graphs and paths to formalize results about transition systems, but since the graph part of the mathematical library in Coq assumes finiteness, they'd have to rewrite it almost from scratch.

[Niels Voss]

Oh I kind of see how you could do that with Quiver now. If we are talking about weighted (non-multi) digraphs, then we basically have

def WeightedGraph (V : Type u) where
    Hom : V -> V -> Prop -- would probably come from extending Quiver.{0}
    val (a b : V) : Hom a b -> Real

This is effectively just a partial function from V x V ->. Real

I'm not sure how to define a multigraph without identity using this. I first thought that maybe we could just do the same thing but with Nat instead of Real, but then that distinguishes between an empty edge set and a 0-edge set.

[Niels Voss]

Actually, now that I thinl about it, making the edge weight decoupled from the existence of an edge is not as weird as it sounds, and might be the right way to go

[Jihoon Hyun]

Niels Voss said:

Actually, now that I thinl about it, making the edge weight decoupled from the existence of an edge is not as weird as it sounds, and might be the right way to go

It actually sounds better to have a separate function-like definition for weight of a graph, than a separate definition (possibly extended) of weighted graph. If we make a separate structure, then all those functions which apply to unweighted graph will also apply to weighted graph, which may result in a duplication of similar theorems.