The Substitution Lemma

The Substitution Lemma relates the value of an expression obtained by substituting f for x in e to the values of f and e. Namely, suppose F:A → B, that is, F is a total function with domain A and codomain B. For any a in A and b in B, we define
F[a ← b]
to be the function G:A → B such that
G(a) = b,         and         
G(x) = F(x),    for x ≠ a.

Substitution Lemma: For all valuations, V,
val(e[x:=f], V) = val(e, V[x ← val(f, V)]).

The proof is by a routine structural induction on e.

For example, if e is a sum e1 + e2, then
val(e[x:=f], V)
= val( (e1 + e2)[x:=f], V)
= val(e1[x:=f] + e2[x:=f], V) by def of substitution into a sum
= val(e1[x:=f], V) + val(e2[x:=f], V) by def of valof a sum
= val(e1, V[x ←val(f, V)] + val(e2, V[x ←val(f, V)]) by structural induction hypothesis
= val(e1+ e2, V[x ←val(f, V)]) by def of valof a sum
= val(e, V[x ←val(f, V)])
which proves the Lemma for sums.

This document last modified