walks

Stream: graph theory

[Alena Gusakov]

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

[Alena Gusakov]

@Yakov Pechersky what do you mean by this exactly?

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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

[Alena Gusakov]

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]

Didn't know it existed tbh

[Yakov Pechersky]

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

[Yakov Pechersky]

That would be is_cycle

[Alena Gusakov]

Could also take advantage of list defs too, like count

[Alena Gusakov]

Which is super convenient

[Bhavik Mehta]

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

[Bhavik Mehta]

Probably @Kyle Miller can be more helpful

[Alena Gusakov]

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]

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

[Alena Gusakov]

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

[Yakov Pechersky]

Can't labeled graphs be done with sigma types?

[Bhavik Mehta]

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]

@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]

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]

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]

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]

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]

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]

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]

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

[Kyle Miller]

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]

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

[Yaël Dillies]

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

[Eric Rodriguez]

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

[Eric Rodriguez]

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

[Yaël Dillies]

Yeah of course

[Eric Rodriguez]

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]

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

[Yaël Dillies]

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

[Yaël Dillies]

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]

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

[Yaël Dillies]

What's that?

[Eric Rodriguez]

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

[Yaël Dillies]

Oh so quiver is actually already a generalisation of multigraph.

[Eric Rodriguez]

Yeah, this is what I was trying to say

[Eric Rodriguez]

undirected things are quite annoying in it though

[Eric Rodriguez]

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

[Yaël Dillies]

Oh

[Yaël Dillies]

So is there any advantage in having multigraph?

[Eric Rodriguez]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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

[Eric Rodriguez]

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

[Yaël Dillies]

Oh yeah, that's great!

[Yaël Dillies]

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

[Kyle Miller]

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

[Kyle Miller]

Multigraphs should allow loops.

[Yaël Dillies]

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]

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]

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]

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

[Kyle Miller]

Indeed (they become loop edges)

[Yaël Dillies]

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]

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]

(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]

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]

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

[Kyle Miller]

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]

Should we then have something like walk and finwalk?