.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