.Open Binary Relations
. Traditional Calculus of Relations
Traditionally a relation is modeled as a set of pairs.  For example
	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
.See http://www.math.csusb.edu/notes/rel/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.
	Grandmother := Mother; Parent.
	Maternal_Grandmother := Mother; Mother.
	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:

	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 do(R) and no(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 
.Key iterate
and underlies the meaning of loops in normal programming languages, see
below.

.Hole

. Relations and Proofs
The algebraic style of proof:
.As_is 	.Net
.As_is 		e1
.As_is 	(y1)|-
.As_is 		= e2
.As_is 	(y2)|-
.As_is 		= e3
.As_is 	(y3)|-
.As_is 		= e4
.As_is 	(y4)|-
.As_is 		= e5
.As_is 	...
.As_is 	.Close.Net
.As_is 	(above)|-(l):  e1 = e[n].
is formalized in mathematics using transitive relations.  See
.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:
.As_is 	for(A,B,C)R =following,
.As_is 	.( A;
.As_is 	 while(B)
.As_is 	.(
.As_is 	 R;
.As_is 	 C
.As_is 	.)
.As_is 	.).

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
.)
.);--(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.
.Close Binary Relations