De Bruijn Notation is a notation created in 1972 by Nicolaas Govert de Bruijn.
#2085on PLDB | 53Years Old |
De Bruijn Notation is a representation system for lambda calculus that eliminates variable names by using numerical indices to refer to binders, avoiding issues with alpha-equivalence and variable capture. It is widely used in theoretical computer science and functional programming implementations.
位 位 2 1
# Represents the lambda term 位x.位y.x y in traditional lambda calculus, where 2 refers to the outer binder (x) and 1 to the inner binder (y).