feat: basic graph definitions - #503
Conversation
|
I have some questions/comments: |
|
Discussion thread on this PR : |
| /-- The endpoint map, sending each edge to its unordered pair of endpoints. -/ | ||
| endpoints : ε → Sym2 α | ||
| /-- Every endpoint of an edge is a vertex. -/ | ||
| incidence : ∀ e ∈ edgeSet, ∀ v ∈ endpoints e, v ∈ vertexSet |
There was a problem hiding this comment.
This may cause a junk value problem on endpoints where an endpoint outside the set must be specified.
To avoid the junk value problem, we can define an edge object separately and define the graph directly over the edgeSet. Note that we use endpoints_id as the identifier for the multiplicity of an edge of the same endpoints
structure UndirectedEdge (α β : Type*) where
endpoints_id : β
endpoints : Sym2 α
deriving DecidableEq
abbrev Edge := UndirectedEdge
structure UndirectedGraph (α β : Type*) where
vertexSet : Set α
edgeSet : Set (Edge α β)
incidence : ∀ e ∈ edgeSet, ∀ v ∈ e.endpoints, v ∈ vertexSetThere was a problem hiding this comment.
Thank you for pointing this out and for the discussion in the Zulip thread. I've updated the definitions in line with your proposed solution to avoid this issue.
| /-- Typeclass for graph-like structures that have a vertex set. -/ | ||
| class HasVertexSet (G : Type*) (V : outParam Type*) where | ||
| /-- The vertex set of the graph. -/ | ||
| vertexSet : G → V | ||
|
|
||
| /-- Typeclass for graph-like structures that have an edge set. -/ | ||
| class HasEdgeSet (G : Type*) (E : outParam Type*) where | ||
| /-- The edge set of the graph. -/ | ||
| edgeSet : G → E |
There was a problem hiding this comment.
If you make these the canonical spelling then you need to restate all the loopless and incidence theorems in terms of them (and probably rename those fields to be loopless' to avoid stealing the preferred name)
There was a problem hiding this comment.
Thanks for pointing this out. I've restated the loopless and incidence theorems in terms of the new typeclasses and renamed the original fields to loopless' to free up the preferred name.
Please record these design decisions in the module docstring for future readers, not just the git history / PR title. |
| @[grind] | ||
| structure SimpleGraph (α : Type*) where | ||
| /-- The finite set of vertices. -/ | ||
| vertexSet : Finset α |
There was a problem hiding this comment.
Inconsistency on the set definitions: SimpleGraph is defined using Finset, whereas Graph is defined using Set.
There was a problem hiding this comment.
Thank you for pointing this out. This design decision was intentional, with the goal of arriving at a definition of SimpleGraph that serves as a canonical graph definition encompassing the most common usage. That said, I agree this introduces an inconsistency, and I've updated it to Set α. Finiteness can be supplied as a separate hypothesis.
| pairs of distinct vertices. -/ | ||
| structure SimpleDiGraph (α : Type*) where | ||
| /-- The finite set of vertices. -/ | ||
| vertexSet : Finset α |
| /-- The set of vertices. -/ | ||
| vertexSet : Set α | ||
| /-- The set of edges. -/ | ||
| edgeSet : Set ε |
There was a problem hiding this comment.
Avoidable junk value problem using the suggested definitions of Arc (similarly to Edge).
|
|
||
| /-- A finite simple graph on `α`: finite vertex and edge sets, edges as unordered pairs of | ||
| distinct vertices. -/ | ||
| edgeSet : Set (Edge α β) |
There was a problem hiding this comment.
Another option here would be Sym2 a -> Set b, which gives the set of edge labels for a given pair of vertices, and the empty set for disconnected nodes
There was a problem hiding this comment.
Thanks for the suggestion! We'd prefer to keep the set-based definition since it's closer to the informal G = (V, E) presentation, whereas your version is closer to the relational definition of Mathlib.Combinatorics.Graph.
There was a problem hiding this comment.
I am happy with the current definitions now. After a long discussion in the Zulip chat, the design is not bad, but it is similar to Mathlib's definitions of simple undirected graphs, whose development of set-based definitions is still in its early stages. We are happy to collaborate as the library grows.
Aside from the fragmentation of definitions in mathlib, one key principle of cslib is efficient computation, and we may redesign the definitions in the future to support efficient computation and reasoning about complexity. We prefer to have all graph definitions (undirected/directed and simple/non-simple) in one place, and to build other objects on top of the proposed graph definitions with efficient computation in mind.
P.S. This PR was a product of the Lean hackathon event at ETH Zurich. More basic primitives for graph algorithms will follow in subsequent PRs.
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
I see that @sorrachai has approved this, but I really do not feel that the Zulip thread has converged on accepting this PR, unless I am missing some other discussion in the graph theory channel.
This is decidedly not my area of expertise, but I am very worried about such a large deviation from very active development in Mathlib. I'd rather take this slowly and have a definite consensus or lack thereof rather than merge something too quickly.
I appreciate your concern. I would like to understand what happens if there is no consensus on this. |
|
I disagree that these definitions are computationally efficient, far from it. An efficient defintion would use lean arrays to represent neighbouring sets, better yet Vectors. This definition is merely a representational change which can be obtained by constructors on mathlib definitions. |
|
Summary. This pulls together the points we've made in the Zulip thread and earlier reviews. The design has two main ideas:
On compatibility with Mathlib. From what I understand, the concern raised so far is mostly not the design itself but the divergence from Mathlib's current API. We'd like eventual alignment too. Mathlib is already moving this way ( Introducing the definitions prevents stalling and enables active development of graph theory on the CSLib side without waiting for Mathlib's API to adapt. We hope Mathlib will push its graph definitions in this direction over time, though that will mean significant adaptation of existing APIs given the accumulated technical debt. If it does, alignment should be straightforward. If it doesn't, we still think the embedded-set design is much better suited to algorithmic graph theory. Automata in CSLib are a close precedent: developed in parallel with Mathlib's, the two have coexisted productively, each handling the use cases best suited to its scope. |
| /-- An undirected edge with a label of type `β` and an unordered pair of endpoints. -/ | ||
| structure Edge (α β : Type*) where | ||
| /-- The edge label, used to distinguish parallel edges. -/ | ||
| edgeLabel : β |
There was a problem hiding this comment.
edgeLabel is misleading. The labeling is intended for a specific pair of points. I would name it "endpointsLabel".
There was a problem hiding this comment.
| edgeLabel : β | |
| endpointsLabel : β |
| ## Main definitions | ||
|
|
||
| * `Edge α β`: an undirected edge with a label of type `β` and endpoints as a `Sym2 α`. | ||
| * `DiEdge α β`: a directed edge with a label of type `β` and endpoints as `α × α`. |
There was a problem hiding this comment.
Use Arc instead of DiEdge
|
Based on the online CSlib meeting today (28-05-2026), we agree to move forward with CSlib graphs using the current PRs, with a minor change to the naming. One important note is that we are happy to migrate/reuse appropriate definitions from Mathlib once their graph library (e.g., the graphLike class and the hierarchy of graph classes) becomes mature. One main question was whether the naming of graphs and digraphs in the PR was appropriate. There are two options:
Option 1 would be an unambiguous definition of what we mean by graphs. On the other hand, Option 2 is standard in a graph theory textbook. (For example, Graphs & Digraphs - 7th Edition - Gary Chartrand). In this case, I am inclining towards the second option. Other than my suggestions/comments in this PR, I don't have any other reservations. |
This seems very much at odds with what has been discussed on Zulip, and I find referring to Mathlib's graph library as not "mature" misleading. What happened to discussion around points like this comment where @BasilRohner stated that they thought they could get what is desired here by defining new "alternative constructor" API that didn't require actually duplicating definitions or this comment about defining new types but proving a proof of an injective map into the existing |
|
@sorrachai and @fmontesi Notwithstanding other discussions, Might I also suggest moving this to a subfolder of foundations in this PR, since technically this PR is defining mathematical foundations for CS? |
|
Hi Shreyas4991, that's fine. We can discuss its home folder in a separate thread. Hi @chenson2018, thanks for the comments. I am referring to the roadmap for GraphLike, which may take some time until it fully develops. Currently, Mathlib has 4 definitions of graphs: Quiver, DiGraph, Graph, SimpleGraphs (and maybe more in automata?). I know that they are working on having a more unified definition via the notion of GraphLike. I am happy to reuse whatever it has in Mathlib. However, as it stands, they only have a simple undirected multi-graph that is a set-based definition that we can potentially reuse. These suggestions from the discussion are valid. However, other than that, they do not have usable directed graphs, directed simple graphs, or undirected simple graphs, which they are working on right now. I think having all those definitions coherently in one place in CSLib is easier, especially for a new contributor. It is extremely simple. My working group downstream is quite happy with the definitions so far. The graph definitions in Mathlib are designed to maximize generality; they are currently quite complicated for newcomers who want to contribute to CSlib. My point is that I am willing to wait for Mathlib until all fragmentations in Mathlib are cleanly resolved before getting involved in the complicated process. I believe in the long run, the best version of the graph will definitely live in Mathlib, and we are happy to migrate to that. I encourage you to join us in the online cslib meeting for further elaboration and discussion. |
I did join last week, but these are pretty early for my current timezone. It would be helpful for these discussions to make their way back to Zulip, especially when there is already an ongoing thread. Would you be able to put a summary in the thread on graph definitions? |
|
Sure, I added the reference to the summary of today's discussion in that thread#CSLib > New graph definitions @ 💬. |
|
Renamed On naming: I'd prefer to keep |
|
@chenson2018 I notice that you requested changes. Can you elaborate what changes you are looking for? |
Thank you for the comments and feedback. Now, it is good time to move on.
|
I don't think any decision was made to merge this PR. Quite the opposite per the thread |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
I still hold the same objections to this PR. In short, I am unclear on: the motivation for duplication of Mathlib, what fundamentally differs in the formalization of graphs this is meant to support, and the responses or lack thereof to the many suggestions on Zulip for bridging this gap. I think this leads to an unnecessary fracture in the ecosystem for graph formalization, an area of active development in Mathlib that has formalized serious results.
If this is the final form of this PR, I am not sure that we'll reach a place of agreement. I'd like to hear from @fmontesi on this, perhaps on the Zulip where it can be easier to communicate.
|
I second Chris. None of the critical points have received adequate response or been addressed so far. So I see no reason to move on. I would actually recommend closing this PR, abandoning the effort to needlessly duplicate Graphs, and instead working within mathlib's process. Graph algorithms can be built perfectly within the existing API and ongoing mathlib work. |
|
Hi @chenson2018, thanks for raising this — I appreciate the concern, and I want to be clear that I'm not proposing we avoid reusing Mathlib. My worry is timing. Several of the pieces we'd be depending on are still WIP upstream, and I don't think it's realistic to block on them landing. I'd suggest we move forward with what we have here and reconcile with Mathlib once those pieces stabilize — that seems like a normal, healthy sequence to me, and it's easier to do once the library has grown enough to show us what the right shared abstractions actually are. The practical concern is that this PR has been open for several months and we still don't have the definitions in. That cost is real, and it compounds — other work is waiting on these. Is there a specific risk you see in landing now and reconciling later that I might be underweighting? If it's something we could address with a TODO or a follow-up issue, I'd be glad to do that. |
|
I want to emphasize that there isn't much duplication at the moment, as Graph in Mathlib is undergoing a major refactoring. |
|
The issue is, going ahead still fractures the library ecosystem and makes repair harder for everyone, contributors, downstream users, and maintainers alike. Even if it takes time, it is best to wait for the refactor and build on what is available until then. Imho, the best thing to do is to close this PR, and speed up the Graph PRs and focus on the addition of the necessary combinatorial lemmas in mathlib. And I wish to emphasize again, that graph algorithms has absolutely no need for these changes. |
This argument doesn't make sense to me. At the end of whatever refactoring is happening in Mathlib, there will still be these definitions in Mathlib, and they would still be duplicated here. If anything, this would be the best time for us to engage with the Mathlib folks and ensure that the refactor lands in a way that both libraries are happy with these definitions. Otherwise, it seems like a real possibility that we end up having the same conversation again in some months, with the difference being that Mathlib has already gone through one major refactoring and would have even less appetite to do so again. |
|
Sure, happy to engage with the Mathlib folks on this. The conclusion so far is to please wait for Mathlib's definitions until the refactoring is complete. One thing I'd ask us to weigh alongside that, though: there's a cost on the other side too. We've had nothing in CSLib on this for months, and that delay has its own price — other work is waiting on these definitions. I'd like us to factor that in rather than treating "wait for upstream" as the default with no downside. The design space is vast, and cslib focus might differ, and we inevitably diverge in the design at some point. We want to take advantage of the fact that we are relatively small and fast to develop graph algorithms independently. I think automata theory has had this issue before, and cslib decided to use cs version, and it has been great so far. |
|
I think we can expect progress in CSLib on the algorithms side soon once the algorithms pr issue is resolved, for which a meeting will soon be arranged. There is 7000-8000 lines of Algolean waiting to be upstreamed. Making progress on CSLib algorithms is, therefore, orthogonal to this duplication. Splintering the graph library for the sake of short-term progress is not a wise choice. In fact the added burden of maintenance and back-and-forth with mathlib will hamper progress even more in the medium term. |
As I've discussed before, I do not think this is analogous. This was a very inactive area of Mathlib, the introduction of |
|
I don't have an opinion about the issues discussed above. But I think it would help a lot if there is a summary of the differences and similarities of the various types of graphs proposed here and those existing in mathlib, perhaps with justifications for the proposed differences. |
Unfortunately, in this particular PR,I don't think it helps at all. The duplication here is clear. Mathlib already has definitions for simple graphs, simple digraphs, and Graphs in general. This definition is easily subsumed within the mathlib definitions and working with them is the correct way forward even if it takes time. Further, I still don't think any justification has been offered for the claim that somehow this PR is the reason for lack of progress in algorithms. To clarify: Justification for this would usually take the form of a Zulip thread, where someone presents their attempt to define simple algorithms under existing definitions. Then respondents experiment with the code and explain the right way to fix the problems they face. If a change is needed in mathlib definitions, they are directed towards the right PRs. This process has simply not happened here, This is despite repeated requests on my part to show where the obstacle is in code. |
7 participants
This PR introduces basic graph definitions:
Graph,SimpleGraph,DiGraph, andSimpleDiGraph, along with coercions and notation that form the basis of algorithmic graph theory in CSLib.Design. We intentionally diverge from Mathlib's graph definitions, prioritizing representations that support algorithmic reasoning. In graph algorithm design, it is common to manipulate graphs in many ways (e.g., dynamic graph operations such as adding or removing nodes/edges, contracting edges, and contracting vertex sets). As a result, we prioritize a minimal, simple definition of graphs that best aligns with how they are defined in the literature on algorithmic graph theory. In particular, we use set-based definitions of both the vertex and edge sets, along with minimal additional attributes, to reduce early proof obligations and select those whose proofs are closer to their textbook counterparts.
General structures. Here we use
Seteverywhere, allowing statements about possibly infinite graphs uniformly without enforcing finiteness through extra axioms. We associate labels with edges for the more general multigraph notions (Graph,DiGraph) via the auxiliaryEdgeandArcrecords, and abstract the label away for the more restricted notions (SimpleGraph,SimpleDiGraph), which useSym2 αandα × αdirectly. The definitions have been tested in practice by further formalizing concepts such as walks (see the GraphAlgorithms Walk module). However, to keep this PR concise, we defer discussion of the Walk design to a later PR.Comparison with PR #427. PR #427 introduced
SimpleGraphwithFinset-based vertex and edge sets and edges viaSym2. Here, we useSetthroughout, treating finiteness as an orthogonal concern rather than baking it into the type, and introduce a hierarchy comprising both general multigraph structures (Graph,DiGraph) with edge labels and specialized structures (SimpleGraph,SimpleDiGraph) without labels, since multi-edges are disallowed there.Main definitions.
Graph: (possibly infinite) undirected multigraphSimpleGraph: (possibly infinite) undirected graph without loops or multi-edgesDiGraph: (possibly infinite) directed graphSimpleDiGraph: (possibly infinite) directed graph without loops or multi-edgesFuture work. We plan to add fundamental graph algorithms building on these definitions.
Co-authored-by: Sorrachai Yingchareonthawornchai sorrachai.cp@gmail.com