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

[Andrew Coppin]

Lauri Alanko wrote:
> With "name collisions" I'm assuming you mean inadvertent variable
> capture. The answer depends on your evaluation strategy. If you never
> reduce inside a lambda (e.g. call-by-name or call-by-value), then you
> will always be substituting a closed term in place of a variable, and
> nothing in a closed term can get captured.
>
> However, if by "as many reductions as possible" you mean "to normal
> form", then you also need to reduce inside lambdas. Then the story is
> different. Consider the following sequence of beta reductions:
>
> (\x. x x) (\y. \z. y z)
> -> (\y. \z. y z) (\y. \z. y z)
> -> \z. (\y. \z. y z) z
> -> \z. \z'. z z'
>
> Notice that in the original form, all variable names were unique, but
> then the variable "z" got duplicated, and the last reduction happened
> _inside_ the "\z." expression, which required renaming of the inner
> "z" in order to avoid variable capture and the erroneous result of
> "\z. \z. z z".
>
> Hope this helps.
>   

Ladies and gentlemen, we have a counter-example!

  (\x1 -> x1 x1) (\y2 -> \z3 -> y2 z3)
  (\y2 -> \z3 -> y2 z3) (\y2 -> \z3 -> y2 z3)
  \z3 -> (\y2 -> \z3 -> y2 z3) z3
  \z3 -> \z3 -> z3 z3

This *should* of course be

  \z3 -> \z4 -> z3 z4

which is a different function.

Now the operative question becomes... how in the name of God to I fix this?

(The obvious approach would be to rerun the renamer; but would 
discarding the variable indicies introduce even more ambiguity? Hmm...)