[Haskell-cafe] Slightly off-topic: Lambda calculus
deniz.a.m.dogan at gmail.com
Sun Jun 21 13:05:16 EDT 2009
2009/6/21 Andrew Coppin <andrewcoppin at btinternet.com>:
> 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.
More information about the Haskell-Cafe