search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
626 stars 143 forks source link

Feature requests to the generic graph theory #1278

Closed binghe closed 2 months ago

binghe commented 3 months ago

Hi,

Below are some feature requests for the generic graph theory (in examples/generic_finite_graphs):

  1. For graphs without node and edge labels, there's the need to have two edges for the same pair of nodes, i.e. the (undirected) edge (m,n) occurred more than once in the graph (based on bagTheory). This is meaningful, more edges change the degree of adjacent nodes.

NOTE: graphs allowing multiple edges between the same pair of nodes is called multigraph (see [1, p.28] or [2]), and it's better to have a dedicated type name for it. Depending on other type variables, a multigraph could have node/edge labels, directed edge, self-loops, potentially infinite nodes and edges, etc.

  1. Is it possible to require (as part of wfgraph) that the type of nodes should be at least countable? Because otherwise there's no way to allocate fresh nodes (e.g. to make a subdivision to an existing edge in the graph, a fresh node must be allocated.)

  2. A large variety of graph theory theorems are expressed on finite graphs having multi-edges and self-loops, I think it's better to have a dedicated name for it, but I'm not sure about this type name. (Maybe fmgraph, indicating "finite multigraphs (self loops allowed)").

--Chun

[1] R. Diestel, Graph Theory, 5th Electronic Edition (2016), 5 ed., vol. 173. Berlin: Springer-Verlag, 2017 [2] https://en.wikipedia.org/wiki/Multigraph

binghe commented 3 months ago
  1. Since the formalization indeed supports infinite nodes (and infinite edges), I suggest we renaming the directory, to example/graph.
binghe commented 2 months ago

Closed by a9c366c0bee1aa54fc6df60b55902bfd5b243538