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 <[email protected]>: > 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe > > _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
