Beta Reduction

What Is Beta Reduction?

Beta reduction applies an abstraction to an argument:

(λx.M) N →β M[x := N]

Take the body M, replace every free occurrence of x with N, and the result is the reduced term. You already know how substitution works from the previous concept — beta reduction is simply the rule that says when to perform it: when an abstraction meets its argument.

What Is a Redex?

A redex (short for reducible expression) is any term of the form (λx.M) N — an abstraction directly applied to an argument.

• (λx.x) a — this is a redex (λx.x applied to a)
• (λy.y y) z — this is a redex (λy.y y applied to z)
• λx.x — NOT a redex (an abstraction, but not applied to anything)
• x y — NOT a redex (x is a variable, not an abstraction)

A redex is the trigger for beta reduction. No redex, no reduction.

Identify the Redex

A redex is a term of the form (λx.M) N — an abstraction applied to an argument. To spot a redex, look for a λ in function position (the left side of an application).

Some terms contain a redex:

• (λx.x) a — the whole term is a redex
• (λy.y) (λz.z) — the whole term is a redex

Some terms contain no redex:

• x y — x is a variable, not an abstraction
• λx.x — an abstraction, but not applied to anything

One Step — Identity

The identity function λx.x returns its argument unchanged:

(λx.x) a →β x[x := a] = a

The body is just x, so substituting a for x gives a. The simplest possible beta reduction.

One Step — Duplication

When the parameter appears more than once in the body, substitution replaces every occurrence:

(λx.x x) y →β (x x)[x := y] = y y

Both xs become y. The argument is copied, not shared.

One Step — Discard

When the parameter does not appear in the body, the argument is simply thrown away:

(λx.z) a →β z[x := a] = z

There are no xs to replace, so a vanishes. The body z is returned unchanged. This is the constant function — it always returns the same thing regardless of its argument.

Not a Redex

Not every application is a redex. A redex requires an abstraction in function position — the left side of the application must start with λ.

• (λx.x) a — redex (abstraction applied to argument)
• x a — NOT a redex (x is a variable, not an abstraction)
• (x y) a — NOT a redex (x y is an application, not an abstraction)

When the function position holds a variable or another application, beta reduction cannot fire. The term is stuck — it cannot be reduced further (at least not at this position).

Result Can Be Another Function

The result of beta reduction does not have to be a simple value. It can be another abstraction — a function waiting for more input:

(λx.λy.x) a →β (λy.x)[x := a] = λy.a

The outer abstraction consumed a, but the inner λy remains. The result λy.a is a new function that ignores its argument and always returns a.

One Step — Free Variables Survive

Beta reduction replaces only the parameter variable. Any other variables in the body are left alone:

(λx.x y) a →β (x y)[x := a] = a y

Here x is bound (replaced by a) but y is free (untouched). Only blanks tagged with the parameter get filled — other tags refer to type pieces from elsewhere and are not ours to set.

Beta Is the Only Rule

Beta reduction is the only computation rule in lambda calculus.

• Variables, abstractions, applications — these define the language
• Free/bound, scope, shadowing — these describe structure
• Alpha equivalence — renames labels without changing meaning
• Substitution — the mechanism beta reduction uses

None of these do anything on their own. Beta reduction is where computation happens: (λx.M) N →β M[x := N]. One rule, applied repeatedly, produces all of computation.