.Open Binary relations In the history logics the theory of relationships between two things: `x is the father of y` for example, is a 20th century development. For a long time statements like `x is the father of y` would be translated into `x is a member of the fathers of y`. This allows some conclusions to be drawn but disguises some important properties. Relations are central to all modern mathematical forms of logic. These relations can appear in two disguises: As predicates with two unknowns, or as sets of pairs of objects. The following can all be treated as the same expression: .Set frank fathered dick, fathered(frank, dick), (frank, dick) in fathered, (frank, dick).fathered, dick in fathered(frank), frank in /fathered(dick), etc. .Close.Set Binary relations are a special case of the n-ary relations: .See http://www/dick/maths/logic_44_n-aryrelations.html There is also a specialized theory of relations between things of the same type: .See http://www/dick/maths/logic_41_HomogenRelations.html MATHS assumes that for any two types `T1` and `T2` then `@(T1>@T2=map[x:T1]{y:X||x R y}. ()|- (r2m): For R:@(T1,T2), x:T1, x.R= R(x)= {y:X||x R y}. .Dangerous_Bend Mathematical relations do not work like English verbs. A sentence like `x is the parent of y` is natural formalized as `x parent y` and as a result `the children of x` as represented `parent(x)`. For R:@(T1,T2), R::@T1->@T2=map[X:@T1]{y:Y||for some x:A(x R y)}. ()|- (r2ms): For R, A:@T1, A.R= R(A)= {y:Y||for some x:A(x R y)}. (r2ms,r2m)|- (r2mu): For R, A, A.R = = R(A) = |[x:A](R(x)). . Elementary Relations Inherited from `Principia Mathematica` and `Z` is a symbol for the relation that holds between a pair of objects: For a:T1, b:T2, a+>b::= {(a,b)}. ()|-(rs): a+>b = rel [x:T1, y:T2](x=a and y=b). MATHS also has the following useful over-loadings for the '+>' symbol: For A:@T1, b:T2, A+>b::= {(a,b) :T1>B::= {(a,b) :T1>B is a pair {(A,B)} and the set of pairs is A>b)={b}. (r2m,def)|- For x:A~{a}, x.(a+>b)={}. . Converse Relations For R:@(T1,T2), /R::@(T2,T1) = rel [x,y](y R x), /R::= `the converse relation to R`. ()|-(c1): /R = (2nd) R (1st). ()|-(c2): /(a+>b)=(b+>a). ()|-(c3): /(A+>b)=(b+>A). ()|-(c4): /(rel [x:T1,y:T2] (W)) ::=(rel [y:T2,x:T1] (W)) By combining the properties of converses and relations as maps (above) we get ()|-(cm1): For y:T2, R:@(T1,T2), y./R=/R(y)={x:T1 || x R y}. ()|-(cm2): For R:@(T1,T2), B:@T2, B./R=/R(B)={x:T1 || for some y:B(x R y)}. .Dangerous_Bend Mathematical relations do not work like English verbs. A sentence like `x is the parent of y` is natural formalized as `x parent y` and as a result `the parents of y` are shown as `/parent(y)` and `the children of x` as `parent(x)`. . Operations on Relations The binary operations on relation of a given type follow from their definition as sets: sets::= http://www/dick/maths/logic_30_Sets.html (sets)|-(sr1): For R:@(T1,T2), S:@(T1,T2), R & S = rel [x:T1,y:T2] (x R y and x S y). (sets)|-(sr2): For R:@(T1,T2), S:@(T1,T2), R | S = rel [x:T1,y:T2] (x R y or x S y). (sets)|-(sr3): For R:@(T1,T2), S:@(T1,T2), R ~ S = rel[ x:T1,y:T2] (x R y not x S y). (Boolean) |-(relations_Boolean): (@(T1,T2), |, {}, &, @(T1,T2), ~ ) in Boolean_algebra. Boolean::=http://www/dick/maths/math_41_Two_Operators.html#Boolean Algebra. . Convenient notations Operators (|) and (&) are both serial. So |(A,B,C) = A| (B|C) = A|B|C = (A|B)|C, for example. MATHS provides a set of synonyms for talking about the sets of objects involved on each side of a relationship. Each suggests a different metaphor, and each is used by some authority or other somewhere: post::= dom(_).(_), -- post condition. rng::=post, -- range. img::=post, --image. pre::=cod(_)./(_), pre-condition. cor::=pre, -- co-range. ddef::=pre, domain of definition (Z). (def) |-(d1): For R:@(T1,T2), rng(R)= post(R) = img(R) = dom(R).R. (def)|-(d2): For R:@(T1,T2), cor(R) = pre(R) = ddef(R) =cod(R)./R. (def)|-(d3): post(R)=|(R) and pre(R)=|(/R), -- using conventions for treating relations as maps and taking unions of maps. (def)|-(d4): For T1,T2,R, R = |[x:pre(R),y:x.R](x+>y) = |[x:pre(R)](x+>x.R) = |[y:post(R)](y./R+>x). For those who would like symbols, it can be shown that (|) can opearate as an \$img in the right context: |-(bar2img): For R:@(T1,T2), | /R=pre(R) and |R=post(R). For R:@(T1,T2), |/(R)::= |(/(R)). (above)|-(duality): pre ( / (_) ) = post and post(/(_))=pre and ... .Open Structures of the Domains of Relations A relationship induces structures on tits domain and codomain. . Totality Notice that the pre-image of a relation is often less than its domain. This happens whenever the relation is partial rather than total... STANDARD::=http://www/dick/maths/math_11_STANDARD.html#Types of relationships. (STANDARD)|- R is total iff pre(R)=post(R) . Structure of the Domain A relation R defines a structure(a complex) on its codomain, For R:@(T1,T2), coi(R) ::={ X:@T1 | for some y( X=y./R ), -- (co-image) .See http://www/dick/maths/logic_31_Families_of_Sets.html (STANDARD)|- R is regular iff post(R)>=={x.R||x:pre(R)}. If a relation is a many to one then the coimage (\$coi) defines a partition. For more on domain structure see .See http://www.csci.csusb.edu/dick/maths/logic_42_Properties_of_Relation.html#coi . Weakest Preconditions The following idea comes from Dijkstra's Discipline of Programming. For any relation R and set of codomain objects A, there is a weakest precondition (largest set) of preconditions that guarantee that their objects can be related to at least one object in A: For R:@(T1,T2), A:@cod(R), wp(A,R) ::= {x:pre(R) || x.R==>A}, -- weakest pre-condition for A, .Close Domain Structure . Products of Relations Binary relations are PARALLEL operators. For R:@(T1,T2), S:@(T2,T3), x R y S z ::= x R y and y S z. For R:@(T1,T2), S:@(T2,T3), R;S::@(T1,T3) = rel[x:T1,y:T3](for some z:T2 (x R z S y)) |- R;S::=for some z:dom(S)( (1st)R z S (2nd) ). The semicolon is a SERIAL operator: (;(R,S,T,...)) ::=(R;S;T;...) . The Identity Relationship Id(X) ::= rel [x,y:T](x in X and x=y) . Algebra of Products MONOID::=http://www.csci.csusb.edu/dick/maths/math_33_Monoids.html |-\$MONOID. (MONOID)|- (@(X,X),(;), Id(X)) in \$Monoid ()|- R ; /R ==> Id(X) Beware of treating converse as if it cancels relations out since (finding an example)|-for all A,R, ( A==>a.R./R ) and for some A,R, ( a.R./R <> A ) .Open Relations between Subsets Given a pair of types each with subsets we can define the idea of `a relation between the subsets`. Notice that if A:@T1 and B:@T2 then x:A>b` is of type @(T1,T2) not of type @({a},{b}). So a relation's type `R:@(T2,T1)` is somewhat independent of its pre-image or domain of definition. This in turn leads to the property that a functions type `f:T2^T1` is independent of its pre-image or domain of definition. Since arrays are modeled as special kinds of functions, this means that an array of 10 integers has the same type as an array of 5 integers. Similarly for arrays of characters. Now equality is only defined between objects of the same type... it may be true or false, but at least defined! Therefore, the MATHS theory allows us to compare strings of characters. It is said that Nasrudin saw a mouse stagger out from the rubble fallen from a volcano that had just finished erupting and he laughed and saying "it took all that noise for the mountain to give birth to a mouse!" . Definitions For A:@T1, B:@T2, A>A and post(R)==>B. The relations between A and B are relations of type @(T1,T2). Thus in MATHS the domain of definition of a relation is a subset of the domain of the relation(a type) and equals its corange, similarly the range of the relation is a subset of its codomain. . Consequences ()|-For A:@T1, B:@T2, R:@(A,B), |/R=cor(R) in @dom(R) and |R=rng(R) in @cod(R) ()|-For A:@T1, B:@T2, R:Sets (R in @(A,B) iff R==>(A>b::= {(a,b)}=rel [x:T1, y:T2](x=a and y=b). |- For A:@T1, b:T2, A+>b::= {(a,b) :T1>