.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> @(A,B).
(above)|- For R:@(T1,T2), A:@T1, B:@T2, A;R;B = R & @(A,B).
Thus in MATHS we avoid the need for special symbols or words to indicate
the limiting of relations used in other systems - Principia Mathematica
and Z for example.
The following abbreviations are natural and unambiguous:
x R y and z...::= x R y and x R z and...
x and y and...Rz::= x R z and y R z and ... [Compare COBOL relations]
.Close Abuses of notation
.Open Operations Used in Formal Specifications
The following are not developed from philosophical or theoretical reasons.
They are created and documented because they are needed to make formal
specifications easier to write and read.
. "Or else"
It is very useful to have special operation that makes a relation total by
linking all the unconnected objects in the domain to an item in the
codomain:
For T1,T2,R, b:T2, R|+>b:@(T1,T2) ::= R | ( (T2~pre(R))+>b ).
Read `|+>` as `or else`.
. An Operation used in the Formal Semantics of Programming languages
In programming we have an assigment operator:
variable := expression;
(Ada, Algol 60 Ada, and Pascal notation).
It indicates that the value associated with the variable is changed to the
value of the expression. In abstract we often want to change
a single value in an array (map) of values like this:
(a,b,c) = (1+>a | 2+>b | 3+>c).
(a,b,c).(2:=x) = (a,x,c).
Here is the formal definition:
For T1,T2, f:T1->T2, v:pre(f), e:T2, f.(v:=e) ::= f~>(v+>e).
The "~>" is the $over_ridden_by operator defined in the next section.
Other books
.Source Nielson & Nielson 92
.See [NielsonNielson92]
use a notation like this
`f [ v +> e]` = f.(v:=e).
This is a handy model for: the state of the RAM in a computer, changing an
item in an array, operating on a direct access file, changes in registers
in a processor, ...
.See http://www/dick/maths/math_14_Dynamics.html#RAM
. Operations from Z
The Z(Zed) notation comes from
research in Europe. Abrial and the Oxford PRG
discovered that a particular operation on relations
is useful for specifying many different problems and domains. In many
specification written in Z the idea of modifying a relation by removing
items that don't lie in a subset of the domain or codoman is quite common.
A \dashed_triangle_left R ::= ~A;R.
()|-(dtl): A \dashed_triangle_left R ={(x,y) :T1> S ::serial(@(T1,T2)) = R \circle_plus S.
over_ridden_by ::= map[R,S] ( R ~> S ).
In Z these are typically used to represent the behavior that is implemented
by classical data structures and files. There is a more abstract model
found in SSADM or OOA/D where dynamics is defined by a network of
interacting and cooperating processes, from which the files (if any) and
other data structures are developed to meet various performance criteria.
.See http://www/dick/maths/logic_44_n-aryrelations.html#Z-like Operators
.Close Operations from Z
.Close Binary relations
**