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

Andrew Coppin andrewcoppin at btinternet.com
Sun Jun 21 12:53:04 EDT 2009

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.

More information about the Haskell-Cafe mailing list