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

[Jon Fairbairn]

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