[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / logic_5_Maps
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun Oct 2 12:01:36 PDT 2011


    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:

    1. 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.

    2. set_of_maps::=set"^"simple_set_expression | set arrow set | "(" L(morphism) ")" set arrow set,

      Note -- Relations imply maps

        Given relationships then mappings must exist.
      1. We can assume that T2^T1 can be modeled as a set of special relations in @(T1,T2).
      2. T2^T1 --- (T1(any)-(1)T2),
      3. (above)|-T2^T1 -->@(T1,T2)


      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.
    4. |- (fun1): For f:T2^T1, x:T1, f(x)=x.f ∈ T2.
    5. |- (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

    6. f(g(x))=x.g.f=f(x.g)=(g(x)).f, or
    7. x.f.g=g(f(x))=(f(x)).g=g(x.f).

      When several mappings are applied then either ';' or 'o' can be used:

    8. 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.

    9. |-For x:T1, y:T2, f:T2^T1, (x, y) in f iff x f y iff y=f(x) iff y=x.f.

      Expressions that are maps

    10. basic_map::=map_symbol loose_binding l_paren expression r_paren | map_symbol l_bracket L(loose_binding) r_bracket expression | maplet.
    11. maplet::= expression "+>" expression | Set_expression "+>" expression.
    12. map_symbol::="map" | "fun" | "λ".


      You can in theory leave out the map symbol but it doesn't make expression any clearer.

      Example map expressions

        map[x:T1](E) ::=The map taking each x of type T1 into E.

      1. x+>e::=The map taking x to e.

      2. 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: Missing Graphic

       \         n(n+1)
       /    i	= --------
       ----        2

    13. For G:T3^(T2^T1), G[x:T1](E) ::=G(map[x:T1](E))
      might be rendered like this
         G (E)

      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:

    14. 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 To_be_done

      	Subs   (E).

      Maps and Relations

      Each many-1 relation entails a map.
    15. (relations)|-For R:T1(any)-(1)T2, R(x) =x.R = the (y:T2||x R y) in T2


    16. (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.

    17. 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:
    18. For f:T2^T1, /f::(@T1)^(T2) =map[y:T2]{x:T1 || y=f(x)},
    19. 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

    20. (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)).

    21. |- (feq2): if dom(f)=dom(g) and cod(f)=cod(g) and for x in dom(f) (f(x)=g(x)) then f=g

    22. (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

    23. (relations)|- (maplet): For a:T1,b:T2, a+>b={(a,b)}=the({a}->{b})= fun[x:{a}](b).
    24. (relations)|- (exfel): (1,4,9)=(1+>2|2+>4|3+>9)in Nat^3.
    25. (relations)|- (felId): For X:@T, Id(X) = map [x:X](x).

    26. (relations)|- (const1): For A:@T1, b:T2, A+>b= { (a,b) || a:A} ∈ T2^T1.
    27. (relations)|- (const2): For A:@T1, b:T2, A+>b = |[a:A](a+>b) = the(A->{b}) = fun[x:A](b).
    28. (relations)|- (union): For A1,A2:@T1, b:T2, A1+>b | A2+>b = (A1|A2)+>b.
    29. (relations)|- (case): For A:#@T1, b:T2, |[i:pre(A)](A[i]+>b) = (|[i:pre(A)]A[i])+>b.
    30. (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:

    31. 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)}.

    32. 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.

    33. |- (apply): for f:A->B, a:A, f(a) =(y:B||(a,y) in f)
    34. (relations)|- (funrel): A->B ==> @(A><B)

      Quantified Maps and Functions and Multiplicities and Cardinalities

    35. (?)|- (fun_card1): for f:A->B, |f| =|A|
    36. (?)|- (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.

    37. (?)|- (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|.
    38. (?)|- (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:

    39. (?)|- (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 [socket symbol] pigeonhole if you can fill this hole]

      Notations A->B->C

      The operator "->" is not associative:
    40. A->(B->C) <> (A->B)->C.

      I am not sure what is the best definition for A->B->C.

      1. A->B->C := A->(B->C).

      (End of Case)
      1. A->B->C := (A->B)->C.

      (Close Case )

      [click here [socket symbol] if you can fill this 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.
    41. (relations)|- (maprel1): img(f)= |(f)=f(cor(f))=f(dom(f)) ==> cod(f),
    42. (relations)|- (maprel2): cor(f)= |(/f)= /f(img(f)) ==> dom(f).
    43. (relations)|- (maprel3): For A,B, f:B^A,Y:@B, Y./f={x||for some y:Y(f(x)=y)})
    44. (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.
    45. (relations)|- (maprel5): For A, B:Sets, C:@A, g:A->B, C;g=Id(C);g= map x:C(g(c)) in C->B.
    46. (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.

    47. For A,B,C:Sets, f:A->B, f:(C->A)->(C->B) ::=map [g:C->A] (f; g).
    48. (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).

    49. For R:@(B,B), f:A->B, R mod f: @(A, A) ::= rel[a1,a2](f(a1) R f(a2).
    50. (-1)|- (funmod1): R mod f = f ; R; / f.
    51. (-2)|- (funmod2): (x1( = mod f) x2) = (x1 in x2.f./f).

      A/f::={b./f:@A || for some b:B }.

    52. (-2)|- (funpart): A >== A/f <> A./f.

      There is also a neat form of the axiom of choice:

    53. Choice::=Net{For all A,B:sets, R:A(any)-(some)B, some f:A->B( f==>R ).}.

    54. |- (axiom_of_choice): Choice.

      Map expressions

      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:

    55. (above)|-(1,4,9) =(1+>1 | 2+>4 | 3+>9)
    56. (above)|- (alt_def_if): if(P,x,y)=P.(true+>x | false+>y)

      A common abreviation is

    57. if A then f else g fi::=(A;f | T~A;g)

      Completing a partial map

    58. For T1,T2, f:T1<>->T2, x:T2, f|+>x::= f| (T1~pre(f))+>x.

      Example Completing a partial map

    59. 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:

    60. 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)

      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.

      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).

    61. (above)|-f.(a:=b) = (a:=b)(f).
    62. (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),

    63. over_ridden_by::= See http://cse.csusb.edu/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:
    64. For f:S1^S2 and g:S3^S4, f><g::(S1><S3)^(S2><S4))= map [x,y](f(x),g(y)).

      Example: Innerproduct

    65. (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).


      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], 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]),

    66. and so on.

    67. 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

    68. For A,B,C:Sets, f:A->B, f::(C->A)->(C->B) = map [g:C->A ](f; g),
    69. (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:

    70. 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:

    71. For Sets A, (_):A->A::=map[a](a).

      So, an expression that contains "(_)" in one or more place, can define a map:

    72. square::Numbers->Numbers=(_)*(_),
    73. double::=(_)+(_),
    74. 4square::=square(double((_))).


      The scope of the implicit "map" form (_) may appear ambiguous, however the definition of f(g) etc gives:
    75. 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.

    76. (1st)!(rest)= (front)!(last) ==> (_).
    77. swap2::X^2->X^2=(2nd,1st). |- (1st,2nd)=(_).
    78. sum::Binary_tree(Numbers)->Numbers,
    79. sum::=()+>0 |+> sum(1st)+sum(2nd).

      We use the definitions for the application of a map to a pair of maps:

    80. For A,B,C:Sets, f:B->C, g1,g2:A->B, f(g1,g2)::A->C=map[a](f(g1(a), g2(a)).
    81. 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))).

      Powers of maps

      Maps inherit power operations (f^n, do(f), while(A)(f)) from relations: [ logic_41_HomogenRelations.html ]

    82. (above)|- (powfun1): For X:Sets, f:X^X, n:0.., f^n in X^X.
    83. (above)|- (powfun2): For X:Sets, f:X^X, f^0 = Id(X) and f^1=f.
    84. (above)|- (powfun3): For X:Sets, f:X^X, n:2.., f^n = f o f^(n-1) = f^(n-1) o f .
    85. In general do(f) is not a map, however the following 'while(A)' does lead to a partial map
    86. (above)|- (while_fun1): For A:@T, while(A)=map [f]( do( A; f ); T~A)..
    87. (above)|- (while_fun2): For A:@T, f:T->T, while(A)(f) in T<>->T~A.
    88. (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:

    89. (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

    90. set_of_maps::=set arrow set|... .
    91. 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,

    92. A left_arrow B ==> A->B,
    93. A>->B::= A->B,
    94. A<-<B::= B>->A,
    95. A---B::= {f:A->B||for all b in B(one a./f)}, -- -- --(bijection)
    96. A-->B::= {f:A->B||A---f(A)}, -- -- --(injection)
    97. A<--B::= B-->A,
    98. A>--B::= {f:A->B||A/f---B}, -- -- --(surjection)
    99. 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).

      Inverse of bijections and isomormorphisms

    100. For f:A---B, /f::B---A=map[x:B]the(/f{x}).

    101. For A,B, f:A---B, f^-1::= /f,
    102. (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

    103. (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),
    104. (above)|- (canon2): if f:A->B then A>==coi(f)=A/f---f(A)==>B,
    105. (above)|- (canon3): if f:A-->B then A---f(A)==>B,
    106. (above)|- (canon4): if f:A>--B then A>==A/f---B,
    107. (above)|- (canon5): for A, B, f:A->B ( f in A-->B iff for some g:B->A (g;f=Id(A)) ),
    108. (above)|- (canon6): for A, B, f:A->B ( f in A>--B iff for some g:B->A (f;g=Id(B)) ),
    109. (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) ),
    110. (above)|- (canon8): for A, B ( A---B = A>--B & A-->B ).

    111. (above)|- (fun_monoid): Monoid( A->A, (;), Id(A)).
    112. (above)|- (fun_sub_monoid): ( A>--A) and ( A-->A) in sub_monoids(A->A).

    113. For A, endomorphisms(A)::=MONOID( Set=>A->A, op=>(;), unit=>Id(A)).

      Monoids are defined and their properties are documented here:

    114. MONOID::= See http://cse.csusb.edu/dick/maths/math_33_Monoids.html#MONOID

    115. (above)|- (iso_group): Group( A---A, ;, Id(A), /).
    116. For A, automorphisms(A)::=GROUP(Set=>A---A, op=>(;), unit=>Id(A), inverse=>(/)).

    117. 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.

      Maps into maps

    118. 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), ... .
    119. For A,B,C, A^B^C::=(A^B)^C.
    120. (above)|- (iso_triple): A^B^C --- A^(B><C) --- A^ (C >< B) --- A^C^B.
    121. For x:T1, y:T2, f:T^(T1><T2), f(x,y) = x f y = (x,y).f in T.
    122. For x:T1, y:T2, f:T^(T1><T2), z=f(x,y) iff ( (x, y, z) in f).
    123. For x:T1, y:T2, f:T^(T1><T2), if T1<>T2 then f::(T^T1)^T2=map[y]( map[x](x f y)),
    124. 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

    125. 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).

      Maps and Sets

      Here are the strongest results that hold for mapping sets into sets.
    126. (sets)|- (f1): For f:X->Y, A1,A2:@X, B1,B2:@Y, f({})={}.
    127. (sets)|- (f2): For f:X->Y, A1,A2:@X, B1,B2:@Y,/f({})={}.
    128. (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) ).
    129. (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) ).
    130. (sets)|- (f5): For f:X->Y, A1,A2:@X, B1,B2:@Y,(if A1 ==> A2 then f(A1) ==> f(A2)).
    131. (sets)|- (f6): For f:X->Y, A1,A2:@X, B1,B2:@Y,(if B1 ==> B2 then /f(B1) ==> /f(B2)).
    132. (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).
    133. (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).
    134. (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).
    135. (sets)|- (f10): For f:X->Y, f o /f ==> Id ==> /f o f.
    136. (sets)|- (f11): For f:X->Y, (f o /f = Id iff f:X>--Y).
    137. (sets)|- (f12): For f:X->Y, (/f o f = Id iff f:X-->Y).
    138. (sets)|- (f13): For f:X->Y, (f o /f = Id = /f o f iff f:X---Y).
    139. (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))).

    140. (sets)|- (f14): For f:X->Y, g:Y->Z, /(f;g)=/g;/f.
    141. (sets)|- (f15): For f:X->Y, g:Y->Z, A:#X, ( g o f )(A)=g(f(A)).

    142. (sets)|- (f16): For f:X->Y,For all X:Sets, POSET(@X, ==>).
    143. (sets)|- (f17): For f:X->Y,For f:X->Y, f:@X->@Y and /f:@Y->@X in continuous.

      The Cantor-Schroeder-Bernstein Theorem

    144. (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:

    145. 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:

    146. For all η>0, there is a δ(η) such that.....
    147. |- (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.

    148. For f,g:X->X, f commutes g::= (f;g=g;f).

      Structure Preserving Maps

      As a rule a notation like
    149. (0,+,-)Int->Int is the set of maps that preserve the value 0 and the operations of addition and negation: the linear map.

    150. For X,Y, g:(X->X|Y->Y), (g)X->Y::={f:X->Y || for all x( f(g(x)=g(f(x)) )}.
    151. 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)) }.
    152. For X,Y, x:X, (x)X->Y::={f:X->Y || f(x) = x:Y )}.

    153. 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,...):

    154. 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:

    155. 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.
    156. isomorphism::=maps that are one to one and onto and preserve a structure.
    157. For A,B:Sets, L:list of structures, L A-->B::={f:L A->B || f:L A---f(A)} -- L monomorphism
    158. monomorphism::=maps that are one to one and preserve a structure.
    159. For A,B:Sets, L:list of structures, L A>--B::= {f:L A->B || f:L A/f---B} -- L epimorphism.
    160. 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:

    161. |- (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

    162. |- (proj2): S = {(p(r), q(r)):X><Y || r:R } in @(X,Y).

      First note that

    163. (above)|-S = /p;R;q and /S = /q;R;p.

      Now consider the following special cases:

      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).

        Functional Dependencies

        When S (the image of R under (p,q)) is itself a map then q is Functionally dependent on p with respect to R:
      1. For R, X, Y,p,q, (R) p->q ::= /p;R;q in X(any)-(0,1)Y.

        In general,

      2. 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>>

      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.

    . . . . . . . . . ( end of section Maps and Functions) <<Contents | End>>

    Notes on MATHS Notation

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

    For a complete listing of pages in this part of my site by topic see [ home.html ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html


  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.