.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 . 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 ... As a result (if A&B = {} etc) then we have defined f: A|B|... ->Y. . 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.(a:=b) = f~(a+>f(a))|(a+>b). .See http://www/dick/maths/logic_40_Relations.html#Operations from Z 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)) and ( A>--A),( A-->A) in sub_monoids(A->A). For A, endomorphisms(A) ::=$MONOID( Set=>A->A, op=>(;), unit=>Id(A)). (above)|- (iso_group): Group( A---A, ;, Id(A), /). For A, automorphisms(A) ::=$GROUP(Set=>A---A, op=>(;), unit=>Id(A), inverse=>(/)). 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