[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng ] / [R J Botting] / [ MATHS ] / intro_dynamics
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue May 19 06:32:54 PDT 2009

Contents


    Dynamics and Relationships

      Copyright

      Richard J Botting 2003 [ http://cse.csusb.edu/dick/ ] You may link to the whole of this document. All other rights are reserved.

      This is part of Chapter 2 of a research monograph tentatively entitled "MATHS for Software Engineering".

      Program Specifications

      Relations behave like the operations and conditions in a programming language because each operation in a program relates the current state to the set of possible future states. If there was always a single next state then the relation is deterministic, and by composing deterministic steps carefully we get an algorithm. In turn an algorithm can be coded for input to a suitable translator giving an executable program. Thus a relation describes a set of acceptable behaviors and the implementor selects a particular algorithm [compare with Kowalski, Hoare 87]. For a dissenting view see footnote2.

      MATHS relations can be written in a form that makes them look like statements in a programming language. Some syntactic sugar is defined for those who want to write while/for/loops/. . . . The key definition is that of a dynamic predicate. Here is an introduction. Formal treatment comes later when we have the techniques [ [ math_14_Dynamics.html ] [ math_75_Programs.html ] ].

      The MATHS approach is very similar to the ones that Tony Hoare evolved:

      Dynamic Predicates

      A predicate is a proposition that has free variables. A dynamic predicate has free variables with primes (') attached to them. Here is an example:
    1. x'=x+y

      After the statement, the value of x is equal to the sum of the old values of x and y. Also, y is unchanged. It could be coded as x:=x+y in Ada/Pascal/... The semantic rule is that "a prime means the new and no prime means the old" [Ross Ashby 56, Part II of Lam & Shankar 90, compare Hehner 84a & 84b, Guttag & Horning 91, Steward 93]. Formally x'=x+y defines a relation on a structured set with variables x and y. So

    2. x'=1

      guarantees that x is 1 afterwards and also that no other variables change.

    3. x'=1-x

      means that the value of x will be complemented - its new value will be the result of subtracting its old value from one while all other variables stay the same.

    4. x=1

      has no primed variable. It means that x has the value one, and does not change - all variables are left untouched. It is a relation that holds between identical states when and only when x has value 1. It filters out all states when x is not 1. It allows computation under a condition. We call it a condition therefore. It can be shown that it is a condition in the sense of Arbib and Manes [87].

      Here is a more general statement of the MATHS interpretation of a predicate that contains variables with primes. Consider a simple state space S which declares m variables x1, x2,...x[m] of types X1, X2, ...X[M]:

    5. S::=$ Net{x1:X1,x2:X2,...,x[m]:X[m]}.

      Let P(y1',y2',y3',...y[n]',x1,x2,x3,...x[m]) be a predicate with n distinct primed variables(y1, y2,...y[n]) which also may also appear without primes as xs. For example in x'=x+y, x1=x, x2=y, and y1=x.

      The relation defined by P(y1', y2', y3', ...y[n]', x1, x2, x3, ...x[m]) is found by: (1) Replacing primed variables (y1,...) by values in the new state(s2), and (2) Replacing non_primed variables(x1,...) by values in the old state(s1), and (3) Adding the requirement that the static (unprimed) variables do not change. So:

    6. P(y1',y2',y3',...y[n]',x1,x2,x3,...x[m])::= rel [s1:S, s2:S]( P(s2.y1, s2.y2, ..., s2.y[n], s1.x1, s1.x2, ...,s1.x[m] ) and for all i:1..m where x[i] not in {y1, y2, ..., y[n]}, s2.x[i]=s1.x[i]).

      A more rigorous definition will be worked out in Chapter 5 meanwhile here are some examples. To specify a process that solves two simultaneous linear equations we write

    7. a*x'+b*y'=c and d*x'+e*y'=f.

      To specify a process that solves a quadratic equation we write

    8. a*x'^2+b*x'+c=0.

      On the other hand

    9. a'*x^2+b'*x+c'=0,

      specifies that x is left alone and a, b, and c are adjusted to fit the equation.

      Binary Relations

      @(T1,T2) symbolizes the relations between T1 and T2. A relation in R:@(T1,T2) can be defined by
    10. For x:T1, y:T2, x R y::@= W(x,y).

      or equivalently by

    11. For R::@(T1,T2)= W((1st), (2nd)).

      /R is the converse relation to R. For example if (_^2) is the 'square' function then /(_^2) is the square root relation. Similarly the arc sine function is written /sin. Further we want /parent_of=child_of. MATHS defines

    12. For R:@(T1,T2), /R::@(T2,T1)= (2nd) R (1st).

      Given two binary relations R and S then
      R; S = The relation between (1st) and (2nd) where for some z, (1st) R z S (2nd),


      R | S = The relation between (1st) and (2nd) where either (1st) R (2nd) or (1st) S (2nd),


      R & S = The relation between (1st) and (2nd) where both (1st) R (2nd) and (1st)S (2nd).

    13. For R: @(T1,T2), S:@(T2,T3), R;S::@(T1,T3)= rel[x:T1,y:T3](for some z:T2 (x R z and z S y)),
    14. S o R::@(T1,T3)= R;S.
    15. R::@(T1><T2)= {(x,y):T1><T2 || x R y }.

      In context, a set can also be used as a relation:

    16. For A:@T, A::@(T,T)=rel[x:T, y:T](x in A and x=y).

      Example: Family Relationships

      Its surprising how quickly you can define even complex situations using these notations:
      1. ... male, female::@being.
      2. parent::@(being,being)=(1st)is a parent of(2nd).
      3. ...
      4. child_of::=/parent.
      5. father::=male;parent.
      6. mother::=female;parent.
      7. son::=male;child_of.
      8. daughter::=female;child_of.
      9. grandfather::=father;parent.
      10. ...
      11. granddaughter::=daughter;child_of.
      12. grandson::=son;child_of.
      13. ...
      14. sibling::@(being,being)= (/parent;parent) ~ (=).
      15. -- I am not my own sibling!
      16. sister::=female;sibling.
      17. ...
      18. uncle::=brother;parent.
      19. ...
      20. niece::=daughter;sibling.
      21. first_cousin::=/parent;sibling;parent.
      22. second_cousin::=/parent;/parent;sibling;parent;parent.
      23. lineal_descendant::= child_of | lineal_descendent; child_of,
      24. ancestor::=parent | parent; ancestor
      25. cousin::=/parent;sibling;parent | /parent;cousin;parent,
      26. first_cousin_once_removed::=/parent;first_cousin | first_cousin;parent.
      27. [From Logic.Natural.KINSHIP]
      28. ...

      Inductive Invariants

      The last four definitions above are like productions in context free grammar. The definitions of ancestor and lineal_descendant illustrate the transitive closure or ancestral relation. It is so common that a special notation is defined: x do(R) y::= x=y, or x R y or x R;R y, or....

      Example:

    17. (above)|-ancestor=parent; do(parent) and lineal_descendant=child_of; do(child_of).

      The defining property of do is that if something is invariant (or fixed, or closed) under R then it will not be changed by any number of Rs[footnote1]:

    18. inv(R)::= the invariants of R
    19. inv(R)::=the sets X such that if x in X and x R y then y in X. Example: families::=inv(parent).
    20. |-For R:@(X,X), F:@X, if F.R ⊆ F then F in inv(R) and F.do(R) ⊆ F.
    21. Example: families.do(parent) ⊆ families.

      Similar to the idea of an invariant set of states is the idea of an stable variable of function:

    22. stable(R)::=The stable functions under R
    23. stable(R)::=the functions f such that R;f=f and, so if f in stable(R) then f in stable(do(R)). Also for all R and f, f is stable under not(R).

      Loops

      Consider the following expression:
    24. SUM::=(n'=1 and s'=0; do(n<>101; s'=s+n and n'=n+1); n=101).

      The definition for SUM looks like a program but is an expression in the calculus of relations [Whitehead & Russell]and so has provable properties. First since the (+) is defined to be an operator on numbers, so the state space is ${n,s:Numbers}. Next define names for the parts of SUM:

    25. S::=(n'=1 and s'=0).
    26. L::=(s'=s+n and n'=n+1).
    27. E::=(n=101). W::=not E.
    28. (S, L, E)|- (eq1): SUM= (S; do(W; L); E).

      Now s is stable under E:

    29. (above)|-E ⊆ (s'=s), or
    30. (above)|-E ==> (s'=s).

      and after E we know that n=101 because

    31. (above)|-post(E)=img(E)={ x :X || x.n=101}.

      Similarly after S we know that n=1 and s=0. Further W by definition will not change s and n. Next we look for something that does not change in L. Both s and n change - in parallel:

    32. (above)|-L = ( (s',n')=(s+n,n+1) ).

      With a little creativity or experience we discover the following invariant set of L:

    33. F::= ( s=1+2+3+4+...+(n-1)).
    34. (above)|-F; L ⊆ F,
    35. (above)|-F in inv(L).

      Similarly

    36. (above)|-F in inv(W) and inv(E),

      so

    37. (above)|-F in inv(W;L).

      Thus

    38. (above)|-(F; do(W; L)) ⊆ F.

      Now

    39. (above)|-S ⊆ F and F;E ⊆ F.

      so

    40. (above)|-SUM = (S; do(W; L); E) ⊆ F and n'=101

      Hence, after SUM, s= 1+2+3+4+...+(n-1) where n=101 = 5050.

      Notice that MATHS is not a programming language. So

    41. x (do(W; L)) y

      is not the same as

    42. x (do(W; L); E) y.

      In the first case y.n can have many values. In the second y.n will be 101. Similarly, when

    43. x ( i=1; i'=2 | i'=3 ) y

      permits y.i=2 even if i<>1, but if x.i=1 then y.i MUST be 2. Whatever happens y.i is either 2 or 3. Such non-determinism seems to be essential for a simple model of processes[Dijkstra 76, Hoare 78, Hoare 85, Gabrielian & Franklin 91].

      Program Structures

      MATHS includes structured programs because
    44. For R:@(S,S), no(R)::@(S,S)= ((1st)=(2nd) and for no y((1st) R y).
    45. For A:@S, R:@(S,S), while(A)(R) ::=(do(A; R); no(A)),
    46. For I,J,K:@(S,S),R:@(S,S), for(I, J, K)(R) ::=(I; while(J) ( (R); K ) ),
    47. For A:@S, R,T:@(S,S), (if A then R else T fi) ::=(A; R | no A; T).

      We can, for example, when n<=m define:

    48. SUM(f, i, n, m, s)::=for(i'=n, i<=m, i'=i+1)(s'=s+f(i))

      and show

    49. (above)|-SUM(f, i, n, m+1, s) = SUM(f, i, n, m, t) and s=t+f(m+1).

      MATHS includes an extension of Dijkstra's Guarded Commands - see chapter 6 for details. Any group of MATHS users can document and then use its own set of abbreviations. For example:

    50. ADA_PDL::=
      Net{
        ...
      1. For A,B,C:@(S,S), loop A; exit when B; C; end loop::= (do ( A; no(B); C); (A; B) ).
      2. ...

      }=::ADA_PDL.

      MATHS can express mixtures of conditions and actions in one relation. A well known enigmatic program is often written:

    51. Enigma::= ( while(n>1) (
    52. if n in even then n'=n/2
    53. else n'=3n+1
    54. fi
    55. ) ).

      In MATHS it can be transformed:

    56. |-Enigma=while(n>1)( 2*n'=n | 2*n'=3*n+1 ).

      Logical Programming?

      MATHS makes the derivation of programs more logical: (1) state the properties of the changed variables as a set of equations and then (2) solve for the primed variables. Similarly, (1) give non-deterministic relationships and reduces them to a form that is compatible with a declarative programming system such as Prolog [Compare Lamport 87].

      Reasoning about Programs

      Finally, MATHS relational expressions follow the calculus of relations which can be used to simplify sequences into disjunctive normal form, like the following:
    57. R = A1 and A2 and A3 and... or B1 and B2 and... or...

      These relations can then be expressed as and/or tables.

      Typical rules are:
      Net


      1. |- (dist): R;(S|T) = (R;S) | (R;T).
      2. |- (cond1): (P(x, y); Q(x, y, y')) = (P(x, y) and Q(x, y, y')).
      3. (cond1)|- (condassign): (Q(x, y); x'=e(x, y) ) = (x'=e(x, y) and Q(x , y)).
      4. |- (assign): (x'=e(x, y); Q(x, y, y')) = (x'=e(x, y) and Q(e(x, y), y, y')).

      (End of Net)

      Footnotes


      (footnote1): Originally in Whitehead and Russell's Principia, the same form is in Floyd's loop invariant technique and reminiscent of Kleene closure in grammar theory. The definition relies on using higher order quantifiers[cf Guerevich 87].


      (footnote2): In theory a better specification of a piece of a program has two relations. The first indicates when the program can be safely used. When the relation holds it does not effect the state of the program. When is does not hold the program has no specified behavior and may not even terminate. The second relation indicates the changes that may occur when the first relation is true and the relation is safe to use. This comes from Parnas's work.

      I plan to expand on this later. I envisage modeling a program as a collection of relations describing when it is safe to use, what resources will be demanded for it to work, and the actual effect of the program.

    . . . . . . . . . ( end of section Dynamics and Relationships) <<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 = Net{radius:Positive Real, center:Point}.

    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