[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng ] / [R J Botting] / [ ] / intro_relation
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Dec 7 14:10:29 PST 2009

# Binary Relations

## Traditional Calculus of Relations

Traditionally a relation is modeled as a set of pairs. For example
1. x is mother of y mentions a relation mother connecting x and y. So we model it as
2. 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
3. eve Mother seth.

Here we define relations in terms of simpler ones using a simple XBNF style grammar:

4. Parent := Mother | Father, A Parent can be a Mother or a Father.
5. Grandmother := Mother; Parent, A Grandmother is the Mother of a Parent.
6. Maternal_Grandmother := Mother; Mother.
7. 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 (|, &, ~,...).

8. Mother | Father (Union)
9. Mother & Father (Intersection, should be null in this case).
10. 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:

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

12. |-x Id y iff x=y.

Define no(R) and do(R) to represent complements and iterations:

13. no(R)::= for no y( xRy),

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

This means that

15. (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:
16. 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:

17. x'=e is like an assignment statement x:=e found in most programming languages.

However MATHS permits

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

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

20. for(A,B,C)R =following, (
1. A;
2. while(B) (
1. R;
2. C
)
).

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

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

22. invariant::=f in monotonic and f(lo)<=0<=f(hi).
23. chop::=following, (
1. --(invariant);
2. while((hi-lo)>error) (
1. mid'=(hi+lo)/2;--(invariant and f(lo)<=f(mid)<=f(hi)); (
1. f(mid)<0; lo'=mid
2. | f(mid)=0; lo'=hi'=mid
3. | 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.

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

# Notes on MATHS Notation

Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

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 ]

# Notes on the Underlying Logic of MATHS

The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

For a more rigorous description of the standard notations see

1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

# Glossary

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