From the Wikipedia: "*calculus* can refer to any method or system of calculation", and that's not an exception for the Lambda Calculus. First of all, lets define the terms of this calculus:

A Lambda Term is something with the form

**x**where*x*is in**V**a set of variables.**(u v)**where*u*and*v*are terms. We use "*v*is applied to*u*" in this case.**(λx.u)**where x is in**V**and u is a term. We use "an abstraction of*x*in*u*" in this case.

Here is one example: (λx.(λy.z) x)

But we cannot compute anything with just terms, so lets show the only rule use to transform these terms into a computation. This rule is quite famous (yeah, I know... famous in the Geeks Hall of Fame...), it is the "Beta reduction":

(λx.u) v → u[x/v]

In order to avoid critics, my nick "Beta" doesn't came from this rule, ok? I will not call my dog "Albert" nor stuff like that!

And now, let explain the meaning of *u[x/v]*. Given terms **u, v**, and a variable **x**, *u[x/v]* means "replace each *free occurrence* of *x* in *u* with *v*". By *free occurrence* of a variable *x *in a term *u *we mean "each time *x* does not appear inside a term of the form *(λx. ...)*".

It is not as hard as it looks. Some examples:

- x[x/y] = y
- (x y)[z/(λf.f)] = (x y)
- (x y)[x/(λf.f)] = ((λf.f) y)

And now some complete examples of lambda terms with beta reductions:

- x does not reduces.
- (λx.x) does not reduces also.
- (λx.x) y reduce to x[x/y], which turns to be equal to y. As you can see, we are applying the term
*y*to the function*(λx.x).*This function is called "identity", because computes the identity function f(x) = x. - (λx.x x) (λx.x x) reduces to (λx.x x)[x/(λx.x x)] = (λx.x x) (λx.x x) that reduces to (λx.x x)[x/(λx.x x)] = (λx.x x) (λx.x x) and so on...

Another important concept is the **alpha conversion**. Alpha conversion means that we will treat all the terms that differs only in the name of the *bounded variables* (variables that are not *free*) as the same term. I.e. (λx.x) and (λy.y) will be the same term for us.

In the next post, I will show how to use this calculus to compute the arithmetics functions, so don't miss it!