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 <algebras2009@googlemail.com>:
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