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

Contents


    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 [socket symbol] 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.

End