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