.Open Homogeneous relations

. Introduction
These notes are based on the following page:
RELATIONS::=http://www/dick/maths/logic_40_Relations.html.

First time readers might like to see
INTRODUCTION::=http://www/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
STANDARD_KINDS::=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.

 For T:Types.

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

. Powers
 
 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)).
 For n:Int, R:@(X,X), R^n::= $pow(R,n).

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

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

So for example:
	()|- R^(0..1) = Id | R.
	()|- R^(1..*) = R^1 | R^2 | R^3 | ....

.RoadWorks_Ahead
Conversion to a homogeneous relation and
.Key Blocks.
 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.

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

iterate::=  map [R:@(X,X)] ( rel [x,y]( for all A:inv(R) (if x in A then y in A))`, 
	`any number of Rs` = `transitive, reflexive closure of R`.
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:
	Id | R | R^2 | R^3 | ...

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

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

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

	(above)|- (inv_do):for all A:inv(R), a:A, b:a.($do(R)) ( b in A ).
	(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 ).
	(above)|- (inv_id1): for R, $do(Id(dom(R)))=Id(dom(R))==>$do(R).
	(above)|- (inv_id2):for R, R.dom.Id.$do=R.dom.Id ==>R.$do.
	(above)|- (do1): for R, R==>$do(R).
	(above)|- (do2): if P==>$do(R) then (P;R) ==> $do(R).  
			-- if P is a power of R so is P;R
	(above)|- (do3): if P=R;$do(S;R) then P=$do(R;S);R.
	(above)|- (do4): R;$do(R)=$do(R);R.
	(above)|- (do5): /$do(R) = $do(/R),
	(above)|- (do6): $do(R) = Id(dom(R))|R; $do(R).
	(above)|- (do7): for R, all n:Nat0, (R^n ==> $do(R)).
	(above)|- (fund_do): for R, $do(R) = |[n:0..](R^n).

	(above)|- (reg_rel): RegularAlgebra(@(X,X), |, {}, (;), Id(X), $do).
.See http://www/dick/maths/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:

 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:
m::=meaning.
 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 ...) ).

simple_programs(B)::=img(m). 
SP(B) ::=simple_programs(B). 
	(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
Enigma::=following,
.Net
	n':Nat;
	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.
.Close.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`.
.See http://www/dick/maths/math_15_Unary_Algebra.html


. Elementary Changes to a Set
Given a set S, a value x,
 For S:@T, x:T, x in S::= `test for x in S`.
 For S:@T, x:T, x|:S::= S'=S|{x}, `Put an x in S`.
 For S:@T, x:T, x:~:S::= (x' in S and S'=S~{x'}),`remove an x from S`.
 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.
 For S:@T, (<=) :order(S), x:T, x:~:S::= (x' in min(S) and S'=S~{x'}),
 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:
 For f:X->Y, x1, x2:X, R:@(Y,Y), x1 R mod f x2 ::@=  f(x1) R f(x2)
or equivalently:
	(above)|- (mod): For R:@(Y,Y), f:X->Y, R mod f =  f;R;/f.
Example:
.Box
	R:= <=
	X:=People
	Y:=Money
	f:=wages
	x <= mod wages y iff `x earns less than y`
.Close.Box

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

. Equivalence Relations
 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.

 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.
 For X, E, x, A:@X, A/E={a/E||a:A}.

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

.See http://www/dick/maths/logic_31_Families_of_Sets.html#Partitions

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

.Dangerous_Bend
	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
	(T, +, 0, -):group.
	R(t1+t2) = R(t1); R(t2).
	R(0)=Id.
.Close.Net

THe best way to describe the structure of these systems (and
any homogeneous relation) is to use the language of Directed
Graphs
DIGRAPH::=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:
.List
	(EF):It is possible to get to a particular set of states.
	(AG):The system always remains in a given set of states.
	(EG):The system can follow a path that lies in a given set.
	(AF):Whatever path the system follows it must go into a given set.
.Close.List
.See http://www/dick/maths/logic_9_Modalities.html

Two of the above($EF and $AG) are easily stated by using $do(R):
	EF(t,R,S) ::= some ( t.$do(R) & S ).
	AG(t,R,S) ::= (t.$do(R) ==> S).

The other two($EG and $AF) need a model of paths or trajectories:
	paths:: @(T,T)-> @(T, #T), paths relate elements to strings of elements.
	For R:@(T,T), t:T, t.$paths(R)={ s:#T. head(s)=t and for all (x,y) in s ( x R y).
	trajectories(R,t)::=t.$paths(R).

Given the above we can express $EG and $AF as:
	EG(x,R,S)::= some( t.$paths(R) & #S ).
	AF(x,R,S)::= (t.$paths(R) ==> #T S #T).

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

We can show:
	(above)|-(path1): $AG(t,R,S) iff t.$do(R) ==> S iff t.$paths(R)==>#S.
	(above)|-(path2): $EF(t,R,S) iff some(t.$do(R) & S) iff some (t.$paths(R) & S).

Thus the language of paths and regular expressions is a way to talk about
the behaviors of complex systems.

.Close Homogeneous Relations