2

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"?

Zonko
  • 322
  • 1
  • 13
  • I would guess more context is needed. – mathreadler Jul 27 '17 at 19:27
  • 3
    I think the problem is in the other direction - without $\alpha$-conversion, how do you show $\lambda x.x=\lambda y.y$? (To clarify: obviously $\alpha$-conversion isn't needed to show $(\lambda x.x)\alpha=(\lambda y.y)\alpha$ for all $\alpha$, but this fact alone doesn't give us true equality as far as I can tell.) – Noah Schweber Jul 27 '17 at 19:28

1 Answers1

4

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.

hmakholm left over Monica
  • 286,031