Multi-Step Reduction

More Than One Step

Sometimes one beta reduction step produces a term that contains a new redex (a reducible expression — an abstraction applied to an argument).

Consider: (λx.λy.y) a b

This looks like one big expression, but application is left-associative, so it parses as ((λx.λy.y) a) b.

Step 1: The redex is (λx.λy.y) a. Substitute a for x in λy.y. Since x does not appear in the body, the result is just λy.y. The full term becomes (λy.y) b.

Step 2: Now (λy.y) b is a new redex. Substitute b for y in y, giving b.

We write this chain: (λx.λy.y) a b →β (λy.y) b →β b

Two-Step Reduction

When a term requires two beta reduction steps, work through them one at a time.

Example: (λx.λy.x) a b

Step 1: The outermost redex is (λx.λy.x) a. Substitute a for x in λy.x to get λy.a. The term becomes (λy.a) b.

Step 2: Now (λy.a) b is a redex. Substitute b for y in a. Since y does not appear in a, the result is just a.

Final result: a

Keep each step small and check: did the result create a new redex? If so, reduce again. If not, you are done.

When to Stop Reducing

A redex (reducible expression) is an abstraction applied to an argument: (λx.M) N. Beta reduction replaces one redex at a time.

You stop reducing when the term contains no more redexes. A term with no redexes is said to be in normal form — it cannot be reduced further.

For example:

• a is in normal form (just a variable, no redex)
• λx.x is in normal form (an abstraction, but not applied to anything)
• a b is in normal form (a is a variable, not an abstraction)
• (λx.x) a is not in normal form (it contains a redex)

We will study normal forms in depth later. For now, the key idea: keep reducing until there is nothing left to reduce.

Is There Another Step?

After performing a beta reduction step, look at the result and ask: does it contain a redex?

A redex is the pattern (λx.M) N — an abstraction directly applied to an argument. If you see this pattern anywhere in the result, another step is possible.

If the result is a variable (a), an abstraction not applied to anything (λx.M), or an application where the left side is not an abstraction (a b), then there is no redex and reduction is complete.

Scanning for redexes is a skill: look for a λ inside parentheses with an argument next to it.

Two Steps with Self-Application

Some reductions involve duplication: when the body uses the parameter more than once, the argument gets copied.

Consider: (λx.x x)(λy.y)

Step 1: Substitute λy.y for x in x x. Since x appears twice, the argument is duplicated:

(λy.y)(λy.y)

Step 2: Now apply the first λy.y to the second. Substitute λy.y for y in y:

λy.y

The identity function applied to itself returns itself. Two steps, and the result is a lambda — a function, not a plain variable.

Reduction Sequence

A reduction sequence shows each step of beta reduction with the →β arrow between them:

(λx.λy.x) a b →β (λy.a) b →β a

When multiple steps are needed, we can also write →β* (read "reduces in zero or more steps") to show the start and end without listing every intermediate term:

(λx.λy.x) a b →β* a

The →β* notation is shorthand. It does not skip steps — it just hides them. Every →β* can be expanded into individual →β steps.

To check a sequence, verify each arrow: is the left side a term with a redex, and is the right side the correct result of reducing that redex?

The Result Can Be a Function

After beta reduction, the result does not have to be a simple variable like a or b. It can be a lambda — a function waiting for an argument.

Example 1: (λx.λy.x) a →β λy.a

One argument was consumed, but the result λy.a is still a function. It will discard its argument and return a. This is partial application — not all arguments have been supplied yet.

Example 2: (λx.x)(λy.y) →β λy.y

The identity applied to the identity returns the identity. The result is a function, and that is perfectly normal.

In lambda calculus, functions are values. A reduction that produces a lambda is just as "finished" as one that produces a variable — as long as no redexes remain.

Stuck Expressions

Not every application is a redex. A redex requires an abstraction in the function position: (λx.M) N. When the function position is a variable, there is nothing to substitute and no reduction is possible.

x y — x is a variable, not an abstraction. No redex. The term is "stuck."

a (λx.x) — a is a variable, not an abstraction. No redex. Still stuck, even though the argument is a function.

(λx.x) a — λx.x is an abstraction applied to a. This is a redex.

A stuck term is not an error — it is simply a term that cannot be reduced further. It is in normal form. In a larger computation, stuck terms arise naturally when a free variable occupies the function position.