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

[Dušan Kolář]

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