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 ∈ vertexSet
| /-- 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)
Please record these design decisions in the module docstring for future readers, not just the git history / PR title. |
5 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.
GraphandDiGraph(undirected and directed multigraphs) useSetto allow statements about possibly infinite graphs. Specialized structures (SimpleGraph,SimpleDiGraph) useFinsetdirectly rather than enforcing finiteness through additional properties, keeping the most commonly used types lightweight and directly computable. 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 introduce general structures (Graph,DiGraph) that useSet, while keepingFinsetin the specialized types (SimpleGraph,SimpleDiGraph) commonly used in algorithmic reasoning. Additionally, we drop edge labels inSimpleGraphandSimpleDiGraph, since multi-edges are disallowed, simplifying downstream reasoning.Main definitions.
Graph: (possibly infinite) undirected multigraphSimpleGraph: finite undirected graph without loops or multi-edgesDiGraph: (possibly infinite) directed graphSimpleDiGraph: finite 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