Reduction Strategies

Multiple Redexes

When a term contains more than one redex (a reducible expression -- an abstraction applied to an argument), you must choose which one to reduce. For example:

(λx.x) ((λy.y) z)

This term has two redexes:

1. The outer redex: (λx.x) ((λy.y) z) -- the whole term
2. The inner redex: (λy.y) z -- inside the argument

Both are valid choices. A reduction strategy is a rule that determines which redex to reduce at each step. Different strategies can lead to different intermediate terms, though confluence guarantees that if both reach a normal form, it will be the same one.

What Is Normal Order?

Normal order reduction always selects the leftmost outermost redex. In a term with multiple redexes, find the one that:

1. Is not contained inside any other redex (outermost)
2. Among outermost redexes, is furthest to the left

For example, in (λx.x) ((λy.y) z):

• The outer redex (λx.x) ((λy.y) z) is outermost
• The inner redex (λy.y) z is nested inside the argument

Normal order picks the outer redex first.

What Is Applicative Order?

Applicative order reduction always selects the leftmost innermost redex. This means:

1. Find redexes that contain no other redexes (innermost)
2. Among innermost redexes, pick the leftmost

In effect, applicative order evaluates arguments before applying them. In (λx.x) ((λy.y) z):

• The inner redex (λy.y) z contains no other redexes -- it is innermost
• Applicative order reduces it first, giving (λx.x) z
• Then the outer redex (λx.x) z is reduced, giving z

Normal Order Example

Normal order always reduces the leftmost outermost redex.

Consider (λx.x) ((λy.y) z). There are two redexes:

• Outer: (λx.x) ((λy.y) z) -- the entire term
• Inner: (λy.y) z -- nested inside the argument

Normal order picks the outer redex. Reducing it substitutes ((λy.y) z) for x in the body x, giving (λy.y) z. Then the remaining redex (λy.y) z reduces to z.

Normal order path: (λx.x) ((λy.y) z) →β (λy.y) z →β z

Applicative Order Example

Applicative order always reduces the leftmost innermost redex.

Consider (λx.x) ((λy.y) z). There are two redexes:

• Outer: (λx.x) ((λy.y) z) -- the entire term
• Inner: (λy.y) z -- inside the argument

Applicative order picks the inner redex. Reducing (λy.y) z gives z. The term becomes (λx.x) z. Then the remaining redex reduces to z.

Applicative order path: (λx.x) ((λy.y) z) →β (λx.x) z →β z

Identify the Strategy

The two fundamental reduction strategies are:

• Normal order: always reduce the leftmost outermost redex. The outermost redex is reduced before its arguments are simplified.

• Applicative order: always reduce the leftmost innermost redex. Arguments are fully reduced before being passed to the function.

These two strategies represent opposite philosophies: normal order works from the outside in, while applicative order works from the inside out.

Call-by-Name

Call-by-name is a restricted form of normal order. Like normal order, it reduces the leftmost outermost redex. But it adds one restriction: never reduce inside a lambda body.

Normal order will enter λx.M and reduce redexes inside M. Call-by-name stops as soon as the outermost term is an abstraction.

For example, λx.(λy.y) x contains a redex inside the body. Normal order reduces it to λx.x. Call-by-name leaves it alone -- the outer λx means the term is "good enough."

Call-by-name corresponds to lazy evaluation in programming languages like Haskell: arguments are passed unevaluated, and computation inside a function body does not proceed until the result is demanded.

Call-by-Value

Call-by-value is a restricted form of applicative order. Like applicative order, it reduces arguments before applying a function. But it adds one restriction: never reduce inside a lambda body.

A redex (λx.M) N is only reduced when N is a value -- a term that cannot be reduced further without entering a lambda. In pure lambda calculus, values are abstractions: λx.M.

For example, in (λx.x) ((λy.y) z):

• Call-by-value first reduces (λy.y) z to z (a value in this context), then reduces (λx.x) z to z

Call-by-value corresponds to eager evaluation in languages like JavaScript, Python, and C: arguments are fully evaluated before being passed to a function.

Strategy Matters

Can different strategies give different results? In a sense, yes.

Consider (λx.λy.y) ((λz.z z)(λz.z z)).

The argument (λz.z z)(λz.z z) is the term $\Omega$ -- it reduces to itself forever and has no normal form.

• Normal order reduces the outer redex first. The function λx.λy.y discards its argument (it never uses x). The result is λy.y -- the identity function. Normal form found.

• Applicative order reduces the argument first, trying to simplify $\Omega$ before passing it in. But $\Omega$ reduces to itself. Applicative order loops forever and never reaches a normal form.

Both strategies agree when they both terminate. But when a diverging subterm exists, normal order may still succeed by discarding it, while applicative order is forced to evaluate it.

Normal Order Guarantee

The standardization theorem gives normal order a unique guarantee:

If a term has a normal form, normal order reduction will find it.

No other standard strategy makes this promise. Applicative order may diverge on terms that have a perfectly good normal form -- it gets stuck reducing arguments that will be discarded.

Normal order succeeds because it reduces outermost redexes first. If a function discards its argument, normal order never wastes time reducing that argument. Applicative order is forced to reduce it regardless.

This does not mean normal order is always faster or always better. It means normal order is complete -- it will never miss a normal form that exists.