By Letter: Non-alphabet | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
  Email this page to a friend

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].

< Previous Terms Terms Containing De Bruijn notation Next Terms >
Debian GNU/Hurd
Debian GNU/Linux
De Bruijn graph
name capture
DEC Alpha

Web Standards & Support:

Link to and support Powered by LoadedWeb Web Hosting
Valid XHTML 1.0!Valid CSS! FireFox Extensions