strong normalization

strong normalization means for every term, every rewrte sequence, it evenetrually terminate.
It is the good property that come form the typed mechanism of typed lamda cauculus, while the untyped one dont has this property.
So typed calculus can eventrually rewriten to a normal form.

there are also the weak normalization, which means always exist at least one rewrite sequence that reduce to a normal form.