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

Dušan Kolář kolar at fit.vutbr.cz
Mon May 29 09:46:28 EDT 2006

```>>
>>
>>  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).
>
Yes, those of yours are equal of no doubt.
Those of mine are not, that's even my opinion, on the other hand, I was
not precise enough in my explanation. Those of mine have the same
behavior unless you mean something else by variables b and c. Otherwise
the behavior is the same, isn't it? If the behavior is the same, they
can be interchanged and, thus, they are equal...

OK, I agree this may be a more "philosophical" question. ;-)

Thanks,

Dusan

```