De Bruijn notation

    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)