[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_22_graphs
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun Oct 2 12:06:23 PDT 2011



      What are graphs and digraphs

      If you draw some things and connect them with arrows then you have got a directed graph or digraph. Leave off the arrow heads and it is a graph! You can also have the traditional "graph of a function" that uses two axes and dots to connect points on the axes.

      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 modeling points in a plane by two numbers. Each pair of numbers was shown as a point. A set of pairs of numbers defined a figure. A function defined a curve -- the graph of the function.

      In the 19th and 20th centuries these ideas were made more general and abstract as directed graphs(Digraph): a set of things some of which are connected in pairs.

      Wolfram associates have a good, short, visual introduction [ Graph.html ] to the many types of graphs and digraphs.

      Digraphs are abstracted from diagrams. Diagrams are used to help people understand software. A diagram is a digraph with labelled and/or iconic nodes and arcs plus a tidy layout. Thus digraphs underlie a lot of software (and hardware) designs.

      Graphs are nearly always best drawn by humans. The algorithms for drawing digraphs are often ineffective because layout is an aesthetic problem. There several sites dedicated to algorithms for laying out graphs: [click here [socket symbol] if you can fill this hole]

      There are is a special problems for using digraphs in an ASCII based language like MATHS. Finding a short and easy to read notation is tackled in these notes. Alternately one of the new GXL markup languages might be used.

      Graph eXchange Language

      We now (2001) have a standard way to encode digraphs derived from the XML:
    1. GXL::= See http://www.gupro.de/GXL/, Graphical Interchange language.
    2. GXL.dtd::= See http://www.gupro.de/GXL/gxl.dtd.



        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, 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. finite_sets stands for a finite subset of some given generic type.

        Table of Digraph Definitions

        If you browser does not handle tables see [ math_22_Graphs.notable.html ]
        Berge DIGRAPH Net{Nodes:Set, Γ:(@Nodes)^(Nodes|@Nodes)}
        Harary & Norman & Cartwrite NET Net{X,V:Set, first,second:X->V, arc:= (first,second), loop:= arc&Id(V)}
        '' RELATION NET with arc in X(0..1)-(1)V
        '' DIGRAPH RELATION with 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}

        (Close Table)

        My Definition of a Directed Graph

      1. digraph::= $ DIGRAPH.
      2. DIGRAPH::=
        1. Nodes::Sets,
        2. Arcs::@(Nodes><Nodes). -- Arcs act as a relation between Nodes.

        3. ARC::= Net{1st,2nd:Nodes}.
        4. (above)|- (DG1): Arcs in @ARC.
        5. (DG1)|- (DG2): PARALLEL(Arcs, Nodes). -- So that we can use the relation to define paths simply. If a Arcs is treated as a parallel operator then if (a,b,c) is a sequence of Nodes then
        6. Arcs(a,b,c) = a Arcs b Arcs c = (a Arcs b) and (b Arcs c).

          To see an explanation of the general form see

        7. PARALLEL::= See http://cse.csusb.edu/dick/maths/notn_12_Expressions.html#Parallel Operators and [ Parallelism in math_11_STANDARD ]
        8. paths::= {x:#Nodes|| Arcs(x)},

          The definitions of paths above uses DG2 -- the parallelism of Arcs:

        9. (DG2)|- (DG3): for all x:paths, i:1..(|x|-1) ((x[i],x[i+1]) in Arcs.

          So for example if (a, b, c) is in paths then a,b, and c are in Nodes and

          1. (a,b) in Arcs
          2. (b,c) in Arcs

          The idea of paths and trajectories can be defined in the calculus of relations: [ paths in logic_41_HomogenRelations ]

          Note that just listing a set of paths does not completely define all digraphs. Some nodes may be isolated and not be in any paths/arcs. It is also shorter to show cycles like this: circlet(alph, beta, gamma) rather than pathlet(alph, beta, gamma, alph). See Presentations below.

        10. cycles::= {x:paths||(x[|x|]=x[1]}.
        11. loops::= {x:cycles|| |x|]=2}.

          Notice that

        12. no loops =this digraph has no arcs from a node to itself.

          Given a node there is a set of arcs that point at it -- in and a set of arcs that come out of it.

        13. in::Nodes->@Arcs= map [n] (Arcs;{n}),
        14. (def)|- (DG4): for all n, in(n)={(i,n)||for some (i,n) in Arcs}.
        15. nodes_in:: Nodes->@Nodes= map [n]({i||for some (i,n) in Arcs}).
        16. nodes_in:: @Nodes->@Nodes= map [N] (|[n:N]nodes_in(n)).

        17. out:: Nodes->@Arcs= map [n] ({n};Arcs),
        18. (def)|- (DG5): for n, out(n)={(n,o)||for some (n,o) in Arcs}.
        19. nodes_out:: Nodes->@Nodes= map [n] ({o||for some (n,o) in Arcs}).
        20. nodes_out::@Nodes->@Nodes= map [N](|[n:N]nodes_out(n)).

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

        24. ARROW::= Net{from, to:Nodes},
        25. Arrows::@$ ARROWS.
        26. |- (DG8): Arcs={(from,to):Nodes><Nodes | $(ARROW) in Arrows}.
        27. (DG8)|- (DG9): Arrows={$(ARROW)||(from, to) in Arcs}.

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

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

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

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

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

        39. strongly_connected_components::= Nodes/connected_with.

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

        42. |- (DG13): weakly_connected_to in equivalence_relation(Nodes).
        43. connected_components::= Nodes/connected_to.

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



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


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


      6. DIGRAPH_MORPHISMS::=DIGRAPH with following,
          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]


          In Mathematics Presenations are simple ways of expressing complex algebras, For example presenting a group by giving a few expressions that are equal rather than listing all the combinations of all the values. The following allows a digraph to be presented/described succintly as a combination of paths, cycles, and isolated nodes.

          Combining Digraphs

          Given two digraphs we can form their union and intersection:

        1. For G1, G2: digraph, G1 | G2:: digraph = $ DIGRAPH(Nodes=> G1.Nodes | G2.Nodes, Arcs=> G1.Arcs | G2. Arcs ).

        2. For G1, G2: digraph, G1 & G2:: digraph = $ DIGRAPH(Nodes=> G1.Nodes & G2.Nodes, Arcs=> G1.Arcs & G2. Arcs ).

        3. For G1, G2: digraph, G1 ~ G2:: digraph = $ DIGRAPH(Nodes=> G1.Nodes ~ G2.Nodes, Arcs=> G1.Arcs ~ G2. Arcs ).

          Warning: the above operations are not products or coproducts in the category of digraphs and morphisms.

          We can use the above to describe, simply, digraphs in terms of the paths and cycles that make them up. For example:

        4. p1=pathlet((dick, meg, johnr)).
        5. p2=pathlet((dick, frank, johnb)).
        6. my_ancestor_tree= p1|p2.

        7. Pentangle::= circlet(1,2,3,4,5) | circlet(1,3,5,2,4).

          It is a fairly easy exercise to prove that:

          1. Any finite graph has at least on presentation as the union of pathlets, circlets, and nodes.
          2. Any such Presentation has precisely one (minimal) graph.

          Isolated Nodes

        8. For S:Sets, n:#S, nodes(n)::= $ GRAPH(Nodes=>img(n), Arcs={}).


        9. PATHLET::=

          1. |- (P0): DIGRAPH and connected,
          2. |- (P1): Arcs in (1)-(0..1).
          3. |- (P2): Nodes in finite_set.
          4. |- (P3): for one e:Nodes, out(e) = {}.
          5. (P3)|-end:=the e:Nodes(out(e) = {}).
          6. (P1, P3)|- (P4): For n:Nodes~{end}, one out(e).
          7. (P1, P3, P2)|- (P5): for one n:Nodes~{end}, no in(n).
          8. start::=the n:Nodes~{end}(no in(n)).

        10. pathlet::= $ PATHLET.
        11. For S:Sets, p:#S, pathlet(s)::= $ PATHLET(Nodes=>img(s), paths={s}).


        12. CIRCLET::=

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

        13. circlet::= $ CIRCLET.
        14. For S:Sets, p:#S, circlet(s)::= $ CIRCLET(Nodes=>img(s), cycles={s}).

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


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

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


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

        4. ORIENTED_TREE::=following
            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, 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])

          (End of Net ORIENTED_TREE)

          Also see [ PART_WHOLE in math_21_Order ]

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

        Directed Acyclic Graphs(DAGs)

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

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

      Labelled Digraphs

        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.

    4. labeled_digraph::= $ LABELLED_DIGRAPH.
    5. labeled_dag::= $ LABELLED_DIGRAPH and cycle={}.

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


      Derivation Digraphs

      I used the following system to model set of interelated steps in a MATHS proof.
    7. DERIVATION::=
      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) = "".


      Undirected Graphs

      A set of things connected by lines (no arrowheads) is an undirected graph or graph. The things are called nodes or vertices. The connections are called edges.

      Any homogeneous relation defines a graph. Any graph defines a homogenenous relation. [ logic_41_HomogenRelations.html ]

    8. GRAPH::=following,
        A simple definition is a set plus a set of edges. Each edge is an unordered pair -- a set with to nodes.
      1. Set:Sets.
      2. Nodes::=Set.
      3. Edges::@Sets.
      4. |- (G1): For all e:Edges, |e| = 2.
      5. complete::@= ( |(Edges) = Set ).
      6. edge_connected::@(Edges, Edges)= rel[e,f]( e&f<>{})

        Every GRAPH is automatically a symmetric DIGRAPH:

      7. Arcs::@(Set><Set)={ (x,y). {x,y} in Edges }.
      8. (above)|-DIGRAPH(Nodes, Arcs).

        This includes all the definitions of paths, edges, connect_to, strongly_connected, and so on as part of GRAPH.

      (End of Net GRAPH)

      Notice that for each DIGRAPH there is a corresponding GRAPH defined by
    9. For d:digraph, graph(d)::= $ GRAPH(d.Nodes, Edges=> {{x,y}. (x,y) in d.Arcs and x<>y }).


      Hypergraphs are a natural extension of graphs. There is a set of nodes and a set of sets of nodes. Here the graph is drawn as a set of points and the edges are overlapping boundaries around sets of points. A modern variation are Harel's Higraphs below(HIGRAPH).

      The following is based on Berge's book on Graphs and Hyoergraphs:

    10. HYPERGRAPH::=following
      1. Set:Sets.
      2. Nodes::=Set.
      3. Edges::@Sets
      4. |- (H1): For no e:Edges, e={}.
      5. |- (H2): |(Edges) = Set.
      6. directly_connected::@(Set, Set)= rel[x,y]( for some e:Edges({x,y}==>e)).
      7. connected::=do(directly_connected).
      8. edge_connected::@(Edges, Edges)= rel[e,f]( e&f<>{})

      9. n.Edge::= {e: Edges. |e| = n }.
      10. Loops::=1.Edge.
      11. Edges = |[ n:1.. ]( n.Edge ).

      (End of Net HYPERGRAPH)

      Notice that all complete GRAPHs are HYPERGRAPHS:

    11. (above)|-if GRAPH with complete then HYPERGRAPH.

      Bayesian 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

      1. Distinctions::Sets=given.
      2. Variable::=Distinctions.
      3. Probabilities::=Real [0..1].
      4. Node_labels::=Distinctions.

        The arcs indicate conditional dependencies between random variables.

      5. Arc_labels::=Conditional_Probabillity_Tables.
      6. |- (BN0): LABELLED_DIGRAPH.
      7. |- (BN1): cycle={}.

        conditional_probability_table -- shows for each combination of the values of the labels on the Nodes_in the probability of the Node's variable's distribution.

        [ math_81_Probabillity.html ]

    13. BBN::=BAYESIAN_NETWORK, "Bayesian Belief Network".


      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.

        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.


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


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


      1. HIGRAPH::=following
        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}

        (End of Net 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::=
          [ 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) )).


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


  1. do::=transitive closure of a relation, [ do in logic_41_HomogenRelations ]

    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

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


  3. 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).
  4. given::reason="I've been told that...", used to describe a problem.
  5. given::variable="I'll be given a value or object like this...", used to describe a problem.
  6. goal::theorem="The result I'm trying to prove right now".
  7. goal::variable="The value or object I'm trying to find or construct".
  8. 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.
  9. hyp::reason="I assumed this in my last Let/Case/Po/...".
  10. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  11. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  12. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.