[Haskell-cafe] Slightly off-topic: Lambda calculus

[Bertram Felgenhauer]

Miguel Mitrofanov wrote:
> Correction: I think that one can find an expression that causes name 
> clashes anyway, I'm just not certain that there is one that would clash 
> independent of whichever order you choose.

Yes there is.

Consider

 (\f g -> f (f (f (f (f (f g)))))) (\l a b -> l (b a)) (\x -> x)

which has 6 variables in total. This reduces to the normal form

 \a b c d e f g -> g (f (e (d (c (b a)))))

which requires 7 variables. So without alpha-conversion at least one of
the original 6 variables will clash with itself.

Bertram