graph typeclasses

Stream: graph theory

[Kyle Miller]

I had some ideas for how the graph theory refactor might go, and so I made a branch with partial progress #10963.

The idea is to have typeclasses such as

class has_adj (G : γ) (V : out_param $ Type v) := (adj : V → V → Prop)

along with property typeclasses such as

class is_adj_symmetric (G : γ) (V : out_param $ Type v) [has_adj G V] : Prop :=
(adj_symm [] : symmetric (has_adj.adj G))

That way, anything that implements various subsets of these gets access to generic functions like neighbor_set.
The only real downside seems to be that we lose dot notation.

One thing I made sure to take care doing was making sure we are able to preserve nice defeq properties. For simple_graph, one can still prove this with iff.rfl:

lemma mem_edge_set {v w : V} : ⟦(v, w)⟧ ∈ edge_set G ↔ adj G v w := iff.rfl

This is implemented by allowing instances to choose their own definitions for things like edge_set so long as they satisfy some property.

[Yaël Dillies]

branch#quantum_graph/src/combinatorics/quantum/hierarchy.lean now contains 17 structures and their 17 corresponding classes.

[Kyle Miller]

It would be good to pool ideas for this @Yaël Dillies, since this refactor is a good amount of design work (and this PR is just an essay into the problem), and it has many consequences for the graph theory library.

I'm hoping we can do it in an incremental way so we don't inadvertently lose things. I've broken some nice-looking proofs trying to make some general things work.

[Yaël Dillies]

Of course!

[Yaël Dillies]

One thing I'm noting is that your is_adj_symmetric class does not extend has_adj. Instead, this is what I do:

/-- `symm_rel_class F α` states that `F` is a type of symmetric relations on `α`.

Extend this class when you extend `symm_rel`. -/
class symm_rel_class (F : Type*) (α : out_param $ Type*) extends rel_class F α α :=
(to_fun_symm (f : F) : symmetric (to_fun f) . obviously)

[Yaël Dillies]

Also, I introduce the new notation a ⟶[G] b for the type of edges from a to b in multigraph G (actually only requires quiver_class).

[Kyle Miller]

I did that so it's possible to include/exclude different axioms. For example, you can define a new structure implementing has_adj and imbue it with is_adj_symmetric and is_adj_reflexive and now you have reflexive graphs.

[Kyle Miller]

I decided to make has_edges (similar to quiver_class) extend has_adj to avoid some unpleasantness when it comes to giving has_edges a default has_adj implementation.

[Yaël Dillies]

I agree that symmetry and irreflexivity can be made mixins.

[Yaël Dillies]

I was also thinking about making a default implementation for the adjacency relation.

[Kyle Miller]

The way it works here is that you're required to implement has_adj such that ∀ (v w : V), (edges v w).nonempty ↔ adj v w is satisfied. While that completely constrains what it is, since you're allowed to implement adj yourself, you can give it whatever definition would be most convenient.

[Yaël Dillies]

Yeah of course.

[Yaël Dillies]

And yet it only constrains it for this specific family of graphs.

[Kyle Miller]

Btw, in multigraph you need to take care what happens for self-loops. A similar problem occurs in branch#hedetniemi, though at least yours has only "one-ended" and "two-ended" self-loops.

[Yaël Dillies]

What do you mean? I was wondering whether I needed hom_fun a a : (a ⟶ a) → (a ⟶ a) to be the identity. Is it that?

[Kyle Miller]

You have to decide whether it's the identity or whether it's an involution with no fixed points.

[Kyle Miller]

The first in my experience is easier to deal with, but the second ensures that every edge has exactly two darts.

[Yaël Dillies]

I've identified 5 families of graphs that each have different data fields:

• Prop-valued graphs: rel, simple_digraph, symm_rel, simple_graph. Each have an adjacency relation α → β → Prop or α → α → Prop.
• Hypergraphs: hypergraph. Has a set of nonempty hyperedges set (set α).
• option-valued graphs, aka weighted/labeled graphs: weighted_digraph, weight_simple_digraph, weight_graph, weight_simple_graph. Each have a weight relation α → β → option W or α → α → option W.
• Sort-valued graphs: quiver, simple_quiver, multigraph, simple_multigraph. Each have edges functions α → α → Sort*.
• Weighted Sort-valued graphs: weight_quiver, weight_simple_quiver, weight_multigraph, weight_simple_multigraph. Each have edges functions α → α → Sort* and edge weights (a ⟶ b) → W.

