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!