[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / logic_41_HomogenRelations
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Mon Feb 28 07:58:20 PST 2011

Contents


    Homogeneous relations

      Introduction

      These notes are based on the following page:
    1. RELATIONS::= See http://cse.csusb.edu/dick/maths/logic_40_Relations.html.

      First time readers might like to see

    2. INTRODUCTION::= See http://cse.csusb.edu/dick/maths/intro_relation.html, before looking at RELATIONS above and the rest of this page.

      There is special listing of the special kinds of homogeneous relations (transitive, reflexive, etc) in

    3. STANDARD_KINDS::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html#Kinds of relations

      Definition of Homogeneous Relations

      Homogeneous relations have the same type for domain and codomain. As a result, for any type the homogeneous relations for that type form a complex algebra. They are closed under union, intersection and complement. A homogeneous relation can be composed with itself, giving another relation of the same type - hence powers and series of relations. In other words we have a boolean algebra and a monoid combined together.

    4. For T:Types.

    5. For A:@T, A^2::= A><A.
    6. (-1)|-for A, A^2---A^@---A^(0..1).
    7. For X:@T, x,y:variables, W:expression(@), rel [x,y:T](W) ::= {(x,y):X><X ||(W)},
    8. null_relation::@(T,T)= rel [x,y:T](false).
    9. (-1)|- (nr): null_relation= {}.

      Powers

    10. For n:Int, R:@(X,X), pow(R, n)::@(X,X)= if n=0 then Id(X) else if n=1 then R else if n=-1 else /R else if n<0 then (/R)^(-n) else if n>1 then R;( R^(n-1)).
    11. For n:Int, R:@(X,X), R^n::= pow(R,n).


    12. (above)|-for n,m:Int, R^(n+m)=R^n ; R^m

    13. For N:@Int, R:@(X,X), R^N::= |{ R^n || n:N}.

      So for example:

    14. (above)|-R^(0..1) = Id | R.
    15. (above)|-R^(1..*) = R^1 | R^2 | R^3 | ....

      .RoadWorks_Ahead Conversion to a homogeneous relation and Blocks.

    16. For R:@(X, X><Z ), {R}::@(X,X)= R;map[x:X, z:Z] (x).

      Note -- the above defines {...} to act like a block in C/C++/Java/PHP etc. by removing any variables (Z) added to R inside the braces.

      Invariants and Iterations

      This is a way to handle iterative (and recursive) programs that dates back to Whitehead and Russel's work. The idea is simple: If some property is not changed by applying a relation, then iterating many times also leaves it unchanged. So, iterating a relation any number of times does not change those things that can not be varied by a single use of the relation. Hence we define the invariants of a relation. Floyd(and hence Hoare) used this to assign meanings to programs and prove their properties.

    17. invariants::= map[ R:@(X,X)] {A:@X || for x:A, y:X ( if x R y then y in A)},
    18. Invariants of R=sets that are closed or invariant under R.
    19. inv::=invariants.

    20. iterate::= map [R:@(X,X)] ( rel [x,y]( for all A:inv(R) (if x in A then y in A))`,
    21. any number of Rs = transitive, reflexive closure of R.
    22. do::=iterate.

      Note: do is short hand. For documents that are read by people who are new to MATHS then iterate should be used.

      This implies that do(R) is the limit of the Kleene series:

    23. Id | R | R^2 | R^3 | ...

      Informally, do(R) is the smallest upper bound of the above series of sets.


    24. (pow)|- (Nat_do): R^Nat0 = R^(0..*) = do(R).

    25. For R:@(X,X), R^*::=do(R).


    26. (above)|- (inv_do): for all A:inv(R), a:A, b:a.(do(R)) ( b in A ).
    27. (above)|- (no_do): for x,y ( not x do(R) y) iff for some A:inv(R) ( x in A and y not in A ).
    28. (above)|- (inv_id1): for R, do(Id(dom(R)))=Id(dom(R))==>do(R).
    29. (above)|- (inv_id2): for R, R.dom.Id.do=R.dom.Id ==>R.do.
    30. (above)|- (do1): for R, R==>do(R).
    31. (above)|- (do2): if P==>do(R) then (P;R) ==> do(R).
    32. -- if P is a power of R so is P;R
    33. (above)|- (do3): if P=R;do(S;R) then P=do(R;S);R.
    34. (above)|- (do4): R;do(R)=do(R);R.
    35. (above)|- (do5): /do(R) = do(/R),
    36. (above)|- (do6): do(R) = Id(dom(R))|R; do(R).
    37. (above)|- (do7): for R, all n:Nat0, (R^n ==> do(R)).
    38. (above)|- (fund_do): for R, do(R) = |[n:0..](R^n).


    39. (above)|- (reg_rel): RegularAlgebra(@(X,X), |, {}, (;), Id(X), do). [ math_45_Three_Operators.html ]

      Programs on a Set of Relations

      Given a set of relations B:@@(X,X), then the closure of B|{Id} with respect to union(|), composition(;) is also closed with respect to iteration (do). The smallest regular algebra which contains B is defined to be the set of programs on the operations B:

    40. For B:@@(X,X), Programs(B)::@@(X,X)::=smallest{R:@@(X,X)|| B==>R and RegularAlgebra(R, |, {}, (;), Id(X), do)}.

      This definitions as an algebra has some deep implications -- for example, if P:Programs(B) then Q defined by Q::=E(Q) for some programs(B|{Q}) is also a program.

      Simple Programs

      For a set of strings B which represent a set of relations in @(X,X), the set of simple programs on base B, SP(B) is the set of meanings of the finite regular expression of items in B as expressions in @(X,X). To set this up we first define a homomorphism from regular expressions into relations and then apply it to the set of finite regular expressions:
    41. m::=meaning.
    42. For B:@Character, m:B->@(X,X), E:=regular_expression(B), m::= the [m:E->@(X,X)] ( for all A,B:E( m(A|B)=m(A)|m(B) and m(A;B)=M(A);m(B) and ...) ).

    43. simple_programs(B)::=img(m).
    44. SP(B)::=simple_programs(B).
    45. (above)|-SP(B)=>>Programs(B) (while): For A:@T,while(A) ::= [R:@(T,T)](do(A;R);(T~A)), [Botting 87] (for): For A:@T,for(I,J,K) ::= [R:@(T,T)](I;while(J)({R};K)), [Kernighan & Ritchie] (do-od): For A:@T,do F+>f [] G+>g od::= do{F;f|G;g};@(T,T)~(F|G), [Dijkstra 76]

      Example: The Enigmatic Hailstone Sequence

    46. Enigma::=following,
      Net
      1. n':Nat;
      2. while(n>1)(2*n'=n | 2*n'=3*n+1)},

        Source: Lagarias 85, J.C. Lagarias, "The 3x+1 problem and its generalizations," American Math Monthly, V92, Jan 1985, pp33-22.


      (End of Net Enigma)

      Invariants and Fixed Points of Functions

      Notice that when the relation is a function f:X->X that has a fixed point p, then f(p)=p and so p f p and so {p} in inv(f). Thus fix(f) ==> inv(f). However any cycle of f (where f^r(x)=x) also defines another invariant of f. [ math_15_Unary_Algebra.html ]

      Elementary Changes to a Set

      Given a set S, a value x,
    47. For S:@T, x:T, x in S::= test for x in S.
    48. For S:@T, x:T, x|:S::= S'=S|{x}, Put an x in S.
    49. For S:@T, x:T, x:~:S::= (x' in S and S'=S~{x'}),remove an x from S.
    50. For S:@T, x:T, X~:S::= (X ==> S and S'=S~X), -- accept and remove any members of X in S.

      If S is ordered then the minimum values are input first - whatever sequence they are output. So a poset is MATHS's model to COBOL's SORT verb or a library sort.

    51. For S:@T, (<=) :order(S), x:T, x:~:S::= (x' in min(S) and S'=S~{x'}),
    52. For S:@T, X:@T, X|:S::= S'=S|X, -- put members of X into S.

      By giving S different structures then many standard data storage systems can be modeled: RAM, Queues, stacks, Bags,... .

      Relations under a mapping

      Given a homogeneous relation on a set and a map into that set then there is an equivalent relation in the domain in the map.

      This is the paradigmatic example of a powerful technique - using inverse mappings to transfer structure from codomain to domain:

      Notation:

    53. For f:X->Y, x1, x2:X, R:@(Y,Y), x1 R mod f x2::@= f(x1) R f(x2) or equivalently:
    54. (above)|- (mod): For R:@(Y,Y), f:X->Y, R mod f = f;R;/f. Example:
      1. R:= <=
      2. X:=People
      3. Y:=Money
      4. f:=wages
      5. x <= mod wages y iff x earns less than y

      Results:

    55. (above)|- (mod_pow): (R mod f)^n = (R^n)mod f.
    56. (above)|- (do_mod): do (R mod f) = (do(R))mod f.

      Equivalence Relations

    57. For X: @T, Equivalence_relations(X)= {E:@(X,X)|| I ==> E = (E ; E) = /E}.

      Equivalence relations partition their set into non-overlapping parts. This is done by associating with each element in X the set of elements that are equivalent to it: / :: X><Equivalence_relations(X) -> @@X.

    58. For X: @T, E: Equivalence_relations(X), x:X, x/E={y:X||x E y}.

      The family of all these sets then forms a partition.

    59. For X, E, x, A:@X, A/E={a/E||a:A}.


    60. (above)|- (eqr_part1): X>==X/E.
    61. (above)|- (eqr_part2): X/E in partition(X).

      [ Partitions in logic_31_Families_of_Sets ]

    62. For all f:X->Y, (Id(X)/f) in Equivalence_relations(X).

      .Dangerous_Bend

    63. X./f is not X/f.

      Paths and Trajectories

      Homogeneous relations provide a handy way to talk about changing systems. If the relation R holds between the current state and a future state then the powers: R^2, R^3, ... describe multi-step changes and do(R) the long term possibilities.

      A continuous time system with sates in S based on a set of durations T can be modelled as a map R from T into @(S,S), if:
      Net

      1. (T, +, 0, -): group.
      2. R(t1+t2) = R(t1); R(t2).
      3. R(0)=Id.

      (End of Net)

      THe best way to describe the structure of these systems (and any homogeneous relation) is to use the language of Directed Graphs

    64. DIGRAPH::= See http://www.csci.csusb.edu/dick/maths/math_22_graphs.html#DIGRAPH.

      There has been much research on the long term properties of such systems. There are 4 properties that are commonly studied:

      1. (EF): It is possible to get to a particular set of states.
      2. (AG): The system always remains in a given set of states.
      3. (EG): The system can follow a path that lies in a given set.
      4. (AF): Whatever path the system follows it must go into a given set.

      [ logic_9_Modalities.html ]

      Two of the above(EF and AG) are easily stated by using do(R):

    65. For Type T, t:T, S:@T, R:@(T,T).
    66. EF(t,R,S)::= some ( t.do(R) & S ).
    67. AG(t,R,S)::= (t.do(R) ==> S).

      The other two(EG and AF) need a model of paths or trajectories:

    68. paths::@(T,T)-> @(T, #T), paths relate elements to strings of elements.
    69. For R:@(T,T), t:T, t.paths(R)={ s:#T. head(s)=t and for all (x,y) in s ( x R y).
    70. trajectories(R,t)::=t.paths(R).

      Given the above we can express EG and AF as:

    71. EG(t,R,S)::= some( t.paths(R) & #S ).
    72. AF(t,R,S)::= (t.paths(R) ==> #T S #T).

      Notice the use of regular expressions to describe sets of paths.

      We can show:

    73. (above)|- (path1): AG(t,R,S) iff t.do(R) ==> S iff t.paths(R)==>#S.

      Thus the language of paths and regular expressions is a way to talk about the behaviors of complex systems. There is no reason not to use grammars to express irregular patterns as well.

    . . . . . . . . . ( end of section Homogeneous 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