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'$.
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?