Normal forms

When do we stop reducing?

We stop reducing when we reach the Normal form (NF), i.e. when there are not more redexes left to reduce. A normal form then is a term which does not contain any redex. A term that can be reduced to a normal form is said to be normalisable.

$$(\lambda x.a(\lambda y.xy))bc\to_\beta a(\lambda y.by)c$$ (15)

Which is a normal form (application associates to the left).

Weak Head Normal Form — Stop reducing when there are no redexes left, but without reducing under an abstraction.