.Open Dynamics
. Introduction
Changes can be described as a before-after relationship.
In other words by a relation between prior and later states.
The calculus of relations, therefore, gives a structured way to describe 
dynamics - sequences (;), selections (|), and repetition (do).   Special 
operators define a common serial interface.  Intersection and complement 
operations on relations define a less useful(?) form of concurrency. The 
elementary expressions are predicates with dynamic variables: a prime("'")
indicates the new values of those variables that are expected to change 
(dynamic variables) with others being unchanged (static variables).

Simple Case - one component or variable can change.
	$ Net{S,W(x',x,y,z)}::=  rel [s1,s2:$ $S](s1.z=s2.z and s2.y=s1.y and W(s2.x, s1.x, s2.y, s2.z) )
.Open Examples of simple changes
	  $ Net{ x,y,z:Int, x'=y+1} =  rel [s1,s2:$ Net{x,y,z:Int}](s2.z=s1.z and s2.y=s1.y and  s2.x=s2.y+1)
	  $ Net{ x,y,z:Int, x'=x+y } =  rel [s1,s2:$ Net{x,y,z:Int}] (s2.z=s1.z and s2.y=s1.y and s2.x=s1.x+s2.y)
.Close Examples of simple changes
In general a dynamic predicate contains one or more variables that end with
apostrophes. These variables are called the dynamic variables, and the 
others are called the static variables.  For example in
	           $ Net{ x,y,z:T, x'=y and y'=x}
we have
		Dynamic variables ={`x`, `y`},
	 and
		 Static variables ={`z`}
so
	 $ Net{ x,y,z:T, x'=y and y'=x) = rel [s1,s2:$ Net{x,y,z:T}](s2.z=s1.z and  s2.x=s1.y and s2.y=s1.x)

A more general form is:
$ Net{S, W(x1', x2',...,  x1, x2,..., z1, z2,...))}  ::=   rel [s1,s2:$ $S] (s2.(z1, z2,..)=s1.(z1, z2,...) and W(s2.x1, s2.x2, ..., s1.x1, s1.x2, ..., s2.z1, s2.z2,...)
where S is any documentation defining the state space.

If there are several assertions they are equivalent to their conjunction:
	$ Net{x,y:Real, x'=y, y'=x}=$ Net{x,y:Real, x'=y and y'=x}.

Notice that if a predicate appears that has no dynamic variables then it 
specifies a condition - something that must be true for the process to 
complete successfully.


If a record (in a database, program, object, etc) is described by 
documentation `Net{D}` and `w` is a dynamic predicate in the variables of 
`D` then
	update::=$ Net{D, w}
defines a change to a record with structure documented by `D`. So ` x 
update x' ` specifies a change to record `x`.

For example, given
	enrollments::= $ $ENROLLMENT, 
	ENROLLMENT::=Net{ student:students, class:classes, grade:grades},

then
	For s:students, c:classes, g:grades, `change grade of s in c to g `::=$ Net{ENROLLMENT, student=s, class=c, grade'=g},
and

	For a,d:classes, `student s adds a drops d`::=$ Net{ENROLLMENT,  student=s, class=d, class'=a }.

If a record (in a database, program, object, etc) is described by named 
documentation `N=Net{D}` then`N'` (N-prime) stands for network with the same 
variables as N, but with he variables in its wffs decorated by a prime[ as in 
Z]. For example
Example_of_prime_in_action::=Net{
students::=PERSON->STUDENT,
STUDENT::=following,
.Net 
   person::people.
   class_level::FR|SO|JR|SR,
   units::Real,
   GPA::Real.
 |-(inv): class_level=FR iff units<25.00,...
.Close.Net
then
|- STUDENT'=following
.Net
   person::people.
   class_level::FR|SO|JR|SR,
   units::Real,
   GPA::Real.
   |-(inv): class_level'=FR iff units'<25.00,...
.Close.Net
Notice that the primes are not placed on the declarations.  Thus
\Delta_STUDENT::=Net{ |-$STUDENT. |-$STUDENT'.}
means the same as writing
\Delta_STUDENT::=following,
.Net
   person::people.
   class_level::FR|SO|JR|SR,
   units::Real,
   GPA::Real.
 |-  class_level=FR iff units<25.00,...
 |-  class_level'=FR iff units'<25.00,...
.Close.Net
By the way the effect of a duplicate label on a statement is merely make it ambiguous and so invisible to the outside world.  Labels do not change the meanings - they make it easier for simple markup system to do part of the work of making formal documentation look good.  Notice that when combining two schema like
this duplicate labels are hidden.

Putting these above rules to work we can document the end of quarter update to an enrolment as
 For s:students, c:classes,g:{A,B,C,D,F}, finish_class(s, c, g) ::=$ following,
.Net
 |- $STUDENT. 
 |- $STUDENT'.
|-(gpa):   units'*GPA'=units*GPA+g.(A+>4 | B+>3 | C+>2 | D+>1 | else+>0 ),
|-(units):   units'=units+units(c)
.Close.Net finish_class
The occurence of `STUDENT` and `STUDENT'` in the above definition declares
the variables { person, class_level, units,  GPA} and also enforces the 
formula `class_level=FR iff units<25.00,...` before and `class_level'=FR 
iff units'<25.00,...`

}=::Example_of_prime_in_action.

In general the effect of 
	\Delta_D::=$ following,
.Net
 |-D.
 |-D'.
.Close.Net 
is to assert that the constraint in D must be invariant under any change that uses \Delta_D, or just has `D, D'` in it.  Hence (like Z), for a piece of documentation `D` with name `N` we can define
	\Delta(N) ::= N with N'.
Similarly, the need for a set of variable to remain constant can be documented by:
	\Xi(N) ::=\Delta(N) and for  v:variables(N)(v=v').


. Conveniences
It is usually convenient to omit the types of the variables when dynamic 
predicates appear in a relational expression. In this case the the 
predicate inherits the previous state space.  Further, the dollars and 
braces can be ommitted without ambiguity.

	If	Example=(y:Int;  y'=x; do(y>3; y'=y-3);y<=3)
	then
 	Example	=$ Net{y:Int}; $ Net{y'=x};do($ Net{y>0}; $ Net{y'=y-3};$ Net{y<=0}
		=$ Net{y::Int,y'=x};do($ Net{y:Int, y>0}; $ Net{y:Int,  y'=y-3};$ Net{y:Int, y<=0}.

. Dynamic Sets and Maps
The same prime notation can be used to indicate changes in sets and maps.  Large numbers
of real systems the state of the system is described by sets of objects and/or maps
between objects.  These are often implemented using data bases and/or object-oriented
technologies.  The system can change because an object has moved from one set to another.
For example a student `s` graduates and so moves from `Undergraduate` to `Alumnus`:
	Undergraduate' = Undergraduate ~ s and Alumnus'=Alumnus|s.

. Dynamic Relations
Data Base changes often involve adding and removing rows in tables.  These are
also sets.  The 
.See Dynamic Set
notation can also be used.

. Dynamic Maps
Similarly, if we have a map we can add a new `maplet`
	f' = f | (x+>e),
or remove one (creating a partial map):
	f' = f ~ (x+>f(x)),
or do both:
	f' = f ~ (x+>f(x))|(x+>e).

This last operation is common enough to give rise to a special notation
	f(x):=e.

Another, similar notation, indicates a change in the value of one element of a map.
Since
	f.(x:=e) = f ~ (x+>f(x))|(x+>e),
we can show the change
	f' = f.(x:=e).

In the above the map or function `f` is acting like
.Key Random Access Memory
with `x` as an address and `e` as an expression indicatng the new value stored in a location.

In all the above, if `y` is not `x` then `f'(y) = f(y)` -- only one element changes.

However, the notation
	f(x)' = e,
does not say that a single element of `f` is changing.  It also permits any other
element/item to change as well!  THis notation should be avoided.

.Open Calculations
There is a calculus of programs!  Here is a taster:

. Problem
Given N1 and N2 are Dynamic - calculate $ $N1;$ $N2.
. Algorithm

Suppose   $ $N3= $ $N1; $ $N2  then   N3 is found by
.List
	Add assertions of form v=v'' for all variables v that are not dynamic in N1 or N2.
	Add an apostrophe to all variables in N2.
	Combine all declarations and definitions.
	If a variable appears with one apostrophe but not with two then add an apostrophe to it
	Apply existential quantifier to all variables with a single  apostrophe.
	Change single prime variables to other names, and hide them
	Replace double primes by primes.
	Simplify and remove redundant invariant assertions
.Close. List
. Example Calcuations
()|-(ex1): (x'=x+1;x'=a*x)=(x'=a*x+a).
. Proof of ex1
Consider{ (x'=x+1;x'=a*x)=
	=(x'=x+1 and (x''=a*x' and  a=a''))
	= (x'=x+1 and x''=a*x' and  a=a'')
	=for some x'(x'=x+1 and x''=a*x' and a=a'')
	=for some w(w=x+1 and x''=a*w and a=a'')
	= for some w(w=x+1 and x'=a*w and a=a')
 (simp)	=for w:=x+1(x'=a*w and a=a')
 (subs)	=( x'=a*(x+1))
 (alg)	=(x'=a*x+a).
}
|- (arith swap): (x'=x-y;y'=x+y;x'=y-x) = (x'=y and y'=x)
. Proof of arith swap
This assumes that the operations of plus and minus etc follow the normal rules of algebra - a group even when overflow occurs.
Consider{ (x'=x-y;y'=x+y;x'=y-x)
	=  $ Net{x'=x-y, y'=y, y''=x'+y', x''=x'};x'=y-x
	=  for some a,b(a=x-y and  b=y and  y''=a+b and  x''=a);x'=y-x
	= ((y''=x-y+y and  x''=x-y);x'=y-x)
	= ((y'=x and  x'=x-y);x'=y-x)
	= (y'=x and  x'=x-y and  y''=y' and  x''=y'-x')
	= (x'=y and y'=x)
}.
()|-(exercise): (x'=x^y;y'=x^y;x'=y^x) = (x'=y and y'=x) where x^y=map[i:bits(x)] (x[i] iff y[i]).
()|- (Shuttle swap): (z'=x; x'=y; y'=z) ==> (x'=y and y'=x)
. Proof of Shuttle swap
Consider{ (z'=x; x'=y; y'=z)
	= ( (z'=x; x'=y); y'=z)
	= ( z'=x and x'=y and y'=y); (y'=z)
	=$ Net{  ( z'=x and x'=y and y'=y) and y''=z' ) }
	=$ Net{  z'=x and x'=y and y'=y and y''=z'  }
			= $ Net{  z'=x and x''=y and y'=y and y''=z'  }
	  		= ( z''=x and x''=y and y'=y and y''=z''=x)
	  		= ( x''=y and y''=z''=x)
	  		= ( x'=y and y'=z'=x)
	  		==> ( x'=y and y'=x)
}.

. Quasi-Normal Form
It is easy to show that any relational expression with no 'do's and made up
of simple dynamic predicates can have its semicolons removed and be reduced
to a non-unique but standard conjunctive form:
Consider{	(x>0; y'=2*x; y<6; x'=y-1)
 		=(x>0;y'=2*x; y<6 and x'=y-1 )
 		=(x>0;y'=2*x and y<6 and x'=2*x-1 )
 		=(x>0 and y'=2*x and y<6 and x'=2*x-1 )
 		=(x>0  and 2*x<6 and y'=2*x and x'=2*x-1 )
 		=(x in [0..3] and y'=2*x and x'=2*x-1 )
 		=(x in [0..3] and (x',y')=(2*x-1, 2*x)).
}.
Consider{	(x<0; x'=-x | x>=0)
 		= (x<0 and x'=-x | x>=0)
 		= (  (x<0 and x'=-x ) or x>=0).
}.
.Close Calculations
.Open Sequential Structures
. Sequence
	R1;R2;R3;...
. Blocks
(block): 	with(D)(R)
. Selections
(sel):	R1|R2|R3|...
(ifthenelse):	C;R1 | (~C);R2
(case):	|[c:cases](R(c))
. Iterations
(iter):	do(R)
(while):	do(C; R);no(C)
(for):	with(i)(i'=a; while(b)(S; c)
(until):	R; do(C; R);no(C)
.Close Sequential Structures

.Open Concurrent Structures
See
.See http://www/dick/maths/math_76_Concurency.html
and
.See http://www.csci.csusb.edu/dick/maths/math_73_Process_algebra.html
for more.

. Data flow Diagrams
DFD::="Data Flow Diagrams".

These are still used by systems analysts even tho'
they are no longer fashionable
.See http://www.csci.csusb.edu/dick/papers/rjb04bDFDs/
and misunderstood.

A combination 
of my Flosets and standard Digraphs can be used to model
systems of communicating parts:
.See http://www.csci.csusb.edu/dick/maths/math_23_Flow_Diagrams.html
without specifying the precise interactions.

.Hole
. Parallel Operations
The intersection of two relations  requires both of them to hold:
	Simultaneous	R1 & R2

Notice that a simple expression can stop the processing
	|-(x'=x+1) & (x'=x-1) = false.

Worse
	|-(x'=x+1) & (y'=y+1) = false.
Because each assignment locks the other variable!  However:
	|-(x'=x+1 and y'=y') & (y'=y+1 and x'=x') = (x'=x+1 and y'=y+1),
and does what was probably wanted.

This motivates the follwoing two abbreviations:
	free(v) ::=(v'=v'),
	lock(v) ::=(v=v'),

.RoadWorksAhead
	wait(v) :=until( v<>v' ) ( free(v) ).

Most intractable problems have a form like this.
.Hole
.Close Concurrent Structures
.Close Dynamics