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

   Here is a biblical use of a relation (Mother) connecting to people: eve and seth
3. eve Mother seth.

   Here we define relations in terms of simpler ones using a simple XBNF style grammar:

4. Parent := Mother | Father.
5. Grandmother := Mother; Parent.
6. Maternal_Grandmother := Mother; Mother.
7. MaternalAncestor := Mother; do(Parent);

   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:

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

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

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

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

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

    This means that
    

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

    The 'do' can also be written as iterate and underlies the meaning of loops in normal programming languages, see below.

    [click here if you can fill this hole]

    Relations and Proofs

    The algebraic style of proof:

     	.Net

     		e1

     	(y1)|-

     		= e2

     	(y2)|-

     		= e3

     	(y3)|-

     		= e4

     	(y4)|-

     		= e5

     	...

     	.Close.Net

     	(above)|-(l):  e1 = e[n].

    is formalized in mathematics using transitive relations. See [ logic_25_Proofs.Algebra and Calculations ] for more.

    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:

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

    However MATHS permits

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

15. 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: while(R)(S) ::= do(R;S);no(R). for(A,B,C)R::=(A; while(B)(R;C)).

    Formatting programs

    In MATHS there is a special way to format nested expressions like the above:

     	for(A,B,C)R =following,

     	.( A;

     	 while(B)

     	.(

     	 R;

     	 C

     	.)

     	.).

    Rendered like this

16. for(A,B,C)R =following, (
    1. A;
    2. while(B) (
       1. R;
       2. 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::=following, (
    1. --(invariant);
    2. while((hi-lo)>error) (
       1. mid'=(hi+lo)/2;--(invariant and f(lo)<=f(mid)<=f(hi)); (
          1. f(mid)<0; lo'=mid
          2. | f(mid)=0; lo'=hi'=mid
          3. | f(mid)>0; hi'=mid
          )
       );-- -- --(invariant and hi-lo <= error)
       
    ).

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