2025-05-26
At least a familiarity with the lambda calculus, including how it is evaluated. Some base knowledge of programming languages is also assumed.
Let's look at a little imaginary term, in some lambda-calculus-like language. For future note, we call the lambda a "binder", as it binds a variable. There are other types of binders, e.g. let, but we will only consider lambdas for the moment.
λ f. (λ y f. (f y)) f
We can perform what's called "beta reduction" on this term — essentially, function application, applying f to the lambda.
λ f. (λ y f. (f y)) (f)
substitute [y := f] in λ y f. (f y)
λ f. (λ f. f f)
Uh oh. We've accidentally captured a variable! Instead of f referring to the outer f, now it refers to the inner f. This is "the capture problem", and it is quite annoying. Generally to avoid this, we need to rename everything1 in our "substituted" term to names that are free (do not occur) in the "subsitutee" so nothing is accidentally captured. What if we could introduce a notation that avoids this?
De Bruijn indexes are a naming scheme where:
Let's rewrite that term above using this system:
λ (λ λ (0 1)) 0
Here's some ascii art showing what refers to what:
λ (λ λ (0 1)) 0
| | \———/ | |
| | | |
| \————————————/ |
\———————————————————————/
Now, how does this help us with our substituion problem? Surely if we naively subtitute we will still have binding issues - and indeed we do:
λ (λ λ (0 1)) 0
->
λ (λ (0 0))
No good!
What De Bruijn indexes allow us to do is simply avoid capturing. The rule is simple: Every time we go past a binder when substituting, we increment every free variable2 in our substituted term by one, to avoid the new binder. Just once, we decrement every free varible in the substitutee, to account for the removal of the binder:
λ (λ λ (1 2)) 0
^ ^ ^
a b c
->
λ (λ (1 1))
^ ^ ^ ^
a b | \ decremented by one
|
\ incremented by one when we passed "through" lambda c
Now we're cool! Everything works as expected, and it takes much less work (and is much more predictable!).
At the bottom of this post there's a little widget that can convert terms to de Bruijn for you, if you want to play around!
De Bruijn levels work similar to De Bruijn indexes, in that we use numbers to refer to binders. However, in De Bruijn levels, the lowest number refers to the least recently bound item.
Recall that:
Named: λ f. (λ y f. (f y)) f
Indexes: λ (λ λ (0 1)) 0
Now, with levels:
Levels: λ (λ λ (2 1)) 0
This has the same diagram of what refers to what:
λ (λ λ (2 1)) 0
| | \———/ | |
| | | |
| \————————————/ |
\———————————————————————/
(As it should! These two representations represent the same term.)
As you might expect, de Bruijn indexes and levels are each beneficial in their own situations.
Generally, De Bruijn indexes are "more useful" than De Bruijn levels, as they're "more local". In order to work with levels, you need to know "how deep" you are in a term at all times.
De Bruijn indexes give us the advantage that we can freely create new binders without the need for any information about where in a term we are, whereas de Bruijn levels give us the advantage when moving a term under a binder, free variables in said term do not need to be modified. Generally, one has many more free variables in a term than bound ones.
λ (λ λ (2 1)) 0
^ this zero...
->
λ (λ (1 0))
^ ^ is still zero!
|
\ we had to modify this one though
Something that can come up quite a lot in various contexts is comparing whether two terms are equal or not. There are many complicated ways to do so, but de Bruijn gives us an advantage in a critical one, called "alpha-equivalence". Consider the following two terms:
λf. λx. f x
λg. λy. g y
These terms should clearly be equal, right? They do the exact same thing. In this case, we consider them "alpha-equivalent", meaning they are equal up to the names of variables. Alpha renaming is the process of renaming one term to match the names of another, so that they are "clearly" equal.
Let us consider the de Bruijn index representation of both of these terms:
λf. λx. f x => λ λ 1 0
λg. λy. g y => λ λ 1 0
Isn't that nice? They've gone from being alpha-equivalent, but not quite equal, to being equal. de Bruijn gives us the ability to compare terms for equality without having to consider alpha-equivalence at all.
De Bruijn indexes and levels can also be summed up via the following:
λa. λb. λc. c
indexes:
λ λ λ 0
^ ^ ^
2 1 0
levels:
λ λ λ 2
^ ^ ^
0 1 2
if you’re “here”
v
λ λ λ
Try it out! Some example terms to try:
\f x. f x
\x x. x
\x. (x (\y. y))
\x. \y. y x -- will not work
do \x. (\y. y x) or \x y. y x instead
(sorry, it does over-parenthesize a bit :P)
It is worth noting that there are several other methods for gaining the same, or similar, advantages as de Bruijn gives. This post is not intended to explain them, but I will list several here so that the curious reader may read further (tip: when searching, append "lambda calculus" to find the right results quicker):
As you can see, there are many approaches! Jesper Cockx has an excellent summary of almost all of these, which can be found here. Notably, many are intended for formalization efforts rather than for computational usage.