Slide 12.7: Curried functions (cont.)
Slide 12.9: Substitution
Home

Lambda Reduction

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