|
![](/i/fill.gif) |
>> 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
|
![](/i/fill.gif) |