[Haskell-cafe] Slightly off-topic: Lambda calculus
lennart at augustsson.net
Sun Jun 21 18:17:46 EDT 2009
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
More information about the Haskell-Cafe