de bruijn notation

1 definition found

de bruijn notation - Free On-line Dictionary of Computing (26 May 2007) :

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