[Haskell-cafe] Slightly off-topic: Lambda calculus
lennart at augustsson.net
Sun Jun 21 18:16:52 EDT 2009
As others have pointed out, it is not enough to rename before reduction.
It should be pretty obvious since when you do substitution and copy a
lambda expression into more than once place you will introduce
variables with the same name. You can keep unique variables by
"cloning" during substitution, i.e., renaming the bound variables.
On Sun, Jun 21, 2009 at 6:53 PM, Andrew
Coppin<andrewcoppin at btinternet.com> 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe