[Haskell-cafe] about beta NF in lambda calculus
ryani.spam at gmail.com
Sat Mar 21 15:46:20 EDT 2009
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.
2009/3/21 Algebras Math <algebras2009 at googlemail.com>:
> 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?
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe