Traditional Calculus of Relations

Traditionally a relation is modeled as a set of pairs. For example
1. x is mother of y mentions a relation mother connecting x and y. So we model it as
2. Mother := { (x,y) || x is mother of y }

   Mathematics provides a rich language for talking about relationships. For the traditional notation see [ rel.html ] In my pages the language is encoded using ASCII.

   Relations in MATHS

   So for example:
3. eve Mother seth.
4. Parent := Mother | Father.
5. Grandmother := Mother; Mother.
6. MaternalAncestor := Mother; do(Mother);

   Relations have all the operators of sets (|, &, ~,...) plus plus one of their own - composition. Since this models exactly how ';' is meant to work in most programming languages MATHS symbolizes the product of two relations R and S as R;S:

7. For R,S:relations, x(R;S)y::= for some z ( x R z and z S y).

   'Id' is the identity or 'do nothing' relationship.
   

8. |-x Id y iff x=y.

   Define do(R) and no(R) to represent iterations and complements:

9. no(R) ::= for no y( xRy),

10. do(R) ::= the relation X such that X=Id | X;R

    This means that
    

11. (do) |-do(R)=( Id|do(R);R).

    [click here if you can fill this hole]

    Relations and Programs

    This page shows how mathematical relations can be used to model programs!

    A program statement can be modeled as a relation between the state of a machine before the statement, and its possible states afterwards. A simple way to symbolise this kind of relation is to use a predicate with primes(') put after one or more variables. These imdicate the new values of the variables that can change - all others are fixed. For example:

12. x'=e is like an assignment statement x:=e found in most programming languages.

    However MATHS permits

13. f(x')=0 as well as x'=f(0).

    So, for example, a well known algorithm for finding the root of a function can be specified by

14. f in monotonic and f(lo)<=0<=f(hi) and f(lo')<=0<=f(hi') and hi'-lo'<=error.

    A predicate without a primed variable defines a set. Dynamic predicates look like statements in a powerful computer language. This is enhanced because the operators on relations look and feel like program structures.

    Hence we can define C or C++ like control structures:

15. while(R)(S) ::= do(R;S);no(R).
16. for(A,B,C)R::=(A; while(B)(R;C)).

    Also we can define a 'comment' to be, for any text:

17. --(text) ::=Id.

    A relational expression describes something that often can be coded as a program.

    For example if a function f is continuous and 'monotonically increasing' in a range of values from 'lo' to 'hi' then the following relation describes the well known bisection procedure:

18. invariant::=f in monotonic and f(lo)<=0<=f(hi).
19. chop::=(--(invariant);
20. while((hi-lo)>error)
21. ( mid'=(hi+lo)/2;--(invariant and f(lo)<=f(mid)<=f(hi));
22. ( f(mid)<0; lo'=mid
23. | f(mid)=0; lo'=hi'=mid
24. | f(mid)>0; hi'=mid
25. )
26. );--(invariant and hi-lo <= error)
27. ).

    Relations do not express an algorithm unless the expression defines an association from every possible previous state to a uniquely determined final state. Such relations are called Functions or maps.

. . . . . . . . . ( end of section Binary Relations) <<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, and give them a name. 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.

Notes on the Underlying Logic of MATHS

For a complete listing of pages by topic see [ home.html ]