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

Dušan Kolář kolar at fit.vutbr.cz
Mon May 29 10:43:47 EDT 2006


Jon Fairbairn wrote:
> On 2006-05-29 at 15:46+0200 =?UTF-8?B?RHXFoWFuIEtvbMOhxZk=?= wrote:
>   
>>>> 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. ;-)
>>     
>
> There's no sensible way of regarding (\x. x b x) and (\x. x
> c x) as equal, other than by specifying that b and c are
> bound to the same value. More formally, I think the usual
> way of dealing with free variables is to talk about contexts
> C[[ _ ]] that bind some variables, and then asking whether
> the expressions under consideration are equal in all
> contexts. So for your expressions, if we choose C1 [[ _ ]] =
> (\b c . _ (\x.x)) (\x y.x) (\x y. y), then we have that
>
> C1 [[(\x. x b x)]] = (\b c . (\x. x b x) (\x.x)) (\x y. x) (\x y. y)
>                    = \y . (\x.x)
> but
> C1 [[(\x. x c x)]] = (\b c . (\x. x c x) (\x.x)) (\x y. x) (\x y. y)
>                    = \y.y
>
> and those are clearly not equal (substitution into contexts
> is allowed to capture free variables, it's what they're
> for!).
>
> So you can say that your two expressions are equal in
> contexts that bind b and c to equal values, but otherwise
> not.
>
> Does that help? It's OK to ask philosophical questions about
> lambda calculus -- in a sense it's why it was invented.
>
>   
Thank you!

This is very good explanation.

Dusan


More information about the Haskell-Cafe mailing list