*λ*expression in a form we can work with, easier for any reason. A

*λ*expression can't be reduced more is called normal.

**Alpha Conversion**

α-conversion is nothing but renaming a bound variable in a

*λ*expression. We all know in mathematics that the function f(x)=2x exactly has the same property as f(y)=2y has, the same idea exists in

*λ*calculus but has a special naming, α-conversion. So both

*λx.x*and

*λy.y*are the equal term, the identity function, we sometimes say that

*λy.y*is the α-equivalent of

*λx.x.*

It is obvious we can't change x to y in f(x)=xy+x, the same is true in

*λ*calculus. So

*λz.*

*λy.z*

*y+x*is α-equivalent of

*λx.*

*λy.xy+x*but

*λx.*

*λx.xx+x*is not.

Now if you rename a free variable in a

*λ*expression, the process is called substitution, you may need to do some α-conversion before substituting a free variable. This is what we usually do in programming too. When we want to change the name of a variable we need to make sure there is no other variable in its scope with the same name.

**Eta Conversion**

η-conversion says if

`is a bound variable (or at least not a free variable) in term`

*x*`then (`

*T*`and`

*λx.T) x*`are equal. This is what we already saw in our previous posts too and basically says that if we evaluate a`

*T**λ*function application with its bound variable, we'll have the main

*λ*function as the result.

**Beta Reduction**

β reduction helps to reduce a function application, it says that

*(λx.T) T'*can be reduced to*T [x:=T']*, which means if you just substitute*x*with*T'*in*T*you'll have the result of the*λ*function application.
An example is (

*λx.x) (x+y)*can be α-converted to (*λz.z) (x+y)*and then simply β reduced to*x+y.*Note we just did a α-conversion to make the reduction easier to understand.
Another example is reducing (

*λx.λy.x y) y.*First we run an α-conversion to have (*λx.λz.x z) y*now to be clearer let us write it in this way (*λx.(λz.x z)) y*which gives us this result*λz.y z.*