Le 29 mai 06 à 14:30, Dušan Kolář a écrit :
Hello all,
I'm asking in place of several my colleagues and myself of course.
The question is almost off topic. It is from lambda calculus
definition, in particular, definition of alpha reduction (and
others as well).
Alpha reduction definition: a lambda expression (\v.e) can be
transformed (reduced) to (\v'.e[v'/v]) if the substitution e[v'/v]
is valid.
Beta reduction definition: a lambda expression (e1 e2) can be
reduced to the expression e[e2/v] if e1 is of the form (\v.e) and
if the substitution e[e2/v] is valid.
Eta reduction definition: a lambda expression e can be reduced to a
lambda expression (\v.e v) if v is not free in e.
OK. If we have these two expressions:
1) (\x.x b x)
2) (\x.x c x)
The question is, are they equal? (They are not identical, of course.)
For answer "no", there is a strong argument - there is no reduction
sequence that can make these identical.
On the other hand, their "meaning" expresses the same operation.
Well, what is the answer? I will be lucky with any link to WWW
resource or your opinion. Nevertheless, the more formal and precise
your answer will be the more I will be lucky. ;-)
If b and c are free, then no, they can't be considered equal, and i
don't see how you can find a common "meaning" in this case either.
Those two are equivalent: (\b.\x.x b x) = (\c.\x.x c x).
-- Matthieu Sozeau
http://mattam.org_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
