## Stream: graph theory

### Topic: walks

#### Alena Gusakov (Feb 22 2021 at 23:46):

Why not define walks as lists with a chain constraint? Then you get lots of defns and lemmas for free

#### Alena Gusakov (Feb 22 2021 at 23:47):

@Yakov Pechersky what do you mean by this exactly?

#### Yakov Pechersky (Feb 22 2021 at 23:50):

Something like a structure that takes a g : graph V, start : V, seq : list V, with the constraint that seq.chain start g.adj

#### Yakov Pechersky (Feb 22 2021 at 23:51):

Then for a path, you say nodup (start :: seq) or something like that

#### Yakov Pechersky (Feb 22 2021 at 23:51):

I just started reading Bollobas (Bhavik suggested it), so these could be very naive questions

#### Alena Gusakov (Feb 23 2021 at 00:01):

I haven't tried using the chain API so I'm not really sure! I'll have to try it at some point

#### Alena Gusakov (Feb 23 2021 at 00:02):

Didn't know it existed tbh

#### Yakov Pechersky (Feb 23 2021 at 00:12):

Then cycles are a constraint that is like (∀ h : seq ≠ []), seq.last h ≠ start

#### Yakov Pechersky (Feb 23 2021 at 00:13):

That would be is_cycle

#### Alena Gusakov (Feb 23 2021 at 00:14):

Could also take advantage of list defs too, like count

#### Alena Gusakov (Feb 23 2021 at 00:15):

Which is super convenient

#### Bhavik Mehta (Feb 23 2021 at 00:17):

Ah I mentioned this a while ago - iirc the problem with that is that it doesn't generalise nicely to labelled graphs

#### Bhavik Mehta (Feb 23 2021 at 00:18):

Probably @Kyle Miller can be more helpful

#### Alena Gusakov (Feb 23 2021 at 00:20):

Wacky idea but what if we also used chains to describe walks in labelled graphs where incidence between edges is the relation instead of adjacency

#### Alena Gusakov (Feb 23 2021 at 00:21):

That would fit into the design choice of treating edges as their own objects (useful for matroids)

#### Alena Gusakov (Feb 23 2021 at 00:31):

Suppose edges are defined as sets of vertices, that would allow for things like hypergraphs eventually too

#### Yakov Pechersky (Feb 23 2021 at 00:48):

Can't labeled graphs be done with sigma types?

#### Bhavik Mehta (Feb 23 2021 at 00:55):

But for labelled multigraphs, you'll end up with some heterogeneous list type, at which point you might as well use the inductive type Kyle suggested in the first place

#### Kyle Miller (Feb 23 2021 at 01:20):

@Yakov Pechersky If you think that structure would be better, I'd suggest trying to prove that if two vertices are connected by a walk, then they are also connected by a path. That module I wrote was primarily to work out how to do that in as clean a way as I knew how.

There are a couple nice properties about that definition. The first is that it gives a category of walks on the graph. The second is that the definition of a path involves defining the support, which seems like it would be a useful finset to have around anyway.

#### Kyle Miller (Feb 23 2021 at 01:23):

It seems like it could be useful taking the inductive type I wrote and generalize it to arbitrary relations, then specialize it for simple graphs. I think there's still a walk->path result in the general case.

#### Kyle Miller (Feb 23 2021 at 01:30):

Actually, rather than generalizing it to relations, it might be nice to generalize it to directed multigraphs (i.e., "relations" of type a -> a -> Sort*)

#### Alena Gusakov (Feb 23 2021 at 02:02):

I haven't tried using the chain API so I'm not really sure! I'll have to try it at some point

#### Kyle Miller (Feb 24 2021 at 19:13):

I forgot to mention that my code for walks was mostly based on https://github.com/leanprover-community/mathlib/blob/hedetniemi/src/graph_theory/paths.lean

#### Yakov Pechersky (Feb 24 2021 at 19:14):

I'm testing it out right now, adding a lot of walk API that probably isn't really needed. There's missing list.chain API to do so that would be nice to have anyway. Thanks for the pointer.

#### Yakov Pechersky (Feb 24 2021 at 19:15):

An example of what I have right now:

