# Does a term being normalizable mean the same as the term has a normal form?

From Types and Programming Languages by Pierce

A term $$t$$ is in normal form if no evaluation rule applies to it— i.e., if there is no $$t'$$ such that $$t -→ t'$$.

and

A term $$t$$ is typable (or well typed) if there is some $$T$$ such that $$t : T$$.

In the pure simple typed lambda calculus:

we consider another fundamental theoretical property of the pure simply typed lambda-calculus: the fact that the evaluation of a well- typed program is guaranteed to halt in a ﬁnite number of steps—i.e., every well-typed term is normalizable.

Does a term being normalizable mean the same as the term has a normal form?

Here is a term which has no normal form in the untyped lambda calculus:

Recall that a term that cannot take a step under the evaluation relation is called a normal form. Interestingly, some terms cannot be evaluated to a nor- mal form. For example, the divergent combinator

$$omega = (λx. x x) (λx. x x);$$

contains just one redex, and reducing this redex yields exactly omega again! Terms with no normal form are said to diverge.

In the pure simple typed lambda calculus,

• is $$omega$$ typable (i.e. well-typed)?
• is $$omega$$ normalizable?
• does $$omega$$ have a normal form?

It is well known that $$\omega = (\lambda x . x x) (\lambda x . x x)$$ is not typeable, nor is it normalizable. It is not normalizable because it has an evaluation step ($$\beta$$-reduction) which evaluates it to itself, so we get $$\omega \mapsto \omega \mapsto \omega \cdots$$.
To see that it is not typeable, observe that already its subexpression $$\lambda x . x x$$ is not typeable. For if $$x$$ has type $$T$$ then in order for $$x x$$ to have a type, $$T$$ must be of the form $$T \equiv T \to S$$ (because $$x$$ is applied to something, therefore by the typing rules it must have a function type). But there is no type $$T$$ such that $$T \equiv T \to S$$, because the type on the right-hand side is larger (as a syntactic expression) than the type on the left-hand side.