De Bruijn notation, and why it's useful

Summary

Debruijn indexes + levels, and why they're handy Debruijn indexes + levels, and why they're handy 2025-05-26 dark mode? back? De Bruijn and why we use it Assumed knowledge At least a familiarity with the lambda calculus, including how it is evaluated. Some base knowledge of programming languages is also assumed. The problem 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 everything 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? Presenting: De Bruijn Indexes! De Bruijn indexes are a naming scheme where: We use natural numbers to refer to lambdas, and Zero refers to the "most recent" lambda; one refers to the second most recent, etc. 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 variable in our substituted term by one, to avoid the new ...