.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,
`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
.Key iterate
and underlies the meaning of loops in normal programming languages, see
below.
In comparison with normal programming languages a while-loop like this
.As_is while(i<>1)
.As_is {
.As_is if(even(i))
.As_is i/=2;
.As_is else
.As_is i=3*i+1;
.As_is }
can be expressed in MATHS as this expression:
do(i<>1; (even(i); i:/2 | odd(i); i:*3:+1 ) ) no(i<>1);
.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