Nguage> 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)
