# De Bruijn notation

﻿
De Bruijn notation

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.

## Formal definition

Terms ($M, N, \ldots$) in the De Bruijn notation are either variables (v), or have one of two wagon prefixes. The abstractor wagon, written [v], corresponds to the usual λ-binder of the λ calculus, and the applicator wagon, written (M), corresponds to the argument in an application in the λ calculus.

$M,N,... \ ::=\ v\ |\ [v]\;M\ |\ (M)\;N$

Terms in the traditional syntax can be converted to the De Bruijn notation by defining an inductive function $\mathcal{I}$ for which:

\begin{align} \mathcal{I}(v) &= v \\ \mathcal{I}(\lambda v.\ M) &= [v]\;\mathcal{I}(M) \\ \mathcal{I}(M\;N) &= (\mathcal{I}(N))\mathcal{I}(M). \end{align}

All operations on λ-terms commute with respect to the $\mathcal{I}$ translation. For example, the usual β-reduction,

$(\lambda v.\ M)\;N\ \ \longrightarrow_\beta\ \ M[v := N]$

in the De Bruijn notation is, predictably,

$(N)\;[v]\;M\ \ \longrightarrow_\beta\ \ M[v := N].$

A feature of this notation is that abstractor and applicator wagons of β-redexes are paired like parentheses. For example, consider the stages in the β-reduction of the term $(M)\;(N)\;[u]\;(P)\;[v]\;[w]\;(Q)\;z$, where the redexes are underlined:[2]

\begin{align} (M)\;\underline{(N)\;[u]}\;(P)\;[v]\;[w]\;(Q)\;z &{\ \longrightarrow_\beta\ } (M)\;\underline{(P[u:=N])\;[v]}\;[w]\;(Q[u:=N])\;z \\ &{\ \longrightarrow_\beta\ } \underline{(M)\;[w]}\;(Q[u:=N,v:=P[u:=N]])\;z \\ &{\ \longrightarrow_\beta\ } (Q[u:=N,v:=P[u:=N],w:=M])\;z. \end{align}

Thus, if one views the applicator as an open paren ('(') and the abstractor as a close bracket (']'), then the pattern in the above term is '((](]]'. De Bruijn called an applicator and its corresponding abstractor in this interpretation partners, and wagons without partners bachelors. A sequence of wagons, which he called a segment, is well balanced if all its wagons are partnered.

## Advantages of the De Bruijn notation

In a well balanced segment, the partnered wagons may be moved around arbitrarily and, as long as parity is not destroyed, the meaning of the term stays the same. For example, in the above example, the applicator (M) can be brought to its abstractor [w], or the abstractor to the applicator. In fact, all commutatives and permutative conversions on lambda terms may be described simply in terms of parity-preserving reorderings of partnered wagons. One thus obtains a generalised conversion primitive for λ-terms in the De Bruijn notation.

Several properties of λ-terms that are difficult to state and prove using the traditional notation are easily expressed in the De Bruijn notation. For example, in a type-theoretic setting, one can easily compute the canonical class of types for a term in a typing context, and restate the type checking problem to one of verifying that the checked type is a member of this class.[3] De Bruijn notation has also been shown to be useful in calculi for explicit substitution in pure type systems.[4]

## References

1. ^ De Bruijn, Nicolaas Govert (1980). "A survey of the project AUTOMATH". In Hindley J. R. and Seldin J. P.. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press. pp. 29–61. ISBN 0-123-49050-2. OCLC 6305265.
2. ^ Kamareddine, Fairouz (2001). "Reviewing the classical and the De Bruijn notation for λ-calculus and pure type systems". Logic and Computation 11 (3): 363–394. doi:10.1093/logcom/11.3.363. ISSN 0955-792X.  The example is from page 384.
3. ^ Kamareddine, Fairouz; Nederpelt, Rob (1996). "A useful λ-notation". Theoretical Computer Science 155: 85–109. doi:10.1016/0304-3975(95)00101-8. ISSN 0304-3975.
4. ^ De Leuw, B.-J. (1995). Generalisations in the λ-calculus and its type theory. Masters Thesis, University of Glasgow .

Wikimedia Foundation. 2010.

### Look at other dictionaries:

• Bruijn — Nicolaas Govert de Bruijn Pour les articles homonymes, voir De Bruijn. Nicolaas Govert de Bruijn (9 juillet 1918 ) est un mathématicien hollandais affilié comme professeur émérite de l Université Technique d Eindhoven. Il s est intéressé à… …   Wikipédia en Français

• De Bruijn index — In mathematical logic, the De Bruijn index is a notation invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms in the λ calculus with the purpose of eliminating the names of the variable from the notation.[1] Terms… …   Wikipedia

• Nicolaas Govert de Bruijn — Pour les articles homonymes, voir De Bruijn. De Bruijn à Oberwolfach, dans les années 1960 Nicolaas Govert de Bruijn (né le 9 juillet 1918) est un mathématicien …   Wikipédia en Français

• Nicolaas Govert de Bruijn — Born 9 July 1918 (1918 07 09) (age 93) …   Wikipedia

• De Bruijn — is a Dutch surname. It may refer to: Chantal de Bruijn Cornelis de Bruijn, Dutch artist and traveler Daniëlle de Bruijn Inge de Bruijn, Dutch swimmer Nicolaas Govert de Bruijn, Dutch mathematician Maarten de Bruijn Nick de Bruijn Pi de Bruijn In… …   Wikipedia

• Lambda-Notation — Der Lambda Kalkül ist eine formale Sprache zur Untersuchung von Funktionen, die Funktionsdefinitionen, das Definieren formaler, sowie das Auswerten und Einsetzen aktueller Parameter regelt. Inhaltsverzeichnis 1 Geschichte 2 Der untypisierte… …   Deutsch Wikipedia

• Nicolaas Govert De Bruijn — Pour les articles homonymes, voir De Bruijn. Nicolaas Govert de Bruijn (9 juillet 1918 ) est un mathématicien hollandais affilié comme professeur émérite de l Université Technique d Eindhoven. Il s est intéressé à plusieurs branches des… …   Wikipédia en Français

• Nicolaas govert de bruijn — Pour les articles homonymes, voir De Bruijn. Nicolaas Govert de Bruijn (9 juillet 1918 ) est un mathématicien hollandais affilié comme professeur émérite de l Université Technique d Eindhoven. Il s est intéressé à plusieurs branches des… …   Wikipédia en Français

• Big O notation — In mathematics, big O notation is used to describe the limiting behavior of a function when the argument tends towards a particular value or infinity, usually in terms of simpler functions. It is a member of a larger family of notations that is… …   Wikipedia

• Dickman-de Bruijn function — In analytic number theory, Dickman s function is a special function used to estimate the proportion of smooth numbers up to a given bound.Dickman s function is named after actuary Karl Dickman, who defined it in his only mathematical publication …   Wikipedia