- Functions and Maps
- : Simple Functions
- : Example of a simple function
- : More complex functions
- : Semantics of 'fun' etc
- : Manipulating Maps.
- : Rules
- : Operations on maps:
- : Exercise 2
- : Piecewise Definitions
- : Proof of d1
- Acknowledgements
- : Thanks1
- Notes on MATHS Notation
- Notes on the Underlying Logic of MATHS
- Glossary

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

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

- 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 -> 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 -> 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 λ expressions

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

unsigned int fudge(unsigned int x)

{ return 3*x+1;

}

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

f::A -> B=e.

is logically a combination of a declaration and an equallityf::A -> B,

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

- For Type T, f:T->T, 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.

(End of Net)

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

## 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)).
[ Thanks1 ]
- (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

- 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}><Number->2nd |-> (1st-1)+(2nd+1).
- (+)|-(0+1)= 1.
- (+)|-(1+1)= (0+2)=2.
- *::infix(Number)= {0}><Number->0 | {1}><Number->2nd |-> 2nd+(1st-1)*2nd.
- ^::infix(Number)= Number><{0}->1 | Number><{1}->1st |-> 1st*(2nd^(1st-1)).

(End of Net)

## Piecewise Definitions

Commonly we define a new function piecemeal.So instead of

- f::= A+>....|B+>..... | c+>....,
we can write

or

or even a table**Table**x:A x:B c ... ... ...

(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

or**Table**even odd 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 )

- |- (1): double(x)=2*x for some x,
- 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) }.

- STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html
# Glossary

- 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).
- given::reason="I've been told that...", used to describe a problem.
- given::variable="I'll be given a value or object like this...", used to describe a problem.
- goal::theorem="The result I'm trying to prove right now".
- goal::variable="The value or object I'm trying to find or construct".
- 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.
- hyp::reason="I assumed this in my last Let/Case/Po/...".
- QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
- QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
- RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last
assumption (let) that you introduced.

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.

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

. . . . . . . . . ( end of section Acknowledgements) <<Contents | End>>

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 ]

For a more rigorous description of the standard notations see