[Yaël Dillies]

Edge coloring is the same as edge weight, except that it's a structure rather than being part of the definition.

[Yaël Dillies]

One takeaway is that edge weight is very different to weight between two vertices, and should be treated as such.

[Yaël Dillies]

What I dislike with the mixin approach is that it fails to go through the four main families of graphs, although they clearly have the same "nothing", "irreflexive", "symmetric", "symmetric and irreflexive" relation. Irreflexivity works, but not symmetry.

[Yaël Dillies]

Something else the mixin approach misses is types for the graphs that respect the mixin, which is definitely needed for some constructions. For example, without simple_graph, we can't talk about the complement of a simple graph, because that involves not complementing G.adj a a. So either we don't use mixins, or we must introduce disparity between graph types and graph classes.

[Yaël Dillies]

Kyle Miller said:

It would be good to pool ideas for this

How do you want to do that? Because I thought I was the only one working on it at the moment, so we effectively duplicated a huge chunk of work...

[Kyle Miller]

Yaël Dillies said:

How do you want to do that? Because I thought I was the only one working on it at the moment, so we effectively duplicated a huge chunk of work...

Like this discussion we're having, since until now I didn't have a clear idea what you were up to. Being able to make universal definitions for graph theory is something I've had my eye on since the beginning, but the right ideas never really came together to make something ergonomic and workable.

Usually in other projects what we'd need to do is create a proposal (an RFC) and get community support before changing the way things work at such a deep level, and I figure the next best thing is to have a couple competing implementations. We have two refactorings that work in substantially different ways, so there is certainly some design discussion to be done.

[Kyle Miller]

At a high level, I've been thinking of this as a universal algebra problem: how do we deal with the fact that each type of combinatorial object is some collection of data and properties? Depending on which data exists and which properties hold, can we let those objects use some shared definitions? Can we support having forgetful morphisms from a graph type that that is more constrained to a less-constrained type? Can we support having additional data that isn't under the purview of the graph theory library itself?

One solution is having two parts: (1) typeclasses for properties and (2) concrete implementations. What I think is the ideal is giving users the freedom to take any structure they might have defined and then implement instances to make it appropriately graphy. Ideally one would only need to then define things that are truly specific to the particular application.

Yaël Dillies said:

Something else the mixin approach misses is types for the graphs that respect the mixin, which is definitely needed for some constructions. For example, without simple_graph, we can't talk about the complement of a simple graph, because that involves not complementing G.adj a a. So either we don't use mixins, or we must introduce disparity between graph types and graph classes.

The intent of the mixins is just to give additional definitions and lemmas. They definitely are not sufficient to be able to define constructions on graphs themselves, since for that you need to know specific details about the underlying structure.

In the branch, simple_graph is the plain old structure from before, but it uses a standard implementation of a typeclass that gives it sym2 V edges via its symm property. It has to go on and define the boolean_lattice unaided, though, since that really depends on extensionality properties of the type.

