6.3 Evaluation

---

6.3 Evaluation

To define the evaluation relation on nameless terms, the only thing we need to change (because it is the only place where variable names are mentioned) is the beta-reduction rule, which must now use our new nameless substitution operation.

The only slightly subtle point is that reducing a redex "uses up" the bound variable: when we reduce ((λx.t₁₂) v₂) to [x ↦ v₂]t₁₂, the bound variable x disappears in the process. Thus, we will need to renumber the variables of the result of substitution to take into account the fact that x is no longer part of the context. For example:

•  

  (λ.1 0 2) (λ.0) → 0 (λ.0) 1

  (not 1 (λ.0) 2).

Similarly, we need to shift the variables in v₂ up by one before substituting into t₁₂, since t₁₂ is defined in a larger context than v₂. Taking these points into account, the beta-reduction rule looks like this:

The other rules are identical to what we had before (Figure 5-3).

6.3.1 Exercise [⋆]

Should we be worried that the negative shift in this rule might create ill-formed terms containing negative indices?

6.3.2 Exercise [⋆⋆⋆]

De Bruijn's original article actually contained two different proposals for nameless representations of terms: the deBruijn indices presented here, which number lambda-binders "from the inside out," and de Bruijn levels, which number binders "from the outside in." For example, the term λx. (λy. x y) x is represented using deBruijn indices as λ. (λ. 1 0) 0 and using deBruijn levels as λ. (λ. 0 1) 0. Define this variant precisely and show that the representations of a term using indices and levels are isomorphic (i.e., each can be recovered uniquely from the other).

---