# Maths - λ Calculus

The usual way that we define a function on this site is something like:

s: x -> x*x

That is, the function (named s in this case) that takes x to x*x, that is the square function.

This particular example could be used like this

s(2) = 4

An alternative notation for function definition is lambda calculus. It is called lambda calculus because it is denoted by the Greek character lambda: λ. So the above example would be written:

s = λx.x*x

Where the character(s) between 'λ' and '.' is (are) the variable(s). So this function takes whatever the value of x may be and replaces it with x*x in this example. This is known as 'binding' the value of x and x is known as a bound variable.

One of the advantages of this notation is that, when used in a computer program, it can define the function in the place where it is being used rather than have it defined separately from where it is used. That we don't need to name the function, it is an 'anonymous' function.

So ( λx.x*x) 2 has the value 4. That is the square function applied to the value 2.

In some notations and computer languages (such a lisp) this would be written:

( λx.x*x 2 )

That is: the function and its arguments are all written inside the brackets. Perhaps the safest way to avoid any confusion is to write it like this:

( (λx.x*x) 2 )

An advantage of defining and using the function in the same place like this that we can nest lambda functions within other lambda functions to give us second order logic.

### Functions of Multiple Variables and Currying

We can denote a function of multiple variables like this:

λxy.x*x + 3*y

which returns x squared plus 3 times y.

That is several bound variables (in this case x and y) can be placed between 'λ' and '.'.

However this is not strictly necessary because a function of multiple variables can always be converted into a function of a single variable by Currying. So the function above is equivalent to:

λxy.x*x + 3*y
= λx.(λy.x*x + 3*y)

That is, a single variable function that returns a function that then gives the value required. In the general case we have:

λxy...z.M = λx.(λy. ... (λy.M) ...)

where M is some expression of xy...z.

Strictly I shouldn't use '=' but syntactic identity instead.

### Nested Lambda Expressions

We can have multiple variables, not all variables need to be bound λ expressions, as a particular variable is bound by a λ expression then the dimension of the function is reduced. For example we might have a function of 3 variables x,y and z so we can think of this as a 3-dimensional function. If this is wrapped in an expression like λx.(...) then x will be bound. So we can think of this as taking a function of 3 variables and returning a function of 2 variables. We can then wrap this in an expression like λy.(...) and then we will have a function of 1 variable.

### Program Examples

 example: lambda function for 'square' (\x -> x*x) ```Prelude> (\x -> x*x) 3 9 Prelude> ```