. Warning
This is an older version of my notes on Graph theory designed
for browsers that can not handle tables.  I strongly suggest
you transfer to
.See http://www/dick/maths/math_22_graphs.html
if your browser can handle tables.  Its more readable and has fewer errors
and more links...
.Open Graphs
The idea of a graph -- a mathematical picture of a relationship
between two sets -- goes back to Descartes.  He invented a way of
describing or modelling points in a plane by two numbers.  A
set of pairs of numbers defines a figure on this plane.  A function
defines a curve -- the graph of the function.

In the 19th and 20th centuries these ideas were made more general
and so more abstract as directed graphs: a set of things some of which
are connected in pairs.
.Open Digraphs
.Open Introduction
The directed graph or digraph is an intuitive model that has been useful in
many problems.  As a result it has many equivalent definitions.  Knuth 
remarked twenty years ago on the number of different words in use and the
habit of every author to select a new set of definitions of the same set of
words [Knuth69,Vol 1.2.3.4, p362].
 
A digraph always has a set of objects - called vertices or nodes.  These are
connected or linked in pairs. An Edge is the name given to an undirected link
between two nodes, while an arc stands for a directed edge. In the following
table V stands for Vertices or Nodes, E for edges, and A for Arc.
 
. Table of Digraph Definitions
.As_is From	Name        Synopsis,
.As_is --------------------------------------------------- 
.As_is 
.As_is Berge
.As_is		DIGRAPH
.As_is				Net{Nodes:Set, \Gamma:(@Nodes)^(Nodes|@Nodes)}
.As_is 
.As_is Harary & Norman & Cartwrite
.As_is 		NET       
.As_is				Net{X,V::Set, first,second::X->V,
.As_is				 arc::=  (first,second), loop::=  arc&Id(V)}
.As_is    ''	RELATION
.As_is				Net{NET, arc in X(0..1)-(1)V}
.As_is    ''	DIGRAPH
.As_is				Net{RELATION, loop=0}
.As_is 
.As_is Birkhoff&Bartee
.As_is		GRAPH 
.As_is				Net{N,A:Set, phi:A->(N><N)}
.As_is 
.As_is Manna	GRAPH 
.As_is				Net{V:finite_set, L:set, A:@(V><L><V)}
.As_is 
.As_is Harary	GRAPH 
.As_is				Net{V:Set, X:@V,  for all x:X(|x|=2)}
.As_is 
.As_is Berge	p-GRAPH
.As_is				Net{p:Nat1, S:Set, n:S^2->0..p}
.As_is 
.As_is Wilson	GRAPH
.As_is				Net{V,E:finite_set, E:(V^2)->Nat0}
.As_is    ''	DIGRAPH
.As_is				Net{V,E:finite_set, E:@(V^(2bag??))}
.As_is    ''	SIMPLE_GRAPH
.As_is				Net{V,E, E:@(V^2)}
.As_is 
.As_is Carre	Graphs_&_Networks
.As_is				Net{X:finite_set, U:@(X^2)}
.As_is 
.As_is Dossey, Otto, Spence, VanDen Eynden
.As_is    ''	directed_graph	
.As_is				Net{V:finite_sets, E:@(V^2)&finite_set}
.As_is --------------------------------------------------- 
 
