Re: de Bruijn indices

[Chet Murthy <chet@watson.ibm.com>]

>>>>> "GH" == Gerard Huet <Gerard.Huet@inria.fr> writes:

    GH> 1. They lead to efficient implementations. My original
    GH> implementation of the constructive engine in Coq's early
    GH> versions used de Bruijn indices, and performed reasonably
    GH> well. It leads to a completely applicative implementation of
    GH> lambda-calculus, and the cost of lifting may be reduced by
    GH> Okasaki-like data structures. I still remember the day when
    GH> this super-hacker declared that he was going to replace all
    GH> this inefficient stuff by slick hashtables - only to undo
    GH> everything 2 months later because he was 30% slower.

It turns out that deBruijn indices are *significantly* more efficient
than explicit names.  Moreover, the renaming operations that must be
introduced to use explicit names are essentially the same as the
"lifting", etc, operations used in deBruijn indices.

I once modified Coq to use explicit names, and after spending a month
or so, trying to make it as fast as Coq with deBruijn indices,
switched back.

That experiment, and finding that every _single_ avenue for improved
performance, with explicit names, was a dead end, pretty much
convinced me that deBruijn indices are much faster.

Also, regarding human-readability, I think it is a red herring to ask
whether the term Lambda("x",Ref 2) (which corresponds to something
like ("lambda x. y") is more readable than Lambda("x",Var "y").

In both cases, without the "environment" that binds free variables to
values, types, or "meanings" of some sort, the meaning of the term is
undefined.  So we need to keep these environments around, and once we
have them, well, we can always just lookup the name, if want it.

Moreover, it is only during debugging that having the "explicit name"
actually buys us anything in readability.  At runtime, if the program
ever prints out something, it does so with respect to this
"environment", so there's always a good name to use.  If it is
manipulating terms, well, it couldn't very well use the name for
anything other than a lookup, since even in explicit names, the name
can be modified, e.g. by alpha-conversion.

Again, I started out as an "explicit name fanatic", and was converted
to the "creed of deBruijn indices", by hard experience.  I would
recommend that before anyone write off deBruijn indices, they attempt
to build a _large_ system (ok, so Coq isn't large by commercial
standards, but by the standards of academic systems it ain't small)
both ways.

--chet--