2009/6/21 Andrew Coppin <andrewcop...@btinternet.com>: > 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.
I'm no expert, but it sounds to me like you're doing the equivalent of "de Bruijn indexing", which is a method to avoid alpha conversion, which is basically what you're worried about. Therefore, I'm guessing that there will be no name collisions. -- Deniz Dogan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
