[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. ;-)



More information about the Haskell-Cafe mailing list