@[ext]
structure simple_graph (V : Type u) :=
(adj' : V → V → Prop)
(symm : symmetric adj' . obviously)
(loopless : irreflexive adj' . obviously)

instance simple_graph.has_simple_undirected_edges {V} (G : simple_graph V) :
  has_simple_undirected_edges G V :=
graph.default_simple_undirected_edges G G.adj' G.symm

I'm not discounting the possibility that there might be a way to define graph constructions in a general way, though.

[Kyle Miller]

Regarding Sort-valued graphs -- there's this relationship between E -> sym2 V multigraphs and V -> V -> Sort* (plus involutions) multigraphs, and I was hoping we could find a way to unify them in some way. One thing I don't like about the latter is it doesn't give a good type for the incidence_set. What I'm looking into is whether a graph typeclass might specify how this type is meant to work for a given concrete graph type.

Or, in other words, somehow finding a design where graphs represented either way could be considered to be multigraphs as far as the general library is concerned.

[Kyle Miller]

Also, regarding what you mention about mixins not going through all the families of graphs you've outlined, I didn't mean to claim that the ones I've written handle everything yet. They only handle basic properties of directed/undirected graphs that might be reflexive/irreflexive at the moment. Things like edge labels/weights and vertex labels/weights would need more typeclasses.

[Kyle Miller]

Yaël Dillies said:

One takeaway is that edge weight is very different to weight between two vertices, and should be treated as such.

Could you elaborate a bit on this observation? Is it that α → α → option W is not enough for edge weights?

[Kyle Miller]

Also, I'm wondering how you imagine hypergraphs fit in with the rest of the graph types -- they've always seemed like they're their own thing to me, other than that every simple graph may be regarded as being a hypergraph, too. (Not saying they shouldn't be addressed; I just want to understand what hypergraphs can do for graphs and vice versa.)

[Yaël Dillies]

Kyle Miller said:

Depending on which data exists and which properties hold, can we let those objects use some shared definitions? Can we support having forgetful morphisms from a graph type that that is more constrained to a less-constrained type? Can we support having additional data that isn't under the purview of the graph theory library itself?

One solution is having two parts: (1) typeclasses for properties and (2) concrete implementations. What I think is the ideal is giving users the freedom to take any structure they might have defined and then implement instances to make it appropriately graphy. Ideally one would only need to then define things that are truly specific to the particular application.

I'm sorry but you're just explaining my refactor back to me :grinning:

[Yaël Dillies]

This is the hierarchy I've been thinking about, where each arrow is a forgetful functor:
Graph hierarchy V1
It's a bit outdated compared to #11000. I got rid of fun_fun_like, which means the squiggly arrows are not evil anymore (as expected, they commute with all other arrows, but they can change the type of the fun_fun_like instance, which is a problem for Lean's TC inference as it will only every synthesize one of the two possibilities). And a few more types joined the dance. But the gist is there.

[Yaël Dillies]

Kyle Miller said:

Yaël Dillies said:

One takeaway is that edge weight is very different to weight between two vertices, and should be treated as such.

Could you elaborate a bit on this observation? Is it that α → α → option W is not enough for edge weights?

Just so that we're clear, I'm differentiating:

• Adjacency weight: α → α → option W
• Edge weight: sym2 α → option W
• Hom weight: Π a b : α, (a ⟶ b) → W
• Hom edge weight: edge [[(a, b)]] → W

So what I'm saying is that hom weight and adjacency weight are too different to be unified. You can turn on into the other, but there's no practical way for one to directly generalize the other.

[Yaël Dillies]

Kyle Miller said:

Also, I'm wondering how you imagine hypergraphs fit in with the rest of the graph types -- they've always seemed like they're their own thing to me, other than that every simple graph may be regarded as being a hypergraph, too. (Not saying they shouldn't be addressed; I just want to understand what hypergraphs can do for graphs and vice versa.)

I gave up on trying to fit them in my hierarchy, until I actually thought it wasn't too hard to just fit them in. The problem is less technical than semantic. Should we turn hypergraphs into simple graphs (which is what #11000 currently does), or simple graphs into hypergraphs? And if so, how? I can think of several ways to do that in either direction and all of them have their merits.
So I think I'm going to exclude hypergraphs from the hierarchy not because it can't handle them, but because we haven't decided what it should mean.

[Yaël Dillies]

Kyle Miller said:

Regarding Sort-valued graphs -- there's this relationship between E -> sym2 V multigraphs and V -> V -> Sort* (plus involutions) multigraphs, and I was hoping we could find a way to unify them in some way. One thing I don't like about the latter is it doesn't give a good type for the incidence_set.

