Directed Graph Theory

[Simon Dold]

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

[Alexander van der Vekens]

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