[Haskell-beginners] about beta NF in lambda calculus

[Brent Yorgey]

On Sat, Mar 21, 2009 at 07:59:25PM +0000, Algebras Math wrote:
> sorry, I missed something..
> 
> actually  (\x.x) (\x.x) reduces to \x.x, they are equal under beta
> reduction, isn't it?
> (\x.x) (\x.x) =beta \x.x.
> 
> so they are the same?

It depends what you mean by "equal", but usually what we mean by
"equal" is actual structural equality, so (\x.x) (\x.x) and \x.x are
not equal, since they are different terms (one is an application of
one term to another, the other is a lambda term).  It makes no
difference whether one reduces to the other; they are not the _same_
term so they are not equal.*

However, sometimes we _don't_ want to distinguish between terms which
reduce to one another; in this case we can define some sort of
equivalence relation, and say, for example, S =beta T if S can be
reduced to T by a series of beta reductions, or vice versa.  But it is
important to realize that =beta is just an equivalence relation we
have defined, it is not the same thing as equality.  It is quite
possible to have S =beta T but S /= T, as in your example.

-Brent

*Technical note: actually, we usually allow terms to be equal "up to
alpha equivalence", that is, you are allowed to rename bound
variables.  So (\x.x) and (\y.y) are equal, since you can convert
between them by renaming x to y, which doesn't really change anything.



> 
> On Sat, Mar 21, 2009 at 7:37 PM, Brent Yorgey <byorgey at seas.upenn.edu>wrote:
> 
> > On Sat, Mar 21, 2009 at 07:28:48PM +0000, Algebras Math wrote:
> > > 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?
> >
> > Exactly.
> >
> > > 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?
> >
> > If a term _has_ a normal form, we can be confident that we will
> > eventually reach a normal form by reducing it; if a term _is in_
> > normal form, we know that reducing it will have no effect.  It is
> > useful to distinguish them in the same way as it is useful to
> > distinguish between someone who _is currently_ at home and someone who
> > is at the grocery store but has a way of getting home.  (\x.x) (\x.x)
> > reduces to \x.x, but they are not the same term.  We could "avoid"
> > having (\x.x) (\x.x) become a normal form by simply choosing not to
> > reduce it.
> >
> > Does that help?
> >
> > -Brent
> > _______________________________________________
> > Beginners mailing list
> > Beginners at haskell.org
> > http://www.haskell.org/mailman/listinfo/beginners
> >