Directed Binary Graph (Lattice) as Irreflexive Poset

[Brian Larson]

Alexander van der Vekens contributed an impressive collection of definitions and theorems for graph theory.  Most of it applies to undirected hypergraphs, but most of 16.1 seems generally applicable.

I want to model a directed binary graph, G, that has many of the properties of a poset, but has a partial order relation which is irreflexive, ( lt ` f ) rather than ( le ` f ).

I need graph G = <. V , E >. where V is a set of vertices, and E is a set of binary, directed edges on V,

E C_ ( V x V ) where the direction is from the first element of the ordered pair, to the second element, with the following properties:

• E must connect V
  
• E must be acyclic
• E must have a distinguished "start" vertex (least vertex l e. V), from which there must be a path to every other vertex in V
• E must have a distinguished "end" vertex (upper bound u e. V), to which there must be a path from every other vertex in V
• Existence of a path from V1 to V2 determines V1 < V2

df-vtx and df-iedg look like a good start to represent vertices and edges as extensible structures.

However, these properties of E look like a poset with lt derived from le by df-plt.

How do I require edges E to also be a poset with V = ( Base ` E ) and ( lt ` E ) defined as path existence?

Does G being connected follow from ( E e. Poset )?

--Brian

[Alexander van der Vekens]

Hi Brian,

it's great that you are interested in graph theory. Although I work only with undirected graphs (at the monment), the definitions in 16.1 should be general enough to be used also for other kinds of graphs.

A definition for directed pseudographs (allowing multiedges and loops) could be (analogous to the definition df-upgr for undirected pseudographs):

    df-dpgr $a |- DPGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e --> ( v X. v ) } $.

If you want to have directed multigraphs (pseudographs without loops), you could define them as follows:

df-dmgr $a |- DMGraph = { g | [. ( Vtx ` g ) / v ]. [. ( iEdg ` g ) / e ]. e : dom e --> { x e.  ( v X. v ) | ( 1st ` x ) =/= ( 2nd ` x ) } } $.

The other conditions you listed would be more complicated to formalize. Maybe the start and end vertices could be modelled by providing an ordered set (maybe Words) as domain of the edge function e, and the first vertex of the first edge and the second vertex of the last edge could be regarded as start vertex resp. end vertex.

I hope these hints are sufficient for you to continue.

Alexander

[Thierry Arnoux]

Posets, Tosets and Lattices are already defined in set.mm. I imagine one may define a function F mapping them to their corresponding graphs : vertices are the same base, edges are something like the set { <. x, y >. | ( x ( le ‘ P ) y /\ -. E. z ( x ( le ‘ P ) z /\ z ( le ‘ P ) y ) ) }
Then, I think ran F would be the set of graphs you’re interested in.
BR,
_
Thierry

[Alexander van der Vekens]

Good hint, Thierry!

But instead of mapping a Poset etc. as extensible structure to a graph, the extensible structure can be made a graph (that's because the structure is extensible!) by inserting an edge function into the slot ".ef", using the sSet operator. See, for example, ~structtousgr.

As edge function, ( _I |` E ) could be chosen with E = { <. x, y >. | ( x ( le ‘ P ) y /\ -. E. z ( x ( le ‘ P ) z /\ z ( le ‘ P ) y ) ) } as proposed by Thierry.

[Brian Larson]

Thierry and Alexander,

Thank you for the hints. structtousgr looks like a good example to study.

I was not aware of the sSet operator.  That looks like a good way to enforce the partial-order property.

The definition of E also prevents self-loops.

I'd also add existential uniqueness to disallow multiedges.

Least and greatest elements seem straightforward to define.

A path predicate would be existence of a chain of edges from one vertex to another.

Acyclic could be enforced by requiting that not vertex had a path to itself.

--Brian

[Alexander van der Vekens]

Hi Brian,

here are some additional remarks/hints on your points:

On Friday, December 31, 2021 at 11:58:47 PM UTC+1 brianral...@gmail.com wrote:

Thierry and Alexander,

Thank you for the hints. structtousgr looks like a good example to study.

I was not aware of the sSet operator.  That looks like a good way to enforce the partial-order property.

The definition of E also prevents self-loops.

Yes, because, of  -. E. z ( x ( le ‘ P ) z /\ z ( le ‘ P ) y ). But this condition also prevents many Posets to become graphs (at least ones with edges). For example, the field of the real numbers as Toset (see ~retos) would become a graph with no edges, because for every x,y there is a z with ( x ( le ‘ P ) z /\ z ( le ‘ P ) y . An alternative definition for the edges could be  E = { <. x, y >. | x ( lt ‘ P ) y }, but this would result in much more edges (not only edges between direct neighbors regarding the order relation).

 

I'd also add existential uniqueness to disallow multiedges.

This is not necessary, because  by choosing ( _I |` E ) as edge function (the edges are indexed by themselves), there is no way to have multiedges ( ( _I |` E ) is a 1-1 function, see ~f1oi)

Least and greatest elements seem straightforward to define.

I think the functions lub and glb  could be used for this.

A path predicate would be existence of a chain of edges from one vertex to another.

Paths are already defined (see df-pths), but for undirected graphs only. The definition of paths is based on the definition of walks, and the definition of walks strongly depends on the property of a graph to be undirected. Unfortunately, I see now way to provide a (usable) definition for walks/trails/paths etc. which would work for directed as well as undirected graphs.

Acyclic could be enforced by requiting that not vertex had a path to itself.

If there was a definition `DCycles` for cycles in directed graphs (as provided by ~df-cycls for undirected graphs). this condition could be expressed by using this definition, e.g., `( DCycles `` G ) = (/)`.