Normalization property

Summary

A rewriting system has the normalization property when every computation can end in a normal form, an object that cannot be rewritten further. The weak form asks that some reduction path reaches a normal form; the strong form asks that every reduction path is finite. Strong normalization is also called termination. The untyped lambda calculus is not normalizing, while the simply typed lambda calculus is strongly normalizing.