Given the Y combinator, Y (\x.x) has no normal form. However, (\a. (\x. x)) (Y (\x. x)) does have a normal form; (\x. x). But it only reduces to that normal form if you reduce the (\a. ...) redex, not if you reduce its argument. So depending on evaluation order you might not reach a normal form. -- ryan 2009/3/21 Algebras Math :

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?

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?

Thanks

Alg

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Sat, Mar 21, 2009 at 07:29:05PM +0000, Algebras Math wrote:

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?

Spoken like a mathematician :) (Well, only sort of.) The way to avoid it is not to perform the work of beta conversion. Similarly, you may say that people are either dead or will eventually die, so why distinguish between a person who is dead and a mortal, live person? -- Antti-Juhani Kaijanaho, Jyväskylä, Finland http://antti-juhani.kaijanaho.fi/newblog/ http://www.flickr.com/photos/antti-juhani/

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