If above is true, I am confused why we have to distinguish the terms which have NF and be in NF? isn't the terms have NF will eventually become in NF? or there are some way to avoid them becoming in NF?
Another way to think about it: what about terms which have no NF? And given both kinds of terms, how do you distinguish them? By normal-order reduction, but that is a semi-decision procedure: if a term has a NF, normal-order reduction will eventually reach it, but if a term has no NF, there may not be a way to tell. There is a trivial decision procedure for whether a term is in NF, but none for whether a term has a NF. That is enough of a difference to warrant the distinction, in most cases;-) Btw, NF (as in: no redices) is rather extreme, so you might want to look up HNF (head normal form: no head redices), which is useful for actually assigning meaning to terms, and WHNF (weak head normal form: no head redices outside of lambda abstraction), which is what implementations of languages like Haskell use during evaluation. Normal-order reduction reaches these forms in order, if they exist: term->WHNF->HNF->NF. Claus