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) )
- $ 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)
. . . . . . . . . ( end of section Examples of simple changes) <<Contents | End>>
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} thenN' (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
then
- |-STUDENT'=following
Net
Notice that the primes are not placed on the declarations. Thus
- Δ_STUDENT::=Net{ |-STUDENT. |-STUDENT'.}
means the same as writing
- Δ_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,...
(End of 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
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
- Δ_D::=$ following,
Net
is to assert that the constraint in D must be invariant under any change that uses Δ_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)::=Δ(N) and for v:variables(N)(v=v').
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}.
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
[ 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
- Δ_STUDENT.
- ...
- s in Undergraduate.
- Undergraduate:~ s.
- Alumnus:|s.
(End of Net)
where the three dots (...) hide some conditions on the student's record for
graduation.
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
[ Dynamic Sets ]
(above) can be used. Here are a couple samples:
Marriage
- Married' = Married | {(bride, groom)}.
- Married' = Married | bride+>groom.
Divorce
- wife Married husband and Married' = Married ~ (wife, husband) and Divorced' = Divorced | (wife, husband).
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
Random Access Memory
or
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.
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),
[ over_ridden_by in logic_40_Relations ]
Similarly f.(x:=e) is
- f' = if( x in ddef(f), f ~ (x+>f(x))|(x+>e), f | (x+>e) ).
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
Add, Delete, and Update functions
define in
- UDA_WITH_KEY::= See 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.
It is tempting to define a special operator, for example
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.
An
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><T) the operation is to first delete items and then add the
changed ones, or
- S' = { t:T || for some s:S ( (s,t) in U ) }, or equivalently
- S' = S.U, or even
- S:.U.
[ Z-like%20Operators in logic_44_n-aryrelations ]
There is a calculus of programs! Here is a taster:
Given N1 and N2 are Dynamic - calculate $ N1;$ N2.
Suppose $ N3= $ N1; $ N2 then N3 is found by
- 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
- (above)|- (ex1): (x'=x+1;x'=a*x)=(x'=a*x+a).
- 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)
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)
}.
- (above)|- (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]).
- (above)|- (Shuttle swap): (z'=x; x'=y; y'=z) ==> (x'=y and y'=x)
- 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)
}.
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).
}.
. . . . . . . . . ( end of section Calculations) <<Contents | End>>
- R1;R2;R3;...
(block): with(D)(R)
(sel): R1|R2|R3|...
(ifthenelse): C;R1 | (~C);R2
(case): |[c:cases](R(c))
(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)
. . . . . . . . . ( end of section Sequential Structures) <<Contents | End>>
See
[ math_76_Concurency.html ]
and
[ math_73_Process_algebra.html ]
for more.
- DFD::="Data Flow Diagrams".
These are still used by systems analysts even tho'
they are no longer fashionable
[ 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:
[ math_23_Flow_Diagrams.html ]
without specifying the precise interactions.
[click here if you can fill this hole]
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.
[click here if you can fill this hole]
. . . . . . . . . ( end of section Concurrent Structures) <<Contents | End>>