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]. (2003-06-15)
