[Haskell-beginners] about beta NF in lambda calculus

[Brent Yorgey]

On Sat, Mar 21, 2009 at 07:28:48PM +0000, Algebras Math wrote:
> hi,
> 
> What is the different between 'in beta normal form' and 'has beta normal
> form' ? Does the former means the current form of the term is already in
> normal form but the latter means that it is not a normal form yet and can be
> reduced to be normal form? Like  \x.x is in NF and (\x.x) (\x.x) has NF?

Exactly.

> 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?

If a term _has_ a normal form, we can be confident that we will
eventually reach a normal form by reducing it; if a term _is in_
normal form, we know that reducing it will have no effect.  It is
useful to distinguish them in the same way as it is useful to
distinguish between someone who _is currently_ at home and someone who
is at the grocery store but has a way of getting home.  (\x.x) (\x.x)
reduces to \x.x, but they are not the same term.  We could "avoid"
having (\x.x) (\x.x) become a normal form by simply choosing not to
reduce it.

Does that help?

-Brent