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) )

Examples of simple changes

1. $ 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)
2. $ 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

1. $ Net{ x,y,z:T, x'=y and y'=x} we have
2. Dynamic variables ={x, y},
3. and
4. Static variables ={z} so
5. $ 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:

6. $ 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

7. 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

8. enrollments::= $ ENROLLMENT,
9. ENROLLMENT::=Net{ student:students, class:classes, grade:grades},

   then

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

11. 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 Z]. For example

12. Example_of_prime_in_action::=
    Net{

    1. students::=PERSON->STUDENT,
    2. STUDENT::=following,
       Net
       1. person::people.
       2. class_level::FR|SO|JR|SR,
       3. units::Real,
       4. GPA::Real.
          
       5. |- (inv): class_level=FR iff units<25.00,...

       
       (End of Net)
       
       then
       
    3. |-STUDENT'=following
       Net
       1. person::people.
       2. class_level::FR|SO|JR|SR,
       3. units::Real,
       4. GPA::Real.
          
       5. |- (inv): class_level'=FR iff units'<25.00,...

       
       (End of Net)
       
       Notice that the primes are not placed on the declarations. Thus
    4. Δ_STUDENT::=Net{ |-STUDENT. |-STUDENT'.} means the same as writing
    5. Δ_STUDENT::=following,
       Net
       1. person::people.
       2. class_level::FR|SO|JR|SR,
       3. units::Real,
       4. GPA::Real.
          
       5. |-class_level=FR iff units<25.00,...
          
       6. |-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

    6. For s:students, c:classes, g:{A,B,C,D,F}, finish_class(s, c, g) ::=$ following,
       Net
       
       
       1. |-STUDENT.
          
       2. |-STUDENT'.
          
       3. |- (gpa): units'*GPA'=units*GPA+g.(A+>4 | B+>3 | C+>2 | D+>1 | else+>0 ),
          
       4. |- (units): units'=units+units(c)

       
       (End of 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

13. Δ_D::=$ following,
    Net
    
    
    1. |-D.
       
    2. |-D'.

    
    (End of 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
14. Δ(N)::= N with N'. Similarly, the need for a set of variable to remain constant can be documented by:
15. Ξ(N)::=Δ(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.

16. If Example=(y:Int; y'=x; do(y>3; y'=y-3);y<=3)
17. then
18. 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:
19. 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 [ Dynamic Set ] notation can also be used.

    Dynamic Maps

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

    This last operation is common enough to give rise to a special notation

23. f(x):=e.

    Another, similar notation, indicates a change in the value of one element of a map. Since

24. f.(x:=e) = f ~ (x+>f(x))|(x+>e), we can show the change
25. f' = f.(x:=e).

    In the above the map or function f is acting like 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

26. 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.

    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
    

    1. Add assertions of form v=v'' for all variables v that are not dynamic in N1 or N2.
    2. Add an apostrophe to all variables in N2.
    3. Combine all declarations and definitions.
    4. If a variable appears with one apostrophe but not with two then add an apostrophe to it
    5. Apply existential quantifier to all variables with a single apostrophe.
    6. Change single prime variables to other names, and hide them
    7. Replace double primes by primes.
    8. Simplify and remove redundant invariant assertions

    Example Calcuations

    
    
    1. (above)|- (ex1): (x'=x+1;x'=a*x)=(x'=a*x+a).

       Proof of ex1

    2. Consider{
       (x'=x+1;x'=a*x)=
       1. =(x'=x+1 and (x''=a*x' and a=a''))
       2. = (x'=x+1 and x''=a*x' and a=a'')
       3. =for some x'(x'=x+1 and x''=a*x' and a=a'')
       4. =for some w(w=x+1 and x''=a*w and a=a'')
       5. = for some w(w=x+1 and x'=a*w and a=a')
       6. (simp) =for w:=x+1(x'=a*w and a=a')
       7. (subs) =( x'=a*(x+1))
       8. (alg) =(x'=a*x+a).
          }
       
       
    3. |- (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.
    4. Consider{
       (x'=x-y;y'=x+y;x'=y-x)
       1. = $ Net{x'=x-y, y'=y, y''=x'+y', x''=x'};x'=y-x
       2. = for some a,b(a=x-y and b=y and y''=a+b and x''=a);x'=y-x
       3. = ((y''=x-y+y and x''=x-y);x'=y-x)
       4. = ((y'=x and x'=x-y);x'=y-x)
       5. = (y'=x and x'=x-y and y''=y' and x''=y'-x')
       6. = (x'=y and y'=x)
          }.
       
       
    5. (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]).
       
    6. (above)|- (Shuttle swap): (z'=x; x'=y; y'=z) ==> (x'=y and y'=x)

       Proof of Shuttle swap

    7. Consider{
       (z'=x; x'=y; y'=z)
       1. = ( (z'=x; x'=y); y'=z)
       2. = ( z'=x and x'=y and y'=y); (y'=z)
       3. =$ Net{ ( z'=x and x'=y and y'=y) and y''=z' ) }
       4. =$ Net{ z'=x and x'=y and y'=y and y''=z' }
       5. = $ Net{ z'=x and x''=y and y'=y and y''=z' }
       6. = ( z''=x and x''=y and y'=y and y''=z''=x)
       7. = ( x''=y and y''=z''=x)
       8. = ( x'=y and y'=z'=x)
       9. ==> ( 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:
    8. Consider{
       (x>0; y'=2*x; y<6; x'=y-1)
       1. =(x>0;y'=2*x; y<6 and x'=y-1 )
       2. =(x>0;y'=2*x and y<6 and x'=2*x-1 )
       3. =(x>0 and y'=2*x and y<6 and x'=2*x-1 )
       4. =(x>0 and 2*x<6 and y'=2*x and x'=2*x-1 )
       5. =(x in [0..3] and y'=2*x and x'=2*x-1 )
       6. =(x in [0..3] and (x',y')=(2*x-1, 2*x)).
          }.
    9. Consider{
       (x<0; x'=-x | x>=0)
       1. = (x<0 and x'=-x | x>=0)
       2. = ( (x<0 and x'=-x ) or x>=0).
          }.

    . . . . . . . . . ( end of section Calculations) <<Contents | End>>

    Sequential Structures

    Sequence

    1. 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)

    . . . . . . . . . ( end of section Sequential Structures) <<Contents | End>>

    Concurrent Structures

    See [ math_76_Concurency.html ] and [ math_73_Process_algebra.html ] for more.

    Data flow Diagrams

    1. 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]

       Parallel Operations

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

       Notice that a simple expression can stop the processing
       

    3. |-(x'=x+1) & (x'=x-1) = false.

       Worse
       

    4. |-(x'=x+1) & (y'=y+1) = false. Because each assignment locks the other variable! However:
       
    5. |-(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:

    6. free(v)::=(v'=v'),
    7. lock(v)::=(v=v'),

       .RoadWorksAhead

    8. 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>>

. . . . . . . . . ( end of section Dynamics) <<Contents | End>>

Notes on MATHS Notation

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 might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

For a more rigorous description of the standard notations see