De Bruijn notation

For the representation of variables with natural numbers, see De Bruijn index.

In mathematical logic, the De Bruijn notation is a syntax for terms in the λ calculus invented by the Dutch mathematician Nicolaas Govert de Bruijn.[1] It can be seen as a reversal of the usual syntax for the λ calculus where the argument in an application is placed next to its corresponding binder in the function instead of after the latter's body.

  1. ^ De Bruijn, Nicolaas Govert (1980). "A survey of the project AUTOMATH". In Hindley J. R. and Seldin J. P. (ed.). To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press. pp. 29–61. ISBN 978-0-12-349050-6. OCLC 6305265.