You are here: irt.org | FOLDOC | 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 » debugger » debugging

FOLDOC, Topics, 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, ?, ALL