General Programming Language Terminology - sagr4019/ResearchProject GitHub Wiki

De Bruijn indices

De Bruijn indices describe a uniform method to abstract names of variables. The variable names are replaced by numbers. The numbers are composed of the distance between the declaration and the occurrence of a variable.

Example:

λx. λy. λz. x z (y z) => λ λ λ 3 1 (2 1)

λ stands for a variable declaration i.e. λx is a declaration of the variable x. The indices start with a number > 0

references

en.wikipedia.org

related work

An-ML-Implementation-of-the-Lambda-Calculus

ttic.uchicago.edu