Can any one please help:
Attachment 22313
Printable View
Can any one please help:
Attachment 22313
Alpha-conversion needs to be performed to avoid variable capture. This happens when reducingand the term N has some free variable y that would become bound if N is substituted for x in M because there is a
somewhere inside M. To avoid capture of y,
in M has to be renamed into some
. For example, in problem (a), x would be captured if substituted for y in
, so this bound x has to be renamed.
Consider problem (b). I'll omit some parentheses and will writefor
.
-> (substituting
for x)
-> (need to rename y because the argument has y free)
-> (substituting
for x)