7.2 Shifting and Substitution

---

7.2 Shifting and Substitution

The definition of shifting (6.2.1) can be translated almost symbol for symbol into OCaml.

   let termShift d t =     let rec walk c t = match t with       TmVar(fi,x,n) → if x>=c then TmVar(fi,x+d,n+d)                       else TmVar(fi,x,n+d)     | TmAbs(fi,x,t1) → TmAbs(fi, x, walk (c+1) t1)     | TmApp(fi,t1,t2) → TmApp(fi, walk c t1, walk c t2)     in walk 0 t 

The internal shifting is here represented by a call to the inner function walk c t. Since d never changes, there is no need to pass it along to each call to walk: we just use the outer binding of d when we need it in the variable case of walk. The top-level shift ↑^d (t) is represented by termShift d t. (Note that termShift itself is not marked recursive, since all it does is call walk once.)

Similarly, the substitution function comes almost directly from Definition 6.2.4:

   let termSubst j s t =     let rec walk c t = match t with       TmVar(fi,x,n) → if x=j+c then termShift c s else TmVar(fi,x,n)     | TmAbs(fi,x,t1) → TmAbs(fi, x, walk (c+1) t1)     | TmApp(fi,t1,t2) → TmApp(fi, walk c t1, walk c t2)     in walk 0 t 

The substitution [j ↦ s]t of term s for the variable numbered j in term t is written as termSubst j s t here. The only difference from the original definition of substitution is that here we do all the shifting of s at once, in the TmVar case, rather than shifting s up by one every time we go through a binder. This means that the argument j is the same in every call to walk, and we can omit it from the inner definition.

The reader may note that the definitions of termShift and termSubst are very similar, differing only in the action that is taken when a variable is reached. The untyped implementation available from the book's web site exploits this observation to express both shifting and substitution operations as special cases of a more general function called tmmap. Given a term t and a function onvar, the result of tmmap onvar t is a term of the same shape as t in which every variable has been replaced by the result of calling onvar on that variable. This notational trick saves quite a bit of tedious repetition in some of the larger calculi; §25.2 explains it in more detail.

In the operational semantics of the lambda-calculus, the only place where substitution is used is in the beta-reduction rule. As we noted before, this rule actually performs several operations: the term being substituted for the bound variable is first shifted up by one, then the substitution is made, and then the whole result is shifted down by one to account for the fact that the bound variable has been used up. The following definition encapsulates this sequence of steps:

   let termSubstTop s t =     termShift (-1) (termSubst 0 (termShift 1 s) t) 

---