.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 `t`s 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
**