Zulip Chat Archive

Stream: new members

Topic: How do I represent a graph?


view this post on Zulip Huỳnh Trần Khanh (Feb 10 2021 at 09:07):

A tree sounds like something inductive so I think that'd be easy to represent. How about a graph?

view this post on Zulip Huỳnh Trần Khanh (Feb 10 2021 at 09:08):

In competitive programming I'd represent a graph using an array of arrays where graph[vertex] is the list of nodes adjacent to that vertex.

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 09:09):

There are 5 ways to represent a graph at least. You could use the version in mathlib but that might not be designed for performance issues but rather for reasoning. Another issue is that there are five different things which people mean when they say the word graph

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 09:11):

As a mathematician I am mostly interested in reasoning about objects so I don't care about the internal implementation, all I need is an interface which is good enough for me to make whatever API I need. With your background I suspect that implementation issues might be more important to you, but then of course the implementation you go for will depend on exactly which operations you want to be quick

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 09:13):

In short there are multiple answers to your question and the best one for you will depend on your use case

view this post on Zulip Huỳnh Trần Khanh (Feb 10 2021 at 09:15):

Hmm I want something that's easy to reason about, I don't really care about performance for now. But I just did a quick search on the mathlib page and I only saw moving octopuses :joy:

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 09:17):

I've not been following the graph theory stuff, but there is an entire stream about it which you might not know about -- #graph theory

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 09:17):

I think people aren't subscribed by default to it

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 09:18):

I had assumed we'd got the definition by now!

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 09:19):

docs#simple_graph ?

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 09:20):

Of course you might have another notion of graph in mind, the word is used to mean several related but different things in the mathematical literature

view this post on Zulip Huỳnh Trần Khanh (Feb 10 2021 at 09:25):

This is the notion of graph I had in mind https://csacademy.com/app/graph_editor/ and yeah, it looks like docs#simple_graph is the thing I'm looking for. The docs looks really intimidating though.

view this post on Zulip Kyle Miller (Feb 10 2021 at 19:18):

The simple_graph type is pretty much representing a simple graph as an adjacency matrix. If G : simple_graph V, then V is the vertex type and G.adj v w represents that v is adjacent to w. It doesn't support multiple edges or loops of course. If you want the finite set of vertices adjacent to a vertex, there's G.neighbor_finset v.

view this post on Zulip Kyle Miller (Feb 10 2021 at 19:19):

I just quickly wrote this, but if you want the array of arrays representation (well, linked list of linked lists) then you could try something like this:

structure graph :=
(adj_lists : list (list ))
(has_verts :  (adj_list  adj_lists) (n  adj_list), n < adj_lists.length)

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 19:20):

I suppose eventually we will have a simple_graph constructor that takes in an adjacency matrix as a matrix.

view this post on Zulip Kyle Miller (Feb 10 2021 at 19:25):

Here's another possible definition for a (locally finite) graph:

import data.finset

structure graph (V : Type*) :=
(adj_set : V  finset V)

What finset does, essentially, is to force your algorithm to not care about the ordering of an adjacency list. That might be difficult to write algorithms for, but if V is orderable then sort from data.finset.sort can give you a list of the adjacent vertices.

view this post on Zulip Kyle Miller (Feb 10 2021 at 19:29):

You could also work with graphs with ordered adjacency lists:

structure graph' (V : Type*) :=
(adj_list : V  list V)

There's a function graph' V -> graph V by sending each adjacency list to an adjacency finset. Maybe if you write algorithms for graph', you could then prove the algorithm descends to graph.

view this post on Zulip Kyle Miller (Feb 10 2021 at 19:34):

These three types I gave are all for some version of directed multigraphs, by the way. It would be up to you to add a condition for having edges going in both directions. For example, you might do

structure graph (V : Type*) :=
(adj_list : V  list V)
(symm :  v (w  adj_list v), v  adj_list w)

view this post on Zulip Alena Gusakov (Feb 10 2021 at 20:34):

I suppose eventually we will have a simple_graph constructor that takes in an adjacency matrix as a matrix.

Could you not just use from_rel? I'm gonna try that

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 20:36):

Oh, I meant giving Lean an actual matrix like:

import data.matrix.notation
-- adjacency matrix of a triangle
#check ![![0,1,1], ![1,0,1], ![1,1,0]]

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 20:37):

Maybe what I'm describing should be a tactic or something? Not sure...

view this post on Zulip Alena Gusakov (Feb 10 2021 at 20:51):

Ah I see

view this post on Zulip Alena Gusakov (Feb 10 2021 at 20:53):

Wait so like

def graph_from_matrix (M : matrix α α R) (h : M = M) : simple_graph α :=
{ adj := λ v w, M v w = 1  v  w,
  sym := λ v w h2, by { rw [ transpose_apply M, h], exact h2.1, ne.symm h2.2 },
  loopless := λ v h, h.2 rfl }

view this post on Zulip Bryan Gin-ge Chen (Feb 10 2021 at 20:57):

Yep, exactly. This could make it easier to define / specify certain explicit graphs.

view this post on Zulip Alena Gusakov (Feb 10 2021 at 20:59):

Yeah I think it would be super useful for digraphs/multigraphs especially

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 21:51):

You might even say

(h : M = M . dec_trivial)

view this post on Zulip Yakov Pechersky (Feb 10 2021 at 21:52):

If there's the proper decidable instance in place.


Last updated: May 13 2021 at 22:15 UTC