In mathematical logic, the De Bruijn notation is a syntax for terms in the λ calculus invented by the Dutch mathematician Nicolaas Govert de Bruijn. 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.

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

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

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

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

in the De Bruijn notation is, predictably,

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 ${\displaystyle (M)\;(N)\;[u]\;(P)\;[v]\;[w]\;(Q)\;z}$, where the redexes are underlined:

${\displaystyle {\begin{aligned}(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{aligned}}}$