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
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:
- GXL::= See http://www.gupro.de/GXL/,
Graphical Interchange language.
- GXL.dtd::= See http://www.gupro.de/GXL/gxl.dtd.
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.
Table of Digraph Definitions
If you browser does not handle tables see
[ math_22_Graphs.notable.html ]
| From | Name | Synopsis
|
|---|
| 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}
|
My 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}.
- (above)|- (DG1): Arcs in @ARC.
- (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
- 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
- PARALLEL::= See http://csci.csusb.edu/dick/maths/notn_12_Expressions.html#Parallel Operators
and
[ Parallelism in math_11_STANDARD ]
- paths::= {x:#Nodes|| Arcs(x)},
The definitions of paths above uses DG2 -- the parallelism of Arcs:
- (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
- (a,b) in Arcs
- (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.
- cycles::= {x:paths||(x[|x|]=x[1]}.
- loops::= {x:cycles|| |x|]=2}.
Notice that
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.
- 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)).
- Γ::(@Nodes)^Nodes,
- |- (DG6): For all x,y:Nodes><Nodes, (x,y) in Arcs iff x in Γ(y).
- (DG6)|- (DG7): Γ=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::=
- 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
[ 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}.
(End of 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, ...
[click here
if you can fill this hole]
Presentations
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:
- For G1, G2: digraph, G1 | G2:: digraph = $ DIGRAPH(Nodes=> G1.Nodes | G2.Nodes, Arcs=> G1.Arcs | G2. Arcs ).
- For G1, G2: digraph, G1 & G2:: digraph = $ DIGRAPH(Nodes=> G1.Nodes & G2.Nodes, Arcs=> G1.Arcs & G2. Arcs ).
- 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:
- p1=pathlet((dick, meg, johnr)).
- p2=pathlet((dick, frank, johnb)).
- my_ancestor_tree= p1|p2.
- Pentangle::= circlet(1,2,3,4,5) | circlet(1,3,5,2,4).
It is a fairly easy exercise to prove that:
- Any finite graph has at least on presentation as the union of pathlets, circlets, and nodes.
- Any such Presentation has precisely one (minimal) graph.
Isolated Nodes
- For S:Sets, n:#S, nodes(n)::= $ GRAPH(Nodes=>img(n), Arcs={}).
Pathlets
- PATHLET::=
Net{
- |- (P0): DIGRAPH and connected,
- |- (P1): Arcs in (1)-(0..1).
- |- (P2): Nodes in finite_set.
- |- (P3): for one e:Nodes, out(e) = {}.
- (P3)|-end:=the e:Nodes(out(e) = {}).
- (P1, P3)|- (P4): For n:Nodes~{end}, one out(e).
- (P1, P3, P2)|- (P5): for one n:Nodes~{end}, no in(n).
- start::=the n:Nodes~{end}(no in(n)).
}=::
PATHLET.
- pathlet::= $ PATHLET.
- For S:Sets, p:#S, pathlet(s)::= $ PATHLET(Nodes=>img(s), paths={s}).
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.
- For S:Sets, p:#S, circlet(s)::= $ CIRCLET(Nodes=>img(s), cycles={s}).
. . . . . . . . . ( end of section Presentations) <<Contents | End>>
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),(!), ()),
Trees
- FREETREE::= DIGRAPH and weakly_connected and semicycles={}.
- tree::= FREETREE and |roots| =1.
- forest::= FREETREE and |roots| >=1.
- ORIENTED_TREE::=following
Net
Compare Knuth Vol 1, 2.3.4.,
Knuth 69, Donald Knuth, "Art of Computer Programming".
(Nodes=>S, arcs=>E, Γ=>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'))}
- (above)|- (OT2): for all v, one v...r,
- (above, cycles)|- (OT3): cycles=0,
Keonig's Infinity Lemma
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 μ: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)
- DAG::= DIGRAPH and cycle={}.
- 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
- LABELLED_DIGRAPH::= DIGRAPH and
- 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
I used the following system 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= !) ")" the
arc_label(in(n)) "(" 1st o node_label(n) "):" 2nd o node_label(n),
where !) ::= f(a) ! !![x:A] (f(x)) | !![x:A] (f(x)) ! f(a)
and !![x:{}]f(a) = "".
}=::
DERIVATION.
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 ]
- GRAPH::=following,
Net
A simple definition is a set plus a set of edges. Each edge
is an unordered pair -- a set with to nodes.
- Set:Sets.
- Nodes::=Set.
- Edges::@Sets.
- |- (G1): For all e:Edges, |e| = 2.
- complete::@= ( |(Edges) = Set ).
- edge_connected::@(Edges, Edges)= rel[e,f]( e&f<>{})
Every GRAPH is automatically a symmetric DIGRAPH:
- Arcs::@(Set><Set)={ (x,y). {x,y} in Edges }.
- (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
- For d:digraph, graph(d)::= $ GRAPH(d.Nodes, Edges=> {{x,y}. (x,y) in d.Arcs and x<>y }).
Hypergraphs
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:
- HYPERGRAPH::=following
Net
Notice that all complete GRAPHs are HYPERGRAPHS:
- (above)|-if GRAPH with complete then HYPERGRAPH.
Bayesian Networks
Causal networks, belief networks, influence diagram...
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::=
- BBN::=BAYESIAN_NETWORK, "Bayesian Belief 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 ).
- (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.
- 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
[ 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
- HIGRAPH::=following
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}
(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.
- 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{
[ 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)),
- (above)|- (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)
. . . . . . . . . ( end of section Harel Higraphs) <<Contents | End>>
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 = Net{radius:Positive Real, center:Point}.
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