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.