6.1 Terms and Contexts

---

6.1 Terms and Contexts

De Bruijn's idea was that we can represent terms more straightforwardly—if less readably—by making variable occurrences point directly to their binders, rather than referring to them by name. This can be accomplished by replacing named variables by natural numbers, where the number k stands for "the variable bound by the k'th enclosing λ." For example, the ordinary term λx.x corresponds to the nameless term λ.0, while λx.λy. x (y x) corresponds to λ.λ. 1 (0 1). Nameless terms are also sometimes called de Bruijn terms, and the numeric variables in them are called de Bruijn indices^[2] Compiler writers use the term "static distances" for the same concept.

6.1.1 Exercise [⋆]

For each of the following combinators

   c0 = λs. λz. z;   c2 = λs. λz. s (s z);   plus = λm. λn. λs. λz. m s (n z s);   fix = λf. (λx. f (λy. (x x) y)) (λx. f (λy. (x x) y));   foo = (λx. (λx. x)) (λx. x); 

write down the corresponding nameless term.

Formally, we define the syntax of nameless terms almost exactly like the syntax of ordinary terms (5.3.1). The only difference is that we need to keep careful track of how many free variables each term may contain. That is, we distinguish the sets of terms with no free variables (called the 0-terms), terms with at most one free variable (1-terms), and so on.

6.1.2 Definition [Terms]

Let T be the smallest family of sets {T₀, T₁, T₂,...} such that

1. k Î T_n whenever 0 ≤ k < n;

2. if t₁ Î T_n and n > 0, then λ.t₁ Î T_n-1;

3. if t₁ Î T_n and t₂ Î T_n, then (t₁ t₂) Î T_n

(Note that this is a standard inductive definition, except that what we are defining is a family of sets indexed by numbers, rather than a single set.) The elements of each T_n are called n-terms.

The elements of T_n are terms with at most n free variables, numbered between 0 and n - 1: a given element of T_n need not have free variables with all these numbers, or indeed any free variables at all. When t is closed, for example, it will be an element of T_n for every n.

Note that each (closed) ordinary term has just one de Bruijn representation, and that two ordinary terms are equivalent modulo renaming of bound variables iff they have the same de Bruijn representation.

To deal with terms containing free variables, we need the idea of a naming context. For example, suppose we want to represent λx. y x as a nameless term. We know what to do with x, but we cannot see the binder for y, so it is not clear how "far away" it might be and we do not know what number to assign to it. The solution is to choose, once and for all, an assignment (called a naming context) of de Bruijn indices to free variables, and use this assignment consistently when we need to choose numbers for free variables. For example, suppose that we choose to work under the following naming context:

•  

  Г	=	x ↦ 4
  		y ↦ 3
  		z ↦ 2
  		a ↦ 1
  		b ↦ 0

Then x (y z) would be represented as 4 (3 2), while λw. y w would be represented as λ. 4 0 and λw.λa.x as λ.λ.6.

Since the order in which the variables appear in Г determines their numerical indices, we can write it compactly as a sequence.

6.1.3 Definition

Suppose x₀ through x_n are variable names from ⋎. The naming context Г = x_n, x_n-1, ... x₁, x₀ assigns to each x_i the de Bruijn index i. Note that the rightmost variable in the sequence is given the index 0; this matches the way we count λ binders—from right to left—when converting a named term to nameless form. We write dom(Г) for the set {x_n, ..., x₀} of variable names mentioned in Г.

6.1.4 Exercise [⋆⋆⋆ ↛]

Give an alternative construction of the sets of n-terms in the style of Definition 3.2.3, and show (as we did in Proposition 3.2.6) that it is equivalent to the one above.

6.1.5 Exercise [Recommended, ⋆⋆⋆]

1. Define a function removenames_Г (t) that takes a naming context Г and an ordinary term t (with FV(t) ⊆ dom(Г)) and yields the corresponding nameless term.

2. Define a function restorenames_Г (t) that takes a nameless term t and a naming context Г and produces an ordinary term. (To do this, you will need to "make up" names for the variables bound by abstractions in t. You may assume that the names in Г are pairwise distinct and that the set ⋎ of variable names is ordered, so that it makes sense to say "choose the first variable name that is not already in dom(Г).")

This pair of functions should have the property that

• removenames_Г (restorenames_Г (t)) = t

for any nameless term t, and similarly

• restorenames_Г (removenames_Г (t)) = t,

up to renaming of bound variables, for any ordinary term t.

Strictly speaking, it does not make sense to speak of "some t Î T"—we always need to specify how many free variables t might have. In practice, though, we will usually have some fixed naming context Г in mind; we will then abuse the notation slightly and write t Î T to mean t Î T_n, where n is the length of Г.

^[2]Note on pronunciation: the nearest English approximation to the second syllable in "de Bruijn" is "brown," not "broyn."

---