6.2 Shifting and Substitution

< Free Open Study >

Our next job is defining a substitution operation ([k ↦ s]t) on nameless terms. To to this, we need one auxiliary operation, called "shifting," which renumbers the indices of the free variables in a term.

When a substitution goes under a λ-abstraction, as in [1 ↦ s](λ.2) (i.e., [x ↦ s](λy.x), assuming that 1 is the index of x in the outer context), the context in which the substitution is taking place becomes one variable longer than the original; we need to increment the indices of the free variables in s so that they keep referring to the same names in the new context as they did before. But we need to do this carefully: we can't just shift every variable index in s up by one, because this could also shift bound variables within s. For example, if s = 2 (λ.0) (i.e., s = z (λw.w), assuming 2 is the index of z in the outer context), we need to shift the 2 but not the 0. The shifting function below takes a "cutoff" parameter c that controls which variables should be shifted. It starts off at 0 (meaning all variables should be shifted) and gets incremented by one every time the shifting function goes through a binder. So, when calculating , we know that the term t comes from inside c-many binders in the original argument to ↑^d. Therefore all identifiers k < c in t are bound in the original argument and should not be shifted, while identifiers k ≥ c in t are free and should be shifted.

6.2.1 Definition [Shifting]

The d-place shift of a term t above cutoff c, written , is defined as follows:

We write ↑^d (t) for .

6.2.2 Exercise [⋆]

What is ↑² (λ.λ. 1 (0 2))?
What is ↑² (λ. 0 1 (λ. 0 1 2))?

6.2.3 Exercise [⋆⋆ ↛]

Show that if t is an n-term, then is an (n+d)-term.

Now we are ready to define the substitution operator [j ↦ s]t. When we use substitution, we will usually be interested in substituting for the last variable in the context (i.e., j = 0), since that is the case we need in order to define the operation of beta-reduction. However, to substitute for variable 0 in a term that happens to be a λ-abstraction, we need to be able to substitute for the variable number numbered 1 in its body. Thus, the definition of substitution must work on an arbitrary variable.

6.2.4 Definition [Substitution]

The substitution of a term s for variable number j in a term t, written [j ↦ s]t, is defined as follows:

6.2.5 Exercise [⋆]

Convert the following uses of substitution to nameless form, assuming the global context is Г = a,b, and calculate their results using the above definition. Do the answers correspond to the original definition of substitution on ordinary terms from §5.3?

[b ↦ a] (b (λx.λy.b))
[b ↦ a (λz.a)] (b (λx.b))
[b ↦ a] (λb. b a)
[b ↦ a] (λa. b a)

6.2.6 Exercise [⋆⋆ ↛]

Show that if s and t are n-terms and j ≤ n, then [j ↦ s]t is an n-term.

6.2.7 Exercise [⋆ ↛]

Take a sheet of paper and, without looking at the definitions of substitution and shifting above, regenerate them.

6.2.8 Exercise [Recommended, ⋆⋆⋆]

The definition of substitution on nameless terms should agree with our informal definition of substitution on ordinary terms. (1) What theorem needs to be proved to justify this correspondence rigorously? (2) Prove it.

< Free Open Study >