Zulip Chat Archive

Stream: graph theory

Topic: paths


view this post on Zulip Jalex Stark (Aug 12 2020 at 03:44):

Michael Hahn took a stab at defining eulerian circuits, with the intent to cross the konigsberg bridges problem off of freek's 100 theorem list

view this post on Zulip Jalex Stark (Aug 12 2020 at 03:45):

the code is in this repo
https://github.com/apurvnakade/mc2020-projects

view this post on Zulip Jalex Stark (Aug 12 2020 at 03:47):

we tried for a bit using the inductive type of paths defined in the hedetniemi branch, but we felt like we were reimplementing basic list API

view this post on Zulip Jalex Stark (Aug 12 2020 at 03:53):

so then we made an implementation with lists at the core

view this post on Zulip Jalex Stark (Aug 12 2020 at 03:54):

the compatibility condition called p.adj is not quite right, maybe it's enough to separate it into three structure fields

view this post on Zulip Jalex Stark (Aug 12 2020 at 04:00):

Alena then started to use the same definition of path, with the goal of characterizing trees as graphs in which any pair of points has a unique path between them

view this post on Zulip Jalex Stark (Aug 12 2020 at 04:01):

her code is in yet another repo
https://github.com/agusakov/graph_theory_2020

view this post on Zulip Jalex Stark (Aug 12 2020 at 04:04):

I think michael proves that a vertex is incident to an odd number of edges in a path if and only if the path is not a cycle and the vertex is the head or tail,
up to several sorries which are somewhere between basic API and basic theorems

view this post on Zulip Jalex Stark (Aug 12 2020 at 04:05):

I guess both of these authors have reasons for writing in their own repo, but hopefully after the process of their first PRs, they'll see the light and want to work in branches on the mathlib repo

view this post on Zulip Aaron Anderson (Aug 12 2020 at 04:07):

A good test of a path definition for simple graphs would be proving that powers of adjacency matrices count paths (https://github.com/leanprover-community/mathlib/pull/3672)

view this post on Zulip Aaron Anderson (Aug 12 2020 at 04:10):

Jalex Stark said:

Alena then started to use the same definition of path, with the goal of characterizing trees as graphs in which any pair of points has a unique path between them

I'd be interested to see how easy it is to translate between the path-connected definition of connected that Alena is using and an inductive definition of connected

view this post on Zulip Aaron Anderson (Aug 12 2020 at 04:11):

where by inductive definition I guess I mean the transitive closure of adjacency

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:35):

This is the totally-not-battle-tested definition of a path I'm pulling out of thin air:

structure path (n : ) :=
(vertex_map : fin (n + 1)  V)
(edge_map : fin n  E)
(reasonable_definition : the edges connect the right vertices)

view this post on Zulip Alena Gusakov (Aug 12 2020 at 21:36):

Ohhh okay gotcha

view this post on Zulip Alena Gusakov (Aug 12 2020 at 21:36):

Interesting

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:37):

It's less good for defining connectedness, but it'd nice to just say that the vertex map or the edge map is injective

view this post on Zulip Alena Gusakov (Aug 12 2020 at 21:37):

Makes sense

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:37):

and there are some ok lemmas for functions from fin

view this post on Zulip Alena Gusakov (Aug 12 2020 at 21:38):

It might also make induction easier I think? In like, really specific cases lol

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:39):

I think it'd make induction marginally harder, because lists are literally an inductive type, but fin has some definitions like fin.tail and fin.init to work around that

view this post on Zulip Alena Gusakov (Aug 12 2020 at 21:40):

*make induction easier for me to follow lol

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:40):

One place I think it would be better is proving the adjacency matrix formula for counting paths

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:42):

@Jalex Stark, just want to invite your critique on this alternate definition of a path

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:43):

or maybe, I'll move to the paths stream...

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:44):

(deleted)

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:44):

Aaron Anderson said:

This is the totally-not-battle-tested definition of a path I'm pulling out of thin air:

structure path (n : ) :=
(vertex_map : fin (n + 1)  V)
(edge_map : fin n  E)
(reasonable_definition : the edges connect the right vertices)

I think the right test is to reimplement the API we already have

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:44):

starting with induction_on

view this post on Zulip Alena Gusakov (Aug 12 2020 at 21:45):

please make it be (vertex_map : fin n → V) and (edge_map : fin (n - 1) → E)

view this post on Zulip Alena Gusakov (Aug 12 2020 at 21:46):

though I guess that would be bad for cases where you don't have vertices

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:47):

