In general, for some expressions E, E' and a variable V, we want E[E'/V] to be the result of putting E' into the expression E everyplace that V had occured free in E. However, it is possible that a variable, which occurs free in E', might "accidentally" become bound if we stick it into E.
For example:
E = \x . y x (which means apply y some parameter) E' = xIf we naively apply the definition, we would get \x. x x for E[E'/y]. But this would be the function which applies the parameter itself--which is clearly not what we had before. (Note that if E' had been some other variable--say z--this substitution would have worked. What we need is some rules to check that this problem does not occur.)
If E is: Then E[E'/V] is: V E' V' (where V <> V') V' (V does not occur) E1 E2 E1[E'/V] E2[E'/V] (struct induction) \V. E1 \V. E1 (V always bound) \V'. E1 \V'. E1[E'/V] (V <> V' and V' not free in E') \V'. E1 \V''. E1[V''/V'][E'/V] (V <> V' and (pick V'' free in E and E') V' is free in E') Use the rules above to work out: i) (\y. x (\x. x))[(\y. y x)/x] ii) (y (\z. x z))[(\y. z y)/x]Answer