i) (\y. x (\x. x))[(\y. y x)/x]

Clearly the body is an abstraction, the variable to substitute
for is not the binder, but the binder is not free in the
expression to be substituted in.
So, we consider the substitution against the body; and, since
it is an application, we consider the substitution against 
each part.
First we have (x[(\y. y x)/x]).  The term is just a variable,
and the one to be substituted for, so just replace.
Then we have the other term ((\x. x)[(\y. y x)/x]), but the
binder matches the variable to substitute for, so we just
get the second term back.
Therefore the answer is:

	(\y. (\y. y x) (\x. x))

ii) (y (\z. x z))[(\y. z y)/x]

The expression is an application, so apply the substitution
to each term.
The first term is just a variable not matching the "V".  So,
we just get the term back.
The second term is an abstraction where the binder does not
match the "substitution variable" (x and z), and the binder
is free in "E'" (\y. z y).  So we must pick a new variable,
call it "u", and update the body of the abstraction and
change the name of the binder.  Then we apply the subsitution
to the body of the abstraction (each of the two terms).
The first of these is the matching variable, replace with E',
the second is a non-matching variable, just return it.
So the answer is:

	(y (\u. (\y. z y) u))

BACK