[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng ] / [R J Botting] / [ ] / intro_function
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Fri Dec 18 11:11:36 PST 2009

# 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 [ 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).
1. A -> B::=Set of functions mapping objects of type A into B,
2. For f:A -> B and for all a:A there is one b:B such that b=f(a).

Similarly (A><B) -> 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><B -> C we can write it between its operands:

3. a f b::=f(a,b) and
4. a f b in C. So
5. + in int><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:

6. sqr::int -> int = (_)*(_). Functions of two arguments can be written with '(1st)' and "(2nd)" in place of the first and second arguments
7. add::int><int -> int =The sum of (1st) and (2nd),
8. (add)|-add(1,2) = The sum of 1 and 2.

## Example of a simple function

9. hypotenuse::real><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
10. For variable:Domain,..., name(arguments)::=expression. For example:
11. For x:Real, sqr(x)::=x*x.
12. For x,y:Real, hypotenuse(x,y)::=sqrt(sqr(x)+sqr(y)).

Functions are often expressed as λ expressions

13. λ arguments.expression The λ notation was the first notation that let us describe a function without actually giving a name:
14. λ 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:

15. map[x:T](e(x)) or
16. fun[x:T](e(x)). Thus we can write:
17. sqr=fun [x:Real](x*x),

18. Notice. fudge::=fun[x:Natural](3*x+1) gives a name to the function.

This is like C.....

` 	unsigned int fudge(unsigned int x)`
` 	{ return 3*x+1;`
` 	}`

However

19. '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

20. For x:Integers,
21. f(x)::=0,
22. g(x)::=x+1,
23. h(x)::=x*x. then
24. g=fun[x](x+1), h=fun[x](x*x),
25. and
26. g=(_)+1, h=(_)*(_),

The extended XBNF includes definitions like the following

27. For x:A, f(x)::B=e.

It means:

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

29. f::A -> B= e'. where e' has each free x replaced by "(_)",....

For example, three definitions of a trebling function:

30. For i:Nat, treble(i)::=3*i.
31. treble::Nat->Nat = fun[ i:Nat](3*i).
32. treble::Nat->Nat = 3*(_).

As in other areas of XBNF, a definition like

` 	f::A -> B=e.`
is logically a combination of a declaration and an equallity
` 	f::A -> B,`
` 	|- f=e.`

We can now also write higher order functions or functors that produce functions and act on functions:

33. For f:int->int, selfapply(f)::=fun[x:int]( f(f(x)) ).
34. 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:

35. selfapply::=fun[f:int->int](fun[x:int]( f(f(x)) )).
36. 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:

37. For f:int->int, sum(f)::int->int=fun[n:int](sum i:0..n of f(i)).
38. For f:int->int, n:int, if 0>n then sum(f)(n)=0.
39. For f:int->int, n:int, if 0=n then sum(f)(n)=f(0).
40. For f:int->int, n:int, if 0<n then sum(f)(n)=f(n)+sum(f)(n-1).

Higher order functions can even by generic or polymorphic so that they work on functions of different types in similar ways:

41. For Type T, f:T->T, selfapply(f)::=fun[x:T]( f(f(x)) ).
42. 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
43. fun[x:A](e) has type A -> B.

The defining rules are

44. For all f:A -> B, f=fun[x:A](f(x)).
45. 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:
46. f(g(h(k(3))))

The technique is to start in the middle and work backwards to the outside:

47. k(3) first
48. then put k(3) into h(_)
49. then put h(k(3)) into g(_)
50. ...

We often need to calculate what a function does in general. For example suppose

51. For x:Integers,
52. f(x)::=0,
53. g(x)::=x+1,
54. h(x)::=x*x.

So

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

56. h(g(x))=f(x+1)=(x+1)*(x+1)=x^2+2*x+1,

or:

57. h(g(x))=(g(x))*(g(x))=(x+1)*(x+1)=x^2+2*x+1.

So we end up with

58. h(g(x)) is an expression that maps an x into x^2+2*x+1.

In other words the function

