[Haskell-cafe] about beta NF in lambda calculus

[Ryan Ingram]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>