Re: de Bruijn indices

Re: de Bruijn indices

[John R Harrison]

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.

Re: de Bruijn indices

[John R Harrison]

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.

Re: de Bruijn indices

[Trevor Jim]

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

Re: de Bruijn indices

[Benjamin C. Pierce]

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

This is pretty much how the Pict front end works.  We started out with a
standard deBruijn representation, but later switched to a scheme where,
during parsing, we choose a globally unique spelling for each bound name
(they're not *that* ugly).  We have to do a little work later to make
sure that uniqueness is maintained, but it seems faster on the whole.

       B
       
       

RE: de Bruijn indices

[Greg Morrisett]

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

But alpha-conversion is a form of substitution...  

> 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.
> 
> Of course, it would result in uggggggly names -- uglier than deBruijn
> numbers, unless similar tricks were played in pretty-printing.

This is essentially what we did in TAL -- each variable had
a string-based name and a number field.  Numbers defaulted
to zero (and weren't printed).  When we needed to alpha-convert 
something, we incremented a global counter and used this for
the new number (keeping the string the same.)  You do end
up with foo_12349 this way, but only if something has to be
alpha-converted -- and that turned out to be pretty rare.

Again, I haven't re-implemented things with De Bruijn, and
would like too.  It may be that TAL would run faster with
a well-implemented scheme.  

Two side notes:

1. The reason I can't easily re-implement TAL using de Bruijn
instead of explicit names, is that I exposed my term datatypes
to make pattern matching easy.  If I'd been coding in something
like Java, I suspect I would've abstracted terms enough that
re-writing the code would've been easier.  One problem with
ML is that the convenience of pattern matching tends to direct
you (or at least me) to expose too much representation information.
Abstract patterns would help a lot...

2. I seem to recall that there are subtle issues with
typed calculi (especially dependently-typed calculi) and
de Bruijn?  Certainly explicit substitutions are tricky
in this setting...

-Greg

Re: de Bruijn indices

[Chet Murthy]

>>>>> "GM" == Greg Morrisett <jgm@cs.cornell.edu> writes:

    GM> Well, I can say from my own experience that de Bruijn isn't
    GM> always best.  Neither NuPRL nor the TAL type-checker uses
    GM> indices, prefering named variables instead.  For both,
    GM> preserving original names is really useful when debugging.

I can't speak to TAL.  I _can_ speak for Nuprl, having implemented a
version of Nuprl in SML/NJ in 1990, and having re-implemented it, by a
process of iterative migration, in Coq, in 1992-1994.

Explicit names were *significantly* slower than deBruijn indices.  The
costs were there, even though I did the standard tricks of caching
free-vars under binders, and even though I wrote the most careful code
I could think of to make explicit names faster.

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.

Of course, it would result in uggggggly names -- uglier than deBruijn
numbers, unless similar tricks were played in pretty-printing.

--chet--

Re: de Bruijn indices

[John Max Skaller]

Chet Murthy wrote:
> 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)

Actually, if you multiply the size of Coq by 10, to get the equivalent
size for a C/C++ program, it isn't that small by commercial standands
either. :-)

-- 
John (Max) Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
checkout Vyper http://Vyper.sourceforge.net
download Interscript http://Interscript.sourceforge.net

Re: de Bruijn indices

[Markus Mottl]

On Wed, 11 Oct 2000, Simon Peyton-Jones wrote:
> Indeed, if any participant of this discussion is so motivated, I would
> dearly love to publish a paper about the practical aspects of
> efficient management of substitution and bound variables in the
> Journal of Functional Programming.  It doesn't have to be a "new idea".
> Just articulating the unpublished experience and laying out design tradeoffs
> that we've seen in this discussion would be excellent. 

The developers of the Teyjus-implementation of LambdaProlog have tried
very hard to develop better ways of handling bindings, especially what
concerns higher-order unification - this is a highly performance-critical
aspect of LambdaProlog, which allows reasoning about higher-order abstract
syntax. They could surely contribute valuable input on their experience.
Some interesting papers on this topic can be found on their sites.

The main architects of Teyjus and LambdaProlog (Gopalan Nadathur and
Dale Miller):

  http://www-users.cs.umn.edu/~gopalan
  http://www.cse.psu.edu/~dale

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

RE: de Bruijn indices

[Simon Peyton-Jones]

| comparisons.  I really think the community needs a bunch
| of "systems" paper on this topic that do a careful examination 
| of the tradeoffs for important applications like type-checkers,
| compilers, and theorem provers.  Like realistic techniques
| for garbage collection, too much is locked in the brains of 
| implementors.

Indeed, if any participant of this discussion is so motivated, I would
dearly love to publish a paper about the practical aspects of
efficient management of substitution and bound variables in the
Journal of Functional Programming.  It doesn't have to be a "new idea".
Just articulating the unpublished experience and laying out design tradeoffs
that we've seen in this discussion would be excellent. 

Send me a paper!  (Or send it to Greg, who's also a JFP editor.)

Simon

RE: de Bruijn indices

[Greg Morrisett]

Well, I can say from my own experience that de Bruijn 
isn't always best.  Neither NuPRL nor the TAL type-checker
uses indices, prefering named variables instead.  For
both, preserving original names is really useful when
debugging.  

When implementing TAL, I assumed de Bruijn would be faster,
since what we do is a lot of (a) comparisons between
terms, (b) lots of beta-reductions.  To make comparisons
go fast, it's important to make the common case pointer
equality.  Like Shao, we found hash consing to be very
effective for this.  

At first blush, it seems that using de Bruijn would be better 
in this situation, as any two alpha-equivalent terms will
hash-cons together.  However, it was fairly easy to arrange
most of the alpha-equivalent terms to use the same names
(TAL is the output of a compiler after all), so we could
get good hash-consing to start with -- all we had to do 
was preserve it.  Furthermore, there's the potential to get
more hash-consing with a named scheme.  For instance, for
(\y.\z.y z) and (\z.\y.y z), you can at least share the
"y z".  Not so for de Bruijn.

The way we made substitution work well and fast was, like
Simon, to keep track of the free variables of a term.  
(We computed this information lazily and then memoized it
in the term.)  Shao did something similar in the Flint
IL.  This had two effects:  one, we could minimize re-naming
bound variables, and two, we could cut off substitution
earlier.  I'm not sure how these optimizations translate
into a de Bruijn setting (I'm sure there's some way, but
I haven't thought it through.)

I also tried out a form of explicit substitutions with
the named scheme (Shao did this in the Flint IL), but
found that the overhead was not worth it.  I think in
part this was because we were forced to do deep
sub-type comparisons on terms, and hence, had to push
the substitutions down to the leaves.  I think if you
buy into de Bruijn, then you more or less have to buy
into explicit substitutions too.

On the other hand, we never got around to implementing
a de Bruijn version of the type-checker.  I would like
to do this someday and also try the higher-order abstract 
syntax tricks.

The folks at CMU are working on an interface that allows
you to choose which representation you want.  Like the
Flint folks and us, they hope to do some detailed
comparisons.  I really think the community needs a bunch
of "systems" paper on this topic that do a careful examination 
of the tradeoffs for important applications like type-checkers,
compilers, and theorem provers.  Like realistic techniques
for garbage collection, too much is locked in the brains of 
implementors.

-Greg

Re: de Bruijn indices

[Chet Murthy]

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

Re: de Bruijn indices

[Gerard Huet]

In defense of de Bruijn indices :

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

2. The apparent complexity of lifting is to my view an inherent complexity
of substitution, which you have better face up rather than put under the
rug of name management of symbol tables, for which you will have to pay the
price in unexpected places. And when the going gets rough, at least your DB
indices behave well in natural recursions. When I set to understand fully
Bohm's theorem, down to programming a running Bohm discriminator, I used DB
indices, which generalise well to Bohm trees (ie potentially infinite
lambda-terms). I do not think I would have succeded in programming this
stuff without this explicit and concrete control on variable references.
And I could even publish the code itself, which is available as commented
Caml code in the paper:
G. Huet An Analysis of Bohm's theorem, Theoretical Computer Science 121
(1993) 145-167.

3. You can do proofs by induction on the corresponding structure, and thus
prove meta-theoretical results in a direct and clean way. You can even hope
to actually mechanise the formal development. See for instance:
G. Huet "Residual theory in lambda calculus: a formal development". J.
Functional programming 4,3 (1994) 371-394.
where a fair portion of the syntactic theory of beta-reduction is done
completely formally, using DB indices again. 

Gérard

Re: de Bruijn indices

[Markus Mottl]

On Thu, 05 Oct 2000, Patrick M Doane wrote:
> You should take a look at Frank Pfenning's course notes for his class on
> Computation and Deduction. The chapter on compilation covers the use of de
> Bruijn indices as well some interesting judgements abouts the compilation
> process. This chapter is located at:

De Bruijn indices are, btw., also explained (and implemented) in the
tutorial "Functional Programming using Caml Light" in Chapter 12:

  http://caml.inria.fr/tutorial/index.html

People who are interested in optimum performance for handling bindings
might also want to try out Christophe Raffalli's "bindlib":

  http://www.lama.univ-savoie.fr/sitelama/Membres/pages_web/RAFFALLI/bindlib.html

It's said to be even more efficient.

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

Re: de Bruijn indices

[Patrick M Doane]

> Could you provide a reference to de Bruijin indexing? I recall reading
> about it some time ago, and after having searched my books here, I
> cannot find any references to it. So I probably saw it in a paper some
> time ago... Anyway, I would be interested since I have an interpreter
> name-lookup problem heretoo.

You should take a look at Frank Pfenning's course notes for his class on
Computation and Deduction. The chapter on compilation covers the use of de
Bruijn indices as well some interesting judgements abouts the compilation
process. This chapter is located at:

  http://www.cs.cmu.edu/~fp/courses/comp-ded/notes/chap6.pdf

The rest of the course notes are excellent for those interested in
formally representing theorems about programming languages in a logical
framework. 

Patrick Doane