Examples
Numbers of objects in a part of system per unit time.
Data Types being used in each part of a system.
Frequencies with which something is done.
Number of derivations of a string in a particular grammar.
FLOW::= Net{
Flows can be combined, and the order in which this is done does not effect
the result. There is also a null or zero flow  which has no effect when
combined with any other flow. This set of assumptions is describes an
Abelian Monoid:
Abelian_monoid(Set=>Flows, op=>+, u=>0).
We require that there is at least one nonzero flow  ie at least two:
 Flows>1.
We can recognise when one flow contains another. This can be modelled as
a partially ordered set:
poset(Set=>Flows, order=>(<=), inverse=>(>=), strict=>(<),
strict_inverse=>(>)).
A combined flow is greater than or equal to its parts:
 for all f1,f2:Flows( f1+f2>=f1,f2 ).
One flow is greater than another if and only if the first results by adding
a flow to the second one:
for all f1,f2 ( f1<f2 iff for some f3:Flows( f3<>0 and f1+f3=f2) ).
 for some f(f<>0) and for all f(0+f=f),
 for some f(f<>0 and 0+f=f),
 for some f(0<f),
 some Flows & />(0).
Adding a flow to two flows preserves their order:
for all f1,f2,f3, if f1<f2 then f1+f3<=f2+f3.
 for f1,f2, if f1<f2 then f1<>f2.
 0<=0. Consider{0+0=0}
 for all f:Flows (0<=f). Consider{f, 0+f=f}
 for all f, f<>0(f>0).
 for all f1,f2:Flows, if f1<>0 then f1+f2<>0,
 Po{
 (1): f1,f2:Flows,
 (2): f1<>0,
 (3): f1+f2=0,
 (2)  (4): f1>0,
 (3, 4, >)  (5): f1+f2>0,
  (6): f1+f2>f2,
 (6, 3)  (7): 0>f2,
  (8): 0=f2.
}
 for all f1,f2, if f1+f2=0 then f1=0=f2.
 for no f (f<0),
 Po{
 (1): f<0,
 (1)  (2): f<>0,
 (Monoid)  (3): 0+f=f,
 (<)  (4): 0<f,
 (trans <)  (5): 0<0,
 (strict <)  (6): 0<>0,
}
}=:: FLOW.
floset::=FLOW.
for all POSITIVE_SEMIRING(Set,+.0,.,1,...) (FLOW(Set,+,0))
[MATHS.41 Two Operators.semiring]
({0,1}, {(0,1)+>1, (1,1)+>1,...},0,{(0,0),(0,1),(1,1)})
The above is half of a Boolean algebra.
(Nat0,+,0) in floset.
([0..),+,0) in floset.
These are quantitative flows.
For all S:Sets, (@S,,{},==>) in floset.
This is a qualitive flow.
([0..1],max,0) in floset
A Fuzzy flow.
For all S:Sets, (F,+,0,<=):floset, (S>F, + , [s]0,<=) in floset.
in this case (+)=[x,y:S>F]([s](x(s)+y(s))).
For S:Sets,
Bag(S)::=FLOW(S>Nat0,+, 0).
FuzzySet(S)::=FLOW(S>[0..1], max, 0).
The following could be used in qualitative and quantitative Data Flow
Diagrams
For Data={Customer, Invoice, Invoice_item, Order, Order_item, ...},
((@Data, , {}) in FLOW ).
For all Data:Finite_set,
(Data>Nat0,+,0,<=) in floset.
for all a,b:@Nat0^Data(a < b ::= for all i:Data (a[i] < b[i]) ).
This is a quantitive model.
(Data>@,,{},==>) in floset.
This is a qualitive model.
If these two models describe the same system then there is a homomorphism
from the quantitive model to the qualitive, based on the map
qualify:(Data>Nat0)>(@Data) ::=map[S]0./S,
qualify(S)={d:DataS(d)>0}.
The following example, could be part of a model of Ozone depletion:
For Parts:={Ground, Lower_atmosphere, Upper_atmosphere, ...},
Chemicals:={H2O, CO2, O2, O3, NOn, SOn, C, S, N, ...},
((Real^Chemicals,+,0) in FLOW), ((Real^Chemicals)^Parts,+,0) in FLOW).
The following would be used in parts of D. Knuth's analysis of algorithms:
For Frequencies:=Nat0, ((Frequencies, +, 0) in FLOW ).
In general:
squash(n)::(S>Nat0)>(S>0..n) with addition redefined so that
a*b=min{a+b,n}.
is a homomorphism from a complex model to a simpler one.
.Exercise
Investigate the category of all flosets with homomorphisms that preserve 0,
monoids and order. Are there free flosets (initial obejects) which can be
mapped onto any other floset? Do products and coproducts make sense?
(Hint  monoids have a similar category  but in what sense?)
.Project
Use a floset to model for the numbers of tokens in a Petrie Net, or marked
directed graph. What are the simplest expressions of the firing rules?
. . . . . . . . . ( end of section Flosets) <<Contents  End>>
Informally a flow diagram is a collection of parts that have flows
connecting them.
.Example
Simple assembler program reads lines of source code lines and produces
words of object code.
 .DFD Sample::=( Parts=>{Source, SASS, Object},
 External_entities=>{Source,Object},
 Flow=>{0,lines,words,lines+words},
 lines+lines=lines,
 words+words=words,
)
.Theory
 FFD::=
