Luis Ziliani

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!

A Term Rewriting System (TRS) is a very powerful yet simple math tool used, for instance, for the creation of computational models. Given a set of function symbols S, and an (uncountable) set of variables V, I will define rewriting rule by example.

Suppose we have the “constant” function (function without parameters) 0 (representing a 0 in the natural numbers), the unary function S (as the successor of a number), and the binary function + (as the add operation). Let x and y be in V. These are rewriting rules to compute the add of two numbers:

0 + x → x
S(x) + y → x + S(y)

The arrow can be seen as a “rewrite as” relation. For example, S(S(0)) + S(0) rewrites by the second rule to S(0) + S(S(0)), then to 0 + S(S(S(0))), to achieve the final computation with the first rule: S(S(S(0))). And this is exacty what we expected: 2+1 = 3. Yeah, I know that it doesn’t look like a very big science discovery, but we will soon see that with more complex rules we are going to be able to compute anything.

This blog will contain all the news about my progress in my master thesis, entirely sponsored by Manas Technology Solutions. The idea will be to translate a lambda calculus with explicit substitutions with named variables to a calculus à la de Bruijn. If you have no idea what I’m talking about, don’t be afraid, wait for more posts to come!