Refactor and quivers?

Stream: graph theory

[Rémi Bottinelli]

Hey, iirc, I was told at some point about some big refactor of the simple_graph API potentially based on quivers. Since I'm now somewhat working with quivers as directed graphs and using has_involutive_inverse to talk about those as kinds of undirected graphs, I was wondering about the status of it all. @Yaël Dillies refered me to a pull request for undirected multigraphs as tuples Vertices,Edges,Start,End,Reversal. How does it all fit together?

[Kyle Miller]

Sorry, I've not really been following Lean recently. What is the idea to make the simple_graph API be based on quivers? Quivers are for a type of vertices with an attached set of arrows. How would you get any sort of lattice structure on the type of simple graphs with a given vertex type?

[Rémi Bottinelli]

Oh, I must be misremembering the quiver part then? But what about the refactor? Am I misremembering that part too?

[Kyle Miller]

Looking through some mentions, I see your thread where Yaël says multigraphs shouldn't be based on quivers: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Geometric.20group.20theory/near/303100448

[Kyle Miller]

My feeling is that we're going to have parallel theories, the quiver-based graph theory, and something more like a "bundled" graph theory where the edge structure is part of the type.

[Kyle Miller]

And then we should have more API to carry results from one side to another.

[Yaël Dillies]

This to me sounds like a reasonable solution, except for the obvious code duplication it entails.

[Kyle Miller]

Incidentally, one API inconsistency is quiver paths vs graph walks -- quivers build their paths from the end, but graphs build their walks from the front. One reason graphs do it this way is that it coincides with the list API, which is nice. I haven't had a chance to dig into why quivers work the way they do -- I suspect it has something to do with the fact that in category theory morphism composition is opposite the usual function composition.

[Kyle Miller]

@Yaël Dillies Yeah I agree, but putting my software architect hat on, when developing software it tends to be better to allow duplication in the short term, since you often don't know ahead of time what abstraction you should use to unify everything. Once things get too abstract, it can get arbitrarily difficult to unwind.

[Rémi Bottinelli]

My feeling is that we're going to have parallel theories, the quiver-based graph theory, and something more like a "bundled" graph theory where the edge structure is part of the type.

So, it would be reasonable to continue with has_involutive_reverse and develop a quiver-based graph theory starting with quivers parallelly to what is currently there?

[Rémi Bottinelli]

That's something I wouldn't have expected to be accepted in mathlib? What would the rationale for that be?

[Kyle Miller]

For a long time, mathlib had completely parallel additive and multiplicative monoid libraries until someone figured out how to write metaprogramming to unify them, just to give an example precedent.

[Kyle Miller]

It's not clear to me yet that there's a good way to unify quivers and simple graphs -- they have fairly different languages (i.e., the sorts of terms you write about them) and interfaces.

[Rémi Bottinelli]

I was naïvely going to ask why not simply base simple_graph on Prop-valued quivers with reverses but then it seems there is some troubles with those (Prop-valued quivers) making reverseal complicated. Is that the sole reason (notwithstanding the practical issue that it would be a lot of work for little clear gains) ?

[Kyle Miller]

It's because simple_graph V is the type of all simple graphs that have the given vertex type. When you're working with quivers, you have only a single graph structure on the given type V because it's a typeclass.

[Rémi Bottinelli]

By the way, I'm not sure I get the problem with Prop-valued quivers.

[Kyle Miller]

Is there a problem with Prop-valued quivers? The definition of docs#quiver allows them

[Yaël Dillies]

There's no problem with them. They are just not "simple graphs".

[Rémi Bottinelli]

Mmh, but then, is it "sensible" to fix a vertex set and look at all simple_graphs on it, rather than have simply simple_graphs and morphisms and a way to describe having the same vertex set?

[Rémi Bottinelli]

Kyle Miller said:

Is there a problem with Prop-valued quivers? The definition of docs#quiver allows them

I'm refering to this comment which I don't really know how to interpret

[Yaël Dillies]

Oh that must be because of the ⊕ that appears just below. You could replace that with psum.

[Rémi Bottinelli]

Oh, alright, then I see no problem with basing everything off quivers :)

[Rémi Bottinelli]

More seriously, that means s/psum/sum/ would be PRable?

[Yaël Dillies]

What do you mean?

[Yaël Dillies]

docs#psum is already in core Lean

[Rémi Bottinelli]

right, just making it so that the restriction on level is dropped in the file I linked to

[Rémi Bottinelli]

Alright, that's on my todo list then: it probably also entails adding psum.swap and related.

[Kyle Miller]

Rémi Bottinelli said:

Mmh, but then, is it "sensible" to fix a vertex set and look at all simple_graphs on it, rather than have simply simple_graphs and morphisms and a way to describe having the same vertex set?

This is one of those long-standing design tensions -- do we work with an "actual" lattice or do we work with morphisms modulo isomorphism?

In my experience, it is less of a hassle formalizing things when you can find a single type that everything is a term of -- this tends to lead to fewer dependent type issues. When you are working with simple_graph and simple_graph.subgraph, it can be possible to work with just a single vertex type.

For example, this way it's not so hard to formulate that every simple_graph is the sup of all the one-edge graphs le to it.

[Rémi Bottinelli]

Oh, yeah, I was meaning to say, an ugly hack for this is to have not a single vertex type, àla quivers, but then if you want to talk about the lattice, you just play with subgraphs.

[Rémi Bottinelli]

And _in some sense_, it's cleaner.But if doing the quiver version in parallel is OK, I guess it solves this question.

[Antoine Labelle]

I also think that the quiver version could be pertinent. It would probably be fairly similar to the proposition in the PR you mention in your first message, but with the advantage that we could use the already existing quiver API.