de Bruijn indices
- categories
- abstract syntax
The premier nameless representation of variables. A variable is represented by a de Bruijn index; i.e., a natural number indicating how many binders must be crossed in order to reach the variable's binding site.
\begin{tabular}{c|c} \( \lambda x. x \) & \( \lambda. 0 \) \\ \( \lambda x. \lambda y. x \) & \( \lambda. \lambda. 1 \) \\ \( \lambda k. \lambda f. \lambda x. kx(fx) \) & \( \lambda. \lambda. 20(10) \) \end{tabular}