Re: [Haskell-cafe] about beta NF in lambda calculus

2009-03-22 Thread Claus Reinke
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

[Haskell-cafe] about beta NF in lambda calculus

2009-03-21 Thread 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

Re: [Haskell-cafe] about beta NF in lambda calculus

2009-03-21 Thread 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.

Re: [Haskell-cafe] about beta NF in lambda calculus

2009-03-21 Thread Eugene Kirpichov
Thus, if you use normal-order evaluation (which Haskell uses), you will inevitably reach the normal form if and only if it exists at all. So, if all you care about is the normal form (if you don't care about computation time), then terms that *have* an NF and terms that *are* in NF are

Re: [Haskell-cafe] about beta NF in lambda calculus

2009-03-21 Thread Antti-Juhani Kaijanaho
On Sat, Mar 21, 2009 at 07:29:05PM +, 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

Re: [Haskell-cafe] about beta NF in lambda calculus

2009-03-21 Thread Eugene Kirpichov
Actually I was also going to provide exactly the same example, but hesitated to :) 2009/3/21 Antti-Juhani Kaijanaho antti-juh...@kaijanaho.fi: On Sat, Mar 21, 2009 at 07:29:05PM +, Algebras Math wrote: If above is true, I am confused why we have to distinguish the terms which have NF and