I currently much prefer the V -> V -> Sort* multigraphs because they fit in the hierarchy much better. You can just drop properties of the map and get quiver, or strenghten it to get simple_multigraph (or simple_quiver). Also, do you consider set (Π a b, a ⟶[G] b)` a bad type?

[Arthur Paulino]

I've thought about the graph API refactor a few times and now that Yael mentioned it I wanted to ask: have you guys gone any further in this introspection?
At the moment, the only solid ground I've found is that we're going to lose dot notation

[Vincent Beffara]

Could you point me to it? I'm late in the game and need to catch up :-)

[Arthur Paulino]

Kyle gave it a go here: #10963
And Yael did it here: #11000
Then they started discussing the consequences of such choices above

[Vincent Beffara]

Sorry for asking what should be obvious to me - what do you mean by losing the dot notation?

[Arthur Paulino]

It means that, given two adjacent vertices v and w in a graph G, we would no longer be able to say G.adj v w

[Vincent Beffara]

So we would have to say adj G v w instead? As a beginner this feels like an obstacle maybe. Unless there is a better way using a convenient notation...

[Arthur Paulino]

Exactly, you can see it in many places of Kyle's PR. He did exactly that

[Vincent Beffara]

Since a graph "is just an adj relation", is there a way to have a coercion from a graph on V to V -> V -> Prop and say G v w? Or is that a more terrible idea than I imagine?

[Vincent Beffara]

(Or just adj v w and let typeclass magic occur?)

[Arthur Paulino]

Vincent Beffara said:

(Or just adj v w and let typeclass magic occur?)

I particularly like this idea, if it's possible. But let's hear it from the experts (Kyle, Yael and Bhavik)

[Yaël Dillies]

I originally wanted that, but it doesn't quite work for a tricky reason. Multigraphs are just decorated functions V -> V -> Sort*, so you want them to be coerced to V -> V -> Sort*. But multigraphs are also just graphs with more edges, so you want a coercion (or an instance with the refactor) to graphs. But then when G is a multigraph, G a b can either mean the type of edges between a and b or the derived adjacency relation.

[Yaël Dillies]

That on its own wouldn't be such a problem because Lean can infer the type from context, but it turns out that the typeclass way to do this (Anne's docs#fun_like) involves forgetting some parameter of the instance, and this parameter is precisely the Prop/Sort* distinction. That means Lean can't use context to infer the correct instance to use and will always synthesize the same (although I don't know which!)

[Yaël Dillies]

Here's an oldish version of the hierarchy I want: https://leanprover.zulipchat.com/user_uploads/3121/0aLDRUql5XHnaPCPphk-YNS6/21c84d5a-050a-48b6-8027-01c0724b2a35.jpg

[Yaël Dillies]

Each arrow is a forgetful functor, and they all commute, EXCEPT that when you go through a squiggly line the type might have changed (given the type, the values commute, but there might be two types).

[Yaël Dillies]

In that regard, having dedicated functions adj and homs (that is, cutting the top of the above hierarchy) seems like the easiest solution.

[Kyle Miller]

@Yaël Dillies I just want to make sure you know what I meant by "competition" earlier, since I've realized this can be easily misunderstood: I wanted us to do some thesis-antithesis-synthesis sort of thing. There are a number of design goals that are hard to keep all in mind, if we're each even aware of all of them, and having competing designs (the thesis and antithesis) we can explore better. Then, we need to synthesize, which I've been planning on looking into, but things have come up the last couple weeks... I'm very glad you took up the challenge and put together what you think the graph theory library should look like, which is invaluable.

[Kyle Miller]

As part of synthesis, something I've been working on in the background is a lean PR to be able to preserve dot notation using a fairly simple system. The idea, roughly, that we can give structures an attribute that's a list of namespaces to search when doing extended dot notation. This gives us an object-oriented-like interface (but with static method resolution), that I think will make working with more general graph classes more pleasant.

All I need to do is make it pretty print, and also test it more to make sure it actually meets our needs.

[Kyle Miller]

Dot notation, while I think it's important, isn't the only design consideration here.

I want to be sure that we're not taking any compromises when it comes to how different graph objects get to define themselves, for defeq reasons. There are probably at least ten ways to define a multigraph, and I want us to be able to use any one of those definitions and get standard lemmas about them. For example, a directed multigraph is either a pair of maps (s t : E -> V) or a single map (edges : V -> V -> Sort*). You can go through a generic transformation to go between these representations, but I'd rather that we have the freedom to choose on a case-by-case basis. It's doable, too.