Probably the easiest way to fix this was already proposed by Deniz Dogan: de Bruijn indices. On 21 Jun 2009, at 21:57, Andrew Coppin wrote:
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...)
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe