The variables in the λ-calculus are unnecessary and
the *nameless λ-calculus* dispenses with them entirely.
Independently both Berkling and de Bruijn came up with such a scheme.
We shall call the nameless λ-calculus the Λ-calculus.

The alphabet of Λ-terms is defined as follows:

- index sign:
`#`

, - numbers:
`0`

,`1`

,`2`

, ..., - abstractor:
`Λ`

, - parentheses and dot:
`(`

,`)`

,`.`

.

The set of Λ-terms, S, is defined inductively as follows:

`#n`

∈S, where`n`

is a natural number,- if
`M`

∈S; then`Λ.M`

∈S, - if
`M,N`

∈S then`(MN)`

∈S.

The parentheses are usually dropped if they are not needed to give a unique reading.
We call Λ-terms of the form `#n`

indices.
We call Λ-terms of the form `(MN)`

applications.
We call Λ-terms of the form `Λ.M`

abstractions.

The function φ that converts λ-terms to Λ-terms defined as follows:

φ(`x`

, ρ) = `#n`

where `n`

= ρ(`x`

),

φ(`λx.M`

, ρ) = `Λ.M'`

where `M'`

= φ(`M`

, ρ'),
and ρ'(y) = 0 if y=`x`

, otherwise ρ'(y) = 1 + ρ(y)

φ(`(M N)`

, ρ) = `(M' N')`

where `M'`

= φ(`M`

, ρ) and `N'`

= φ(`N`

, ρ)

Given an initial ρ such that ρ(y) is undefined for all y, the Λ-term conversion of the λ-term `M`

is φ(`M`

, ρ).

Note how indices are similar to addresses in a stack frame built during nested function calls in typical programming languages. Indices are sometimes known as de Bruijn indices.

Examples of Λ-terms follow:

`Λ.#0`

which is the equivalent of`λx.x`

`Λ.Λ.#1`

which is the equivalent of`λx.λy.x`

`(Λ.#0 Λ.#0)`

which is the equivalent of`(λx.x λy.y)`

W. Kluge. *Abstract Computing Machines. A Lambda Calculus Perspective.* Springer, 2005.

Copyright © 2014 Barry Watson. All rights reserved.