2009/6/21 Andrew Coppin
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