Example
2013
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 the 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-conversions can take place, and more of that shortly.
We will use the symbol '⇒' to mean that one formula can be re-written to another, so, for example, λa.a ⇒ λb.b means that λa.a can be rewritten (reduced) to λb.b (in this case by a one step alpha reduction).
Try to prove the following:-
a) λa.a ⇒ λb.b
b) λw.(λx.(λy.w a) w) ⇒ λu.(λx.(λy.u a) u)
c) λw.(λx.(λy.w a) w) ⇒ λy.(λx.(λy.y a) y)
[Click on a formula to select it, choose a rule from the menu.]
One of them cannot be done.
In our implementation of alpha reduction, we haven't made available the rewriting of a subformula by alpha reduction. The reason for this is that the only time we need alpha reduction 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)!
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.
egs.
(λx.x y) beta reduces to y
(λx.(x x) λy.y) beta reduces to (λy.y λy.y) and that beta reduces to λy.y
This rule can be used on sub-expressions of an expression.
HINT: Beta-reduction is always used on a application, that is, on an expression of the form (<leftExpr> <rightExpr>) and, in turn, the left expression has to be a lambda abstraction ie 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.
Roughly, an expression M=>N (M beta reduces to N) iff
i) it alpha converts to N,
ii) N is the result of a single beta reduction on M,
iii) M and N are identical applications except one of M's subexpressions has been beta reduced to get
N,
iv) M and N are identical abstractions except one of M's subexpressions has been beta reduced to get N
Then two expressions M and N are 'equal', written M=N, iff i) they are alpha-convertible, ii) one can be beta-reduced from the other, or iii) there's another expression E which they are both equal to.
Video illustrating the software in use
Try to prove the following:-
a) (λw.w a) ⇒ a
b) (λx.(x x) λy.y) ⇒ λy.y
c) ((λx.λy.y a) b) ⇒ b
Now, you may not always be able to make the beta reduction you want to because of capturing. However, any lambda expression contains only a finite number of variables and we have infinitely many variables available to us. So we can use alpha conversion to change the variable of the suspect piece to some totally new variable and then do the beta reduction without capture. For example, the expression
(λx.λy.x y) reduces to λy.y ? or does it?
Apparently it should reduce, since it is an application with an abstraction in the function position. However what seems likely as a simple beta reduction is λy.y which is forbidden because of the capture. But if
(λx.λy.x y) is alpha converted to (λx.λz.x y) the new expression reduces to λz.y.
There is a third reduction rule, which we will not need at all. It is just mentioned here for completeness.
Eta reduction (extensional equality of functions)
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).