On Sun, Jun 21, 2009 at 05:53:04PM +0100, Andrew Coppin 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.
Lambda calculus is one of those things that seems simple in theory (because it IS simple in theory) but can be tricky to implement correctly. I recommend reading the first few chapters of Benjamin Pierce's "Types and Programming Languages" for a good discussion of the issues involved (including explanations and implementations of both a "named" style, and a "de Bruijn index" style), and then also "I am not a number, I am a free variable" by McBride and McKinna, which explains a "locally nameless" style which mixes the best of both worlds. -Brent _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
