|
![](/i/fill.gif) |
>>> 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.
My whole program is "human interface". It doesn't do anything "useful",
it's just to allow a human being to easily observe the reduction
sequence. To that end, I'd like the program to avoid screwing around
with the human-provided variables names as much as is feasible. OTOH,
I'd also like the thing to *work*... ;-)
> 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.
Well, I think if I can relabel the variables after each expression
transformation to recover uniqueness, it should work.
(Unfortunately the labeller currently looks only at the variable *names*
and ignores the index values. That means that expressions which already
have indicies can get renamed incorrectly.)
--
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*
Post a reply to this message
|
![](/i/fill.gif) |