[Haskell-cafe] Slightly off-topic: Lambda calculus

[Brent Yorgey]

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