De Bruijn notation

language A variation of lambda notation for specifying

functions using numbers instead of names to refer to formalparameters. 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 alphaconversion.

[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].

(2003-06-15)