Reduction in Lambda Calculus

Question

I have been recently studying about lambda calculation and i have many doubts about reduction and substitution . What is alpha and beta reduction are? And when and why are they used ?.

It would be great if someone could tell any good resources on reduction and substitution in lambda caculus.

Answer 1

Beta reduction is just the primary application rule used for computation within the lambda calculus. It is applied through substitution as shown:

If you had the lambda term: (\x.x) and some value to the right of it: y

Then you would substitute all the bound variables to the right of the (.) in your lambda term. The bound variables are the variables that match the variable left of the (.), so in this case x.

The reduction would be of the form:
(\x.x)y    //y gets bound to all occurences of x to the right of the period
y

Where y is bound to all occurrences of x in the lambda expression. This is the identity function.

Alpha "reductions" are usually called alpha equivalences or alpha rewrite rules. They state that you can change the name of any lambda term and its bound variables without changing the meaning of the expression.

For example using the identity function from above we could just as easily written the lambda term as (\j.j). It wouldn't change the outcome of our application as shown:

(\j.j)y    //y gets bound to all occurrences of j to the right of the period
y

As to learning resources: the wikipedia page is pretty detailed, but notation heavy and would probably require a few good rereads.

If you're just looking for better intuition as to how lambda calculus works, most computer science departments have slides laying around.

You might find these helpful: http://www.classes.cs.uchicago.edu/archive/2002/winter/CS33600/slides/Lesson2.pdf https://www.utdallas.edu/~gupta/courses/apl/lambda.pdf