Chapter 6: Nameless Representation of Terms

---

Overview

In the previous chapter, we worked with terms "up to renaming of bound variables," introducing a general convention that bound variables can be renamed, at any moment, to enable substitution or because a new name is more convenient for some other reason. In effect, the "spelling" of a bound variable name is whatever we want it to be. This convention works well for discussing basic concepts and for presenting proofs cleanly, but for building an implementation we need to choose a single representation for each term; in particular, we must decide how occurrences of variables are to be represented. There is more than one way to do this:

1. We can represent variables symbolically, as we have done so far, but replace the convention about implicit renaming of bound variables with an operation that explicitly replaces bound variables with "fresh" names during substitution as necessary to avoid capture.

2. We can represent variables symbolically, but introduce a general condition that the names of all bound variables must all be different from each other and from any free variables we may use. This convention (sometimes called the Barendregt convention) is more stringent than ours, since it does not allow renaming "on the fly" at arbitrary moments. However, it is not stable under substitution (or beta-reduction): since substitution involves copying the term being substituted, it is easy to construct examples where the result of substitution is a term in which some λ-abstractions have the same bound variable name. This implies that each evaluation step involving substitution must be followed by a step of renaming to restore the invariant.

3. We can devise some "canonical" representation of variables and terms that does not require renaming. ^[1]

4. We can avoid substitution altogether by introducing mechanisms such as explicit substitutions (Abadi, Cardelli, Curien, and Lévy, 1991a).

5. We can avoid variables altogether by working in a language based directly on combinators, such as combinatory logic (Curry and Feys, 1958; Barendregt, 1984)-variant of the lambda-calculus based on combinators instead of procedural abstraction-or Backus' functional language FP (1978).

Each scheme has its proponents, and choosing between them is somewhat a matter of taste (in serious compiler implementations, there are also performance considerations, but these do not concern us here). We choose the third, which, in our experience, scales better when we come to some of the more complex implementations later in the book. The main reason for this is that it tends to fail catastrophically rather than subtly when it is implemented wrong, allowing mistakes to be detected and corrected sooner rather than later. Bugs in implementations using named variables, by contrast, have been known to manifest months or years after they are introduced. Our formulation uses a well-known technique due to Nicolas de Bruijn (1972).

^[1]The system studied in this chapter is the pure untyped lambda-calculus, λ (Figure 5-3). The associated OCaml implementation is fulluntyped.

---