.Open Maps and Functions
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,
. Note -- Relations imply maps
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.
. Applying functions and maps
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 \in T2.
|-(fun2): For f:T3^(T1>" expression | Set_expression "+>" expression.
map_symbol::="map" | "fun" | "\lambda".
. Note
You can in theory leave out the `map symbol` but it doesn't make expression any clearer.
.Open Example map expressions
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`.
.See Elementary maps
.Close
You can replace "map" in the above by the Greek letter \lambda 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.
.See http://www/dick/maths/logic_40_Relations.html#Operations from Z
.See http://www/dick/maths/logic_44_n-aryrelations.html#Z-like Operators
.See 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:
.Image summation.gif Missing Graphic
.As_is ____
.As_is \ n(n+1)
.As_is / i = --------
.As_is ---- 2
.As_is i:1..n
For G:T3^(T2^T1), G[x:T1](E) ::=G(map[x:T1](E))
.As_is G[x:T1](E)
might be rendered like this
.As_is G (E)
.As_is 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
.Image substitution.gif To_be_done
.As_is
.As_is e
.As_is Subs (E).
.As_is x
. Maps and Relations
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.
. Inverse functions and Maps
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.
. Equality of functions/Maps
(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) ).
. Elementary Maps/Functions
(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} \in 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.
. Maps between subsets of types.
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, |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.
.Hole pigeonhole
. Notations A->B->C
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).
.Else
A->B->C := (A->B)->C.
.Close.Case
.Hole
Until resolved: avoid expressions like `A->B->C`.
. Maps as Relations
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.
. Map expressions
A map in S1^S2 is isomorphic to a subset of S2>(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)
. Completing a partial map
For T1,T2, f:T1<>->T2, x:T2, f|+>x::= f| (T1~pre(f))+>x.
. Example Completing a partial map
reverse = "" +> "" |+> reverse(rest) ! (1st)
. Case by Case definitions
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:
.As_is .Table Dom Cod
.As_is .Row x:A f(x)
.As_is .Row x:B g(x)
.As_is ...
.As_is .Close.Table
It is also valid to define maps piecemeal, with one definition per
case:
.As_is f::A->Y=... ,
.As_is f::B->Y=... ,
.As_is ...
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 `x`s 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.
. Assignment to elements in a Map
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).
()|- f.(a:=b) = (a:=b)(f).
()|-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::=http://www/dick/maths/logic_40_Relations.html#over_ridden_by
. Expressions containing maps and functions
Similary there is a useful notation that (f,g) indicates a map when needed:
For f:S1^S2 and g:S3^S4, f>Real, y:J->Real, +(* o (x>Y[i]=map[x](f[i](x)),
(f[i], f[j]) ::X->Y[i]>Y[i]>(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((_))).
. Note
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.
. Example of 1st, 2nd etc.
(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>C=map[a1:A1, a2:A2](f(g1(a1), g2(a2))).
. Powers of maps
Maps inherit power operations (f^n, do(f), while(A)(f)) from relations:
.See http://www/dick/maths/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
. Arrow Notation
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<-->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----A,
Note. If the mapping also preserves a structure
.See Structure Preserving Maps
then we talk about:
morphisms, isomorphisms(bijection), epimorphisms($surjection), and monomorphisms($injections).
. Inverse of bijections and isomormorphisms
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)),
. Canonical Decompositions of arrows
(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::=http://www/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::=http://www/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.
. Maps into maps
For A:@T1, B:@T2, C:@T3,a:A, b:B, c:C,map[a:A,b:B](c) ::= map[(a,b):(A>****< B) --- A^C^B.
For x:T1, y:T2, f:T^(T1>T2 then f::(T^T1)^T2=map[y]( map[x](x f y)),
For x:T1, y:T2, f:T^(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>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.
. The Cantor-Schroeder-Bernstein Theorem
(sets)|-(CSB): For all X,Y, if some X-->Y and some Y-->X then some X---Y.
. Quantifiers and Skolem functions
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 \eta>0, there is a \delta(\eta) 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))))
. Morphisms and Commutative Maps
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).
. Structure Preserving Maps
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 | 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`.
. Images of finite sets under one or more maps
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>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).
. Normalization
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.
.Close Special cases
. Pairs and functions
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.
.Close Maps and Functions
**