T2^T1 symbolises the maps from T1 and T2. Informally then, a map in T2^T1
takes an object of type T1 and returns a particular object of type T2.
Maps are also called functions or mappings. T2^T1 ( the collection of all
maps between T1 and T2) is also assumed to be a type:
- For all T1, T2: Types, T2^T1::Types.
The above means that we can apply all the tools of logic to maps
that we can to individuals. Thus we can have variables and
constants that refer to maps. We can have quantifiers applied to maps.
We will define a form of equality and be able to reason with it.
- set_of_maps::=set"^"simple_set_expression | set arrow set | "(" L(morphism) ")" set arrow set,
- MODELED_AS_RELATIONS::=
Net{
Given relationships then mappings must exist.
- We can assume that T2^T1 can be modeled as a set of special relations in @(T1,T2).
- T2^T1 --- (T1(any)-(1)T2),
- (above)|-T2^T1 -->@(T1,T2)
}=::
MODELED_AS_RELATIONS.
The defining property of functions is that they operate on objects to
produce other objects. For each map(=function) f from T1 to T2 and
for each x in T1 there is a corresponding element of T2 which is
written f(x) or x.f. Functions(=Maps) are used to build expressions.
- |- (fun1): For f:T2^T1, x:T1, f(x)=x.f ∈ T2.
- |- (fun2): For f:T3^(T1><T2), x:T1, y:T2, x f y=f(x,y)=(x,y).f ∈ T3
Prefix and suffix forms are equivalent but shouldn't be applied to a single argument. An expression like f(x).g is ambiguous and should be written as
- f(g(x))=x.g.f=f(x.g)=(g(x)).f,
or
- x.f.g=g(f(x))=(f(x)).g=g(x.f).
When several mappings are applied then either ';' or 'o' can be used:
- f(g(h(x)))=f o g o h(x)=x.h;g;f.
However sometimes the different forms can be mixed. For example, an expression like n.th(x) = (n.th)(x) and has type X when x:X^N, n:N, th: (X^(X^N))^N. Similarly an expression like 2.ft * 6.inch is ok and has type Area because ft, inch:Length^Number.
- |-For x:T1, y:T2, f:T2^T1, (x, y) in f iff x f y iff y=f(x) iff y=x.f.
- basic_map::=map_symbol loose_binding l_paren expression r_paren | map_symbol l_bracket L(loose_binding) r_bracket expression | maplet.
- maplet::= expression "+>" expression | Set_expression "+>" expression.
- map_symbol::="map" | "fun" | "λ".
You can in theory leave out the map symbol but it doesn't make expression any clearer.
map[x:T1](E) ::=The map taking each x of type T1 into E.
- x+>e::=The map taking x to e.
- X+>e::=The constant map taking each element in X to the value of e.
[ Elementary maps ]
You can replace "map" in the above by the Greek letter λ or the word "fun" if the audience would prefer them.
The Z operators that replace pairs of items that make up a map are defined as operations on relations.
[ Operations from Z in logic_40_Relations ]
[ Z-like Operators in logic_44_n-aryrelations ]
[ Map expressions ]
The subscript notation ([...]) is not necesary when there is just one
binding and the map_symbol is present. Subscripting is particular useful
when combined with a serial operator, in which case the subscript can be
typeset underneath an enlarged or specialised symbol:
+[i:1..n]i = n(n+1)/2 might look like this when printed:
____
\ n(n+1)
/ i = --------
---- 2
i:1..n
- For G:T3^(T2^T1), G[x:T1](E) ::=G(map[x:T1](E))
G[x:T1](E)
might be rendered like this
G (E)
x:T1
If E(x) is an expression of type T2 with free variable x of type T then for any expression e that returns a value of type T:
- For Types T,T2, x:variable, E(x):expression(T2), e:expression(T), (map [x:T](E(x)))(e)=(e).map [x:T](E(x)) = E(e) = (e).[x](E).
Notice that (e).([x]E) substitutes e for all free x in E:
Subs^(e)[x](E) ::=(e).([x]E)
or when printed
e
Subs (E).
x
Each many-1 relation entails a map.
- (relations)|-For R:T1(any)-(1)T2, R(x) =x.R = the (y:T2||x R y) in T2
Similarly,
- (relations)|-for all f:T2^T1, one R: @(T1,T2), all x:T1(x R f(x)).
MATHS will use the same symbol, but when function f appears in a context
demanding a set then it will be interpretted as a member of @(T1,T2) rather
than of T2^T2.
- For f:T2^T1, f::@(T1,T2) ={(x,f(x)) || x:dom(f)}
Notice that the domain of the function is the first or left-hand side of
the relation.
Normally an invese function is only defined on 1-to-1 functions. In
MATHS
when a function or map is between two known types then the inverse map
can be defined as follows:
- For f:T2^T1, /f::(@T1)^(T2) =map[y:T2]{x:T1 || y=f(x)},
- For f:T2^T1, /f::(@T1)^(@T2) =map[Y:@T2]{x:T1 || for some y:Y(y=f(x))},
Notice that if f is generic mapping any type T into a fixed type then
it should not be inverted.
- (euclid)|- (feq1): if f=g then dom(f)=dom(g) and cod(f)=cod(g) and for x in dom(f) (f(x)=g(x)).
- |- (feq2): if dom(f)=dom(g) and cod(f)=cod(g) and for x in dom(f) (f(x)=g(x)) then f=g
- (feq1, feq2)|- (feq): (f=q) iff ( dom(f)=dom(g) and cod(f)=cod(g) and for x:dom(f) ( f(x) = g(x) ).
- (relations)|- (maplet): For a:T1,b:T2, a+>b={(a,b)}=the({a}->{b})= fun[x:{a}](b).
- (relations)|- (exfel): (1,4,9)=(1+>2|2+>4|3+>9)in Nat^3.
- (relations)|- (felId): For X:@T, Id(X) = map [x:X](x).
- (relations)|- (const1): For A:@T1, b:T2, A+>b= { (a,b) || a:A} ∈ T2^T1.
- (relations)|- (const2): For A:@T1, b:T2, A+>b = |[a:A](a+>b) = the(A->{b}) = fun[x:A](b).
- (relations)|- (union): For A1,A2:@T1, b:T2, A1+>b | A2+>b = (A1|A2)+>b.
- (relations)|- (case): For A:#@T1, b:T2, |[i:pre(A)](A[i]+>b) = (|[i:pre(A)]A[i])+>b.
- (relations)|- (simple): {a}+>b=a+>b.
It is very useful to be able to use a finer classification of maps than between types. Commonly maps are defined between subsets of types:
- For A:@T1, B:@T2, A->B={f:T2^T1|| for all x:T1, if x in A then for some b in B ((x,b) in f) else for no y in T2((x,y) in f)}.
- Hence objects in A->B have type T2^T1 (not B^A).
Note well that this means that all maps between subsets of two types have the
same type. Thus a list of 3 characters and a list of 5 characters are of the
same type. Further the lists of 3 characters are disjoint from the lists of 5 characters.
Again note that the range of definition of a map is not necesarily a complete
type - thus all maps are partial maps... or to put it another
way all types have an "undefined" element, and elements outside the
domain of a function map into this element.
- |- (apply): for f:A->B, a:A, f(a) =(y:B||(a,y) in f)
- (relations)|- (funrel): A->B ==> @(A><B)
- (?)|- (fun_card1): for f:A->B, |f| =|A|
- (?)|- (fun_card2): |A->B|=|B|^|A|
The following is often called the Pigeon-hole principle by mathematicians.
It can be used as an effective validation and documentation method in formal analysis.
- (?)|- (pigeon_hole_1): For f:A->B, if f in A(n..m)-(1)B then for all b:B ( |b./f| in n..m) and n.|B|<=|A|<=m.|B|.
- (?)|- (pigeon_hole_1): For f:A->B, r:=(+[b:B]|b./f|)/|B|, if f in A(n..m)-(1)B then |A|=r*|B| and n<=r<=m.
Similarly, for a pair of maps: f:A->B and g:B->C, the multiplicities multiply:
- (?)|- (multmult): For f: A(n1..m1)-(1)B, g: B(n2..m2)-(1)C then f;g in A(n1*n2..m1*m2)-(1)C.
[click here pigeonhole if you can fill this hole]
The operator "->" is not associative:
- A->(B->C) <> (A->B)->C.
I am not sure what is the best definition for A->B->C.
Case
- A->B->C := A->(B->C).
(End of Case)
Case
- A->B->C := (A->B)->C.
(Close Case )
[click here if you can fill this hole]
Until resolved: avoid expressions like A->B->C.
Maps are special relations, so many properties are documented in that
section of the notes. In MATHS the type of a map in A->B depends on the
types of A and B (T1 and T2 respectively), and so the domain and codomain
are the T1 and T2, NOT A and B. However A is the corange of the map - its
domain of definition.
- (relations)|- (maprel1): img(f)= |(f)=f(cor(f))=f(dom(f)) ==> cod(f),
- (relations)|- (maprel2): cor(f)= |(/f)= /f(img(f)) ==> dom(f).
- (relations)|- (maprel3): For A,B, f:B^A,Y:@B, Y./f={x||for some y:Y(f(x)=y)})
- (relations)|- (maprel4): For A,B,C, f:B->C, g:A->B, x:A, g o f = f; g and g(f(x)) = (x.f).g = g o f(x) = x.f;g.
- (relations)|- (maprel5): For A, B:Sets, C:@A, g:A->B, C;g=Id(C);g= map x:C(g(c)) in C->B.
- (relations)|- (maprel6): For A, B, C :Sets, g:A->B, if B==>C then g;C=g;Id(C)= map x:C(g(c)) in A->C.
- For A,B,C:Sets, f:A->B, f:(C->A)->(C->B) ::=map [g:C->A] (f; g).
- (exempla)|-sqrt( (1,4,9)) =(1,4,9);sqrt={(1,1),(2,4),(3,9)};sqrt={(1,1),(2,2),(3,3)}= (1,2,3).
- For R:@(B,B), f:A->B, R mod f: @(A, A) ::= rel[a1,a2](f(a1) R f(a2).
- (-1)|- (funmod1): R mod f = f ; R; / f.
- (-2)|- (funmod2): (x1( = mod f) x2) = (x1 in x2.f./f).
A/f::={b./f:@A || for some b:B }.
- (-2)|- (funpart): A >== A/f <> A./f.
There is also a neat form of the axiom of choice:
- Choice::=Net{For all A,B:sets, R:A(any)-(some)B, some f:A->B( f==>R ).}.
- |- (axiom_of_choice): Choice.
A map in S1^S2 is isomorphic to a subset of S2><S1 and S3^S4 to a subset of S4><S3. Thus if f:S1^S2 and g:S3^S4 then f|g and f&g are also sets and relations. Sometimes they are also functions.
n particular, when S2&S4={}, we have f1|f2 in (S2|S4)->(S1|S3).
This makes it easy to express maps as the union of some elementary maps:
- (above)|-(1,4,9) =(1+>1 | 2+>4 | 3+>9)
- (above)|- (alt_def_if): if(P,x,y)=P.(true+>x | false+>y)
A common abreviation is
- if A then f else g fi::=(A;f | T~A;g)
- For T1,T2, f:T1<>->T2, x:T2, f|+>x::= f| (T1~pre(f))+>x.
- reverse = "" +> "" |+> reverse(rest) ! (1st)
A common construction for a case by case map is when we have a set of
mutually disjoint sets {A,B,...} and a different map expression for each
one (f,g,...). A useful abreviation is:
- For A,B,..., A&B={},... f, g,..., (A+>[x]f | B+>[x]g |...) ::=(A+>[x:A]f | B+>[x:B]g |...).
When complex this can be shown as a table:
.Table Dom Cod
.Row x:A f(x)
.Row x:B g(x)
...
.Close.Table
It is also valid to define maps piecemeal, with one definition per
case:
f::A->Y=... ,
f::B->Y=... ,
...
In all the notations if the various subsomains (A, B, ...) are disjoint
then the above defines a valid function with a unique value for each
item in A|B|... .
As a result then we have defined f: A|B|... ->Y.
If any of the cases overlap then one must prove that the same value is
determined in the ovrlap. For example, in the Real numbers, you can
define x^n as a product of n xs when n is a natural number, and
also as exp(y*log(x)) for Real & Positive y
because the two definitions are equal when y=n is a Natural number.
A useful operator (:=) changes a single value in a map:
(relations) |-for A,B, a:A, b:B, f:A->B, (a:=b)(f) ::= f over_ridden_by (a+>b).
- (above)|-f.(a:=b) = (a:=b)(f).
- (above)|-f.(a:=b) = f~(a+>f(a))|(a+>b).
Note 2009/05/22: the notation f'(a)=b is non-deterministic in that any map with
f(a)=b is acceptable. Avoid using the "'" with maps, functions, and arrays.
(An array is a function with a finite domain). Instead use f(a)' = b if you
want to use the prime notation to change one element of a map:
(f(a)' = b) ::= (a:=b)(f),
- over_ridden_by::= See http://cse.csusb.edu/dick/maths/logic_40_Relations.html#over_ridden_by
Similary there is a useful notation that (f,g) indicates a map when needed:
- For f:S1^S2 and g:S3^S4, f><g::(S1><S3)^(S2><S4))= map [x,y](f(x),g(y)).
- (exercise)|-for I,J:Finite(Nat), x:I->Real, y:J->Real, +(* o (x><y)) = +[(i,j):I><J](x[i]*y[j]) = +(x) * +(y).
Compare
Source: Jim Bachus, "Can Programming be liberated from the Von Neuman Bottleneck", The Turing Lectures (ACM 85)
In MATHS, a map is often treated as a projection of one set of objects into
another set. Given n such maps then they map an element into a
n-tpl. Suppose we have n maps: f1, f2, f3, ..., f[n] mapping from
X into Y1, Y2, Y3, ..., Y[n] respectively. Then we write
f[i]::X->Y[i]=map[x](f[i](x)),
(f[i], f[j]) ::X->Y[i]><Y[j]=map[x](f[i](x), f[j](x)),
(f[i], f[j], f[k]) ::X->Y[i]><Y[j]><Y[k]=map[x](f[i](x), f[j](x), Y[k]),
- and so on.
- For X:Sets, Y:#Sets, n:=|Y|, f:(1..n)->(X-> |(Y) ), g:1..m->img(f), x:X, f.g = map[i]( f.(g[i])).
In general this becomes the following definition
- For A,B,C:Sets, f:A->B, f::(C->A)->(C->B) = map [g:C->A ](f; g),
- (def)|-For A,B,C:Sets, f:A->B, g:C->A, f(g) = f;g = g o f
Developing the above further, we get the following ideas: First, an expression containing a map expresses a map:
- For A,B,C:Sets, f:B->C, g:A->B, f(g)::A->C=map[a:A](f(g(a)).
Second, let "(_)" symbolize the identity map:
- For Sets A, (_):A->A::=map[a](a).
So, an expression that contains "(_)" in one or more place, can define a map:
- square::Numbers->Numbers=(_)*(_),
- double::=(_)+(_),
- 4square::=square(double((_))).
The scope of the implicit "map" form (_) may appear ambiguous, however the definition of f(g) etc gives:
- g(map[x](f(x)), a) = map[x](g(f(x), a)= g(f(map[x](x)), a) = g(f((_)), a).
Functions of two or more arguments can be simply expressed by putting projection functions (1st,2nd,3rd,...rest,last,front,...n.th...) in expresssions.
- (1st)!(rest)= (front)!(last) ==> (_).
- swap2::X^2->X^2=(2nd,1st). |- (1st,2nd)=(_).
- sum::Binary_tree(Numbers)->Numbers,
- sum::=()+>0 |+> sum(1st)+sum(2nd).
We use the definitions for the application of a map to a pair of maps:
- For A,B,C:Sets, f:B->C, g1,g2:A->B, f(g1,g2)::A->C=map[a](f(g1(a), g2(a)).
- For A1,A2,B,C:Sets, f:B->C, g1:A1->B,g2:A2->B, f(g1,g2)::A1><A2->C=map[a1:A1, a2:A2](f(g1(a1), g2(a2))).
Maps inherit power operations (f^n, do(f), while(A)(f)) from relations:
[ logic_41_HomogenRelations.html ]
- (above)|- (powfun1): For X:Sets, f:X^X, n:0.., f^n in X^X.
- (above)|- (powfun2): For X:Sets, f:X^X, f^0 = Id(X) and f^1=f.
- (above)|- (powfun3): For X:Sets, f:X^X, n:2.., f^n = f o f^(n-1) = f^(n-1) o f .
- In general do(f) is not a map, however the following 'while(A)' does lead to a partial map
- (above)|- (while_fun1): For A:@T, while(A)=map [f]( do( A; f ); T~A)..
- (above)|- (while_fun2): For A:@T, f:T->T, while(A)(f) in T<>->T~A.
- (above)|- (While_fun3): cor(while(A)f) = {a:A || for some n:Nat0( f^n(a) in T~A}.
Iterated partial maps can have a well defined value:
- (above)|- (while_fun4): For T:Types, Y:@T, X:@X~{Y,{}}, f:X->Y, while(cor(f))f in T<>->T.
Source: Mills 72, Harlan D. Mills, Mathematical Foundations for Structured Programming, IBM Federal Systems Division (Report No. FSC 72-6012) Gettysburg MD Febuary 1972
- set_of_maps::=set arrow set|... .
- left_arrow::= "->" |">->" | ">--" |">==" |"==>" |"-->" |"---" |">=>"|...
The notation is inspired by the fact that every function can be decomposed
into three steps: (1) partition (>==), (2)bijection(---), (3)injection(==>).
For A,B,
- A left_arrow B ==> A->B,
- A>->B::= A->B,
- A<-<B::= B>->A,
- A---B::= {f:A->B||for all b in B(one a./f)}, -- -- --(bijection)
- A-->B::= {f:A->B||A---f(A)}, -- -- --(injection)
one-one.
- A<--B::= B-->A,
- A>--B::= {f:A->B||A/f---B}, -- -- --(surjection)
onto.
- A--<B::= B>--A,
Note. If the mapping also preserves a structure
[ Structure Preserving Maps ]
then we talk about:
morphisms, isomorphisms(bijection), epimorphisms(surjection), and monomorphisms(injections).
- For f:A---B, /f::B---A=map[x:B]the(/f{x}).
- For A,B, f:A---B, f^-1::= /f,
- (above)|- (recip): for A,B, f:A---B, f^-1 = the [g] (f;g=Id(B) and g;f=Id(A)),
- (above)|- (canon1): For f:A->B, dom(f)<==A=cor(f)>==coi(f)=cod(f)/f={b./f||b:cod(f)} and coi(f)---img(f)=rng(f)==>B==>cod(f),
- (above)|- (canon2): if f:A->B then A>==coi(f)=A/f---f(A)==>B,
- (above)|- (canon3): if f:A-->B then A---f(A)==>B,
- (above)|- (canon4): if f:A>--B then A>==A/f---B,
- (above)|- (canon5): for A, B, f:A->B ( f in A-->B iff for some g:B->A (g;f=Id(A)) ),
- (above)|- (canon6): for A, B, f:A->B ( f in A>--B iff for some g:B->A (f;g=Id(B)) ),
- (above)|- (canon7): for A, B, f:A->B ( f in A---B iff for one g:B->A (f;g=Id(B) & g;f=Id(A) ),
- (above)|- (canon8): for A, B ( A---B = A>--B & A-->B ).
- (above)|- (fun_monoid): Monoid( A->A, (;), Id(A)).
- (above)|- (fun_sub_monoid): ( A>--A) and ( A-->A) in sub_monoids(A->A).
- For A, endomorphisms(A)::=MONOID( Set=>A->A, op=>(;), unit=>Id(A)).
Monoids are defined and their properties are documented here:
- MONOID::= See http://cse.csusb.edu/dick/maths/math_33_Monoids.html#MONOID
- (above)|- (iso_group): Group( A---A, ;, Id(A), /).
- For A, automorphisms(A)::=GROUP(Set=>A---A, op=>(;), unit=>Id(A), inverse=>(/)).
- GROUP::= See http://cse.csusb.edu/dick/maths/math_34_Groups.html#GROUP
Laplace's theorem is almost a converse of this - any group is a subgroup of
a group of automorphisms. Finite groups can therefore be modeled as
sub-groups of permutations of the integers(1..n---1..n), without loosing
generallity.
- For A:@T1, B:@T2, C:@T3,a:A, b:B, c:C, map[a:A,b:B](c) ::= map[(a,b):(A><B)](c), ... .
- For A,B,C, A^B^C::=(A^B)^C.
- (above)|- (iso_triple): A^B^C --- A^(B><C) --- A^ (C >< B) --- A^C^B.
- For x:T1, y:T2, f:T^(T1><T2), f(x,y) = x f y = (x,y).f in T.
- For x:T1, y:T2, f:T^(T1><T2), z=f(x,y) iff ( (x, y, z) in f).
- For x:T1, y:T2, f:T^(T1><T2), if T1<>T2 then f::(T^T1)^T2=map[y]( map[x](x f y)),
- For x:T1, y:T2, f:T^(T1><T2), if T1<>T2 then f::(T^T2)^T1=map[x]( map[y](x f y)).
When T1=T=T2 - see Math.STANDARD.INFIX
- For f:(B><C)(any)-(1)A, b:B, c:C, a:A, b f c = f(b,c) in A.
Notice that if f:T1^T2^T3, z:T3, y:T2 then f(z) in T2><T1 and (f(z))(y) in T1 and (f(z))(y) = (g(y))(z) = h(z,y) for unique g:T1^T3^T2 and h:T1^(T2><T3).
However when T2 and T3 are different we can use f to stand for g and h when in a context demanding a function of the type.
However, normally it is not true that (A^(B^C) --- A^B^C).
Here are the strongest results that hold for mapping sets into sets.
- (sets)|- (f1): For f:X->Y, A1,A2:@X, B1,B2:@Y, f({})={}.
- (sets)|- (f2): For f:X->Y, A1,A2:@X, B1,B2:@Y,/f({})={}.
- (sets)|- (f3): For f:X->Y, A1,A2:@X, B1,B2:@Y,for all x:X( x in A iff f(x) in f(A) ).
- (sets)|- (f4): For f:X->Y, A1,A2:@X, B1,B2:@Y,for all x:X( f(x) in A iff x in /f(A) ).
- (sets)|- (f5): For f:X->Y, A1,A2:@X, B1,B2:@Y,(if A1 ==> A2 then f(A1) ==> f(A2)).
- (sets)|- (f6): For f:X->Y, A1,A2:@X, B1,B2:@Y,(if B1 ==> B2 then /f(B1) ==> /f(B2)).
- (sets)|- (f7): For f:X->Y, A1,A2:@X, B1,B2:@Y,f(A1 | A2) = f(A1) | f(A2) and /f(B1 | B2) = /f(B1) | /f(B2).
- (sets)|- (f8): For f:X->Y, A1,A2:@X, B1,B2:@Y, f(A1 & A2)==>f(A1) & f(A2) and /f(B1 & B2) = /f(B1) & /f(B2).
- (sets)|- (f9): For f:X->Y, A1,A2:@X, B1,B2:@Y, f(A1~A2)<==f(A1)~f(A2) and /f(B1~B2)= /f(B1)~/f(B2).
- (sets)|- (f10): For f:X->Y, f o /f ==> Id ==> /f o f.
- (sets)|- (f11): For f:X->Y, (f o /f = Id iff f:X>--Y).
- (sets)|- (f12): For f:X->Y, (/f o f = Id iff f:X-->Y).
- (sets)|- (f13): For f:X->Y, (f o /f = Id = /f o f iff f:X---Y).
- (sets)|- (f13): For X,Y:Sets, f:X>--Y, P:Y->@( for all x:X (P(f(x)) iff for all y:Y(P(y))).
- (sets)|- (f14): For f:X->Y, g:Y->Z, /(f;g)=/g;/f.
- (sets)|- (f15): For f:X->Y, g:Y->Z, A:#X, ( g o f )(A)=g(f(A)).
- (sets)|- (f16): For f:X->Y,For all X:Sets, POSET(@X, ==>).
- (sets)|- (f17): For f:X->Y,For f:X->Y, f:@X->@Y and /f:@Y->@X in continuous.
- (sets)|- (CSB): For all X,Y, if some X-->Y and some Y-->X then some X---Y.
For any well formed formula W(x,y) with x:X and y:Y the following is assumed:
- for all x:X, some y:Y (W(x,y)) iff for some f:X->Y, all x:X (W(x, f(x))).
In general this is tantamount to assuming the axiom of choice. The function f is called a Skolem function and this leads to ways of extending Prolog and also underlies the common mathematical idiom:
- For all η>0, there is a δ(η) such that.....
- |- (Skolem): For W(x,y):wff(for all x:X, some y:Y (W(x,y))) iff (for some f:X->Y, all x:X (W(x, f(x))))
Any many cases there are a class of maps between to structures that
preserve the structure in some special way. These are called 'morphisms'.
The simplest set of morphisms are those which preserve or transmit a
particular operation or map faithfully.
- For f,g:X->X, f commutes g::= (f;g=g;f).
As a rule a notation like
- (0,+,-)Int->Int
is the set of maps that preserve the value 0 and the operations
of addition and negation: the linear map.
- For X,Y, g:(X->X|Y->Y), (g)X->Y::={f:X->Y || for all x( f(g(x)=g(f(x)) )}.
- For X,Y, o:(X><X->X | Y><Y->Y), (o)X->Y::= {f:X->Y || for all x1,x2:X( f(x1 o x2)=f(x1) o f(x2)) }.
- For X,Y, x:X, (x)X->Y::={f:X->Y || f(x) = x:Y )}.
- For X,Y, a,b, (a, b)X->Y ::= ((a)X->Y) & ((b)X->Y).
Hence, for L a list of operations (o1,o2,o3,...):
- For L:#operations, f:L X->Y::=&{(o)X->Y || o:img(L)}
Special names are used for morphisms which are one-one and/or onto:
- For A,B:Sets, L:list of structures, L A---B::={f:L A->B || for all b in B(one a./f) and /f:L B->B}-- L isomorphism.
- isomorphism::=maps that are one to one and onto and preserve a structure.
- For A,B:Sets, L:list of structures, L A-->B::={f:L A->B || f:L A---f(A)} -- L monomorphism
- monomorphism::=maps that are one to one and preserve a structure.
- For A,B:Sets, L:list of structures, L A>--B::= {f:L A->B || f:L A/f---B} -- L epimorphism.
- epimorphism::=maps that are onto and preserve a structure.
Suppose that p:T->X and R:Finite_set(T)~{}, then p(R) is the image of R
under p. When p is (1)-(1) then the image is isomorphic to R. In this
case there is no loss of information in using p(R) in place of R. In data
base terms p can act as an identifier of the relation R:
- |- (proj1): p in ids(R) iff p in R---p(R) iff p in R-->X.
Suppose that p:T->X, q:T->Y, and R:Finite_set(T)~{}, then p(R) and q(R) are
the images of R under p and q respectively. If either p or q is (1)-(1)
then the associated image is isomorphic to R. Suppose that this is not so,
then both p and q destroy information when applied to R. It is still
possible for p and q together to carry enough data to enable R to be
reconstructed.
Thus consider
- |- (proj2): S = {(p(r), q(r)):X><Y || r:R } in @(X,Y).
First note that
- (above)|-S = /p;R;q and /S = /q;R;p.
Now consider the following special cases:
If i:S---R and for all r:R (i(p(r),q(r))=r)
then the maps p and q are orthogonal co-ordinates for R. In data base terms (p,q):R---S can act as an identifier of the relation R: (p,q) in ids(R). In categorical terms (p,q) are cannonical morphisms establishing a product (X><Y).
When S (the image of R under (p,q)) is itself a map then q is Functionally dependent on p with respect to R:
- For R, X, Y,p,q, (R) p->q ::= /p;R;q in X(any)-(0,1)Y.
In general,
- For R, X, Y,p,q, a:arrow, (R) p a q ::= /p;R;q in p(R) a q(R).
A data base has many entities and/or relations - finite subsets of
types - with mappings between them. The data base specifies the type of
each entity/relationship R and its special identifier. The identifier is
called the key of the entity or relation. For an entity E write
structure(E) for the type of elements in the set and key(E) the key,
then for R to be a valid entiry/relation of type E then key(E) in ids(R).
Further R is in third normal form (3NF) if whenever (R)p->q then
p=key(R). Notice that,(1) the key must be an identifier(1NF), (2) If
(R)p->q then the whole of p must be whole the key(2NF), and (3) if
(R)r->q then r must be the key as well (3NF).
In other words the complete logical structure of a data base can be described by specifying the relations and their key identifiers alone.
. . . . . . . . . ( end of section Special cases) <<Contents | End>>
Functions are equivalent to special types of relations. We could have defined functions as special binary relations - special sets of pairs. The reverse is possible - we could have started with functions and defined pairs in terms of projection functions, and sets as maps into the set of {true, false}, and so on. In practice we make use of all equivalent formulations according to what is most inspiring and expressive for the current need.