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

[Brian Hulley]

Dušan Kolář wrote:
>>> [snip]
>>> 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.
>>
>> 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.

But if the variables are different surely one must assume they *might* be 
bound to different expressions and hence the expressions \x. x b x and \x. x 
c x cannot be considered equivalent.


> Otherwise the behavior is the same, isn't it? If the behavior is the
> same, they can be interchanged and, thus, they are equal...

Perhaps this distinction is between equivalence versus equality under some 
specific model?

Regards, Brian.

-- 
Logic empowers us and Love gives us purpose.
Yet still phantoms restless for eras long past,
congealed in the present in unthought forms,
strive mightily unseen to destroy us.

http://www.metamilk.com