Mathematics for Computer Science

Chapter 7 Recursive Data Types172

Here’s how the recursive definition of the substitution function would find the
result of substituting3xforxin thex.x1/:

subst.3x;x.x1//

Dsubst.[ 3 x];[x[xC[ 1 ] ] ]/ (unabbreviating)

D[subst.[ 3 x];x/subst.[ 3 x];[xC[ 1 ] ]/] (by Def 7.4.3 7.17)

D[ [ 3 x]subst.[ 3 x];[xC[ 1 ] ]/] (by Def 7.4.3 7.14)

D[ [ 3 x][subst.[ 3 x];x/Csubst.[ 3 x];[ 1 ]/] ] (by Def 7.4.3 7.16)

D[ [ 3 x][ [ 3 x]C[subst.[ 3 x];1/] ] ] (by Def 7.4.3 7.14 & 7.18)

D[ [ 3 x][ [ 3 x]C[ 1 ] ] (by Def 7.4.3 7.15)

D3x.3x1/ (abbreviation)

Now suppose we have to find the value of subst.3x;x.x1//whenx D 2.
There are two approaches.
First, we could actually do the substitution above to get3x.3x1/, and then
we could evaluate3x.3x1/whenxD 2 , that is, we could recursively calculate
eval.3x.3x1/;2/to get the final value 30. In programming jargon, this would
be called evaluation using theSubstitution Model. Because the formula3xap-
pears twice after substitution, the multiplication 3
2 that computes its value gets
performed twice.
The other approach is called evaluation using theEnvironment Model. Namely,
to compute
eval.subst.3x;x.x1//;2/ (7.19)

we evaluate3xwhenxD 2 using just 1 multiplication to get the value 6. Then
we evaluatex.x1/whenxhas this value 6 to arrive at the value 6
5 D 30. So
the Environment Model only computes the value of3xonce and so requires one
fewer multiplication than the Substitution model to compute (7.19). But how do we
know that these final values reached by these two approaches always agree? We can
prove this easily by structural induction on the definitions of the two approaches.
More precisely, what we want to prove is

Theorem 7.4.4.For all expressionse;f 2 Aexp andn 2 Z,

eval.subst.f;e/;n/Deval.e;eval.f;n//: (7.20)

Proof. The proof is by structural induction one.^1

Base cases:

(^1) This is an example of why it’s useful to notify the reader what the induction variable is—in this
case it isn’tn.