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:

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

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 of Λ-terms follow:


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