# 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.

- What is the lambda (λ) calculus?
- Bound vs. free variables in the lambda (λ) calculus
- Delta (δ) rules in the lambda (λ) calculus
- Beta (β) reduction in the lambda (λ) calculus
- Alpha (α) conversion in the lambda (λ) calculus
- Eta (η) conversion in the lambda (λ) calculus
- (This article) Summary of the lambda calculus (λ) evaluation rules
- Lambda calculus (λ) reduction orders and normal form
- 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!

### Recommended Posts

##### Church-Rosser theorems and the lambda (λ) calculus

October 19, 2023

##### Lambda calculus (λ) reduction orders and normal form

October 19, 2023

##### Eta (η) conversion in the lambda (λ) calculus

October 19, 2023