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

Matthieu Sozeau mattam at mattam.org
Mon May 29 09:05:27 EDT 2006

```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
```