[Haskell-cafe] about beta NF in lambda calculus

[Claus Reinke]

> 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