I think the definitions *.af Nodes iArcs *are not necessary (and therefore
should be avoided), because they are exactly the same as *.ef Vtx iEdg*
(except for the names, and I see no need to change the names, see Wikipedia
https://en.wikipedia.org/wiki/Graph_(discrete_mathematics)#Directed_graph:
here we also have vertices and (directed) edges).
The directed graphs can be defined by the existing classes, e.g.:
df-dhgr $a |- DHGraph =
{ g | [. ( Vtx` g ) / n ]. [. ( iEdg ` g ) / a ].
a : dom a --> ( ~P n X. ~P n ) } $.
Furthermore, I see no need for extended structures being both directed and
undirected graphs, i.e., having two different slots .af and .ef.
Furthermore, the empty sets should be considered or excluded from the
definition: What would be the meaning of ( a ` i ) = <. (/) , { a , c } >.
or ( a ` i ) = <. { a , c } , (/) >. or even ( a ` i ) = <. (/) , (/) >.?
A meaningful example would be ( a ` i ) = <. { a , c } , { b } >.,
representing a directed multiedge from the vertices a and c to the vertex b.
Alexander
On Saturday, December 10, 2022 at 5:19:17 PM UTC+1 [email protected] wrote:
> 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/d898e3e8-5e1f-46e9-b300-a5898513ac46n%40googlegroups.com.
