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