Normal Form

In the lambda calculus a normal form is a λ-term that can have no β-reductions applied to it.

A β-reduction choice strategy that leads to normal forms is called normalising or fully normalising.

Examples

• λx.x is a normal form.
• λx.x y is not a normal form as λx.x y →β y

References

W. Kluge. Abstract Computing Machines. A Lambda Calculus Perspective. Springer, 2005.