As others have pointed out, it is not enough to rename before reduction. It should be pretty obvious since when you do substitution and copy a lambda expression into more than once place you will introduce variables with the same name. You can keep unique variables by "cloning" during substitution, i.e., renaming the bound variables.
-- Lennart On Sun, Jun 21, 2009 at 6:53 PM, Andrew Coppin<andrewcop...@btinternet.com> wrote: > OK, so I'm guessing there might be one or two (!) people around here who > know something about the Lambda calculus. > > I've written a simple interpretter that takes any valid Lambda expression > and performs as many beta reductions as possible. When the input is first > received, all the variables are renamed to be unique. > > Question: Does this guarantee that the reduction sequence will never contain > name collisions? > > I have a sinking feeling that it does not. However, I can find no > counter-example as yet. If somebody here can provide either a proof or a > counter-example, that would be helpful. > > _______________________________________________ > 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