Net{
 Parts::Sets.
FLOW.
 flows::Flow^(Parts><Parts).
 For f:Flows, p1,p2:Parts, f=flows(p1,p2)::= f flows from p1 to p2or`p1
sends f to p2 or p2 gets f from p1 or p1 gives f to p2 or p2 takes f
from p1`.
 in_arc:: Parts>(Parts^2)= map p:Parts({(i,p) : Parts^2flows(i,p)<>0}).
 out_arc::Parts>(Parts^2)= map p({(p,o)flows(p,o)<>0}).
 effects::@(Parts,Parts)= {(o,i) : Parts^2flow(o,i)<>0)}.
 effected_by::= /effects.
DIGRAPH(Nodes=>Parts, Arcs=>effects).
[ DIGRAPH in math_22_graphs ]
 (acyclic): loops=0.
The abscence of loops is assumed without loss of generallity, because if
there is a need for a flow to return to a node then a new node with a
single input and output is introduced to provide the feedback. In a
hierachical floww diagram a loop is placed within the refinement of the
part.
 sources::@Parts= {p:Partsfor no i:Parts(i effects p)}.
 sinks::@Parts= {p:Partsfor no o:Parts(p effects o)}.
There shouldn't be any completely isolated Parts.
 (no_isolates): no (sources & sinks).
 output::Parts>Flow= map p(+{flow(a)a:outarc(p)}),
output=(Parts>Flow);outarc;flow;+.
 total_output::@Parts>Flow= map[P](+(output(P)).
 input::Parts>Flow= map [p](+{flow(a)a:inarc(p)}),
 total_input::@Parts>Flow= map [P](+(input(P)).
 external_entities::@Parts.
There is a way to document that some of the nodes are outside the system.
 entities::= source  sinks.
 (ent0): entities ==> external_entities.
An external entity can both send and receive flows.
All sources and sinks should be external entities.
 stores::= {p:Parts~ external_entities  output(p) <= input(p)}.
A store is a part that doesn't produces more than it is given.
 processes::= Parts~ (stores  external_entities).
Processes are nodes where more(>) comes out than comes in.
Thus they must change that which is flowing in the network.
 passive_flows::= {(p,q) : Parts^2p effects q not (p in processes or q in
processes)}
  (pass0): passive_flows=effects~ (Parts><processes  processes><Parts),
In several methods passive flows are not permitted.
If something flows then there is a process that moves it.
 filters::= {p:parts one(in_arc(p)) and one(out_arc(p))}.
 conservative_parts::@Parts= {pp.output=p.input},
  (stores_conserve): conservative_parts==>stores,
 Kirchoff_s_Law::@= (Parts=conservative_parts).
}=:: FFD.
 Uses FFD.
 N::= Parts,
 n::Parts1..N,
 table::1..N><1..N >(PartsFlows).
 for p:Parts( table [ n(p),n(p) ] =p),
 for p1,p2:Parts, f=flow(p1,p2) (
 if n(p1) < n(p2) then table [ n(p1), n(p2) ] =f
 or if n(p1) > n(p2) then table [ n(p2), n(p1) ] =f
 )
Example of A Simple Assembler(SASS)
Table of parts

Source line
SASS word
Object
 HIFFD::=
Net{
 Use FFD.
 elements::@processes.
 refined::= processes~ elements.
 processes>=={refined, elements}.
 refinement::refined>HIFFD.
 refinement:processes(0..)(1)HIFFD.
 for all p:refined (refinement(p) fits p).
For r:FFD, p:Parts, r fits p ::@=
( r.external_entities=(r.Parts & Parts)
and r.external_entities=(effects(p) effected_by(p))
and for all i:effects(p)(r.output(i)=flows(i,p))
and for all o:effected_by(p)(r.input(o)=flows(p,o))
)
}=:: HIFFD.
Context DFD

Source line
SASS word
Object
SASS

Source lines lines
Pass1 label+address
Symbol address
label Pass2 word
Object
. . . . . . . . . ( end of section Formal Flow Diagrams) <<Contents  End>>
DFD::= Net{
Process,Entity,Store,Flow,Identifier::Finite_Sets.
 Processes::= Process^PId,  Parts of system which transform data.
 Entities::= Entity^EId,  Source or destination for data outside this
system.
 Stores::= Store^SId,  parts of system which preserve data unchanged.
 Flows::= Data^Fid.
 Identifier::@#Char.
 Identifier>=={NId, Fid}. Identifers identify nodes or flows.
 NId>=={PId, EId, SId}. Nodes are processes, entities, or stores.
 DIGRAPH,
 Nodes>=={ Processes, Entities, Stores }.
 Arc_label::Arcs>Data.
 for all (x,y): Arcs(x in Processes or y in Processes ).
 Either Gane_and_Sarson, SSADM, ... or Shlaer_and_Mellor.
 if Gane_and_Sarson then
 PId=number #("." number)
 and Eid=lower_case_letter
 and SId="D" number #("." number)
 and Fid=NId "" NId.
}=:: DFD.
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_2_Proofs ]
for more on the structure and rules.
The notation also allows you to create a new network of variables
and constraints, and give them a name. 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.
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 complete listing of pages by topic see
[ home.html ]
