Hello everyone, I want to work with directed graphs in Metamath.
My plan is to "translate" the theorems from $[ set-graphth.mm $] into directed graphs. Changing edges to arcs and vertices to nodes. Mario mentioned that it is important that the definition generalzes well ( https://groups.google.com/g/metamath/c/KdVXdL3IH3k/m/GzU5OsdNCQAJ ). Therefore I want to start with an very general form of directed hypergraphs. My idea is to define them with $c .af $. $( Extend class notation with an arc function. (Compare ~cedgf ) $) carcf $a class .af $. $( Define the arc function (indexed arcs) of a digraph. (Compare ~df-edgf ) $) df-arcf $a |- .af = Slot ; ; 1 8 0 $. $c Nodes iArcs $. $( Extend class notation with the nodes of "digraphs". (Compare ~cvtx ) $) cnds $a class Nodes $. $( Extend class notation with the indexed arcs of "digraphs" (Compare ~ciedg ) $) ciarcs $a class iArcs $. $( Define the function that maps a digraph to the set of its nodes. This definition is very general: It defines the set of nodes for any ordered pair as its first component, and for any other class as its "base set". It is meaningful, however, only if the ordered pair represents a digraph reps. the class is an extensible structure representing a digraph. ( Compare ~df-vtx ) $) df-nds $a |- Nodes = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 1st ` g ) , ( Base ` g ) ) ) $. $( Define the function that mapps a digraph to its indexed arcs. This definition is very general: It defines the indexed arcs for any ordered pair as its second component, and for any other class as its "arc function". It is meaningful, however, only if the ordered pair represents a graph resp. the class is an extensible structure (containing a slot "arc function") representing a graph. (Compare ~df-iedg ) $) df-iarcs $a |- iArcs = ( g e. _V |-> if ( g e. ( _V X. _V ) , ( 2nd ` g ) , ( .af ` g ) ) ) $. $c DHGraph $. $c DSHGraph $. $( Extend class notation with directed hypergraphs. (Compare ~cuhgr ) $) cdhgr $a class DHGraph $. $( Extend class notation with directed simple hypergraphs. (Compare ~cushgr ) $) cdshgr $a class DSHGraph $. ${ $d e g v $. $( Define the class of all directed hypergraphs. An directed hypregraph consists of a set ` n ` (of "nodes") and a function ` a ` (representing indexed "arcs") into the ordered pairs of subests of this set (the empty set excluded). (Compare ~df-uhgr ) $) df-dhgr $a |- DHGraph = { g | [. ( Nodes ` g ) / n ]. [. ( iArcs ` g ) / a ]. a : dom a --> ( ~P n X. ~P n ) } $. $( Define the class of all directed simple hypergraphs. An directed simple hypergraph is a special (non-simple, multiple, multi-) hypergraph for which the arc function ` a ` is an injective (one-to-one) function into ordered pairs of subsets of the set of nodes ` n ` , representing the (one or more) nodes incident to the arc. Note that literature is devided about the definition of hypergraphs. Some require arcs to connect one subset to one node others allow arbitrary subsets as head or tail (including the empty set). Here an arbitrary subset connects to another arbitrary subset of nodes. This definition was chosen to get to directed digraphs by restricting the definition to subsets of size equal to 1 (see ~df-dmgr ). (Compare ~df-ushgr ) $) df-dshgr $a |- DSHGraph = { g | [. ( Nodes ` g ) / n ]. [. ( iArcs ` g ) / a ]. a : dom a -1-1-> ( ~P n X. ~P n ) } $. $} $c DMGraph $. $( Extend class notation with directed multigraphs. (Compare ~cupgr ~cumgr )$) cdmgr $a class DMGraph $. ${ $d a g n x $. $( Define the class of all directed multigraphs. A directed multigraph consists of a set ` n ` (of "nodes") and a function ` a ` (representing indexed "arcs") into pairs of subsets of ` n ` of cardinality one, representing the two nodes incident to the arc. Note that the head and the tail are singelton sets instead of just elements of ` n ` because this allows directed multigraphs to be a subset of directed hypergraphs which require the head and tail to be subsets of ` n ` . If two or more arcs join the same pair of (distinct) nodes, then these arcs are called parallel arcs. (Compare ~df-upgr ~df-umgr ) $) df-dmgr $a |- DMGraph = { g | [. ( Nodes ` g ) / n ]. [. ( iArcs ` g ) / a ]. a : dom a --> { x e. ( ~P n X. ~P n ) | ( ( # ` ( 1st ` x ) ) = 1 /\ ( # ` ( 2nd ` x ) ) = 1 ) } } $. $} My question is if this is the right approach, maybe there is a pitfall that I do not see or something I have to be aware of? Best regards, Simon -- 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/9d16f04d-06da-4674-b65d-36033850b25fn%40googlegroups.com.
