Is there any lambda expression $E$, that when "computed" ($\beta$-reduced) leads to substitution mistakes, even though you never reused a variable in $E$?
EDIT: I certainly know the importance of $\alpha$-equivalence in theoretical lambda calculus, but is it needed for actual computation? Assume I create a machine that could $\beta$-reduce without caring about "name clashes", will there be programs, that even though i never reuse a variable, will still have "name clashes"?
Try reducing this to $\beta$-normal form without $\alpha$-conversion: $$ (\lambda x.xx)(\lambda a.(\lambda b.ab)) $$
If you restrict the reduction strategy it is possible to avoid the problem -- for example, if you start with a closed term without duplicated variables and stick to pure call-by-value reduction to weak head normal form, then you can't possibly get into name-capture problems.