Summary of the lambda calculus (λ) evaluation rules

by Liger Learn

This article is part of a series of articles on the lambda calculus and is also available as a YouTube video.

1. What is the lambda (λ) calculus?
2. Bound vs. free variables in the lambda (λ) calculus
3. Delta (δ) rules in the lambda (λ) calculus
4. Beta (β) reduction in the lambda (λ) calculus
5. Alpha (α) conversion in the lambda (λ) calculus
6. Eta (η) conversion in the lambda (λ) calculus
7. (This article) Summary of the lambda calculus (λ) evaluation rules
8. Lambda calculus (λ) reduction orders and normal form
9. The Church-Rosser theorem and the lambda (λ) calculus

If you have made it here, then you will agree it is probably a good idea to take a second to do a quick summary of the four evaluation rules we covered in the previous articles:

• Delta (δ) rules
  • These are the rules we can use to evaluate “in-built” functions in the lambda calculus such as addition and subtraction.
• Beta (β) reduction
  • This is what we use to apply an argument to a lambda abstraction.
  • We do this by copying the body of the lambda abstraction and replacing all free occurrences of the formal parameter with the argument.
• Alpha (α) conversion
  • This is used to rename variables within a lambda expression.
  • It is sometimes needed before performing a beta-reduction to prevent the name-capture problem from occurring
• Eta (η) reduction
  • This is an optimisation which can be used to remove a lambda abstraction with a simpler expression.

There you have it! In the next article we will be looking at reduction orders in the lambda calculus and what “normal form” means!