Re: de Bruijn indices

[John R Harrison <johnh@ichips.intel.com>]

Chet writes:

| It wasn't the substitution that was killing me, but the
| alpha-conversion, and checks for alpa-conversion.

I find that quite hard to understand. Profiles I've done in HOL Light
indicate that alpha conversion is not that common, and in the vast
majority of successful alpha-equivalence tests the two terms are
actually equal. Indeed after descending a couple of levels, subterms are
usually pointer-equal. Likewise, unsuccessful alpha-equivalence tests
almost always happen when the terms differ grossly near the top level.
Thus, in practice alpha-conversion is little done while
alpha-equivalence testing even of huge terms is not far from being
constant time. Are the typical profiles in Nuprl or Coq so very
different?

Substitution is less efficient than with dB terms, but I've found it
generally acceptable in practice, and certainly a price worth paying for
the conceptual simplicity of presenting a name-carrying interface to the
user rather than exposing floating dB indices.

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

Surely the size of the system is irrelevant: what matters is the size of
the problems it deals with. But anyway, from my own experience (and I
don't think HOL Light is smaller than Coq according to any plausible
metric) the Damascene conversion happened the other way round.

Cheers,

John.