9/13/19
Alpha conversion (Rewrite of bound variables):-
Any abstraction
λ<variable1>.<expr>
can be converted to
λ<variable2>.<expr>/.<variable1> -><variable2> provided the substitution <expr> /. <variable1> -> <variable2> is sound.
In the simplest cases alpha conversion allows you to change, for example, λy.y into λx.x or λz.z. The rule can also be applied to subexpressions— λy.λz.(z y) can be converted to λy.λw.(w y) with the underlined pieces being re-written (question: can it be converted to λy.λy.(y y ) ? if not, why not?)
Normally we regard expressions with rewritten bound variables as same. Sometimes this is called alpha congruence.
Alpha conversion is not going to be a lot of interest to us— we need it only for ensuring that beta-reductions can take place, and more of that shortly.
Beta reduction (the effect of function application):-
Any function application
(λ<variable>.<expr1> <expr2>)
can be converted to
<expr1> /. <variable> -> <expr2> provided the substitution <expr1> /. <variable> -> <expr2> is sound.
e.g.
(λx.x y) beta reduces to y
(λx.(x x) λy.y) beta reduces to (λy.y λy.y)
and (λy.y λy.y) beta reduces to λy.y
This rule can be used on sub-expressions of an expression.
HINT: Beta-reduction is always used on an application, that is, on an expression of the form (<leftExpr> <rightExpr>) and, in turn, the left expression has to be a lambda abstraction i.e. it has to start with λ. So, within the grammar we are using, an expression can be beta-reduced iff it starts with the two characters '(λ'. So try to spot that sequence for it flags possible beta reductions. The expression, or sub-expression, which gets reduced is known as a redex (i.e. reducible expression).
In our implementation of reduction, we haven't made available the rewriting of a subformula by alpha conversion. The reason for this is that the only time we need alpha conversion at all is to push through a beta reduction when there is capture of variable, but our implementation of beta reduction does the alpha rewrite automatically (leaving you to concentrate on more important matters)!
Eta reduction (extensional equality of functions)
This is a third reduction rule, which we will not need at all. It is just mentioned here for completeness. Any abstraction with the form
λ<variable>.(<expr> <variable> )
can be reduced to
<expr> provided <variable> is not free in <expr>.
For example, λx.(y x) can be eta reduced to y.
The motivation behind eta reduction is that the effect of an application of either of the eta expressions is the same. Apply our example expressions to, say, z
(λx.(y x) z) beta reduces to (y z) which is exactly the application of y to z, namely (y z).