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

[Lennart Augustsson]

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.

  -- Lennart

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
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>