Strong normalization

In mathematical logic and theoretical computer science, a rewrite system has the (strong) normalization property or is terminating if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates with an irreducible term, also called a normal form. A rewrite system may also have the weak normalization property, meaning that for every term, there exists at least one particular sequence of rewrites that eventually yields a normal form, i.e., an irreducible term.

The pure untyped lambda calculus does not satisfy the strong normalization property, and not even the weak normalization property. Consider the term ${\displaystyle \lambda x.xxx}$. It has the following rewrite rule: For any term ${\displaystyle t}$,

But consider what happens when we apply ${\displaystyle \lambda x.xxx}$ to itself:

...
Wikipedia