@[simp] lemma last_coe (G : simple_graph V) (v : V) :
(v : G.walk).last = v := rfl


#### Yaël Dillies (Jun 21 2021 at 16:15):

@Kyle Miller I saw you had some good stuff in simple_graph_walks2. Are you okay with me PRing it soon-ish?

#### Kyle Miller (Jun 21 2021 at 16:20):

I've forgotten the exact state of the branch, but here's my last message about it: https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/Construct.20path.20from.20walk.3F/near/219804780

I think @Alena Gusakov might have made use of some of it in another branch -- pinging her in case.

Anyway, it would be great if you PR'd it!

#### Yaël Dillies (Jun 21 2021 at 16:21):

Me offering that was actually from talking to her :grinning:

#### Yaël Dillies (Jun 21 2021 at 16:22):

I'm actually interested in multigraphs, so I will try to generalise your file.

#### Eric Rodriguez (Jun 21 2021 at 16:23):

simple-graph doesn't seem like a great fit for multigraphs honestly

#### Eric Rodriguez (Jun 21 2021 at 16:23):

You may be better off looking at quivers although you may have some struggles

Yeah of course

#### Eric Rodriguez (Jun 21 2021 at 16:23):

I was trying to prove Koningsberg using them and ran into so many issues, but I did actually manage to get some small amounts of code for paths there that typechecked

#### Kyle Miller (Jun 21 2021 at 16:24):

How are you formalizing multigraphs? There are some discussions in this stream about the many ways that are possible.

#### Yaël Dillies (Jun 21 2021 at 16:24):

But I think one can abstract away even from multigraphs, and instead defining walks and paths on an arbitrary relation.

#### Yaël Dillies (Jun 21 2021 at 16:25):

For defining multigraph, I was thinking about a N-weighing of the complete graph. But Alena tells me this might not fit her matroid edges labelling needs.

#### Kyle Miller (Jun 21 2021 at 16:25):

I think there's discussion about that, too -- it would be nice having the category generated by a relation if it doesn't already exist

What's that?

#### Eric Rodriguez (Jun 21 2021 at 16:27):

@Yaël Dillies https://gist.github.com/ericrbg/c2025ecbd87e161f1d4eba4604178336 is what I've got so far with quivesr

#### Yaël Dillies (Jun 21 2021 at 16:29):

Oh so quiver is actually already a generalisation of multigraph.

#### Eric Rodriguez (Jun 21 2021 at 16:29):

Yeah, this is what I was trying to say

#### Eric Rodriguez (Jun 21 2021 at 16:29):

undirected things are quite annoying in it though

#### Eric Rodriguez (Jun 21 2021 at 16:30):

and it's almost too-strongly type theoretic so it can be very frustrating working with it sometimes

Oh

#### Yaël Dillies (Jun 21 2021 at 16:30):

So is there any advantage in having multigraph?

#### Eric Rodriguez (Jun 21 2021 at 16:31):

I'd probably think so? But I think we should take some more care with the API

#### Kyle Miller (Jun 21 2021 at 16:32):

The "path category" (not sure if this is the canonical name) would be a category on a type α with a distinguished relation, where the morphism sets are

inductive path {α : Type u} (r : α → α → Prop) : α → α → Type u
| refl {x : α} : path x x
| cons {x y z : α} (h : r x y) (p : path y z) : path x z


The "walk category" of a simple graph would come from this.

#### Yaël Dillies (Jun 21 2021 at 16:33):

Here I think we can generalise r to Sort u. In my mind this would allow paths on multigraphs.

#### Kyle Miller (Jun 21 2021 at 16:34):

Yeah, I was about to mention that. Then you could also apply it to quivers.

#### Eric Rodriguez (Jun 21 2021 at 16:34):

graph things on Sort are very nice too, because Prop-valued multigraphs ↔ graphs

#### Yaël Dillies (Jun 21 2021 at 16:34):

Oh yeah, that's great!

#### Yaël Dillies (Jun 21 2021 at 16:35):

Although shall we allow loops in multigraphs? Alena says so?

#### Kyle Miller (Jun 21 2021 at 16:35):

The reason simple graphs are special is that they are "simplicial": each edge is identified by its endpoints

