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

[Dušan Kolář]

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