<*language*> A variation of lambda notation for specifying
functions using numbers instead of names to refer to formal
parameters. A reference to a formal parameter is a number
which gives the number of lambdas (written as \ here) between
the reference and the lambda which binds the parameter.
E.g. the function \ f . \ x . f x would be written \ . \ . 1
0. The 0 refers to the innermost lambda, the 1 to the next
etc. The chief advantage of this notation is that it avoids
the possibility of name capture and removes the need for alpha
conversion.

[N.G. De Bruijn, "Lambda Calculus Notation with Nameless Dummies: A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem", Indag Math. 34, pp 381-392].

Last updated: 2003-06-15

Try this search on Wikipedia, OneLook, Google

**Nearby terms:**
debianize « deboursification « De Bruijn graph « **De Bruijn notation** » DEBUG » debugging » debugging an empty file

Loading

Copyright Denis Howe 1985