>> 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!)

> 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.)

-- 
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*

Post a reply to this message