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.zy+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 x is a bound variable (or at least not a free variable) in term T then (λx.T) x and T are equal. This is what we already saw in our previous posts too and basically says that if we evaluate a λ 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.
