The meaning of a lambda expression is found by carrying out its function applications (combinations).
Evaluating a lambda expression is called reduction.
The basic reduction rule involves substituting expressions for free variables in a manner similar to the way that the parameters in a function definition are passed as arguments in a function call.
The main rule for simplifying a lambda expression, called β-reduction, encompasses the operation of function application.
Since substituting for free variables in an expression may cause variable capture, we first need a mechanism for changing the name of a bound variable in an expression.
α-conversion
The choice of a variable name is not important.
A name can be changed provided this is done “systematically.”
This is called α-conversion.
If x and y are variables and E is a lambda expression,
( λx . E ) ⇒α ( λy . E[y/x] )
provided that y does not occur at all in E.
E[y/x] is defined to be the expression E, with y replacing all occurrences of the x in E.
Renaming can be used to prevent name clashes:
λx . ( λx . x ) ⇒α λx . ( λy . y )
Two more examples of α-conversion are
λy . ( λf . f x ) y ⇒α λz . ( λf . f x ) z
λz . ( λf . f x ) z ⇒α λz . ( λg . g x ) z