Zulip Chat Archive

Stream: graph theory

Topic: walks


view this post on Zulip 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

view this post on Zulip Alena Gusakov (Feb 22 2021 at 23:47):

@Yakov Pechersky what do you mean by this exactly?

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Feb 22 2021 at 23:51):

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

view this post on Zulip Yakov Pechersky (Feb 22 2021 at 23:51):

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

view this post on Zulip 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

view this post on Zulip Alena Gusakov (Feb 23 2021 at 00:02):

Didn't know it existed tbh

view this post on Zulip Yakov Pechersky (Feb 23 2021 at 00:12):

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

view this post on Zulip Yakov Pechersky (Feb 23 2021 at 00:13):

That would be is_cycle

view this post on Zulip Alena Gusakov (Feb 23 2021 at 00:14):

Could also take advantage of list defs too, like count

view this post on Zulip Alena Gusakov (Feb 23 2021 at 00:15):

Which is super convenient

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Feb 23 2021 at 00:18):

Probably @Kyle Miller can be more helpful

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Feb 23 2021 at 00:48):

Can't labeled graphs be done with sigma types?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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*)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

Last updated: May 08 2021 at 22:13 UTC