OT - lamba calculus definition - alpha reduction
Hello all, 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. ;-) Thx and regards Dusan
Le 29 mai 06 à 14:30, Dušan Kolář a écrit :
Hello all,
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). -- Matthieu Sozeau http://mattam.org
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
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
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. -- Jón Fairbairn Jon.Fairbairn at cl.cam.ac.uk
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
participants (4)
-
Brian Hulley -
Dušan Kolář -
Jon Fairbairn -
Matthieu Sozeau