With this cite of Monthy Python, I will move into another family of calculi. What's wrong with our good ol' λ-calculus? Nearly nothing, except if you want to implement it in a real PC.
In one of the firsts posts I've mentioned the α-congruence. The idea is that terms that only differs in the name of the variables are "the same". For instance, take
T1 = (λx. x)
T2 = (λy. y)
We said T1 ≡ T2 to say that T1 and T2 are in the same class of equivalence modulo α. In other word, they are the same.
Suppose that we want to store a set of terms with its results. Something like a dictionary of terms used as a cache. Suppose that in that dictionary we have
key: (λx. x) (λx. x), value: (λx. x)
That is, given the identity term applied to himself, the result will be the identity term.
Suppose now that we are computing the result of the term
T = (λy. y) (λy. y) z
It will be a good idea to use the information in the cache, in order to make less computations. But the term in the cache differs from the term T in that the variables aren't the same. So we need to rename them in order to compare them.
A guy named Nicolaas Govert de Bruijn invented a way to avoid this renaming of variables. The idea is quite simple, but yet hard to grasp. Instead of naming the variables, enumerate them by the depth of that variable in the term (respect to the λ operator that bind it). So, for instance, the identity term will be
(λ1)
That is, the 1 refers to the the first λ, looking from the 1 point of view. Another example: (λx.λy. x) will be
(λ(λ2))
Another example: (λx.λy. x y) z will be
(λ(λ2 1)) 1
Note that the free variable z is called 1 in this calculus. Why? Because it can be bounded to an invisible outer λ:
(λz.(λx.λy. x y) z)
Exercise: In the following term, which index (that's the new name for variables) corresponds to which lambda? I will omit some parenthesis.
(λλλ1 2 3 5)
Answer (don't look before thinking!):
(λλλ1 2 3 5)
Another exercise:
λλ(1 2 3) 1
Answer:
(λλ1 2 3) 1
Note that the gray numbers refers to the same variable in a lambda not shown (i.e. a free variable).
Formalizing, the terms in λDB (that's the name of λ-de Bruijn) are:
T ::= n | λT | T T'
where n is a natural number.
We now how to write λDB terms. Now we need to make them calculate something. Let's start by the β-reduction:
(λa) b → a{1 ← b} That's "if I have a function, with the body a, and I execute it with the parameter b, I have to replace every occurrence of 1 in a by b". Why 1? Because that's our variable for the λ we are taking off.
Let's try to define a{1 ← b} by a colored example.
(λλ1 2 3) 1 2 → (λ1 2 3){1 ← 1} 2
Suppose that we said:
(λa){1 ← b} = (λa{1 ← b}) we are making a big mistake: (λ1 2 3){1 ← 1} = λ(1 2 3){1 ← 1}
Now we are changing the red 1, instead of the yellow 2! In order to avoid that, we have to increment the variable we want to replace each time we cross a λ:
(λa){i ← b} = (λa{i+1 ← b}) Let's continue with our example:
(λ1 2 3){1 ← 1} 2 = λ(1 2 3){2 ← 1} 2
Now we have to distribute the replace function:
λ(1 2 3){2 ← 1} 2 = λ(1{2 ← 1} 2{2 ← 1} 3{2 ← 1}) 2
which gives us another rule:
(a b){i ← c} = a{i ← c} b{i ← c} Now we reach the variables, so we have to make the replacement. Suppose that we just put the 1 when we found a 2:
λ(1{2 ← 1} 2{2 ← 1} 3{2 ← 1}) 2 = λ(1 1 3) 2
Something does not looks right. Take a look at the grey numbers. We know that both refers to the same variable. But why they are different? The two of them must to be changed in order to points to the first free variable. First, let's take a look at the 1. Remember that we have to cross a lambda, so now the free variable to what it refers is one lambda away. So instead of just put the term we are replacing, we have to update it to increase the variables for all the lambda we crossed. For that, I will introduce a new operator, called "U" (Update). Having fixed the 1, let's fix the 3. The three right now points to the second free variable, because it has lost one lambda. So, we have to subtract one in each free variable. So, the rules for replacing a variable are:
i{i ←b} = U(0, i, b)
i{j ←b} = i-1 if j > i
i{j ←b} = i if j < i
In our example:
λ(1{2 ← 1} 2{2 ← 1} 3{2 ← 1}) 2 = λ(1 U(0,2,1) 2) 2
The U operator is simple. The first parameters count the lambda it crosses, in order to take into account the bounded variables (i.e. the variables that don't need updating).
U(i, j, (a b)) = U(i, j, a) U(i, j, b)
U(i, j, (λa)) = λU(i+1, j, a)
U(i, j, n) = n + j - 1 if n > i
U(i, j, n) = n if n <= i
Continuing with our example:
λ(1 U(0,2,1) 2) 2 = λ(1 2 2) 2
Now we can execute the beta reduction:
λ(1 2 2) 2 → (1 2 2){1 ← 2} = 1{1 ← 2} 2{1 ← 2} 2{1 ← 2} = U(0, 1, 2) 1 1 = 2 1 1
Note that the expression U(0, 1, x) = x for all term x.
Something I'm not going to show is that there is a bijection between the lambda calculus classic and this calculus. By bijection I mean that they computes the same things in the same way. If we define a translation between terms T (suppose that if t is a lambda term, then T(t) is a lambda DB term, an viceversa).
So, given a term t either in lambda or lambda DB,
t → ... → t'
implies
T(t) → ... → T(t')
Well, that's it for lambda DB. Until next post!