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)
Nearby terms:
debianize « deboursification « De Bruijn graph «
De Bruijn notation » DEBUG » debugging » DEC
|
