On 21-6-2009 21:40, Orchid XP v8 wrote:
>>> In a stunning turn of events, I was just in the middle of having a 
>>> conversation about whether assigning unique indicies to every 
>>> variable in a Lambda expression enables its reduction sequence to be 
>>> computed without name clashes. :-P
>>
>> There is alpha conversion to prevent that, but I guess you are talking 
>> about an implementation not the theory. ;)
> 
> Indeed. It's significantly less trivial than you'd imagine... o_O
> 
>> I seem to remember that labelling just with the level of the nesting 
>> is enough.
> 
> That would be de Bruijn indices. And I'm hoping to avoid needing to go 
> that far... (But we'll see!)

It requires a different implementation and different data structures, 
but as you already have proven that the other path is infeasible...
Having named bound variables is very natural if you were brought up in 
imperative languages, but I don't see the point in functional languages, 
other than in the human interface.

> 
>> If you have unique identifiers throughout your program, that certainly 
>> works.
> 
> Ah, but wait. Simply renaming all the variables before you start is 
> insufficient. Unfortunately.
> 
>   (\x -> x x) (\y -> y)
> 
> Make 'em all unique:
> 
>   (\x1 -> x1 x1) (\y2 -> y2)
> 
> Now beta-reduce:
> 
>   (\y2 -> y2) (\y2 -> y2)
> 
> Oh noes! No longer unique...
> 
> (In this instance it doesn't matter, but somebody showed me a slightly 
> more complicated example where it actually goes wrong.)
> 
I didn't realize you would want to use them at run-time (bad idea IMHO, 
see above). Not your fault, I just did not read carefully.

Post a reply to this message