Recursion and Induction: Substitutions

A *substitution* is a set {*v_0* ← *t_0*, *v_1* ← *t_1*,
…} where each *v_i* is a distinct variable symbol and each *t_i* is a term.
If, for a given substitution *σ* and variable *v*, there is an *i* such
that *v* is *v_i*, we say *v* *is bound* by *σ*. If *v* is bound
by *σ*, then the *binding* of *v* in *σ* is *t_i*, for the
*i* such that *v_i* is *v*. (In set theory, a substitution is just a finite function
that maps the *v_i* to their respective *t_i*.)

The result of *applying* a substitution *σ* to a term *term* is
denoted *term*/*σ* and is defined as follows. If *term* is a
variable, then *term*/*σ* is either the binding of *term* in *σ* or
is *term* itself, depending on whether *term* is bound in *σ*. If
*term* is a quoted constant, *term*/*σ* is *term*. Otherwise, *term* is
`(`*f* *a_1* … *a_n*`)` and *term*/*σ* is `(`*f* *a_1*/*σ* …
*a_n*/*σ*`)`.

**Problem 6. ** Suppose

{x ← (car a), y ← (cdr x)}

What term is `(car (cons x (cons y (cons '"Hello" z))))`/*σ*?

Next: