Mathematics for Computer Science

6.4. Arithmetic Expressions 185

For example, here’s how the recursive definition of eval would arrive at the value
of 3 Cx^2 whenxis 2:

eval.[ 3 +[xx] ];2/Deval. 3 ;2/Ceval.[xx];2/ (by Def 6.4.2.6.11)

D 3 Ceval.[xx];2/ (by Def 6.4.2.6.10)

D 3 C.eval.x;2/
eval.x;2// (by Def 6.4.2.6.12)

D 3 C.2
2/ (by Def 6.4.2.6.9)

D 3 C 4 D7:

Substituting into Aexp’s

Substituting expressions for variables is a standard operation used by compilers
and algebra systems. For example, the result of substituting the expression3xfor
xin the expressionx.x1/would be3x.3x1/. We’ll use the general notation
subst.f;e/for the result of substituting an Aexp,f, for each of thex’s in an Aexp,
e. So as we just explained,

subst.3x;x.x1//D3x.3x1/:

This substitution function has a simple recursive definition:

Definition 6.4.3.Thesubstitution functionfrom AexpAexp to Aexp is defined
recursively on expressions,e 2 Aexp, as follows. Letf be any Aexp.

 Base cases:

subst.f;x/WWDf; (subbingffor variable,x, just givesf) (6.14)

subst.f;k/WWDk (subbing into a numeral does nothing.) (6.15)

 Constructor cases:

subst.f;[e 1 +e 2 ]/WWD[subst.f;e 1 /+subst.f;e 2 /] (6.16)

subst.f;[e 1 e 2 ]/WWD[subst.f;e 1 /subst.f;e 2 /] (6.17)

subst.f;-[e 1 ]/WWD-[subst.f;e 1 /]: (6.18)