- Binary Relations
- : Traditional Calculus of Relations
- : Relations in MATHS
- : Relations and Proofs
- : Relations and Programs
- : Formatting programs
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

- x is mother of y mentions a relation mother connecting x and y. So we model it as
- 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 - eve Mother seth.
Here we define relations in terms of simpler ones using a simple XBNF style grammar:

- Parent := Mother | Father, A Parent can be a Mother or a Father.
- Grandmother := Mother; Parent, A Grandmother is the Mother of a Parent.
- Maternal_Grandmother := Mother; Mother.
- MaternalAncestor := Mother; do(Parent),
A MaternalAncestor is or can be the Mother, the Mother of a Parent, a Mother of a Parent of a Parent, etc. .
Relations have all the operators of sets (|, &, ~,...).

- Mother | Father (Union)
- Mother & Father (Intersection, should be null in this case).
- Mother ~ Father
(Complement, Mther but not Father).
Relations haqve a special operator 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:

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

- |-x Id y iff x=y.
Define no(R) and do(R) to represent complements and iterations:

- no(R)::= for no y( xRy),
- do(R)::= the smallest relation X such that X=Id | X;R
This means that

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

In comparison with normal programming languages a while-loop like this

while(i<>1)

{

if(even(i))

i/=2;

else

i=3*i+1;

}

can be expressed in MATHS as this expression: - do(i<>1; (even(i); i:/2 | odd(i); i:*3:+1 ) ) no(i<>1);
[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:

- x'=e
is like an assignment statement x:=e found in most programming languages.
However MATHS permits

- 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

- 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

- for(A,B,C)R =following,
(
- A;
- while(B)
(
- R;
- C

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

- --(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:

- invariant::=f in monotonic and f(lo)<=0<=f(hi).
- chop::=following,
(
- --(invariant);
- while((hi-lo)>error)
(
- mid'=(hi+lo)/2;--(invariant and f(lo)<=f(mid)<=f(hi));
(
- f(mid)<0; lo'=mid
- | f(mid)=0; lo'=hi'=mid
- | f(mid)>0; hi'=mid

- mid'=(hi+lo)/2;--(invariant and f(lo)<=f(mid)<=f(hi));
(

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.

- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
# Glossary

- 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).
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- 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.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.

. . . . . . . . . ( end of section Binary Relations) <<Contents | End>>

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 ]

For a more rigorous description of the standard notations see