# Nameless Lambda Calculus

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.

## Conversion of λ-terms to Λ-terms

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

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)`

## References

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