All, Just as ancillary information: ∃ a calculator on Hackage called "LambdaCalculator". Its rather short (loc wise) and fun to play with.
Thomas On Sun, Jun 21, 2009 at 10:57 AM, Andrew Coppin<andrewcop...@btinternet.com> 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
