.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 the
Z notation]. 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
.Key Delta
\Delta(N) ::= N with N'.
Similarly, the need for a set of variable to remain constant can be documented by:
.Key Xi
\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
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.
By the way we might wish to add the fact that only Undergraduates can become alumni
s in Undergraduate and Undergraduate' = Undergraduate ~ s and Alumnus'=Alumnus|s.
Using the standard abbreviation
.See ./math_11_STANDARD.html#ASSIGNMENTS
that for any operation `o`, variable `v`, and
expression `e` (of the right types), `v:o e`=`v'= v o e`:
s in Undergraduate and Undergraduate:~ s and Alumnus:|s.
Thus we can write
For s:Person, graduate(s)::=following,
.Net
\Delta_STUDENT.
...
s in Undergraduate.
Undergraduate:~ s.
Alumnus:|s.
.Close.Net
where the three dots (...) hide some conditions on the student's record for
graduation.
. Dynamic Relations
Data Base changes often involve adding and removing rows in tables. The tables
represent relations. Simple relations also can
be treated as sets. The notations for
.See Dynamic Sets
(above) can be used. Here are a couple samples:
.Key Marriage
Married' = Married | {(bride, groom)}.
Married' = Married | bride+>groom.
.Key Divorce
wife Married husband and Married' = Married ~ (wife, husband) and Divorced' = Divorced | (wife, husband).
. Dynamic Maps
Similarly, if we have a partial map with no x defined we can add a new `maplet`
f' = f | (x+>e),
or remove one (turning map into a partial map):
f' = f ~ (x+>f(x)),
But if we start with a map and remove and replace one item:
f' = f ~ (x+>f(x))|(x+>e),
we end up with another map. This is a special case of Relational over riding.
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
or
.Key Array
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.
. Dynamic Partial Maps
These two notations
f(x):=e
f.(x:=e)
are useful when f is a partial map -- even if `x` is not in `ddef(f)`.
The definition,above, of `f(x):=e` has to be changed to allow the creation of new pairs
because we can not remove (x+>f(x)) when `f(x)` does not exist:
f' = if( x in ddef(f), f ~ (x+>f(x))|(x+>e), f | (x+>e) ).
This is actually
f' = f over_ridden_by (x+>e),
.See http://www/dick/maths/logic_40_Relations.html#over_ridden_by
Similarly `f.(x:=e)` is
f' = if( x in ddef(f), f ~ (x+>f(x))|(x+>e), f | (x+>e) ).
. Normalized Data Base Operations
When data in a data base is normalized then every entity is a partial map from
the set of possible prime keys to the other attributes. If
f : @D K->V,
then we can treat it as
f : K<>->V,
and so write (for k:K and e:V),
f(k):=e,
to indicate the creation and/or modification of the relation f.
There are specialized
.Key Add, Delete, and Update functions
define in
UDA_WITH_KEY::=http://cse.csusb.edu/dick/maths/logic_44_n-aryrelations.html#SIMPLE_UDA_WITH_KEY
that can be used to express some common operation succinctly.
. Changing a single attribute in one object of an entity
It is tempting to define a special operator, for example
.As_is f(k).a := e.
to show a change to a single attribute `a` of the object with key `k`
and leaving other objects and attributes untouched.
Unfortunately, some (if not all) entity types in MATHS have internal
constraints that make this guarantee meaning less. For example:
Net{a,b,c:Int. a+b=c},
has the property that changing any one variable forces at least one other
to change.
.Box
An
.Key update operation is best specified
in terms of S being updated by a set
of changes U where each element in U is a pair (an old item, a new item).
So for U:@(T> (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