.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
So for example:
	eve Mother seth.
	Parent := Mother | Father.
	Grandmother := Mother; Mother.
	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:

	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 iterations and
complements:
	no(R) ::= for no y( xRy),

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

This means that
	(do)|- do(R)=( Id|do(R);R).

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

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