[Haskell-cafe] OT - lamba calculus definition - alpha reduction

[Matthieu Sozeau]

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