Actually, keeping all names distinct is not de Bruijn numbering, it's called the Barendregt convention.
On Sun, Jun 21, 2009 at 7:05 PM, Deniz Dogan<deniz.a.m.do...@gmail.com> wrote: > 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 > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