Unfortunately, I think you really can't do that... maybe you'd have to make it `path (n + 1) :='...

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:47):

Also, it really is pretty standard in the literature to have the length of a path be the number of edges

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:48):

See for instance the adjacency matrix formula. The entries of AnA ^ n count paths with nn edges

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:48):

and if you concatenate two paths, you add the number of edges, but not vertices

view this post on Zulip Alena Gusakov (Aug 12 2020 at 21:48):

Yeah that makes sense

view this post on Zulip Alena Gusakov (Aug 12 2020 at 21:49):

For some reason I feel like the way I learned about path lengths is counting the number of vertices but maybe it's such a small detail that I didn't pay attention and have just misremembered it

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:49):

i mean, regardless of whether you remember correctly what your prof said, we should use the definition that's most convenient

view this post on Zulip Alena Gusakov (Aug 12 2020 at 21:50):

Yeah true

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:50):

from my point of view, nat subtraction is never convenient

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:50):

Actually, concatenation would be even easier if you make the path definition even more dependent...

structure path_from (a b : V) (n : ) :=
(vertex_map : fin (n + 1)  V)
(edge_map : fin n  E)
(reasonable_definition : the edges connect the right vertices)
(starts_at : vertex_map 0 = a)
(ends_at : vertex_map n = b)

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:50):

this is the road to dependent type hell

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:50):

That'd be the definition I'd recommend if we were, say, just trying to define the fundamental group...

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:51):

michael and I start with the G.path a b type and then I rewrote everything so that the source and sink were properties instead of part of the type

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:51):

because i just didn't know how to prove some of the bits of the API

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:52):

I think patrick massot and co. have put a definition of path connected topological spaces into mathlib recently, and they were trying to optimize for making it natural to define the fundamental groupoid form there

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:52):

If it really is infeasible that way, then my definition's just a subtype, which is not bad at all

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:53):

but I would recommend following whatever convention team path connected are doing

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:54):

yes, I don't remember but maybe i can quickly find the code

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:54):

It looks like they do define a path as dependent on endpoints (obviously not length)

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:57):

I agree that defining a path in terms of source and target sounds like a pain if you're working with lists, but I think it might be nicer if you're working with fin-tuples

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:59):

i'll think more carefully about any definition you propose after you prove path.cons and path.induction_on with it

view this post on Zulip Aaron Anderson (Aug 12 2020 at 21:59):

Jalex Stark said:

starting with induction_on

Did y'all ever get that working with the induction tactic?

view this post on Zulip Jalex Stark (Aug 12 2020 at 21:59):

I think so

view this post on Zulip Kyle Miller (Aug 13 2020 at 00:38):

Aaron Anderson said:

One place I think it would be better is proving the adjacency matrix formula for counting paths

We should probably make sure we match graph theory terminology. It bugs me as a topologist, but they call paths walks.

(I'm just quoting @Aaron Anderson's comment because somehow that's what made me remember. Counting paths is harder than counting walks.)

view this post on Zulip Aaron Anderson (Aug 13 2020 at 00:46):

Oof, that’s a good point

view this post on Zulip Kyle Miller (Aug 13 2020 at 00:56):

(moving discussion back to paths from maximal path)

view this post on Zulip Kyle Miller (Aug 13 2020 at 00:57):

Ok, one difference between my proposal and the structure for walks from before is that you can't specify the starting and ends points of the path. However, that's always just a subtype away

view this post on Zulip Kyle Miller (Aug 13 2020 at 00:58):

with walks G v w := {p : P n \graphmap G // p 0 = v /\ p n = w

view this post on Zulip Kyle Miller (Aug 13 2020 at 00:59):

(This would be using a coe_to_fn from graphmaps to maps on vertex sets, if that makes any sense to have.)

view this post on Zulip Alena Gusakov (Aug 13 2020 at 01:00):

This is how I was taught too

We should probably make sure we match graph theory terminology. It bugs me as a topologist, but they call paths walks.

view this post on Zulip Kyle Miller (Aug 13 2020 at 01:05):

@Alena Gusakov I'm always tempted to call them paths because of homotopy theory, which is probably the story with everyone else, too. (It's nice that "path connected" still means the same thing, since if two vertices are connected by a walk, then they are also connected by a path. If this weren't the case, I might have been inclined to use the homotopy theory terminology instead.)

view this post on Zulip Alena Gusakov (Aug 13 2020 at 01:06):

Ah yeah, I'm probably one of the people least familiar with homotopy theory here lol

view this post on Zulip Aaron Anderson (Aug 13 2020 at 01:06):

So, walks, loops, and cycles work well with homomorphisms and embeddings

view this post on Zulip Kyle Miller (Aug 13 2020 at 01:06):

I think this is a good test for which ever definition of walks we choose: can you prove that every pair of vertices connected by a walk is connected by a path? (Stronger: can you prove this walk uses a subset of the edges of the walk?)

view this post on Zulip Kyle Miller (Aug 13 2020 at 01:07):

I mean, you'll be able to prove it no matter the definition, I think, but it's a good check for whether it's a good definition.

view this post on Zulip Aaron Anderson (Aug 13 2020 at 01:07):

But I think path is really a multigraph definition

view this post on Zulip Aaron Anderson (Aug 13 2020 at 01:07):

Because of edge injectivity

view this post on Zulip Aaron Anderson (Aug 13 2020 at 01:08):

By the way, since we’re talking about graph homomorphisms and embeddings, check out #3750

view this post on Zulip Kyle Miller (Aug 13 2020 at 01:12):

@Aaron Anderson Good point about paths being a multigraph definition due to edge injectivity.

view this post on Zulip Kyle Miller (Aug 13 2020 at 17:42):

Aaron Anderson said:

By the way, since we’re talking about graph homomorphisms and embeddings, check out #3750

Would you mind explaining how this applies to graph homomorphisms and embeddings? I'm not familiar with order theory, but it seems like it could be useful.

view this post on Zulip Aaron Anderson (Aug 13 2020 at 18:26):

The definition has 0 to do with orders a priori, which is why I’m renaming it

view this post on Zulip Aaron Anderson (Aug 13 2020 at 18:26):

It just says basically that an embedding/equiv maps one relation to another

view this post on Zulip Aaron Anderson (Aug 13 2020 at 18:27):

So if you plug in two graph adjacency relations, you get graph embeddings

view this post on Zulip Kyle Miller (Aug 13 2020 at 18:29):

Oh, ok, that's a nice thing to have. Once you get that in, maybe I should wire sym2 up to it, too, since it has a map function. I guess relating sym2.from_rel, map, and those relation mapping functions.

view this post on Zulip Aaron Anderson (Aug 13 2020 at 18:41):

You could do it now with order_embedding, as long as you rename it rel_embedding when the PR merges


Last updated: May 08 2021 at 22:13 UTC