lambda x. x + zcan be alpha-converted to
lambda y. y + z
(lambda x. M) N = [ N / x ] MSubstitute N for every free occurrence of x in M, renaming bound variables of M as needed to avoid variable capture.
(lambda x. M) N -> [ N / x ] M
lambda x. x and lambda y. ydefine exactly the same function (the identity function).
In contrast, the name of a free variable is important. Free variables cannot be renamed without potentially changing the value of an expression. For example, in the following code fragment (in which x appears as a free variable) , we cannot rename x to y without changing the value of the expression:
3 + x(assume x is bound to 2 and y to 3).
fis a value
x = f(x)
(lambda x.(lambda y. x))y = [y/x](lambda y. x) != lambda y. yy should be free but accidentally becomes bound. To avoid variable capture, all bound variables should be renamed so that their names are different from those of all free variables and all other bound variables.
Y = lambda f. (lambda x. f(xx))(lambda x. f(xx))