.Open Functions and Maps Functions are an important model of all computations that convert input data into output data, without changing anything else. This introduces set theory from the point of view of a computer proffesional using ASCII. For the traditional notation see .See http://www.math.csusb.edu/notes/func/func.html Theory shows that any computation can be modelled by combining some simple functions together by some simple rules. A variation of the theory lead to several important languages: LISP, CPL, and ML. In practice we can not have expressions in a language without having operations, and operations have to be functions. However in many languages a function is more than a mathematical 'pure function'. In these languages a function also makes visible changes in the the values of variables. In C a function can even fail to calculate a value and can be a a procedure. These are best modelled as relations rather than functions (In my humble opinion). All functions have a domain in which they are defined and a co-domain in which their defined values appear. For instance, the square root function sqrt for real numbers has the positive reals as its domain of definition and the reals as its co-domain. . Simple Functions A function is a binary relation that associates every element in its domain with a single, unique and existing element in its codomain (target set). A -> B::=Set of functions mapping objects of type A into B, For f:A -> B and for all a:A there is one b:B such that b=f(a). Similarly (A> C are functions mapping two operands (one in A, and one in B) into a result in C. Addition is an example. If f:A> C we can write it between its operands: a f b ::=f(a,b) and a f b in C. So + in int> int as an example. An intuitive notation for simple functions is the "blank space" function "(_)" which is put in an expression where the argument will be put: sqr::int -> int = (_)*(_). Functions of two arguments can be written with '(1st)' and "(2nd)" in place of the first and second arguments add::int> int =The sum of (1st) and (2nd), (add)|- add(1,2) = The sum of 1 and 2. . Example of a simple function hypotenuse::real> real=sqrt(add(sqr(1st),sqr(2nd))). Higher order functions, and theories need more complicated notations like those defined next. . More complex functions When we want to define a new function and give it a name we use For variable:Domain,..., name(arguments) ::=expression. For example: For x:Real, sqr(x) ::=x*x. For x,y:Real, hypotenuse(x,y) ::=sqrt(sqr(x)+sqr(y)). Functions are often expressed as \lambda expressions \lambda arguments.expression The \lambda notation was the first notation that let us describe a function without actually giving a name: \lambda x.x*x. The above means the function that maps each x into its square. The standard MATHS notation for the function that associates each x in T with a value e(x) is: map[x:T](e(x)) or fun[x:T](e(x)). Thus we can write: sqr=fun [x:Real](x*x), Notice. fudge::=fun[x:Natural](3*x+1) gives a name to the function. This is like C..... .As_is unsigned int fudge(unsigned int x) .As_is { return 3*x+1; .As_is } However 'fun[x:Natural](3*x+1)' is still a function even if we don't give it a special name. We can use a function without having to name it. The 'fun' forms are best used when we need to express a function that doesn't need to be named. For example suppose For x:Integers, f(x) ::=0, g(x) ::=x+1, h(x) ::=x*x. then g=fun[x](x+1), h=fun[x](x*x), and g=(_)+1, h=(_)*(_), The extended XBNF includes definitions like the following For x:A, f(x) ::B=e. It means: f::A -> B = fun[x:A](e). (f is the map from A to B which takes x and returns x e). Or in simple cases: f::A -> B= e'. where e' has each free x replaced by "(_)",.... For example, three definitions of a trebling function: For i:Nat, treble(i)::=3*i. treble::Nat->Nat = fun[ i:Nat](3*i). treble::Nat->Nat = 3*(_). As in other areas of XBNF, a definition like .As_is f::A -> B=e. is logically a combination of a declaration and an equallity .As_is f::A -> B, .As_is |- f=e. We can now also write higher order functions or functors that produce functions and act on functions: For f:int->int, selfapply(f) ::=fun[x:int]( f(f(x)) ). For f:A->B, g:B->C, g o f ::= fun[x:A]( g(f(x)) ). These have the same meaning as the unparameterized definitions: selfapply::=fun[f:int->int](fun[x:int]( f(f(x)) )). o::= fun[f:A->B, g:B->C](fun[x:A]( g(f(x)) )). The most natural way however is to declare the function and then add some properties: For f:int->int, sum(f) ::int->int=fun[n:int](sum i:0..n of f(i)). For f:int->int, n:int, if 0>n then sum(f)(n)=0. For f:int->int, n:int, if 0=n then sum(f)(n)=f(0). For f:int->int, n:int, if 0T, selfapply(f) ::=fun[x:T]( f(f(x)) ). For Sets A,B, C, f:A->B, g:B->C, g o f ::= fun[x:A]( g(f(x)) ). . Semantics of 'fun' etc If e is an expression that returns values of type B when x has values of type A then fun[x:A](e) has type A -> B. The defining rules are For all f:A -> B, f=fun[x:A](f(x)). For all f:A -> B, a:A, (fun[x:A](f(x)))(a)=f(a). . Manipulating Maps. We often need to evaluate expressions made up out of functions: f(g(h(k(3)))) The technique is to start in the middle and work backwards to the outside: k(3) first then put k(3) into h(_) then put h(k(3)) into g(_) ... We often need to calculate what a function does in general. For example suppose For x:Integers, f(x) ::=0, g(x) ::=x+1, h(x) ::=x*x. So f(_)=0, g=(_)+1, h=(_)*(_). Then we might want to work out what happens to x when we apply g and h in turn to it. The easy way is to do algebra on the expression, like this: h(g(x))=f(x+1)=(x+1)*(x+1)=x^2+2*x+1, or: h(g(x))=(g(x))*(g(x))=(x+1)*(x+1)=x^2+2*x+1. So we end up with h(g(x)) is an expression that maps an x into x^2+2*x+1. In other words the function fun[x](h(g(x)) = (_)^2+2*(_)+1, . Rules To evaluate expressions with functions, use algebra, arithmetic, intelligence, and the rules below: .Net (f1): If a term t is equal to expression d, then wherever t appears in e we can put (d) in ts place. (f2): If t(x) is equal to d for all values of x, then t(a) is equal to (d) with every occurrence of x in d replaced by (a). (f3): If an expression e has some holes(_), then (e)(a) is the result of putting a in all the holes in e. (f4):If an expression f has a (fun[x](e)) in it that is not inside another (fun...) , then (f)(a) is equal to f with the (fun[x](e)) modified by replacing each x in e by (a) and removing the fun[x]. (f5): If two expressions evaluate to the same thing then they are equal and vice versa. (arithmetic): You can use your knowledge of arithmetic or a calculator to evaluate expressions. .Close.Net Example .Box Suppose we are given double:: Integer -> Integer. double::= fun[x] (x+x). double::=the function that takes x and returns x+x. square:: Integer -> Integer. square::= (_) * (_). cube:: Integer -> Integer. For all x:Integer, cube(x) ::=x*square(x). If we want the correct value of double(cube(2)) then we can proceed carefully step by step: double(cube(2)) (cube, f2)|- =double(2*square(2) ) (square, f1)|- = double(2*((_) * (_))(2) ) (f3, _:=2)|- =double(2*(2*2)) (arithmetic)|- =double(2*4) (arithmetic)|- = double(8) (double, f1)|- =( fun[x] (x+x))(8) (f4, x:=8)|- = 8+8 (arithmetic)|- =16. .Close.Box . Operations on maps: o and ';' combine two maps to create a new one: For x, (f o g)(x)=f(g(x)) and (g;f)(x)=f(g(x)). .See Thanks1 ()|- f o g = g;f = f(g((_))). The 'o' notation comes from many mathematics texts that use a small 'o' in this way. The semicolon(";") comes from many post-algol-60 programming languages where it separates oeprations that are executed in sequence, so for example: .As_is f; .As_is g means doing f and then doing g. So if x++ adds one to x and x-- subtracts 1 from x then x++; x-- does first one and then the other... Thus, for example when f=0, g=(_)+1, and h=(_)*(_) then h(g(x)) = x^2+2*x+1 and so h o g = g;f = fun[x](h(g(x)) = fun[x](x^2+2*x+1) =(_)^2+2*(_)+1, . Exercise 2 What is g o h? There is also a natural way to describe selections: A+>f|+>g = fun[x]( if x in A then f(x) else g(x)). For example (using f=0, g=(_)+1, and h=(_)*(_) from above) {0}+>g|+>f = fun[x]( if x = 0 then 0+1 else 0). The following set of definitions shows the power of this idea by giving definitions of the arithmetic operations on numbers rather like Peano's technique Arithmetic_operators::=following, .Net Number::Sets=given. _-1::Number->Number=given. _+1::Number->Number=given. ... +::infix(Number)= {0}>2nd |-> (1st-1)+(2nd+1). (+)|-(0+1)= 1. (+)|-(1+1)= (0+2)=2. *::infix(Number)= {0}>0 | {1}>2nd |-> 2nd+(1st-1)*2nd. ^::infix(Number)= Number><{0}->1 | Number><{1}->1st |-> 1st*(2nd^(1st-1)). .Close.Net . Piecewise Definitions Commonly we define a new function piecemeal. So instead of f::= A+>....|B+>..... | c+>...., we can write .Box For x:A, f(x) ::=...., For x:B, f(x) ::=...., f(c) ::=... . .Close.Box or .Box f::A -> Y=..., f::B -> Y=..., f(c) ::Y=.... .Close.Box or even a table .Table x:A x:B c .Row ... ... ... .Close.Table and get a similar effect. So for example, three ways to define a key part of the Hailstone Sequence: hail::Nat->Nat= even+>halve|+>increment(treble). or .Net hail::Nat. for i:even, hail(i)::=halve(i). For i:odd, hail(i)::=increment(treble(i)). .Close.Net or .Table .Row even odd .Row halve treble o increment .Close.Table We can also define maps in terms of itself, as long as this does not lead to an infinite regress. An example is: double(0) ::=0, For x, double(x+1) ::=double(x)+1+1. OR equivalently double::={0}+>f |+> g(g(double(d(_)))), where f(x):=0, g(x)=x+1, d(x)=x-1. So (double)|- double(0)=f(0)=0, (double)|- double(1)=1+1+double(0)=2, (double)|- double(2)=1+1+double(1)=4, (double)|- double(3)=1+1+double(2)=6. It can be shown that (double)|-(d1): for all x >=0, double(x)=2*x. . Proof of d1 Clearly when x=1, double(x)=2*x. .Let |- (1): double(x)=2*x for some x, (1)|- double(x+1) =double(x)+1+1 (algebra)|- =2*x+1+1 (algebra)|- =2*(x+1). .Close.Let So if double(x)=2*x then double(x+1)=2(x+1). By mathematical induction (INDUCTION)|-For all x>=1, double(x)=2*x. In the above the "Let....Close.Let" is just like a block in C or pascal... some new variables and assumptions are introduced, temporarily and used to derive a result. After Let{P....|-Q} you can conclude: if P then Q. The '|-' is put in front of things that can be proved.... Given a set of maps (like {fun[x]0, fun[x](x+1)} for instance) we sometimes need to know what we can generate by using these and the control structures of selection, sequence, and recursion. It turns out that if a integer function can be computed by a computer with infinite storage then it can be expressed in terms of { fun[x]0, fun[x](x+1), fun[x](x-1) }. .Close Functions and Maps .Open Acknowledgements . Thanks1 Thank you to Ulf Schenemann .See http://www.cs.mun.ca/~ulf/ for correcting this. .Close Acknowledgements