De Bruijn notation, and why it's useful

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 ... Read full article.