On Sun, Jun 21, 2009 at 8: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. >
It seems obvious scince beta reduction never introduces new variales... -- Victor Nazarov _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe