Re: de Bruijn indices

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

It's been interesting for me to see a discussion of de Bruijn versus
name-carrying term representations, since it's an issue I've spent some
time thinking about and on which I've changed my opinion at least once. The
different versions of the HOL theorem proving system:

  HOL88     - http://www.cl.cam.ac.uk/Research/HVG/FTP/#hol88
  hol90     - http://www.cl.cam.ac.uk/Research/HVG/FTP/#hol90
  HOL Light - http://www.cl.cam.ac.uk/users/jrh/hol-light/index.html
  hol98     - http://www.cl.cam.ac.uk/Research/HVG/FTP/#hol98

have gone through several different term representations over the years:

  HOL88     - name-carrying
  hol90     - name-carrying at first then de Bruijn
  HOL Light - de Bruijn at first then name-carrying
  hol98     - de Bruijn at first then explicit substitutions

The original HOL88 name-carrying implementation was probably inherited
from Edinburgh or Cambridge LCF. This was quite satisfactory, but over
the years several obscure bugs were found in variable renaming which
could have caused unsoundness, an embarrassment in a system that
stresses its logical consistency. To avoid having the soundness of the
system depend on tricky programming, hol90 changed to using a de Bruijn
representation.

However, all versions of HOL maintain an abstract type of terms with a
name-carrying interface, so the de Bruijn indices must be an internal
detail that is hidden from the user. This makes de Bruijn terms grossly
inefficient for very large abstraction-rich terms. The trivial operation
of recursively descending a term can involve a quadratic amount of work,
since each time a binder is traversed, a variable must be substituted
for a de Bruijn index throughout the body. For this reason, although I
was initially enthusiastic about de Bruijn terms, I rapidly decided they
didn't fit with the HOL worldview and changed HOL Light (my small clean
reimplementation of the system in CAML Light) back to a name-carrying
approach.

Very recently, Bruno Barras has been the driving force behind yet
another term representation for hol98 that admits an efficient ML-style
reduction algorithm. See:

  @INPROCEEDINGS{tphols2000-Barras,
        crossref        = "tphols2000",
        title           = "Programming and computing in {HOL}",
        author          = "Bruno Barras",
        pages           = "17--37"}

  @PROCEEDINGS{tphols2000,
        editor          = "M. Aagaard and J. Harrison",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           13th International Conference, TPHOLs 2000",
        series          = "Lecture Notes in Computer Science",
        volume          = 1869,
        year            = 2000,
        publisher       = "Springer-Verlag"}

All of this goes to show that despite intensive activity in the field,
the basic question of the most appropriate term representation -- even
for a particular narrowly focused application -- is not yet clearly
agreed on.

Cheers,

John.