Mathematics for Computer Science

7.4. Arithmetic Expressions 171

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

eval.[ 3 C[xx] ];2/Deval. 3 ;2/Ceval.[xx];2/ (by Def 7.4.2.7.11)

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

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

D 3 C.2
2/ (by Def 7.4.2.7.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 7.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) (7.14)

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

 Constructor cases:

subst.f;[e 1 Ce 2 ]/WWD[subst.f;e 1 /Csubst.f;e 2 /] (7.16)

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

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