Friday, 9 January 2015

Lambda Calculus, Conversions and Reduction

There are three methods of reducing or converting a lambda expression. Two methods of conversion and one method of reduction. In some books or papers, conversion rules are also considered as reduction rules. These processes are in fact some rewriting rules to help us to change the appearance of a λ 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.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 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.