In October 2020, I started the revision of the definitions and theorems for
Graph Theory (PART 16 of set.mm), based on the discussion in Github issue
#1418:
Since the beginning of dealing with graph theory in set.mm, the question if
graphs shall be represented as ordered pairs (of a set of vertices and a
set of edges) or as extensible structures (the set of vertices as base set,
and a special slot for the edges) was open (the current graph theory in
PART 16 is based on the representation by ordered pairs).
The new approach is based on the definitions ~df-vtx and ~df-iedg for
functions Vtx and iEdg to get the vertices and (indexed) edges of graphs
represented by an arbitrary class G, and this works for G being either an
ordered pair or an extensible structure (and some other, maybe degenerated
cases). If required, other representations could be supported by extending
the two definitions in the future (with no changes of the other definitions
and theorems!). The revised graph theory is build on these two functions
(usually setting V = ( Vtx ` G )and E = ( iEdg ` G ) and using V and E in
the definitions and theorems only), disregarding the concrete
representation of a graph. Therefore, a decision how to represent a graph
will be not necessary anymore.
This was the main objective for the revision of the graph theory.
Additional motivations were:
- Provision of a general framework for graphs
- Alignment of Eulerian Paths with the general concepts of walks, trails
and paths
During the revision, a lot of additional improvements could be achieved:
- simplifications, generalisations and alignments of definitions and
theorems,
- many proof shortenings
- improvement/enhancement of comments
- additional bibliographic references
The revision of PART 16 is currently contained in section "21.34.8 Graph
theory (revised)" of my mathbox.
In the following, the main changes are explained in more detail:
- definition of functions Vtx and iEdg which provides the vertices resp.
indexed edges of an arbitrary class regarded as graph. This allows
representations of graphs as ordered pairs <. V , E >. as well as
extensible structures { <. ( Base ndx ) , V >. , <. ( .ef ndx ) , E >. ,
...}, see sections 21.34.8.1 and 21.34.8.2.
- revision of the definitions for hyper-/pseudo-/multi-/simple graphs
based on the functions Vtx and iEdg , see sections 21.34.8.3, 21.34.8.4 and
21.34.8.7
- relationship between graphs and "incidence structures", see section
21.34.8.3
- the graphs formerly called "multigraphs" are now called
"pseudographs", whereas "multigraphs" are special pseudographs (still with
multiedges, but without loops) now, see section 21.34.8.4
- more systematic usage of the definition of (not indexed) edges, see
section 21.34.8.6
- provison of a definition for subgraphs, see section 21.34.8.9
- provison of a definition for finite graphs, see section 21.34.8.10
- revision of the definitions for neighbors, complete graphs, universal
vertices and connected graphs based on the functions Vtx and iEdg , see
sections 21.34.8.11 and 21.34.8.25
- definition NN0* and related theorems for extended nonnegative integers
added, see section 21.34.7.19
- revision of the definition for the vertex degree based on the
functions Vtx and iEdg and to be appropriate for arbitrary hypergraphs, see
section 21.34.8.12
- revision of the definition for regular graphs (including regular
graphs with infinite degree) based on the functions Vtx and iEdg and to be
appropriate for arbitrary hypergraphs, see section 21.34.8.13
- revision of the definition for walks, closed walks, walks in regular
graphs, trails, (simple) paths, circuits and circles based on the functions
Vtx and iEdg and to be appropriate for arbitrary hypergraphs, see sections
21.34.8.14, 21.34.8.16, 21.34.8.17, 21.34.8.18, 21.34.8.19 and 21.34.8.22
- special theorems for loop-free graphs and walks in loop-free graphs,
see sections 21.34.8.5 and 21.34.8.15
- examples for short walks, trails, etc. (up to a length of 4) added and
revised, mainly based on "words", see section 21.34.8.24
- revision of the definition for (closed) walks as words based on the
functions Vtx and iEdg and to be appropriate for arbitrary hypergraphs, see
sections 21.34.8.20 and 21.34.8.23
- equivalence of walks represented as words and the "usual way" for
pseudographs (which can have multiple edges between two vertices) shown by
using the Axiom of Choice (not required for the corresponding theorem for
simple pseudographs!), see section 21.34.8.20.
- replacement of "Walks/paths of length 2 as ordered triples" by
"Walks/paths of length 2 (as length 3 strings)", see section 21.34.8.21
- revision of the definition of Eulerian paths based on the definition
of walks and trails, see section 21.34.8.26
- revision of the Koenigsberg Bridge problem, based on the revised
definition of eulerian paths (and other, required concepts), see section
21.34.8.27
- revision of the definition of friendship graphs, the friendship
theorem and its proof following Huneke's approach, based on the revised
defintion of friendship graphs, see sections 21.34.8.29, 21.34.8.30 and
21.34.8.31
The next main step will be to replace "PART 16 GRAPH THEORY" entirely by
section
"21.34.8 Graph theory (revised)" of my mathbox. Everything contained in
PART 16 is
contained in section 21.34.8, so there will be no loss of
information/knowledge.
On the contrary, section 21.34.8 (about 1300 statements) provides more
information/knowledge than PART 16 (about 800 statements).
The names I used for class symbols and labels are in part temporary,
because they overlap with the current names in PART 16. They will be
adjusted after PART 16 is replaced by the revised material. However,
suggestions for improved names are always welcome.
I want to ask everybody who is interested in graph theory, and who has some
spare time, to have a look at the revised definitions and theorems in
section 21.34.8 of my mathbox, and to provide advices and suggestions for
further improvements before I continue.
Please give feedback until end of July, I plan to perform the replacement
starting in August.
In the meantime, I will perform some minor additinal
improvements/adjustments, and I will clean up section 21.34.9 of my
mathbox, which is almost completely covered by section 21.34.9. The
remaining theorems will be revised and moved to section 21.34.9. before the
replacement of PART 16.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/943e32d5-63e4-4393-82ea-9e09126d46dbn%40googlegroups.com.
