Beta normal form

Summary

A lambda term is in beta normal form when no beta reduction step can be applied to it. Such a term is a finished computation, its value. By the Church–Rosser theorem, a term has at most one beta normal form up to renaming of bound variables. Some terms, such as $(\lambda x.\, x\, x)(\lambda x.\, x\, x)$, have no normal form at all.