[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_22_Graphs.notable
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun Oct 2 12:05:30 PDT 2011

Contents


    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 [ math_22_graphs.html ] if your browser can handle tables. Its more readable and has fewer errors and more links...

    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.

      Digraphs

        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. Also the term finite_sets indicates a finite subset of some given type.

          Table of Digraph Definitions

           From	Name        Synopsis,
           ---------------------------------------------------
          
          
           Berge
          		DIGRAPH
          				Net{Nodes:Set, \Gamma:(@Nodes)^(Nodes|@Nodes)}
          
          
           Harary & Norman & Cartwrite
           		NET
          				Net{X,V::Set, first,second::X->V,
          				 arc::=  (first,second), loop::=  arc&Id(V)}
              ''	RELATION
          				Net{NET, arc in X(0..1)-(1)V}
              ''	DIGRAPH
          				Net{RELATION, loop=0}
          
          
           Birkhoff&Bartee
          		GRAPH
          				Net{N,A:Set, phi:A->(N><N)}
          
          
           Manna	GRAPH
          				Net{V:finite_set, L:set, A:@(V><L><V)}
          
          
           Harary	GRAPH
          				Net{V:Set, X:@V,  for all x:X(|x|=2)}
          
          
           Berge	p-GRAPH
          				Net{p:Nat1, S:Set, n:S^2->0..p}
          
          
           Wilson	GRAPH
          				Net{V,E:finite_set, E:(V^2)->Nat0}
              ''	DIGRAPH
          				Net{V,E:finite_set, E:@(V^(2bag??))}
              ''	SIMPLE_GRAPH
          				Net{V,E, E:@(V^2)}
          
          
           Carre	Graphs_&_Networks
          				Net{X:finite_set, U:@(X^2)}
          
          
           Dossey, Otto, Spence, VanDen Eynden
              ''	directed_graph
          				Net{V:finite_sets, E:@(V^2)&finite_set}
           ---------------------------------------------------

          Definition of a Directed Graph

        1. digraph::= $ DIGRAPH.
        2. DIGRAPH::=
          Net{
          1. Nodes::Sets,
          2. Arcs::@(Nodes><Nodes). -- Arcs act as a relation between Nodes. ARC:= Net{1st,2nd:Nodes}.
          3. (def)|- (DG1): Arcs in @ARC.
          4. (def)|- (DG2): PARALLEL(Arcs, Nodes). -- So that we can use the relation to define paths etc naturally. [ Parallel Operators in notn_12_Expressions ] and [ Parallelism in math_11_STANDARD ]
          5. paths::= {x:#Nodes|| Arcs(x)},
          6. (def)|- (DG3): for all x:paths, i:1..(|x|-1) ((x[i],x[i+1]) in Arcs.
          7. cycles::= {x:paths||(x[|x|]=x[1]}.
          8. loops::= {x:cycles|| |x|]=2}.

          9. in::Nodes->@Arcs= map [n] (Arcs;{n}),
          10. (def)|- (DG4): for all n, in(n)={(i,n)||for some (i,n) in Arcs}.
          11. nodes_in:: Nodes->@Nodes= map [n]({i||for some (i,n) in Arcs}).
          12. nodes_in:: @Nodes->@Nodes= map [N] (|[n:N]nodes_in(n)).

          13. out:: Nodes->@Arcs= map [n] ({n};Arcs),
          14. (def)|- (DG5): for n, out(n)={(n,o)||for some (n,o) in Arcs}.
          15. nodes_out:: Nodes->@Nodes= map [n] ({o||for some (n,o) in Arcs}).
          16. nodes_out::@Nodes->@Nodes= map [N](|[n:N]nodes_out(n)).

          17. Γ::(@Nodes)^Nodes,
          18. |- (DG6): For all x,y:Nodes><Nodes, (x,y) in Arcs iff x in Γ(y).
          19. (DG6)|- (DG7): Γ=nodes_out.

          20. ARROW::= Net{from, to:Nodes},
          21. Arrows::@$ ARROWS.
          22. |- (DG8): Arcs={(from,to):Nodes><Nodes | $(ARROW) in Arrows}.
          23. (DG8)|- (DG9): Arrows={$(ARROW)||(from, to) in Arcs}.

          24. edges::= { {x,y}:@Nodes||(x,y):Arcs}.
          25. semipaths::= {p:#edges||for i:1..|p|-1(p[i]&p[i+1]<>0)}.
          26. semicycles::= {p:semipaths||p[1]=p[|p|]}.
          27. simple::= {p:#Nodes || p in dom(p)(0..1)-(1) p}.

          28. For p1,p2, p1...p2::= {p:path || p1=p[1] and p2=p[|p|]}.

          29. For p1,p2, p1 connected_to p2::= for some p:p1...p2().
          30. |- (DG10): connected_to in Transitive(Nodes) & Reflexive(Nodes).
          31. |- (DG11): ORDER(Set=>Nodes, relation=>connected_to).

          32. strongly_connected::= for all p1,p2 ( p1 connected_to p2).

          33. For p1,p2, p1 connected_with p2::= p1 connected_to p2 or p2 connected_to p1.
          34. |- (DG12): connected_with in equivalence_relation(Nodes).

          35. strongly_connected_components::= Nodes/connected_with.

          36. weakly_connected_to::= rel [p1,p2]( some p:semipath(p1=p[1] and p2=p[|p|])).
          37. weakly_connected::= for all p1,p2, (p1 weakly_connected_to p2).


          38. |- (DG13): weakly_connected_to in equivalence_relation(Nodes).
          39. connected_components::= Nodes/connected_to.


          40. |- (DG14): for all C:connected_components((Nodes=>C, Arcs=>Arcs&@(C,C)) in weakly_connected).
          41. roots::= {r:Nodes||for all x:Nodes(r connected_to x and for no x:Nodes(x connected_to r)}.


          }=::DIGRAPH.

          Subgraphs

        3. For G:digraph, A:@G.Nodes, G.sub_graph(A)::= the $ DIGRAPH(Nodes=>A, Arcs=>G.Arcs&@(G.A,G.A)).
        4. SUBGRAPH::=
          Net{
          1. DIGRAPH(Nodes=>X, Arcs=>A),
          2. DIGRAPH(Nodes=>Y, Arcs=>B),
          3. |- (S1): X==>Y,
          4. |- (S2): A==>B.

          }=::SUBGRAPH.

        5. For D1,D2:$ DIGRAPH, D1 sub_graph D2::= SUBGRAPH( X=>D1.Nodes, Y=>D2.Nodes, A=>D1.Arcs, B=>D2.Arcs).

          Digraph_morphisms

        6. DIGRAPH_MORPHISMS::=DIGRAPH with following,
          Net

            Arrows are defined as part of the STANDARD definitions of MATHS [ math_11_STANDARD.html ]

          1. 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},
          2. 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}.

          (End of Net DIGRAPH_MORPHISMS)

          All digraphs are epimorphic to a digraph with strongly connect components as nodes.

        7. |- (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:

        8. |- (DM2): For all D1,D2:$ DIGRAPH, D1 sub_graph D2 iff Id in (digraph)D1 ==>D2.

          Connonical expansion

        9. |- (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, ... [click here [socket symbol] if you can fill this hole]

          Circlets

        10. CIRCLET::=
          Net{

          1. |- (C0): DIGRAPH and connected,
          2. |- (C1): Arcs in (1)-(1).
          3. |- (C2): Nodes in finite_set.
          4. (C1, C2)|- (C3): for r=|Nodes|, all s,t:Nodes, one d:Int, all n:Nat0({s} = nodes_out^(d + n * r)(t)>>.

          }=::CIRCLET.
        11. circlet::= $ CIRCLET.

          n-Paths

        12. For G:$ DIGRAPH Paths[n](G) ::= (digraph)(1..n, .+1)->G,
        13. Paths(G)::= Union{Paths[n](G)||n:Nat}, Cycles[n](G) ::= (digraph)(0..n-1, .+1 mod n)->G,


        14. |-Strings(Paths(G),(!), ()),

          Trees

          1. FREETREE::= DIGRAPH and weakly_connected and semicycles={}.
          2. tree::= FREETREE and |roots|=1.

          3. ORIENTED_TREE::=
            Net{
              Compare Knuth Vol 1, 2.3.4.,

              Source: Knuth 69, Donald Knuth, "Art of Computer Programming". (Nodes=>S, arcs=>E, Γ=>parents) ::digraph,

            1. r::S= The root of the tree,
            2. |- (OT0): parents(r)={},
            3. |- (OT1): for all v:S~{r}( |parents(v)|=1 and v...r),
            4. children::=fun[v:S]{v':S || v in parents(v'))}
            5. (above)|- (OT2): for all v, one v...r,
            6. (above, cycles)|- (OT3): cycles=0,

              Keonig's Infinity Lemma

              Source: Knuth 69,Vol 1, 2.3.4.3 Theorem K.

            7. (above)|- (OTK): if for all v(children(v) in finite(S)) and not S in Finite then some μ:Nat-->S, all i:Nat(mu[i+1] in children(μ[i])

            }=::ORIENTED_TREE.

            Also see [ PART_WHOLE in math_21_Order ]

          . . . . . . . . . ( end of section Trees) <<Contents | End>>

          Directed Acyclic Graphs(DAGs)

        15. DAG::= DIGRAPH and cycle={}.
        16. dag::= $ DAG. Gelernter[91] uses the name Trellis for a system where data flows define a DAG.

        . . . . . . . . . ( end of section Digraphs) <<Contents | End>>

        Labelled Digraphs

      1. 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.
        1. Node_labels::Sets,
        2. Arc_labels::Sets,
        3. label::Node_labels^Nodes | Arc_labels^Arcs,
        4. node_label::Nodes;label,
        5. arc_label::Arcs;label.

        (End of Net LABELLED_DIGRAPH.)

      2. labeled_digraph::= $ LABELLED_DIGRAPH.
      3. labeled_dag::= $ LABELLED_DIGRAPH and cycle={}.

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

        9. For Nodes x,y, Arc_labels a, x-a->y::@= ((x Arcs y) and a in label(x,y)).
        10. 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.
      5. DERIVATION::=
        Net{
        1. Label::Sets.
        2. Object::Sets.
        3. Node_labels::=Label><Object.
        4. |- (De0): LABELLED_DIGRAPH.
        5. |- (De1): cycle={}.
        6. |- (De2): For all n:Nodes, a,b:in(n)( arc_label(a)=arc_label(b) ).

        7. 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

      6. BAYESIAN_NETWORK::=
        Net{
        1. Distinctions::Sets.
        2. Probabilities::=Real [0..1].
        3. Node_labels::=Distinctions.
        4. Arc_labels::=Probabillities.
        5. |- (BN0): LABELLED_DIGRAPH.
        6. |- (BN1): cycle={}. [ 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.

      7. 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.

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


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


        5. (above)|- (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.

        6. 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:

        7. |- (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:

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


        }=::CATEGORY.

      8. For the mathematical theory see [ math_25_Categories.html ]

        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

        1. HIGRAPH::=
          Net{
          1. Blobs::Finite_set,
          2. subblob::(@Blobs)^Blobs,
          3. For a,b:Blobs, a in subblob(b)::=a is drawn inside b,
          4. par::(@(Blobs,Blobs))^Blobs,
          5. For a,b,c:Blobs, a(b.par)c ::=`a and c are in the same orthogonal components of b`,
          6. Edges::@(Blobs,Blobs),
          7. 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.

          8. inside::= {(u,v):Blobs^2|| u in subblob(v)},

          9. is_part_of::= (inside; do(inside)),
          10. parts::= map [x:Blobs]({y:Blobs||y is_part_of x},


            (HG0): For no x:Blobs (x is_part_of x ),

          11. |- (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)),
          12. atomic_blobs::= {x:B || subblob(x)=0}

          }=::higraph.

          Semantics of Higraphs

          Semantics are decribed by giving a structure preserving maps(μ_a,μ_b,...) from the syntatic terms into expressions in logic and set theory.

        2. For S,T:Sets, S(>*<)T::Sets= the unordered Cartesian product of S and T
        3. For S,T:Sets, S(>*<)T::Sets= {{s,t}||s in S and t in T}.

        4. Higraph_model::=
          Net{
            [ higraph] .
          1. D::Set=unstructured_elements,

          2. mu_a::@D^atomic_blobs,


          3. |- (HM0): for all x,y:atomic_blobs(if x<>y then mu_a(x) & mu_a(y)=0),
          4. mu_b::@D^Blob,

          5. mu_b::= map [b:Blob]( (>*<)[c:b/par](Union {y:c||mu_a(y)})),


          6. |- (HM1): for all b (if b/par={b} then mu(x)=Union subblob(b)),
          7. (above)|- (HM2): for all a:atomic_blobs(mu_b(a)=mu_a(a)),

          8. Mu_e::@(img(mu_b), img(mu_b)),
          9. 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)

        . . . . . . . . . ( end of section Harel Higraphs) <<Contents | End>>

      . . . . . . . . . ( end of section Graphs) <<Contents | End>>

      Notes on MATHS Notation

      Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

      Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

      The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

      For a complete listing of pages in this part of my site by topic see [ home.html ]

      Notes on the Underlying Logic of MATHS

      The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

      For a more rigorous description of the standard notations see

    1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

      Glossary

    2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
    3. given::reason="I've been told that...", used to describe a problem.
    4. given::variable="I'll be given a value or object like this...", used to describe a problem.
    5. goal::theorem="The result I'm trying to prove right now".
    6. goal::variable="The value or object I'm trying to find or construct".
    7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
    8. hyp::reason="I assumed this in my last Let/Case/Po/...".
    9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
    10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
    11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

    End