Chet Murthy <chet@watson.ibm.com> writes:

> It wasn't the substitution that was killing me, but the
> alpha-conversion, and checks for alpa-conversion.
> 
> Now, there _is_ possibly one way of doing explicit names that would be
> fast enough to be a contender -- where the names are chosen uniquely,
> using a global counter, so no capture check is required.  I can
> imagine that that would be fast.

We used exactly this strategy in the optimizer of SML/NJ (see Journal
of Functional Programming 7(5), September 1997 for some more detail).
Variable names are essentially a string plus a counter, e.g.,
foo15432.  Only compiler writers see these names, so the ugliness of
the output was not a big concern.

A "hidden" expense is that you have to preserve the following critical
invariant through optimization: every variable is bound at most once
in the program.  In our work, we were inlining functions used exactly
once, and the invariant is trivially preserved by this optimization.
In general beta reduction, binding occurrences are duplicated, and so
we have to do alpha renaming there.

I can't comment on how this compares in speed to de Bruijn indices.


-Trevor