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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
