## Stream: graph theory

### Topic: multigraph definition

#### Kyle Miller (Aug 18 2020 at 02:34):

Something that seems like a good definition for multigraphs is

[Chou94] Chou, Ching-Tsun. "A formal theory of undirected graphs in Higher-Order Logic." (1994) https://doi.org/10.1007/3-540-58450-1_40

I remember there also being some things in

Doczkal, Christian and Pous, Damien. (2019). Graph Theory in Coq: Minors, Treewidth, and Isomorphisms

The Chou approach is to have a vertex type V and an edge type E, then take a set of links on V × E × V such that the projection onto E is surjective, such that the set of links is closed under swapping the two vertices, and such that if two links project to the same edge then they are the same up to swapping.

Conceptually, a link is an edge orientation (for non-loop edges -- loop edges only have a single associated link).

There's an implementation of it at https://github.com/leanprover-community/mathlib/tree/graphs/src/combinatorics/graphs but I don't remember exactly what state the branch is in...

#### Kyle Miller (Jan 07 2021 at 23:09):

There are many ways to define unoriented multigraphs, and one of the sticking points to using Chou's definition is that the definition of degree isn't very nice. My educated opinion for the design: a single-vertex graph with a single loop edge should have degree 2, since there are two incident half edges ("darts"). Chou's definition has a single link per loop edge but two links per non-loop edge, so you can't just count incident links to get the degree.

Here are five different definitions of multigraphs: https://gist.github.com/kmill/16257d58a662e570d4762723e762c7a8

I'm thinking something like multigraph₄ is the best, though its disadvantage is that you don't have an edge set per se, but at least in my applications "labeled edge" tends to actually mean "labeled dart." If you need labeled edges.

#### Kyle Miller (Jan 07 2021 at 23:10):

Anyway, if you have any other ideas for the definition of a multigraph (along with test implementations for some basic accessor functions, especially the degree interface), please post them!

It'd be good to also think about how sub-objects would work for each design.

#### Kyle Miller (Jan 08 2021 at 00:01):

A commutative diagram for the structure of an unoriented multigraph along what the maps are supposed to mean:
image.png

#### Peter Nelson (Jan 08 2021 at 14:43):

I've been thinking a little about multigraphs, since they are the right setting for graphic matroids. I think a quite important test is whether it is easy to contract a set of edges. If contraction isn't easy, you're closing off some of the deepest work in graph theory.

I am in favour of a definition that eliminates the need for darts. Here is one in terms of a nat-valued 'incidence function', with math rather than code. A multigraph is a triple (V,E,inc), where V and E are sets, and inc is a function from V x E to nat, that sums to exactly 2 over each edge. If e has ends v1 and v2, then inc(v,e1) = inc(v,e2) = 1, and if e is a loop at v, then inc(v,e) = 2. Hence, the degree of v is just sum (inc( v, . )). This correctly allows loops to contribute degree 2, and proves the handshake theorem by formally reversing the order of summation.

Further, one can contract edges easily; to contract a set X of edges, you quotient V by the equivalence relation whose classes are the components of the subgraph G[X]; then the contraction G/X has this quotient as a vertex set, and its incidences come from summing inc over equivalence classes. This correctly turns nonloop edges into loops where appropriate, contracts non-parallel edges into parallel, etc etc.

#### Kyle Miller (Jan 10 2021 at 18:12):

Thanks @Peter Nelson, that's a clever encoding, and it's worth trying it out. I added my attempt at a formalization of that as multigraph₆ in the gist. One complexity is that the sum is over an infinite set, so I added in a finset support for the summation (I think it's important to be able to handle infinite multigraphs). Another change I made was to have a special inc_type enumeration rather than a nat so that doing things by cases is easier.

That's a good point about needing to support contractions (or, better, minors). I figured being able to define degree shows a basic amount of viability for a multigraph definition, and a definite next step would be to try to implement contraction/minors.

#### Kyle Miller (Jan 10 2021 at 18:15):

(I'll try to get around to make a proper mathlib branch with the definitions under consideration, with one file per multigraph definition. Doing a gist for now was just easier to try to get the conversation going.)

Last updated: May 08 2021 at 23:10 UTC