Zulip Chat Archive

Stream: graph theory

Topic: Refactor and quivers?


Rémi Bottinelli (Oct 14 2022 at 08:55):

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 (Oct 14 2022 at 14:03):

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 (Oct 14 2022 at 14:12):

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

Kyle Miller (Oct 14 2022 at 14:15):

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 (Oct 14 2022 at 14:15):

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 (Oct 14 2022 at 14:16):

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

Yaël Dillies (Oct 14 2022 at 14:17):

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

Kyle Miller (Oct 14 2022 at 14:18):

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 (Oct 14 2022 at 14:20):

@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 (Oct 14 2022 at 14:35):

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 (Oct 14 2022 at 14:37):

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

Kyle Miller (Oct 14 2022 at 14:39):

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 (Oct 14 2022 at 14:40):

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 (Oct 14 2022 at 14:50):

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 (Oct 14 2022 at 14:52):

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 (Oct 14 2022 at 14:52):

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

Kyle Miller (Oct 14 2022 at 14:53):

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

Yaël Dillies (Oct 14 2022 at 14:54):

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

Rémi Bottinelli (Oct 14 2022 at 14:54):

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 (Oct 14 2022 at 14:55):

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 (Oct 14 2022 at 14:56):

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

Rémi Bottinelli (Oct 14 2022 at 14:57):

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

Rémi Bottinelli (Oct 14 2022 at 14:58):

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

Yaël Dillies (Oct 14 2022 at 14:58):

What do you mean?

Yaël Dillies (Oct 14 2022 at 14:59):

docs#psum is already in core Lean

Rémi Bottinelli (Oct 14 2022 at 14:59):

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

Rémi Bottinelli (Oct 14 2022 at 15:02):

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

Kyle Miller (Oct 14 2022 at 15:03):

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 (Oct 14 2022 at 15:11):

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 (Oct 14 2022 at 15:15):

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 (Oct 14 2022 at 15:25):

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.


Last updated: Dec 20 2023 at 11:08 UTC