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

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:

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

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!