#### Kyle Miller (Jun 21 2021 at 16:35):

Multigraphs should allow loops.

#### Yaël Dillies (Jun 21 2021 at 16:37):

So we would have

• simple_graph: loopless, undirected, simple
• multigraph: undirected
• quiver: directed
as a nice hierarchy and, standing out,

• hypergraph: loopless, undirected, but hyperedges

#### Eric Rodriguez (Jun 21 2021 at 16:37):

Kyle Miller said:

The "path category" (not sure if this is the canonical name) would be a category on a type α with a distinguished relation, where the morphism sets are

inductive path {α : Type u} (r : α → α → Prop) : α → α → Type u
| refl {x : α} : path x x
| cons {x y z : α} (h : r x y) (p : path y z) : path x z


The "walk category" of a simple graph would come from this.

what's the difference between this and a poset category?

#### Kyle Miller (Jun 21 2021 at 16:38):

Key constructions multigraphs should support is (1) a type of subgraphs and (2) a type of minors (or at least being able to contract and delete subsets of edges, and have the right algebraic relations on these constructions)

#### Yaël Dillies (Jun 21 2021 at 16:39):

And when we contract an edge, we don't want the other same-end edges to disappear, right?

#### Kyle Miller (Jun 21 2021 at 16:40):

Indeed (they become loop edges)

#### Yaël Dillies (Jun 21 2021 at 16:44):

It seems that us graph-theorists here spend most of our time discussing and writing code, but are always unsure about it so nothing ever gets PRed :stuck_out_tongue:

#### Eric Rodriguez (Jun 21 2021 at 16:46):

There's a couple in the queue! Alena has one which I reviewed ages ago, and @Gabriel Moise (who just finished exams :party_ball:) was doing once on incidence matrices

#### Kyle Miller (Jun 21 2021 at 17:12):

(I've been busy with the whole finishing my degree thing, and unfortunately it has nothing to do with Lean.)

With graphs I've felt there were some unsolved issues that, while I could PR the multigraph code I've written (I'm not sure where the branch is though...), it would be good to do some more research to nail down what would work well in the long term. This is less true now than when he said it, but de Bruijn observed that the more abstract a piece of mathematics, the smaller the gaps, but "less abstract fields, like combinatorics, can be hard since they may contain simple intuitive ideas for which there is no tradition of formalization." (from "Checking mathematics with computer assistance" in Notices of the AMS, Jan 1991)

One issue is ergonomics. I spent a while trying to get subgraphs to "be" graphs, like how subgroups "are" groups, but the tricks used there don't apply, and the tricks I came up with don't seem to be worth the hassle. There are

In addition to the key constructions, another issue is making sure multigraphs will play well with a corresponding directed graph type. You'd want to be able to forget orientations of edges, but also be able to prove things about multigraphs given an arbitrary directed graph representative. There's also the conversion from a multigraph to a simple graph, and you want to relate their connected components somehow.

Testing out implementations for the different possible definitions should show a good way forward.

#### Yaël Dillies (Jun 22 2021 at 18:46):

I don't have answers to those design questions, but I think we can adopt a more PR-friendly approach. Look out for the multigraph PR :wink:

#### Yaël Dillies (Jun 25 2021 at 02:26):

Just thought about something. If we later want to talk about random walks, we should allow infinite walks.

#### Kyle Miller (Jun 25 2021 at 02:54):

Infinite walks might be a different kind of object, and the type of all finite walks is useful in itself (for example, to define connected components). There are a couple ways you might formalize an infinite walk. One is as a function f : nat -> V such that G.adj (f n) (f (n + 1)) for all n. The other is as a kind of limit of finite walks, maybe formalized as a dependent pair w : nat -> V and f : (n : nat) -> G.walk v (w n) such that f n is the restriction of f (n + 1) for each n.

Alena and I had tried formalizing walks as graph homomorphisms from path graphs, but it was very painful defining all the operations you'd want to do with walks. Though, this is another way you could define an infinite walk, as a graph homomorphism from the infinite ray graph.

#### Yaël Dillies (Jun 25 2021 at 02:56):

Should we then have something like walk and finwalk?

Last updated: Dec 20 2023 at 11:08 UTC