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

[Lennart Augustsson]

Actually, keeping all names distinct is not de Bruijn numbering, it's
called the Barendregt convention.

On Sun, Jun 21, 2009 at 7:05 PM, Deniz Dogan<deniz.a.m.dogan at gmail.com> wrote:
> 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.
>
> --
> Deniz Dogan
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>