The Lambda Calculus: Reduction

---

The λ-Calculus Series

1. A Brief History
2. A Quick Primer for λ-Calculus
3. Reduction Explained
4. Church Numerals
5. Arithmetic
6. Logic
7. Pai rs and Lists
8. Combinators

Okay, I promised some of you I would make this one quick. This may be the dullest post in the series, and for that I apologize. I do want to cover it quickly, if not for the 1 curious person out there who cares, then for myself when I need to refresh my memory in 2.6 years.

What we're going to see in this post:

• Why is reduction useful?
• What is reduction?

Why Is Lambda Reduction Useful?

Well, in a nutshell, lambda reduction is what allows us to get useful results in a lambda calculus. In other words, lambda reduction is how we do actual computation in a lambda calculus. If we want to gain any sort of practical insight from the lambda calculus, we're going to need reduction.

The analog to elementary algebraic manipulation is very strong: variable manipulation, simplification of terms, solving systems of equations, etc. When we learn to do these things at the beginning of secondary school, most of us have to practice with countless examples before we ultimately gain a strong intuition for elementary algebra and can work with equations easily and naturally. This resulted in a skill that we can apply to many areas of our lives where we need to find the answer to something that involves a complicated relationship with one or more other things.

In lambda calculus, instead of systems of equations that represent relationships between variables, we have a system whose focus is expressing computation itself. (Though it can, of course, be used perform algebraic manipulations.) As such, reduction is useful because it allows us to better and more clearly analyze our computational expressions.

What Is Lambda Reduction?

There are three types of reduction:  alpha, beta, and eta. Simply put:

• beta reduction is variable substitution;
• alpha reduction is essentially clarification/disambiguation of variable scope;
• eta reduction says that two functions are the same if and only if they give the same result no matter what arguments are given.