59. fun[x](h(g(x)) = (_)^2+2*(_)+1,

## Rules

To evaluate expressions with functions, use algebra, arithmetic, intelligence, and the rules below:
Net
1. (f1): If a term t is equal to expression d, then wherever t appears in e we can put (d) in ts place.
2. (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).
3. (f3): If an expression e has some holes(_), then (e)(a) is the result of putting a in all the holes in e.
4. (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].
5. (f5): If two expressions evaluate to the same thing then they are equal and vice versa.
6. (arithmetic): You can use your knowledge of arithmetic or a calculator to evaluate expressions.

(End of Net)

Example
1. Suppose we are given
2. double::Integer -> Integer.
3. double::= fun[x] (x+x).
4. double::=the function that takes x and returns x+x.
5. square::Integer -> Integer.
6. square::= (_) * (_).
7. cube::Integer -> Integer.
8. 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:

9. double(cube(2))
10. (cube, f2)|-
11. =double(2*square(2) )
12. (square, f1)|-
13. = double(2*((_) * (_))(2) )
14. (f3, _:=2)|-
15. =double(2*(2*2))
16. (arithmetic)|-
17. =double(2*4)
18. (arithmetic)|-
19. = double(8)
20. (double, f1)|-
21. =( fun[x] (x+x))(8)
22. (f4, x:=8)|-
23. = 8+8
24. (arithmetic)|-
25. =16.

## Operations on maps:

60. o and ';' combine two maps to create a new one:
61. For x, (f o g)(x)=f(g(x)) and (g;f)(x)=f(g(x)). [ Thanks1 ]
62. (above)|-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:

` 		f;`
`		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

63. h(g(x)) = x^2+2*x+1 and so
64. h o g = g;f = fun[x](h(g(x)) = fun[x](x^2+2*x+1) =(_)^2+2*(_)+1,

## Exercise 2

65. What is g o h?

There is also a natural way to describe selections:

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

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

68. Arithmetic_operators::=following,
Net
1. Number::Sets=given.
2. _-1::Number->Number=given.
3. _+1::Number->Number=given.

4. ...

5. +::infix(Number)= {0}><Number->2nd |-> (1st-1)+(2nd+1).
6. (+)|-(0+1)= 1.
7. (+)|-(1+1)= (0+2)=2.
8. *::infix(Number)= {0}><Number->0 | {1}><Number->2nd |-> 2nd+(1st-1)*2nd.
9. ^::infix(Number)= Number><{0}->1 | Number><{1}->1st |-> 1st*(2nd^(1st-1)).

(End of Net)

## Piecewise Definitions

Commonly we define a new function piecemeal.

69. f::= A+>....|B+>..... | c+>...., we can write
1. For x:A, f(x)::=....,
2. For x:B, f(x)::=....,
3. f(c)::=... .

or
1. f::A -> Y=...,
2. f::B -> Y=...,
3. f(c)::Y=....

or even a table
Table
x:Ax:Bc
.........

(Close Table)
and get a similar effect. So for example, three ways to define a key part of the Hailstone Sequence:
70. hail::Nat->Nat= even+>halve|+>increment(treble). or
Net
1. hail::Nat. for i:even, hail(i)::=halve(i).
2. For i:odd, hail(i)::=increment(treble(i)).

(End of Net)

or
Table
evenodd
halvetreble 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:

71. double(0)::=0,
72. For x, double(x+1)::=double(x)+1+1.

OR equivalently

73. double::={0}+>f |+> g(g(double(d(_)))),
74. where f(x):=0, g(x)=x+1, d(x)=x-1.

So

75. (double)|-double(0)=f(0)=0,
76. (double)|-double(1)=1+1+double(0)=2,
77. (double)|-double(2)=1+1+double(1)=4,
78. (double)|-double(3)=1+1+double(2)=6.

It can be shown that

79. (double)|- (d1): for all x >=0, double(x)=2*x.

## Proof of d1

80. Clearly when x=1, double(x)=2*x.
Let

1. |- (1): double(x)=2*x for some x,
2. (1)|-double(x+1)
3. =double(x)+1+1
4. (algebra)|-
5. =2*x+1+1
6. (algebra)|-
7. =2*(x+1).

(Close Let )
81. So if double(x)=2*x then double(x+1)=2(x+1).
82. By mathematical induction
83. (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) }.

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

# Acknowledgements

## Thanks1

Thank you to Ulf Schenemann [ http://www.cs.mun.ca/~ulf/ ] for correcting this.

. . . . . . . . . ( end of section Acknowledgements) <<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

# Glossary

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.