1.1. Lambda Terms Without Types🔗

The lambda calculus is a very small language for describing functions. It has no numbers, booleans, loops, or function declarations built in. There are only three ways to make a term:

• a variable, such as x;

• a function λx. e, whose argument is called x and whose body is e;

• an application e₁ e₂, which applies the function e₁ to the argument e₂.

The word untyped means that a lambda does not say what kind of argument it expects. For now, λx. x, λx. x x, and even nonsensical-looking applications are all legitimate terms. Types will be introduced only in the next chapter.

Application associates to the left, so f x y means (f x) y. The body of a lambda extends as far to the right as possible, so λx. f x means λx. (f x).

A lambda binds occurrences of its variable in its body. In λx. x y, the occurrence of x is bound, while y is free. Names can be changed without changing the function: λx. x and λy. y both return their argument. This harmless change of bound names is called alpha-renaming.

Binder names are pleasant for humans but awkward for an implementation. Lean would normally regard the two identity functions above as different syntax trees, and substitution would constantly have to choose fresh names. We avoid that problem by implementing bound variables with de Bruijn indices first. Ordinary named notation will be added on top afterwards.

1.2. De Bruijn Terms🔗

A de Bruijn index tells us how far away a variable's binder is. Index 0 refers to the nearest surrounding lambda, index 1 skips that lambda and refers to the next one, and so on. Because the index records the binder rather than its name, alpha-renaming disappears automatically.

For example:

• λx. x becomes λ 0;

• λx. λy. y becomes λ λ 0;

• λx. λy. x becomes λ λ 1.

The two occurrences of 0 in the first two examples refer to different lambdas: in each case they select the nearest one. To find the binder of an index, start at its occurrence and count lambdas while moving outwards.

We keep names for variables that have no binder inside the term. Thus the implementation distinguishes a bound index 0 from a genuinely free name such as x. This mixed representation lets us work with open terms without introducing a separate representation for their surrounding context.

e ::= n \mid x \mid \lambda.\ e \mid e\ e

The datatype below follows this grammar exactly. The quotation DB[...] is only convenient notation for constructing the corresponding syntax tree.

1.3. Free Variables and Scope🔗

In a well-scoped de Bruijn term, every index refers to a surrounding lambda, while every named variable is free. Thus FV collects precisely the names stored by DB.free. Passing through a de Bruijn lambda does not remove a name, because these lambdas bind indices rather than strings.

\begin{array}{rcl} FV(n) &=& \varnothing\\ FV(x) &=& \{x\}\\ FV(\lambda.\ e) &=& FV(e)\\ FV(e_1\ e_2) &=& FV(e_1) \cup FV(e_2) \end{array}

Our datatype also permits raw terms containing a dangling index. For example, the term 0 has no free name, but it has no lambda for its index to refer to either. We regard such a term as ill-scoped, not as a term with a free named variable. The proposition ScopedAt d t says that every index in t is smaller than the number d of binders supplied by its surroundings. A term is locally closed when it needs no surrounding binders.

Consequently, a closed de Bruijn term must satisfy two independent conditions: it is locally closed, and it contains no free names.

1.4. Capture-Avoiding Substitution🔗

Contracting a beta redex replaces the parameter of a lambda by its argument:

(\lambda x.\ e)\ s \longrightarrow e[x := s].

In ordinary named notation, e[x := s] means “replace the occurrences of x that are free in the body e by s.” This replacement must respect the lambdas already inside e. For example,

(\lambda x.\lambda y.\ x)\ y

must return a constant function whose result is the free variable y. It must not become λy. y, which would turn that free variable into a bound one. With de Bruijn indices the redex is (λ λ 1) y, and the correct result is unambiguously λ y.

The implementation never substitutes for the string x. Instead, beta reduction substitutes for index 0, which refers to the parameter of the lambda being removed. We first define shifting, which adjusts an index when a term passes beneath a binder, and then define substitution itself.

1.5. Beta Reduction🔗

An application whose function is a lambda is called a beta redex:

(\lambda.\ e)\ s.

Contracting the redex removes the lambda and substitutes the argument for index 0 in the body. The resulting term is called the contractum:

(\lambda.\ e)\ s \to_\beta [s/0]e.

A larger term can contain several redexes. We therefore define beta reduction as a relation rather than as a function: one step chooses a single redex. The first rule below contracts a redex at the root; the remaining rules allow one step in the function, the argument, or the body of a lambda.

\frac{}{(\lambda.\ e)\ e' \to_\beta [e'/0]e} \qquad \frac{e_1 \to_\beta e_1'}{e_1\ e_2 \to_\beta e_1'\ e_2} \qquad \frac{e_2 \to_\beta e_2'}{e_1\ e_2 \to_\beta e_1\ e_2'} \qquad \frac{e \to_\beta e'}{\lambda.\ e \to_\beta \lambda.\ e'}

This is full beta reduction. In particular, reduction is allowed beneath a lambda. We have not chosen an evaluation strategy such as call-by-value or call-by-name.

Most calculations require more than one contraction. We write e →βᵇ* e' for zero or more beta steps. “Zero or more” is important: every term reduces to itself.

\frac{}{e \to_\beta^* e} \qquad \frac{e \to_\beta^* e' \qquad e' \to_\beta e''}{e \to_\beta^* e''}

Finally, a term is in normal form if it has no possible beta step. Because we use full beta reduction, a lambda is normal only when its body is normal.