. Definition of a Directed Graph
digraph::=  $ $DIGRAPH.
DIGRAPH::=Net{
Nodes::Sets,
Arcs::@(Nodes><Nodes).  -- Arcs act as a relation between Nodes.
ARC:=  Net{1st,2nd:Nodes}.
	(def)|-(DG1): Arcs in @ARC. 
	(def)|-(DG2): PARALLEL(Arcs, Nodes). -- So that we can use the relation
to define paths etc naturally.
.See http://www/dick/maths/notn_12_Expressions.html#Parallel Operators
and
.See http://www/dick/maths/math_11_STANDARD.html#Parallelism
paths::=  {x:#Nodes|| Arcs(x)}, 
	(def)|-(DG3): for all x:paths, i:1..(|x|-1) ((x[i],x[i+1]) in Arcs.
cycles::=  {x:paths||(x[|x|]=x[1]}.
loops::=  {x:cycles|| |x|]=2}.
 
in::Nodes->@Arcs=  map [n] (Arcs;{n}),
	(def)|-(DG4):  for all n, in(n)={(i,n)||for some (i,n) in Arcs}.
nodes_in:: Nodes->@Nodes=  map [n]({i||for some (i,n) in Arcs}).
nodes_in:: @Nodes->@Nodes=  map [N] (|[n:N]nodes_in(n)).
 
out:: Nodes->@Arcs=  map [n] ({n};Arcs),
	(def)|-(DG5): for n, out(n)={(n,o)||for some (n,o) in Arcs}.
nodes_out:: Nodes->@Nodes=  map [n] ({o||for some (n,o) in Arcs}).
nodes_out::@Nodes->@Nodes=  map [N](|[n:N]nodes_out(n)).
 
\Gamma::(@Nodes)^Nodes,
	|-(DG6): For all x,y:Nodes><Nodes, (x,y) in Arcs iff x in \Gamma(y).
	(DG6)|-(DG7): \Gamma=nodes_out.
 
 
ARROW::=  Net{from, to:Nodes},
Arrows::@$ $ARROWS.
	|-(DG8):Arcs={(from,to):Nodes><Nodes | $(ARROW) in Arrows}.
	(DG8)|-(DG9): Arrows={$(ARROW)||(from, to) in Arcs}.
 
edges::=  { {x,y}:@Nodes||(x,y):Arcs}.
semipaths::=  {p:#edges||for i:1..|p|-1(p[i]&p[i+1]<>0)}.
semicycles::=  {p:semipaths||p[1]=p[|p|]}.
simple::=   {p:#Nodes || p in dom(p)(0..1)-(1) p}.
 
 For p1,p2, p1...p2::=  {p:path || p1=p[1] and p2=p[|p|]}.
 
 For p1,p2, p1 connected_to p2::=  for some p:p1...p2().
|-(DG10): connected_to in Transitive(Nodes) & Reflexive(Nodes).
|-(DG11): ORDER(Set=>Nodes, relation=>connected_to).
 
strongly_connected::=  for all p1,p2 ( p1 connected_to p2).
 
 For p1,p2, p1 connected_with p2::=  p1 connected_to p2 or p2 connected_to p1.
|-(DG12): connected_with in equivalence_relation(Nodes).
 
strongly_connected_components::=  Nodes/connected_with.
 
weakly_connected_to::=  rel [p1,p2]( some p:semipath(p1=p[1] and p2=p[|p|])).
weakly_connected::=  for all p1,p2, (p1 weakly_connected_to p2).
 
|-(DG13): weakly_connected_to in equivalence_relation(Nodes).
connected_components::=  Nodes/connected_to.
 
|-(DG14): for all C:connected_components((Nodes=>C, Arcs=>Arcs&@(C,C)) in
weakly_connected).
roots::=  {r:Nodes||for all x:Nodes(r connected_to x and for no x:Nodes(x
connected_to r)}.
 
}=::DIGRAPH.
. Subgraphs
 For G:digraph, A:@G.Nodes, G.sub_graph(A) ::=  the $ $DIGRAPH(Nodes=>A, Arcs=>G.Arcs&@(G.A,G.A)).
SUBGRAPH::=Net{
	DIGRAPH(Nodes=>X, Arcs=>A),
	DIGRAPH(Nodes=>Y, Arcs=>B),
 |-(S1): X==>Y,
 |-(S2): A==>B.
}=::SUBGRAPH.
 
 For D1,D2:$ $DIGRAPH, D1 sub_graph D2 ::=  SUBGRAPH( X=>D1.Nodes, Y=>D2.Nodes,
A=>D1.Arcs,  B=>D2.Arcs).
 
. Digraph_morphisms
DIGRAPH_MORPHISMS ::=$DIGRAPH with following,
.Net
 
Arrows are defined as part of the STANDARD definitions of MATHS
.See http://www/dick/maths/math_11_STANDARD.html
 
 For D1,D2:$ $DIGRAPH, a:Arrows, ((digraph)D1 a D2) ::=  {f:D1.Nodes a D2.Nodes
|| for all x:D1.Arcs((f o x) in D2.Arcs},
 For D1,D2, a, (cograph)D1 a D2::=  {f:D1.Nodes a D2.Nodes || for all
x:@(D1.Nodes,D1.Nodes)~ D1.Arcs(not (f o x) in D2.Arcs},
(CM): For D1,D2, a, (cograph)D1 a D2=  {f:D1.Nodes a D2.Nodes || for all y:
D2.Arcs((/f o y) in D1.Arcs}.
.Close.Net DIGRAPH_MORPHISMS
 
All digraphs are epimorphic to a digraph with strongly connect components as
nodes.
|-(DM1):For all D:$ $DIGRAPH, some (digraph)D >== the DIGRAPH (Nodes=
D.strongly_connected_components, Arcs={(C1,C2)||some c1:C1,c2:C2(c1
connected_to c2)} ).
 
All subgraphs of a digraph are a digraph submorphism and vice-versa:
|-(DM2):For all D1,D2:$ $DIGRAPH,  D1 sub_graph D2 iff Id in (digraph)D1 ==>D2.
 
Connonical expansion
|-(DM3): For all D1,D2:$ $DIGRAPH, some f:(digraph)D1 >-> D2 then for one
X,Y:$ $DIGRAPH, e,i,m e in (digraph)D1>==X and i in (digraph)X---Y and m in
(digraph)Y==>D2 ).
. Proof of DM3
X.Nodes=D1.Nodes/f, ...
.Hole
 
 
. Circlets
CIRCLET::=Net{
	|-(C0): DIGRAPH and connected,
	|-(C1): Arcs in (1)-(1).
	|-(C2): Nodes in finite_set.
(C1,C2)|- (C3): for r=|Nodes|, all s,t:Nodes, one d:Int, all n:Nat0({s} = nodes_out^(d + n * r)(t)>>.
}=::CIRCLET.
circlet::=  $ $CIRCLET.
 
. n-Paths
 For G:$ $DIGRAPH
Paths[n](G) ::=   (digraph)(1..n, .+1)->G,
Paths(G) ::=  Union{Paths[n](G)||n:Nat},
Cycles[n](G) ::=  (digraph)(0..n-1, .+1 mod n)->G,
 
|- Strings(Paths(G),(!), ()),
 
.Open Trees
 
FREETREE::=  DIGRAPH and weakly_connected and semicycles={}.
tree::=  FREETREE and |roots|=1.
 
ORIENTED_TREE::=Net{ 
Compare Knuth Vol 1, 2.3.4., 
.Source Knuth 69, Donald Knuth, "Art of Computer Programming".
    (Nodes=>S, arcs=>E, \Gamma=>parents) ::digraph,
    r::= `The root of the tree`::S,
    |-(OT0): parents(r)={},
    |-(OT1): for all v:S~{r}( |parents(v)|=1 and v...r),
    children::=fun[v:S]{v':S || v in parents(v'))}
  ()|-(OT2): for all v, one v...r,
    (above, cycles)|-(OT3): cycles=0,

. Keonig's Infinity Lemma 
.Source Knuth 69,Vol 1, 2.3.4.3 Theorem K.
   (above)|-(OTK): if for all v(children(v) in finite(S)) and not S in Finite then some \mu:Nat-->S, all i:Nat(mu[i+1] in children(\mu[i])
}=::ORIENTED_TREE.

Also see
.See http://www/dick/maths/math_21_Order.html#PART_WHOLE

.Close Trees

. Directed Acyclic Graphs(DAGs)
DAG::= DIGRAPH and cycle={}.
dag::=  $ $DAG.
Gelernter[91] uses the name Trellis for a system where data flows define a
DAG.
 
.Close Digraphs
 
. Labelled Digraphs
LABELLED_DIGRAPH::=  DIGRAPH and following
.Net
This assigns a `label` to each node and arc.  It does not permit multiple 
arcs between nodes, even when they have different labels.
	   Node_labels::Sets, 
	   Arc_labels::Sets,
	   label::  Node_labels^Nodes | Arc_labels^Arcs,
	   node_label::Nodes;label,
	   arc_label::Arcs;label.
.Close.Net LABELLED_DIGRAPH.
labeled_digraph::=  $ $LABELLED_DIGRAPH.
labeled_dag::=  $ $LABELLED_DIGRAPH and cycle={}.

LABELLED_GRAPH::=Net{
This allows multiple arcs between nodes as long as the arcs have distinct
labels.
	Nodes::Sets,
	Node_labels::Sets, 
	Arc_labels::Sets,
	node_label::Nodes -> Node_labels,
	arc_label::(Nodes><Nodes)<>->Arc_labels,
	label:: node_label|arc_label,
	Arcs::= pre(arc_label).
	(DIGRAPH)|-(LG_is_DG): $DIGRAPH.

	For Nodes x,y, Arc_labels a, x-a->y::@= ((x Arcs y) and a in label(x,y)).
	For Arc_labels a, (-a->) ::@(Nodes,Nodes)= rel[x,y](x-a->y).

}=::LABELLED_GRAPH.
	
 
. Derivation Digraphs
Can be used to model set of interelated steps in a MATHS proof.
DERIVATION::=Net{
	Label::Sets.
	Object::Sets.
	Node_labels::=Label><Object.
	|-(De0): LABELLED_DIGRAPH.
	|-(De1): cycle={}.
	|-(De2): For all n:Nodes, a,b:in(n)( arc_label(a)=arc_label(b) ).
	
node::syntax= !![n:Nodes]( "(" LIST(1st o nodes_in(n)) ")" the
arc_label(in(n)) "(" 1st o node_label(n) "):" 2nd o node_label(n),
	where !![x:{a}|A](f(a)) ::= f(a) ! !![x:A] (f(x)) | !![x:A] (f(x)) ! f(a)
and !![x:{}]f(a) = "".
 
}=::DERIVATION.
 
. Baysian Networks
Causal networks, belief networks, influence diagram...

.Source Heckerman et al 95, David Heckerman & Abe Mamdami & Michael P WellMan
(Guest Eds)Real-World Applications of Bayesian Neworks, Comm ACM V38n3(Mar
95)pp24-57
BAYESIAN_NETWORK::=Net{
	Distinctions::Sets.
	Probabilities::=Real [0..1].
	Node_labels::=Distinctions.
	Arc_labels::=Probabillities.
	|-(BN0): LABELLED_DIGRAPH.
	|-(BN1): cycle={}.
.See http://www/dick/maths/math_81_Probabillity.html
}=::BAYESIAN_NETWORK.
 
. Categories
A category models a collection of algebra's of the same type and the structure
preserving mappings that connect them.  They allow the definition of free
objects, products and co-products in a very general form.  They are a natural
model to use for a data base or set of interconnected types.  They can be
regarded as a special kind of labelled digraph.

CATEGORY::= LABELLED_GRAPH and Net{
A category has a a way of composing arcs and a set of identity labels.
It is like a kind of partial infix operator system.

	composition::=o::(Arc_labels><Arc_labels)<>->Arc_labels.

	|-(Transitivity):For x,y,z:Nodes, if x Arcs y Arcs z then x Arcs z.
	(Transitivity)|-(precomposition):For x,y,z:Nodes, if x Arcs y Arcs z then (x,z) in pre(o).
	|-(Composition):For x,y,z:Nodes, xy,yz,xz:Arc_labels, if x-xy->y-yz->z then ( yz o xy = xz ).

	()|-(path_composition): For p:path, `the composition of the labels of the arcs in the path p is also a label on an arc connecting the ends of p`.

Each node has a special arc that acts as an identity operation.
	Id::Node_labels --> Arc_labels.

A node can have one identity, and this identity is not the same as any other
identity on other nodes.  A node may or may not have a non-identity self-loop, of course.

The identity labels are interesting because they have no effect on things when composed with them:
	|-(identity): For all x,y,z, xy, yz, Id(y) o xy =xy and yz o Id(y) = yz.

...
In MATHS we indicate a path a sequence like this: x-a->y-b->z-c->w, wherex,y,z,w are either nodes or node labels, and a,b,c are arc labels.

A set of paths is said to `commute` if the composition of the labels on the arcs in each path in the set are all the same.  The set is usually drawn as a diagram of a graph which contains all the paths.  


Example:
	{ x-a->y-b->z, x-c->w-d->z} commutes when b o a = d o c.
	
}=::CATEGORY.


 For the mathematical theory see
.See http://www/dick/maths/math_25_Categories.html
 
.Open Harel Higraphs
 
. Source Harel 88
This is taken from a paper published by David Harel, entitled "On Visual
Formalisms", in Issue number 5 of the 11 volume of the Communications of
Association for Computing Machinary (CACM, May 1988, pp514-530)
 
The following is a transcription into our notation of the "APPENDIX: Formal
Definition of Higraphs", with the exception of the relations `inside` and 
`is_part_of` which we have added to clarify and simplify the presentation.
 
In what follows we present a formal (non-graphical) syntax and semantics for
higraphs with simple bidirectional edges. The reader should have no difficulty
in extending the edges to represent, say, hyperedges.
 
. Syntax	
HIGRAPH::=Net{
Blobs::Finite_set,
subblob::(@Blobs)^Blobs,
	For a,b:Blobs, a in subblob(b) ::=`a is drawn inside b`,
par::(@(Blobs,Blobs))^Blobs,
 For a,b,c:Blobs, a(b.par)c ::=`a and c are in the same orthogonal components
of b`,
Edges::@(Blobs,Blobs),
 For a,b:Blobs, (a,b)in Edges::=`(a,b) is an arrow connecting a to b`,
.Dangerous_bend
In a Higraph an edge is not a boundaries of a Blob but an arrow connecting
blobs.
 
inside::=  {(u,v):Blobs^2|| u in subblob(v)},
 
is_part_of::=  (inside; do(inside)),
parts::=   map [x:Blobs]({y:Blobs||y is_part_of x},
 
(HG0): For no x:Blobs (x is_part_of x ),
|-(HG1): (Nodes=>Blobs, Arcs=>is_part_of ) in dag,
(HG2): For all x:Blobs (par(x) in Equivalence_relation(subblob(x)) ),
(HG3): For all x:Blobs, y,z:subblob(x), (if parts(x) & parts(y) then y equiv z
wrt par(x)),
atomic_blobs::=  {x:B || subblob(x)=0}
}=::higraph.
 
. Semantics of Higraphs
 
Semantics are decribed by giving a structure preserving maps(\mu_a,\mu_b,...)
from the syntatic
terms into expressions in logic and set theory.
 
 For S,T:Sets, S(>*<)T::Sets= `the unordered Cartesian product of S and T`::=
{{s,t}||s in S and t in T},
 
Higraph_model::=Net{
.See higraph.
D::Set=`unstructured_elements`,
 
mu_a::@D^atomic_blobs,
 
	|-(HM0): for all x,y:atomic_blobs(if x<>y then mu_a(x) & mu_a(y)=0),
mu_b::@D^Blob,
 
mu_b::=  map [b:Blob]( (>*<)[c:b/par](Union {y:c||mu_a(y)})),
 
	|-(HM1):for all b (if b/par={b} then mu(x)=Union subblob(b)),
	()|-(HM2):  for all a:atomic_blobs(mu_b(a)=mu_a(a)),
 
Mu_e::@(img(mu_b), img(mu_b)),
Mu_e::=  rel[X,Y](for some x,y(x Edges y and X=mu_b(x) and Y=mu_b(y) )).
 
}=::Higraph_model.
 
.Quote Copyright.
The original was copyrighted by the ACM, However they give permission to copy
all or part without fee provided that the copies are not made or distributed
for direct commercial advantage, and the title and this copywrite notice
appear. ( Copyright 1988 ACM 0001-0782	88/0500-0514 $1.50)
.Close Harel Higraphs
.Close Graphs