Normal Forms

A term in normal form has no redexes. Head and weak head normal form.

8 topics • ~981 words

A fully typeset composing stick has no blank slugs remaining. Every position holds a type piece; there is nothing left to set. The stick is ready to print. A term in normal form is the same: no redexes remain, no reduction can fire. The computation is done.

We have been reducing terms by finding redexes and applying beta reduction. But how do we know when to stop? Normal form gives us the answer: a term is fully reduced when it contains no redexes at all. This is the endpoint of computation in lambda calculus.

What Is Normal Form?

A term is in normal form if it contains no redexes — no subterm of the form (λx.M) N.

Examples of terms in normal form:

  • x — a variable, no redex possible
  • λx.x — an abstraction, but not applied to anything
  • x y — an application, but x is a variable, not an abstraction
  • λx.y z — an abstraction whose body is in normal form

Examples of terms not in normal form:

  • (λx.x) a — contains a redex
  • λy.(λx.x) y — the body contains a redex

A term in normal form cannot be reduced further. It is the final result of the computation.

Recognizing Normal Form

To check whether a term is in normal form, scan it for redexes. A redex is any subterm of the form (λx.M) N — an abstraction applied to an argument.

In normal form (no redex anywhere):

  • a — variable
  • λx.x — abstraction with no redex in the body
  • a b — application, but a is a variable
  • λx.a (b c) — abstraction whose body has no redex

Not in normal form (contains a redex):

  • (λx.x) a — redex at the top level
  • a ((λx.x) b) — redex nested inside an argument
  • λy.(λx.x) y — redex inside the body of an abstraction

Not in Normal Form

A term is not in normal form if it contains at least one redex — a subterm of the form (λx.M) N. The redex does not have to be at the top level. It can be:

  • At the top: (λx.x) a
  • Inside a body: λy.(λx.x) y
  • Inside an argument: a ((λx.x) b)

Anywhere a redex hides, the term is not yet fully reduced.

Head Normal Form

Head normal form (HNF) is a weaker condition than normal form. A term is in HNF if, after peeling off any leading lambdas, the head (leftmost position) is a variable — not a redex.

The head of a term is found by:

  1. Strip outer abstractions: λx₁.λx₂. ... M — look at M
  2. Follow left-associative applications: M N₁ N₂ ... — M is the head

If the head is a variable, the term is in HNF — even if redexes lurk inside arguments or the body.

In HNF:

  • x — head is x
  • λx.x — strip λx, head is x
  • x ((λy.y) a) — head is x (the redex is in an argument, not at the head)

Not in HNF:

  • (λx.x) a — head position is an abstraction applied to an argument
  • (λx.x x)(λy.y) — head is a redex

Weak Head Normal Form

Weak head normal form (WHNF) is even weaker than head normal form. A term is in WHNF if:

  1. It is an abstraction λx.M (regardless of what is in the body), OR
  2. It is a variable applied to zero or more arguments: x N₁ N₂ ...

The key difference from HNF: WHNF does not look inside the body of an abstraction. An abstraction is automatically in WHNF, even if its body contains redexes.

In WHNF:

  • λx.(λy.y) x — an abstraction (body has a redex, but WHNF does not check)
  • x a b — variable at head
  • λx.x — an abstraction

Not in WHNF:

  • (λx.x) a — the outermost form is a redex, not an abstraction or variable-headed application

The hierarchy: Normal form (strictest) $\subset$ HNF $\subset$ WHNF (weakest). Every term in normal form is also in HNF and WHNF. But not every term in WHNF is in normal form.

Classify the Form

A term is in normal form if it contains no redexes — no subterm of the form (λx.M) N. To check, scan every part of the term:

  • Variables are always in normal form.
  • An abstraction λx.M is in normal form if its body M is.
  • An application M N is in normal form if M is not an abstraction (otherwise M N would be a redex) and both M and N are in normal form.

Is This Normal?

To determine whether a term is in normal form, look for the pattern (λx.M) N anywhere in the term. If you find it, the term is not in normal form — it still has a reduction step available.

Remember: a redex requires an abstraction directly applied to an argument. An abstraction by itself (λx.M) is not a redex. A variable applied to something (x y) is not a redex. Only the combination (λx.M) N creates a redex.

Why Normal Forms Matter

In lambda calculus, computation is reduction. You start with a term, find redexes, and reduce them. But what are you reducing toward?

The answer is a normal form — a term with no redexes left. This is the final answer, the result of the computation. Without the concept of normal form, there would be no way to say "this computation is done."

Not every term has a normal form. Some terms, when reduced, produce new redexes endlessly — they never settle. We will study these divergent terms soon. But when a normal form exists, it represents the unique final result (up to alpha equivalence) of the computation.

The weaker forms — HNF and WHNF — matter for practical evaluation strategies. Sometimes you do not need to reduce every last redex. Knowing the head is enough to decide what to do next, and WHNF tells you: "the outermost structure is settled."

Ready to test your understanding?

Bitwit uses spaced repetition to help you truly master concepts like this—not just read about them. Each card generates with different values, so you can't just memorize answers.

Practice Normal Forms →