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

Brent Yorgey byorgey at seas.upenn.edu
Sun Jun 21 13:29:17 EDT 2009

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


More information about the Haskell-Cafe mailing list