De Bruijn Indices and Levels: Solving Variable Capture in Lambda Calculus
2025-05-30
This article introduces De Bruijn indices and levels, elegant solutions to the frustrating problem of variable capture in lambda calculus. By using natural numbers instead of variable names, these methods avoid naming conflicts, simplify substitution, and facilitate easier comparison of term equality. The article clearly explains how both methods work, compares their advantages and disadvantages, and concludes that De Bruijn indices are generally more useful for local operations, while De Bruijn levels are more convenient when moving subterms. This is a great read for programmers familiar with the basics of lambda calculus.