[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_14_Dynamics
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Jan 28 11:50:08 PST 2013

Contents


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

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

      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.

      By the way we might wish to add the fact that only Undergraduates can become alumni

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

    21. s in Undergraduate and Undergraduate:~ s and Alumnus:|s.

      Thus we can write

    22. For s:Person, graduate(s)::=following,
      Net
      1. Δ_STUDENT.
      2. ...
      3. s in Undergraduate.
      4. Undergraduate:~ s.
      5. Alumnus:|s.

      (End of 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 [ Dynamic Sets ] (above) can be used. Here are a couple samples: Marriage
    23. Married' = Married | {(bride, groom)}.
    24. Married' = Married | bride+>groom.

      Divorce

    25. 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
    26. f' = f | (x+>e), or remove one (turning map into a partial map):
    27. f' = f ~ (x+>f(x)),

      But if we start with a map and remove and replace one item:

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

    29. f(x):=e.

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

    30. f.(x:=e) = f ~ (x+>f(x))|(x+>e), we can show the change
    31. 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

    32. 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
    33. f(x):=e
    34. 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:

    35. f' = if( x in ddef(f), f ~ (x+>f(x))|(x+>e), f | (x+>e) ).

      This is actually

    36. f' = f over_ridden_by (x+>e), [ over_ridden_by in logic_40_Relations ]

      Similarly f.(x:=e) is

    37. 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
    38. f : @D K->V, then we can treat it as
    39. f : K<>->V, and so write (for k:K and e:V),
    40. f(k):=e, to indicate the creation and/or modification of the relation f.

      There are specialized Add, Delete, and Update functions define in

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

      Changing a single attribute in one object of an entity

      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
      1. S' = { t:T || for some s:S ( (s,t) in U ) }, or equivalently
      2. S' = S.U, or even
      3. S:.U.

      [ Z-like%20Operators in logic_44_n-aryrelations ]

      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)|-
        7. =for w:=x+1(x'=a*w and a=a')
        8. (subs)|-
        9. =( x'=a*(x+1))
        10. (alg)|-
        11. =(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 [socket symbol] 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 [socket symbol] if you can fill this hole]

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

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

    Notes on MATHS Notation

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

    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 more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary

  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

( End of document ) <<Contents | Top